The Declaration Constructor

An atomic variable declaration followed by a rule is a rule.

By an obvious induction on rules, define which occurrences of variables are free (or undeclared) and which are bound. Suppose that D is a variable declaration, R is a rule, and S is a state of an auxiliary vocabulary. R is (D,S) -perspicuous if it satisfies the following conditions:

• no variable is declared (explicitly or implicitly) more than once in R , and

• Bound(R) is disjoint from Free(R) Var(D) Fun(S).