LP, the Larch Prover -- The instantiate command
The instantiate command provides a method of forward inference, which can
be used to substitute terms for free variables, or to eliminate
universal quantifiers, from facts in LP's logical system.
<instantiate-command> ::= instantiate (<variable> by <term>)+, in <names>
Examples
instantiate s2 by s1 \U s1 in setExtensionality
instantiate x by 0, y by 1 in lemmas
Usage
The instantiate command substitutes (simultaneously) the specified terms
for the named free variables in the named formulas, rewrite rules, and
deduction rules; if a named variable does not occur free in a named fact, but
is bound by an accessible prenex-universal
quantifier in that fact, then that quantifier is eliminated before the
substitution is performed. LP automatically changes bound variables in the
named facts, if needed, to avoid having them bind (or
capture) variables that occur free in the
specified terms.
LP normalizes any nonimmune results from an
instantiation, discarding those that normalize to true and orienting any
resulting formulas into rewrite rules if the automatic-ordering
setting is on. The activity and immunity of the
results are determined by the current values of the activity and immunity
settings. When instantiating a rewrite rule, LP does not use that rule in
normalizing the result.