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
.