perform a generalization
Major Section: PROOF-CHECKER-COMMANDS
Example: (generalize ((and (true-listp x) (true-listp y)) 0) ((append x y) w)) General Form: (generalize &rest substitution)Generalize using the indicated substitution, which should be a non-empty list. Each element of that list should be a two-element list of the form
(term variable), where
termmay use abbreviations. The effect of the instruction is to replace each such term in the current goal by the corresponding variable. This replacement is carried out by a parallel substitution, outside-in in each hypothesis and in the conclusion. More generally, actually, the ``variable'' (second) component of each pair may be
nilor a number, which causes the system to generate a new name of the form
na natural number; more on this below. However, when a variable is supplied, it must not occur in any goal of the current proof-checker state.
When the ``variable'' above is
nil, the system will treat it as the
|_| if that variable does not occur in any goal of the
current proof-checker state. Otherwise it treats it as
|_2|, and so on, until one of these is not among the
variables of the current proof-checker state. If the ``variable''
is a non-negative integer
n, then the system treats it as
unless that variable already occurs among the current goals, in
which case it increments n just as above until it obtains a new
Remark: The same variable may not occur as the variable component of
two different arguments (though
nil may occur arbitrarily many
times, as may a positive integer).