## ACL2-PC::FREE

(atomic macro) ` `create a ``free variable''
```Major Section:  PROOF-CHECKER
```

```Example:
(free x)

General Form:
(free var)
```
Mark `var` as a ``free variable''. Free variables are only of interest for the `put` command; see its documentation for an explanation.

## ACL2-PC::GENERALIZE

(primitive) ` `perform a generalization
```Major Section:  PROOF-CHECKER
```

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

## ACL2-PC::GOALS

(macro) ` `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.

## ACL2-PC::HELP

(macro) ` `proof-checker help facility
```Major Section:  PROOF-CHECKER
```

```Examples:

(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!
```
The proof checker supports the same kind of documentation as does ACL2 proper. The main difference is that you need to type
```(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)`.

## ACL2-PC::HELP!

(macro) ` `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.

## ACL2-PC::HELP-LONG

(macro) ` `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).

## ACL2-PC::HYPS

(macro) ` `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 governors

General Form:
(hyps &optional hyps-indices govs-indices)
```
Print the indicated top-level hypotheses and governors. (The notion of ``governors'' is defined below.) Here, `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`).

## ACL2-PC::ILLEGAL

(macro) ` `illegal instruction
```Major Section:  PROOF-CHECKER
```

```Example:
(illegal -3)

General Form:
(illegal instruction)
```
Probably not of interest to most users; always ``fails'' since it expands to the `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.

## ACL2-PC::IN-THEORY

(primitive) ` `set the current proof-checker theory
```Major Section:  PROOF-CHECKER
```

```Example:
(in-theory
(union-theories *s-prop-theory* '(true-listp binary-append)))

General Form:
(in-theory &optional atom-or-theory-expression)
```
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.

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.

## ACL2-PC::INDUCT

(atomic macro) ` `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 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.

## ACL2-PC::LISP

(meta) ` `evaluate the given form in Lisp
```Major Section:  PROOF-CHECKER
```

```Example:
(lisp (assign xxx 3))

General Form:
(lisp form)
```
Evaluate `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 ((NIL NIL STATE) . (erp-1 val-1 &)) state)`, then 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 (cons stobjs-out val) &)`, and the `lisp` command returns the appropriate error triple
```(mv erp
val
state).
```

Note that the output signature of the form has been lost. The user must know the signature in order to use the output of the `lisp` command. Trans-eval, which is undocumented except by comments in the ACL2 source code, has replaced, in `val`, any occurrence of the current state or the current values of stobjs by simple symbols such as `REPLACED-STATE`. The actual values of these objects may be recovered, in principle, from the `state` returned and the `user-stobj-alist` within that state. However, in practice, the stobjs cannot be recovered because the user is denied access to `user-stobj-alist`. The moral is: do not try to write macro commands that manipulate stobjs. Should the returned `val` contain `REPLACED-STATE` the value may simply be ignored and `state` used, since that is what `REPLACED-STATE` denotes.

## ACL2-PC::MORE

(macro) ` `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.

## ACL2-PC::MORE!

(macro) ` `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.

## ACL2-PC::NEGATE

(macro) ` `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''.

## ACL2-PC::NIL

(macro) ` `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.

## ACL2-PC::NOISE

(meta) ` `run instructions with output
```Major Section:  PROOF-CHECKER
```

```Example:
(noise induct prove)

General Form:
(noise &rest instruction-list)
```
Run the `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`.

## ACL2-PC::NX

(atomic macro) ` `move forward one argument in the enclosing term
```Major Section:  PROOF-CHECKER
```

```Example and General Form:
nx
```
For 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`.

## ACL2-PC::ORELSE

(macro) ` `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"))

General form:
(orelse instr1 instr2)
```
Run the first instruction. Then if it ``fails'', run the second instruction also; otherwise, stop after the first.

This instruction ``succeeds'' if and only if either `instr1` ``succeeds'', or else `instr2` ``succeeds''. If it ``fails'', then the failure is soft.

## ACL2-PC::P

(macro) ` `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`!).

## ACL2-PC::P-TOP

(macro) ` `prettyprint the conclusion, highlighting the current term
```Major Section:  PROOF-CHECKER
```

```Example and General Form:
p-top
```
For 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.

## ACL2-PC::PP

(macro) ` `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`.

## ACL2-PC::PRINT

(macro) ` `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 terminal

General Form:
(print form)
```
Prettyprints the result of evaluating form. The evaluation of `form` should return a single value that is not `state` or a single-threaded object (see stobj).

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 nil state)` where the second result will always be `REPLACED-STATE`.

## ACL2-PC::PRINT-ALL-GOALS

(macro) ` `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.

## ACL2-PC::PRINT-MAIN

(macro) ` `print the original goal
```Major Section:  PROOF-CHECKER
```

```Example and General Form:
print-main
```

Prints the goal as originally entered.

## ACL2-PC::PRO

(atomic macro) ` `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.

## ACL2-PC::PROMOTE

(primitive) ` `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`.

## ACL2-PC::PROTECT

(macro) ` `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`.

## ACL2-PC::PROVE

(primitive) ` `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 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.

## ACL2-PC::PUT

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

```Example:
(put x 17)

General Form:
(put var expr)
```
Substitute `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.

## ACL2-PC::QUIET

(meta) ` `run instructions without output
```Major Section:  PROOF-CHECKER
```

```Example:
(quiet induct prove)

General Form:
(quiet &rest instruction-list)
```
Run the `instruction-list` through the top-level loop with no output.

See also `noise`.

## ACL2-PC::R

(macro) ` `same as rewrite
```Major Section:  PROOF-CHECKER
```

```Example:
(r 3)

General Form:
(rewrite &optional rule-id substitution
;; below are rare arguments, used for disambiguation:
target-lhs target-rhs target-hyps target-equiv)
```
See the documentation for `rewrite`, as `r` and `rewrite` are identical.

## ACL2-PC::REDUCE

(atomic macro) ` `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 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.

## ACL2-PC::REDUCE-BY-INDUCTION

(macro) ` `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 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.

## ACL2-PC::REMOVE-ABBREVIATIONS

(primitive) ` `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 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`.

## ACL2-PC::REPEAT

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

```Example:
(repeat promote)

General Form:
(repeat instruction)
```
The given `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.

## ACL2-PC::REPEAT-REC

(macro) ` `auxiliary to `repeat`
```Major Section:  PROOF-CHECKER
```

See documentation for `repeat`.

## ACL2-PC::REPLAY

(macro) ` `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 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.

## ACL2-PC::RESTORE

(meta) ` `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)`.

## ACL2-PC::RETAIN

(atomic macro) ` `drop all but the indicated top-level hypotheses
```Major Section:  PROOF-CHECKER
```

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

## ACL2-PC::RETRIEVE

(macro) ` `re-enter the proof-checker
```Major Section:  PROOF-CHECKER
```

```Examples:
(retrieve associativity-of-permutationp)
retrieve

General Form:
(retrieve &optional name)
```
Must be used from `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`.

## ACL2-PC::REWRITE

(primitive) ` `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'' 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 `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.