## 3.2.2 Substitutions

We use the notation for a substitution of all free occurrences of the variable in by the expression . Several substitutions can be performed simultaneously with . In particular, we use the syntax to denote the substitution of each identifier in the sequence by . For more information on free identifiers, see Section 3.3.1.3.

Examples:

• corresponds to the predicate .

• corresponds to the predicate .

• corresponds to the predicate , because the is a quantified variable (i.e. it is not a free variable).

• For a sequence the predicate corresponds to .