LP, the Larch Prover -- Substitutions
A substitution is a mapping from variables to
terms (of the appropriate sorts). A substitution
can be applied to a term as well as to a variable; its effect is to replace
(simultaneously) each variable in the term by the substitution applied to that
variable. More precisely, if sigma is a substitution defined on
variables, then sigma extends to terms by setting
A substitution sigma is an instance of a substitution sigma1 if
there is a substitution sigma2 such that
sigma(t) = sigma2(sigma1(t)).
sigma(f(t1, ..., tn)) = f(sigma(t1), ..., sigma(tn))
See also captured.