` `

create a ``free variable''
Major Section: PROOF-CHECKER

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.
` `

perform a generalization
Major Section: PROOF-CHECKER

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).

` `

list the names of goals on the stack
Major Section: PROOF-CHECKER

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.

` `

proof-checker help facility
Major Section: PROOF-CHECKER

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)`

.

` `

proof-checker help facility
Major Section: PROOF-CHECKER

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.

` `

same as `help!`

Major Section: PROOF-CHECKER

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).

` `

print the hypotheses
Major Section: PROOF-CHECKER

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 `cons`

ing `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 `cons`

ing `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 `n`

th 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`

).

` `

illegal instruction
Major Section: PROOF-CHECKER

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.

` `

set the current proof-checker theory
Major Section: PROOF-CHECKER

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.

` `

generate subgoals using induction
Major Section: PROOF-CHECKER

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 goalInduct as in the correspondingGeneral Form: (induct &optional term)

`: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.

` `

evaluate the given form in Lisp
Major Section: PROOF-CHECKER

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) .

` `

proof-checker help facility
Major Section: PROOF-CHECKER

Continues documentation of last proof-checker command visited with
`help`

.

Invoke `help`

for documentation about the proof-checker help
facility.

` `

proof-checker help facility
Major Section: PROOF-CHECKER

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.

` `

run the given instructions, and ``succeed'' if and only if they ``fail''
Major Section: PROOF-CHECKER

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''.

` `

used for interpreting `control-d`

Major Section: PROOF-CHECKER

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.

` `

run instructions with output
Major Section: PROOF-CHECKER

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`

.

` `

move forward one argument in the enclosing term
Major Section: PROOF-CHECKER

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`

.

` `

run the first instruction; if (and only if) it ``fails'', run the
` `

second
Major Section: PROOF-CHECKER

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.

` `

prettyprint the current term
Major Section: PROOF-CHECKER

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`

!).

` `

prettyprint the conclusion, highlighting the current term
Major Section: PROOF-CHECKER

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.

` `

prettyprint the current term
Major Section: PROOF-CHECKER

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`

.

` `

print the result of evaluating the given form
Major Section: PROOF-CHECKER

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)`

.

` `

print all the (as yet unproved) goals
Major Section: PROOF-CHECKER

Example and General Form: print-all-goals

Prints all the goals that remain to be proved, in a pleasant
format.

` `

print the original goal
Major Section: PROOF-CHECKER

Example and General Form: print-main

Prints the goal as originally entered.

` `

repeatedly apply promote
Major Section: PROOF-CHECKER

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.

` `

move antecedents of conclusion's `implies`

term to top-level
` `

hypotheses
Major Section: PROOF-CHECKER

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`

.

` `

run the given instructions, reverting to existing state upon
` `

failure
Major Section: PROOF-CHECKER

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`

.
` `

call the ACL2 theorem prover to prove the current goal
Major Section: PROOF-CHECKER

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 setAttempt to prove the current goal, whereGeneral Form: (prove &rest rest-args)

`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.

` `

substitute for a ``free variable''
Major Section: PROOF-CHECKER

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.

` `

run instructions without output
Major Section: PROOF-CHECKER

Example: (quiet induct prove)Run theGeneral Form: (quiet &rest instruction-list)

`instruction-list`

through the top-level loop with no output.` `

same as rewrite
Major Section: PROOF-CHECKER

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.
` `

call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER

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 hintsAttempt 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.General Form: (reduce &rest hints)

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.

` `

call the ACL2 prover without induction, after going into
` `

induction
Major Section: PROOF-CHECKER

Examples: reduce-by-induction -- attempt to prove the current goal after going into induction, with no further inductionsA 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.(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)

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.

` `

remove one or more abbreviations
Major Section: PROOF-CHECKER

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 termsIf vars is not empty (i.e., notGeneral Forms: (remove-abbreviations &rest vars)

`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`

.

` `

repeat the given instruction until it ``fails''
Major Section: PROOF-CHECKER

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.

` `

auxiliary to `repeat`

Major Section: PROOF-CHECKER

See documentation for `repeat`

.

` `

replay one or more instructions
Major Section: PROOF-CHECKER

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 instructionsReplay the lastGeneral Form: (REPLAY &OPTIONAL n replacement-instruction)

`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.

` `

remove the effect of an UNDO command
Major Section: PROOF-CHECKER

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)`

.

` `

drop all Major Section: PROOF-CHECKER

Example: (RETAIN 2 3) -- keep the second and third hypotheses, and drop the restDrop all top-level hypothesesGeneral Form: (retain &rest args)

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).

` `

re-enter the proof-checker
Major Section: PROOF-CHECKER

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`

.
` `

apply a rewrite rule
Major Section: PROOF-CHECKER

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'' yReplace the current subterm with a new term by applying a rewrite rule. IfGeneral Form: (rewrite &optional rule-id substitution)

`rule-id`

is a positive integer `n`

, then the `n`

th 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.