(atomic macro)
create a ``free variable''
Parent topic: PROOF-CHECKER Home
Example: (free x)MarkGeneral Form: (free var)
var as a ``free variable''. Free variables are only of
interest for the put command; see its documentation for an
explanation.
(primitive)
perform a generalization
Parent topic: PROOF-CHECKER Home
Example: (generalize ((and (true-listp x) (true-listp y)) 0) ((append x y) w))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 formGeneral Form: (generalize &rest substitution)
(term variable), where term may 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 nil or a number,
which causes the system to generate a new name of the form _ or _n,
with n a 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
variable |_| if that variable does not occur in any goal of the
current proof-checker state. Otherwise it treats it as |_0|, or
|_1|, or |_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 |_n|
unless that variable already occurs among the current goals, in
which case it increments n just as above until it obtains a new
variable.
Note: 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).
(macro)
list the names of goals on the stack
Parent topic: PROOF-CHECKER Home
Example and General Form: goals
Goals lists the names of all goals that remain to be proved. They
are listed in the order in which they appear on the stack of
remaining goals, which is relevant for example to the effect of a
change-goal instruction.
(macro)
proof-checker help facility
Parent topic: PROOF-CHECKER Home
Examples:The proof checker supports the same kind of documentation as does ACL2 proper. The main difference is that you need to type(help rewrite) -- partial documentation on the rewrite command; the rest is available using more or more!
(help! rewrite) -- full documentation on the rewrite command
help, help! -- this documentation (in part, or in totality, respectively)
General Forms: (help &optional command) (help! &optional command) more more!
(help command)in a list rather than
:doc command. So, to get all the
documentation on command, type (help! command) inside the
interactive loop, but to get only a one-line description of the
command together with some examples, type (help command). In the
latter case, you can get the rest of the help by typing more!; or
type more if you don't necessarily want all the rest of the help at
once. (Then keep typing more if you want to keep getting more of
the help for that command.)To summarize: as with ACL2, you can type either of the following:
more, more! -- to obtain more (or, all the rest of) the documentation last requested by help (or, outside the proof-checker's loop, :doc)It has been arranged that the use of
(help command) will tell you
just about everything you could want to know about command, almost
always by way of examples. For more details about a command, use
help!, more, or more!.
We use the word ``command'' to refer to the name itself, e.g.
rewrite. We use the word ``instruction'' to refer to an input to
the interactive system, e.g. (rewrite foo) or (help split). Of
course, we allow commands with no arguments as instructions in many
cases, e.g. rewrite. In such cases, command is treated identically
to (command).
(macro)
proof-checker help facility
Parent topic: PROOF-CHECKER Home
Same as help, except that the entire help message is printed without
any need to invoke more! or more.
Invoke help for documentation about the proof-checker help facility.
(macro)
same as help!
Parent topic: PROOF-CHECKER Home
See the documentation for help!.
Help-long has been included in addition to help! for historical
reasons. (Such a command is included in Pc-Nqthm).
(macro)
print the hypotheses
Parent topic: PROOF-CHECKER Home
Examples: hyps -- print all (top-level) hypotheses (hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4 (hyps (1 3) t) -- print hypotheses 1 and 3 and all governorsPrint the indicated top-level hypotheses and governors. (The notion of ``governors'' is defined below.) Here,General Form: (hyps &optional hyps-indices govs-indices)
hyps-indices and
govs-indices should be lists of indices of hypotheses and governors
(respectively), except that the atom t may be used to indicate that
one wants all hypotheses or governors (respectively).
The list of ``governors'' is defined as follows. Actually, we
define here the notion of the governors for a pair of the form
<term, address>]; we're interested in the special case where the
term is the conclusion and the address is the current address. If
the address is nil, then there are no governors, i.e., the list of
governors is nil. If the term is of the form (if x y z) and the
address is of the form (2 . rest) or (3 . rest), then the list of
governors is the result of consing x or its negation (respectively)
onto the list of governors for the pair <y, rest> or the pair
<z, rest> (respectively). If the term is of the form (implies x y)
and the address is of the form (2 . rest), then the list of
governors is the result of consing x onto the list of governors for
the pair <y, rest>. Otherwise, the list of governors for the pair
<term, (n . rest)> is exactly the list of governors for the pair
<argn, rest> where argn is the nth argument of term.
If all goals have been proved, a message saying so will be printed. (as there will be no current hypotheses or governors!).
The hyps command never causes an error. It ``succeeds'' (in fact
its value is t) if the arguments (when supplied) are appropriate,
i.e. either t or lists of indices of hypotheses or governors,
respectively. Otherwise it ``fails'' (its value is nil).
(macro)
illegal instruction
Parent topic: PROOF-CHECKER Home
Example: (illegal -3)Probably not of interest to most users; always ``fails'' since it expands to theGeneral Form: (illegal instruction)
fail command.
The illegal command is used mainly in the implementation. For
example, the instruction 0 is ``read'' as (illegal 0), since dive
expects positive integers.
(primitive)
set the current proof-checker theory
Parent topic: PROOF-CHECKER Home
Example: (in-theory (union-theories *s-prop-theory* '(true-listp binary-append)))If the argument is not supplied, then this command sets the current proof-checker theory (see below for explanation) to agree with the current ACL2 theory. Otherwise, the argument should be a theory expression, and in that case the proof-checker theory is set to the value of that theory expression.General Form: (in-theory &optional atom-or-theory-expression)
The current proof-checker theory is used in all calls to the ACL2
theorem prover and rewriter from inside the proof-checker. Thus,
the most recent in-theory instruction in the current state-stack has
an effect in the proof-checker totally analogous to the effect
caused by an in-theory hint or event in ACL2. However, in-theory
instructions in the proof-checker have no effect outside the
proof-checker's interactive loop.
If the most recent in-theory instruction in the current state of the
proof-checker has no arguments, or if there is no in-theory
instruction in the current state of the proof-checker, then the
proof-checker will use the current ACL2 theory. This is true even
if the user has interrupted the interactive loop by exiting and
changing the global ACL2 theory. However, if the most recent
in-theory instruction in the current state of the proof-checker had
an argument, then global changes to the current theory will have no
effect on the proof-checker state.
(atomic macro)
generate subgoals using induction
Parent topic: PROOF-CHECKER Home
Examples:
induct, (induct t)
-- induct according to a heuristically-chosen scheme, creating
a new subgoal for each base and induction step
(induct (append (reverse x) y))
-- as above, but choose an induction scheme based on the term
(append (reverse x) y) rather than on the current goal
General Form:
(induct &optional term)
Induct as in the corresponding :induct hint given to the theorem
prover, creating new subgoals for the base and induction steps. If
term is t or is not supplied, then use the current goal to determine
the induction scheme; otherwise, use that term.Note: As usual, abbreviations are allowed in the term.
Note: Induct actually calls the prove command with all processes
turned off. Thus, you must be at top of the goal for an induct
instruction.
(meta)
evaluate the given form in Lisp
Parent topic: PROOF-CHECKER Home
Example: (lisp (assign xxx 3))EvaluateGeneral Form: (lisp form)
form. The lisp command is mainly of interest for side
effects. See also print, skip, and fail.
The rest of the documentation for lisp is of interest only to
those who use it in macro commands. If the Lisp evaluation (by
trans-eval) of form returns an ``error triple'' of the form
(mv erp (cons 3 val) &), then val is of the form (erp-1 val-1 &),
and the lisp command returns the appropriate error triple
(mv (or erp erp-1)
val-1
state) .
Otherwise, the trans-eval of form must return an ``error triple''
of the form (mv erp (list* state-out mult val) &), and the lisp
command returns the appropriate error triple
(mv erp
val
state) .
(macro)
proof-checker help facility
Parent topic: PROOF-CHECKER Home
Continues documentation of last proof-checker command visited with
help.
Invoke help for documentation about the proof-checker help
facility.
(macro)
proof-checker help facility
Parent topic: PROOF-CHECKER Home
Continues documentation of last proof-checker command visited with
help, until all documentation on that command is printed out.
Invoke help for documentation about the proof-checker help facility.
(macro)
run the given instructions, and ``succeed'' if and only if they ``fail''
Parent topic: PROOF-CHECKER Home
Example: (negate prove)
General form: (negate &rest instruction-list)Run the indicated instructions exactly in the sense of
do-all, and
``succeed'' if and only if they ``fail''.
Note: Negate instructions will never produce hard ``failures''.
(macro)
used for interpreting control-d
Parent topic: PROOF-CHECKER Home
Example and General form: nil(or,
control-d).
The whole point of this command is that in some Lisps (including
akcl), if you type control-d then it seems, on occasion, to get
interpreted as nil. Without this command, one seems to get into an
infinite loop.
(meta)
run instructions with output
Parent topic: PROOF-CHECKER Home
Example: (noise induct prove)Run theGeneral Form: (noise &rest instruction-list)
instruction-list through the top-level loop with output.
In fact, having output is the default. Noise is useful inside a
surrounding call of quiet, when one temporarily wants output. For
example, if one wants to see output for a prove command immediately
following an induct command but before an s command, one may want to
submit an instruction like (quiet induct (noise prove) s). See also
quiet.
(atomic macro)
move forward one argument in the enclosing term
Parent topic: PROOF-CHECKER Home
Example and General Form: nxFor example, if the conclusion is
(= x (* (- y) z)) and the
current subterm is x, then after executing nx, the current
subterm will be (* (- y) z).
This is the same as up followed by (dive n+1), where n is the
position of the current subterm in its parent term in the
conclusion. Thus in particular, the nx command fails if one is
already at the top of the conclusion.
See also up, dive, top, and bk.
(macro)
run the first instruction; if (and only if) it ``fails'', run the
second
Parent topic: PROOF-CHECKER Home
Example: (orelse top (print "Couldn't move to the top"))Run the first instruction. Then if it ``fails'', run the second instruction also; otherwise, stop after the first.General form: (orelse instr1 instr2)
This instruction ``succeeds'' if and only if either instr1
``succeeds'', or else instr2 ``succeeds''. If it ``fails'', then
the failure is soft.
(macro)
prettyprint the current term
Parent topic: PROOF-CHECKER Home
Example and General Form: p
Prettyprint the current term. The usual user syntax is used, so
that for example one would see (and x y) rather than (if x y 'nil).
(See also pp.) Also, abbreviations are inserted where appropriate;
see add-abbreviation.
The ``current term'' is the entire conclusion unless dive commands
have been given, in which case it may be a subterm of the
conclusion.
If all goals have been proved, a message saying so will be printed
(as there will be no current term!).
(macro)
prettyprint the conclusion, highlighting the current term
Parent topic: PROOF-CHECKER Home
Example and General Form: p-topFor example, if the conclusion is
(equal (and x (p y)) (foo z)) and
the current subterm is (p y), then p-top will print
(equal (and x (*** (p y) ***)) (foo z)).
Prettyprint the the conclusion, highlighting the current term. The
usual user syntax is used, as with the command p (as opposed to pp).
This is illustrated in the example above, where one would *not* see
(equal (if x (*** (p y) ***) 'nil) (foo z)).
Note (obscure): In some situations, a term of the form (if x t y)
occurring inside the current subterm will not print as (or x y),
when x isn't a call of a boolean primitive. There's nothing
incorrect about this, however.
(macro)
prettyprint the current term
Parent topic: PROOF-CHECKER Home
Example and General Form: pp
This is the same as p (see its documentation), except that raw
syntax (internal form) is used. So for example, one would see
(if x y 'nil) rather than (and x y). Abbreviations are however
still inserted, as with p.
(macro)
print the result of evaluating the given form
Parent topic: PROOF-CHECKER Home
Example: (print (append '(a b) '(c d))) Print the list (a b c d) to the terminalPrettyprints the result of evaluating form. The evaluation ofGeneral Form: (print form)
form
should return a single value that is not state.
If the form you want to evaluate does not satisfy the criterion
above, you should create an appropriate call of the lisp command
instead. Notice that this command always returns
(mv nil state state).
(macro)
print all the (as yet unproved) goals
Parent topic: PROOF-CHECKER Home
Example and General Form: print-all-goals
Prints all the goals that remain to be proved, in a pleasant format.
(macro)
print the original goal
Parent topic: PROOF-CHECKER Home
Example and General Form: print-main
Prints the goal as originally entered.
(atomic macro)
repeatedly apply promote
Parent topic: PROOF-CHECKER Home
Example and General Form: pro
Apply the promote command until there is no change. This command
``succeeds'' exactly when at least one call of promote ``succeeds''.
In that case, only a single new proof-checker state will be
created.
(primitive)
move antecedents of conclusion's implies term to top-level
hypotheses
Parent topic: PROOF-CHECKER Home
Examples: promote (promote t)For example, if the conclusion is
(implies (and x y) z), then
after execution of promote, the conclusion will be z and the terms x
and y will be new top-level hypotheses.
General Form: (promote &optional do-not-flatten-flag)Replace conclusion of
(implies hyps exp) or (if hyps exp t) with
simply exp, adding hyps to the list of top-level hypotheses.
Moreover, if hyps is viewed as a conjunction then each conjunct will
be added as a separate top-level hypothesis. An exception is that
if do-not-flatten-flag is supplied and not nil, then only one
top-level hypothesis will be added, namely hyps.
Note: You must be at the top of the conclusion in order to use this
command. Otherwise, first invoke top.
(macro)
run the given instructions, reverting to existing state upon
failure
Parent topic: PROOF-CHECKER Home
Example: (protect induct p prove)General Form: (protect &rest instruction-list)
Protect is the same as do-strict, except that as soon as an
instruction ``fails'', the state-stack reverts to what it was before
the protect instruction began, and restore is given the same meaning
that it had before the protect instruction began. See the
documentation for do-strict.
(primitive)
call the ACL2 theorem prover to prove the current goal
Parent topic: PROOF-CHECKER Home
Examples:
prove -- attempt to prove the current goal
(prove :otf-flg t
:hints (("Subgoal 2" :by foo) ("Subgoal 1" :use bar)))
-- attempt to prove the current goal, with the indicated hints
and with OTF-FLG set
General Form:
(prove &rest rest-args)
Attempt to prove the current goal, where rest-args is as in the
keyword arguments to defthm except that only :hints and :otf-flg are
allowed. The command succeeds exactly when the corresponding defthm
would succeed, except that it is all right for some goals to be
given ``bye''s. Each goal given a ``bye'' will be turned into a new
subgoal. (See hints for an explanation of :by hints.)
Note: Use (= t) instead if you are not at the top of the
conclusion. Also note that if there are any hypotheses in the
current goal, then what is actually attempted is a proof of
(implies hyps conc), where hyps is the conjunction of the
top-level hypotheses and conc is the goal's conclusion.
Note: It is allowed to use abbreviations in the hints.
(macro)
substitute for a ``free variable''
Parent topic: PROOF-CHECKER Home
Example: (put x 17)SubstituteGeneral Form: (put var expr)
expr for the ``free variable'' var, as explained below.
A ``free variable'' is, for our purposes, a variable var such that
the instruction (free var) has been executed earlier in the
state-stack. What (free var) really does is to let var be an
abbreviation for the term (hide var) (see documentation for
add-abbreviation). What (put var expr) really does is to unwind the
state-stack, replacing that free instruction with the instruction
(add-abbreviation var expr), so that future references to (? var)
become reference to expr rather than to (hide var), and then to
replay all the other instructions that were unwound. Because hide
was used, the expectation is that in most cases, the instructions
will replay successfully and put will ``succeed''. However, if any
replayed instruction ``fails'', then the entire replay will abort
and ``fail'', and the state-stack will revert to its value before
the put instruction was executed.
If (put var expr) ``succeeds'', then (remove-abbreviation var) will
be executed at the end.
Note: The restore command will revert the state-stack to its value
present before the put instruction was executed.
(meta)
run instructions without output
Parent topic: PROOF-CHECKER Home
Example: (quiet induct prove)Run theGeneral Form: (quiet &rest instruction-list)
instruction-list through the top-level loop with no output.
See also noise.
(macro)
same as rewrite
Parent topic: PROOF-CHECKER Home
Example: (r 3)See the documentation forGeneral Form: (rewrite &optional rule-id substitution ;; below are rare arguments, used for disambiguation: target-lhs target-rhs target-hyps target-equiv)
rewrite, as r and rewrite are identical.
(atomic macro)
call the ACL2 theorem prover's simplifier
Parent topic: PROOF-CHECKER Home
Examples:
reduce -- attempt to prove the current goal without using induction
(reduce ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
-- attempt to prove the current goal by without using
induction, with the indicated hints
General Form:
(reduce &rest hints)
Attempt to prove the current goal without using induction, using the
indicated hints (if any). A subgoal will be created for each goal
that would have been pushed for proof by induction in an ordinary
proof.
Notice that unlike prove, the arguments to reduce are spread out,
and are all hints.
Note: Induction will be used to the extent that it is ordered explicitly in the hints.
(macro)
call the ACL2 prover without induction, after going into
induction
Parent topic: PROOF-CHECKER Home
Examples:
reduce-by-induction
-- attempt to prove the current goal after going into induction,
with no further inductions
(reduce-by-induction ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
-- attempt to prove the current goal after going into induction,
with no further inductions, using the indicated hints
General Form:
(reduce-by-induction &rest hints)
A subgoal will be created for each goal that would have been
pushed for proof by induction in an ordinary proof, except that the
proof begins with a top-level induction.
Notice that unlike prove, the arguments to reduce-by-induction are
spread out, and are all hints. See also prove, reduce, and bash.
Note: Induction and the various processes will be used to the
extent that they are ordered explicitly in the :induct and :do-not
hints.
(primitive)
remove one or more abbreviations
Parent topic: PROOF-CHECKER Home
Examples:
remove-abbreviations -- remove all abbreviations
(remove-abbreviations v w)
-- assuming that V and W currently abbreviate
terms, then they are ``removed'' in the
sense that they are no longer considered to
abbreviate those terms
General Forms:
(remove-abbreviations &rest vars)
If vars is not empty (i.e., not nil), remove the variables in vars
from the current list of abbreviations, in the sense that each
variable in vars will no longer abbreviate a term.Note: The instruction fails if at least one of the arguments fails to be a variable that abbreviates a term.
See also the documentation for add-abbreviation, which contains a
discussion of abbreviations in general, and show-abbreviations.
(macro)
repeat the given instruction until it ``fails''
Parent topic: PROOF-CHECKER Home
Example: (repeat promote)The givenGeneral Form: (repeat instruction)
instruction is run repeatedly until it ``fails''.Note: There is nothing here in general to prevent the instruction from being run after all goals have been proved, though this is indeed the case for primitive instructions.
(macro)
auxiliary to repeat
Parent topic: PROOF-CHECKER Home
See documentation for repeat.
(macro)
replay one or more instructions
Parent topic: PROOF-CHECKER Home
Examples:
REPLAY -- replay all instructions in the current session
(i.e., state-stack)
(REPLAY 5) -- replay the most recent 5 instructions
(REPLAY 5
(COMMENT deleted dive command here))
-- replace the 5th most recent instruction with the
indicated comment instruction, and then replay it
followed by the remaining 4 instructions
General Form:
(REPLAY &OPTIONAL n replacement-instruction)
Replay the last n instructions if n is a positive integer; else n
should be nil or not supplied, and replay all instructions.
However, if replacement-instruction is supplied and not nil, then
before the replay, replace the nth instruction (from the most
recent, as shown by commands) with replacement-instruction.
If this command ``fails'', then the restore command will revert the
state-stack to its value present before the replay instruction was
executed.
(meta)
remove the effect of an UNDO command
Parent topic: PROOF-CHECKER Home
Example and General Form: restore
Restore removes the effect of an undo command. This always works as
expected if restore is invoked immediately after undo, without
intervening instructions. However, other commands may also interact
with restore, notably ``sequencing'' commands such as do-all,
do-strict, protect, and more generally, sequence.
Note: Another way to control the saving of proof-checker state is
with the save command; see the documentation for save.
The restore command always ``succeeds''; it returns
(mv nil t state).
(atomic macro)
drop all but the indicated top-level hypotheses
Parent topic: PROOF-CHECKER Home
Example:
(RETAIN 2 3) -- keep the second and third hypotheses, and drop
the rest
General Form:
(retain &rest args)
Drop all top-level hypotheses except those with the indicated
indices.There must be at least one argument, and all must be in range (i.e. integers between one and the number of top-level hypotheses, inclusive).
(macro)
re-enter the proof-checker
Parent topic: PROOF-CHECKER Home
Examples: (retrieve associativity-of-permutationp) retrieveMust be used fromGeneral Form: (retrieve &optional name)
outside the interactive proof-checker loop. If
name is supplied and not nil, this causes re-entry to the
interactive proof-checker loop in the state at which save was last
executed for the indicated name. (See documentation for save.) If
name is nil or is not supplied, then the user is queried regarding
which proof-checker state to re-enter. The query is omitted,
however, if there only one proof-checker state is present that was
saved with save, in which case that is the one that is used. See
also unsave.
(primitive)
apply a rewrite rule
Parent topic: PROOF-CHECKER Home
Examples:
(rewrite reverse-reverse)
-- apply the rewrite rule `reverse-reverse'
(rewrite (:rewrite reverse-reverse))
-- same as above
(rewrite 2)
-- apply the second rewrite rule, as displayed by show-rewrites
rewrite
-- apply the first rewrite rule, as displayed by show-rewrites
(rewrite transitivity-of-< ((y 7)))
-- apply the rewrite rule transitivity-of-< with the substitution
that associates 7 to the ``free variable'' y
General Form:
(rewrite &optional rule-id substitution)
Replace the current subterm with a new term by applying a rewrite
rule. If rule-id is a positive integer n, then the nth rewrite
rule as displayed by show-rewrites is the one that is applied. If
rule-id is nil or is not supplied, then it is treated as the number
1. Otherwise, rule-id should be either a rune of or name of a
rewrite rule. If a name is supplied, then any rule of that name may
be used. More explanation of all of these points follows below.
Consider first the following example. Suppose that the current
subterm is (reverse (reverse y)) and that there is a rewrite rule
called reverse-reverse of the form
(implies (true-listp x)
(equal (reverse (reverse x)) x)) .
Then the instruction (rewrite reverse-reverse) would cause the
current subterm to be replaced by y and would create a new goal with
conclusion (true-listp y). An exception is that if the top-level
hypotheses imply (true-listp y) using only ``trivial reasoning''
(more on this below), then no new goal is created.
A rather important point is that if the rule-id argument is a number
or is not supplied, then the system will store an instruction of the
form (rewrite name ...), where name is the name of a rewrite rule;
this is in order to make it easier to replay instructions when there
have been changes to the history. Actually, instead of the name
(whether the name is supplied or calculated), the system stores the
rune if there is any chance of ambiguity. (Formally, ``ambiguity''
here means that the rune being applied is of the form
(:rewrite name . index), where index is not nil.)
Speaking in general, then, a rewrite instruction works as follows:
First, a rewrite rule is selected according to the arguments of the
rewrite instruction. The selection is made as explained above under
``General Form'' above. The ``disambiguating rare arguments'' will
rarely be of interest to the user; as explained just above, the
stored instruction always contains the name of the rewrite rule, so
if there is more than one rule of that name then the system creates
and stores these extra arguments in order to make the resulting
instruction unambiguous, i.e., so that only one rewrite rule
applies. For what it's worth, they correspond respectively to the
fields of a rewrite rule record named lhs, rhs, hyps, and equiv.
Next, the left-hand side of the rule is matched with the current
subterm, i.e., a substitution unify-subst is found such that if one
instantiates the left-hand side of the rule with unify-subst, then
one obtains the current subterm. If this matching fails, then the
instruction fails.
Now an attempt is made to relieve the hypotheses, in much the same
sense as the theorem prover relieves hypotheses except that there is
no call to the rewriter. Essentially, this means that the
substitution unify-subst is applied to the hypotheses and the system
then checks whether all hypotheses are ``clearly'' true in the
current context. If there are variables in the hypotheses of the
rewrite rule that do not occur in the left-hand side of the
conclusion even after the user-supplied substitution (default: nil)
is applied, then a weak attempt is made to extend that substitution
so that even those hypotheses can be relieved. However, if even one
hypothesis remains unrelieved, then no automatic extension of the
substitution is made, and in fact hypotheses that contain even one
uninstantiated variable will remain unrelieved.
Finally, the instruction is applied as follows. The current subterm
is replaced by applying the final substitution, i.e., the extension
of unify-subst by the user-supplied substitution which may in turn
be extended by the system (as explained above) in order to relieve
all hypotheses, to the right-hand side of the selected rewrite rule.
And, one new subgoal is created for each unrelieved hypothesis of
the rule, whose top-level hypotheses are the governors and top-level
hypotheses of the current goal and whose conclusion and current
subterm are the instance, by that same final substitution, of that
unrelieved hypothesis.
Note: The substitution argument should be a list whose elements
have the form (variable term), where term may contain
abbreviations.