4.3.1　Guarded Recursive Specifications with Static Localities