` `

attempt an equality (or equivalence) substitution
Major Section: PROOF-CHECKER

Examples: = -- replace the current subterm by a term equated to it in one of the hypotheses (if such a term exists) (= x) -- replace the current subterm by x, assuming that the prover can show that they are equal (= (+ x y) z) -- replace the term (+ x y) by the term z inside the current subterm, assuming that the prover can prove (equal (+ x y) z) from the current top-level hypotheses or that this term or (equal z (+ x y)) is among the current top-level hypotheses or the current governors (= & z) -- exactly the same as above, if (+ x y) is the current subterm (= (+ x y) z :hints :none) -- same as (= (+ x y) z), except that a new subgoal is created with the current goal's hypotheses and governors as its top-level hypotheses and (equal (+ x y) z) as its conclusion (= (+ x y) z 0) -- exactly the same as immediately above (= (p x) (p y) :equiv iff :otf-flg t :hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar))) -- same as (= (+ x y) z), except that the prover uses the indicated values for otf-flg and hints, and only propositional (iff) equivalence is used (however, it must be that only propositional equivalence matters at the current subterm)If termsGeneral Form: (= &optional x y &rest keyword-args)

`x`

and `y`

are supplied, then replace `x`

by `y`

inside the
current subterm if they are ``known'' to be ``equal''. Here
``known'' means the following: the prover is called as in the `prove`

command (using `keyword-args`

) to prove `(equal x y)`

, except that a
keyword argument `:equiv`

is allowed, in which case `(equiv x y)`

is
proved instead, where `equiv`

is that argument. (See below for how
governors are handled.)
Actually, `keyword-args`

is either a single non-keyword or is a list
of the form `((kw-1 x-1) ... (kw-n x-n))`

, where each `kw-i`

is one of
the keywords `:equiv`

, `:otf-flg`

, `:hints`

. Here `:equiv`

defaults to
`equal`

if the argument is not supplied or is `nil`

, and otherwise
should be the name of an ACL2 equivalence relation. `:Otf-flg`

and
`:hints`

give directives to the prover, as explained above and in the
documentation for the `prove`

command; however, no prover call is made
if `:hints`

is a non-`nil`

atom or if `keyword-args`

is a single
non-keyword (more on this below).

*Remarks on defaults*

(1) If there is only one argument, say `a`

, then `x`

defaults to the
current subterm, in the sense that `x`

is taken to be the current
subterm and `y`

is taken to be `a`

.

(2) If there are at least two arguments, then `x`

may be the symbol
`&`

, which then represents the current subterm. Thus, `(= a)`

is
equivalent to `(= & a)`

. (Obscure point: actually, `&`

can be in any
package, except the keyword package.)

(3) If there are no arguments, then we look for a top-level
hypothesis or a governor of the form `(equal c u)`

or `(equal u c)`

,
where `c`

is the current subterm. In that case we replace the current
subterm by `u`

.

As with the `prove`

command, we allow goals to be given ``bye''s in
the proof, which may be generated by a `:hints`

keyword argument in
`keyword-args`

. These result in the creation of new subgoals.

A proof is attempted unless the `:hints`

argument is a non-`nil`

atom other than :`none`

, or unless there is one element of
`keyword-args`

and it is not a keyword. In that case, if there are
any hypotheses in the current goal, then what is attempted is a
proof of the implication whose antecedent is the conjunction of the
current hypotheses and governors and whose conclusion is the
appropriate `equal`

term.

**Notes:** (1) It is allowed to use abbreviations in the hints.
(2) The keyword :`none`

has the special role as a value of
:`hints`

that is shown clearly in an example above. (3) If there
are governors, then the new subgoal has as additional hypotheses the
current governors.

` `

same as `(lisp x)`

Major Section: PROOF-CHECKER

Example: (acl2-wrap (pe :here))Same asGeneral Form: (acl2-wrap form)

`(lisp form)`

. This is provided for interface tools that
want to be able to execute the same form in raw Lisp, in the
proof-checker, or in the ACL2 top-level loop `(lp)`

.
` `

add an abbreviation
Major Section: PROOF-CHECKER

Example: `(add-abbreviation v (* x y))`

causes future occurrences of
`(* x y)`

to be printed as `(? v)`

, until (unless) a corresponding
invocation of `remove-abbreviations`

occurs. In this case we say that
`v`

``abbreviates'' `(* x y)`

.

General Form: (add-abbreviation var &optional raw-term)Let

`var`

be an abbreviation for `raw-term`

, if `raw-term`

is supplied,
else for the current subterm. Note that `var`

must be a variable that
does not already abbreviate some term.
A way to think of abbreviations is as follows. Imagine that
whenever an abbreviation is added, say `v`

abbreviates `expr`

, an entry
associating `v`

to `expr`

is made in an association list, which we will
call ```*abbreviations-alist*`

''. Then simply imagine that `?`

is a
function defined by something like:

(defun ? (v) (let ((pair (assoc v *abbreviations-alist*))) (if pair (cdr pair) (error ...))))Of course the implementation isn't exactly like that, since the ``constant''

`*abbreviations-alist*`

actually changes each time an
`add-abbreviation`

instruction is successfully invoked. Nevertheless,
if one imagines an appropriate redefinition of the ``constant''
`*abbreviations-alist*`

each time an `add-abbreviation`

is invoked, then
one will have a clear model of the meaning of such an instruction.
The effect of abbreviations on output is that before printing a
term, each subterm that is abbreviated by a variable `v`

is first
replaced by `(? v)`

.

The effect of abbreviations on input is that every built-in
proof-checker command accepts abbreviations wherever a term is
expected as an argument, i.e., accepts the syntax `(? v)`

whenever `v`

abbreviates a term. For example, the second argument of
`add-abbreviation`

may itself use abbreviations that have been defined
by previous `add-abbreviation`

instructions.

See also `remove-abbreviations`

and `show-abbreviations`

.

` `

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

Examples: bash -- attempt to prove the current goal by simplification alone (bash ("Subgoal 2" :by foo) ("Subgoal 1" :use bar)) -- attempt to prove the current goal by simplification alone, with the indicated hintsCall the theorem prover's simplifier, creating a subgoal for each resulting goal.General Form: (bash &rest hints)

Notice that unlike `prove`

, the arguments to `bash`

are spread out, and
are all hints.

**Note:** All forcing rounds will be skipped (unless there are more
than 15 subgoals generated in the first forcing round, an injustice
that should be rectified by the next release).

` `

prove the current goal using bdds
Major Section: PROOF-CHECKER

Examples: bdd (bdd :vars nil :bdd-constructors (cons) :prove t :literal :all)

The general form is as shown in the latter example above, but with
any keyword-value pairs omitted and with values as described for the
`:`

`bdd`

hint; see hints.

This command simply calls the theorem prover with the indicated bdd
hint for the top-level goal. Note that if `:prove`

is `t`

(the
default), then the proof will succeed entirely using bdds or else
it will fail immediately. See bdd.

` `

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

Example and General Form: bkFor example, if the conclusion is

`(= x (* (- y) z))`

and the current
subterm is `(* (- y) z)`

, then after executing `bk`

, the current subterm
will be `x`

.
Move to the previous argument of the enclosing term.

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`

.

` `

insert matching ``bookends'' comments
Major Section: PROOF-CHECKER

Example: (bookmark final-goal)Run the instructions inGeneral Form: (bookmark name &rest instruction-list)

`instruction-list`

(as though this were a
call of `do-all`

; see the documentation for `do-all`

), but first insert
a begin bookend with the given name and then, when the instructions
have been completed, insert an end bookend with that same name. See
the documentation of `comm`

for an explanation of bookends and how
they can affect the display of instructions.
` `

split into two cases
Major Section: PROOF-CHECKER

Example: (casesplit (< x y)) -- assuming that we are at the top of the conclusion, add (< x y) as a new top-level hypothesis in the current goal, and create a subgoal identical to the current goal except that it has (not (< x y)) as a new top-level hypothesisWhen the current subterm is the entire conclusion, this instruction addsGeneral Form: (casesplit expr &optional use-hyps-flag do-not-flatten-flag)

`expr`

as a new top-level hypothesis, and create a subgoal
identical to the existing current goal except that it has the
negation of `expr`

as a new top-level hypothesis. See also `claim`

.
The optional arguments control the use of governors and the
``flattening'' of new hypotheses, as we now explain.
The argument `use-hyps-flag`

is only of interest when there are
governors. (To read about governors, see the documentation for the
command `hyps`

). In that case, if `use-hyps-flag`

is not supplied or is
`nil`

, then the description above is correct; but otherwise, it is not
`expr`

but rather it is `(implies govs expr)`

that is added as a new
top-level hypothesis (and whose negation is added as a top-level
hypothesis for the new goal), where `govs`

is the conjunction of the
governors.

If `do-not-flatten-flag`

is supplied and not `nil`

, then that is
all there is to this command. Otherwise (thus this is the default),
when the claimed term (first argument) is a conjunction (`and`

) of
terms and the `claim`

instruction succeeds, then each (nested)
conjunct of the claimed term is added as a separate new top-level
hypothesis. Consider the following example, assuming there are no
governors.

(casesplit (and (and (< x y) (integerp a)) (equal r s)) t)Three new top-level hypotheses are added to the current goal, namely

`(< x y)`

, `(integerp a)`

, and `(equal r s)`

. In that case, only
one hypothesis is added to create the new goal, namely the negation
of `(and (< x y) (integerp a) (equal r s))`

. If the negation of this
term had been `claim`

ed, then it would be the other way around: the
current goal would get a single new hypothesis while the new goal
would be created by adding three hypotheses.
**Note:** It is allowed to use abbreviations in the hints.

` `

change to another goal.
Major Section: PROOF-CHECKER

Examples: (cg (main . 1)) -- change to the goal (main . 1) cg -- change to the next-to-top goalSame asGeneral Form: (CG &OPTIONAL goal-name)

`(change-goal goal-name t)`

, i.e. change to the indicated
and move the current goal to the end of the goal stack.
` `

change to another goal.
Major Section: PROOF-CHECKER

Examples: (change-goal (main . 1)) -- change to the goal (main . 1) change-goal -- change to the next-to-top goalChange to the goal with the nameGeneral Form: (change-goal &optional goal-name end-flg)

`goal-name`

, i.e. make it the
current goal. However, if `goal-name`

is `nil`

or is not supplied, then
it defaults to the next-to-top goal, i.e., the second goal in the
stack of goals. If `end-flg`

is supplied and not `nil`

, then move the
current goal to the end of the goal stack; else merely swap it with
the next-to-top goal. Also see documentation for `cg`

.
` `

add a new hypothesis
Major Section: PROOF-CHECKER

Examples: (claim (< x y)) -- attempt to prove (< x y) from the current top-level hypotheses and if successful, then add (< x y) as a new top-level hypothesis in the current goal (claim (< x y) :otf-flg t :hints (("Goal" :induct t))) -- as above, but call the prover using the indicated values for the otf-flg and hints (claim (< x y) 0) -- as above, except instead of attempting to prove (< x y), create a new subgoal with the same top-level hypotheses as the current goal that has (< x y) as its conclusion (claim (< x y) :hints :none) -- same as immediately aboveThis command creates a new subgoal with the same top-level hypotheses as the current goal but with a conclusion ofGeneral Form: (claim expr &rest rest-args)

`expr`

. If
`rest-args`

is a non-empty list headed by a non-keyword, then there
will be no proof attempted for the new subgoal. With that possible
exception, `rest-args`

should consist of keyword arguments. The
keyword argument `:do-not-flatten`

controls the ``flattening'' of new
hypotheses, just as with the `casesplit`

command (as described in its
documentation). The remaining `rest-args`

are used with a call the
`prove`

command on the new subgoal, except that if `:hints`

is a non-`nil`

atom, then the prover is not called -- rather, this is the same as
the situation described above, where `rest-args`

is a non-empty list
headed by a non-keyword.
**Notes:** (1) Unlike the `casesplit`

command, the `claim`

command is completely insensitive to governors. (2) It is allowed to
use abbreviations in the hints. (3) The keyword :`none`

has the
special role as a value of :`hints`

that is shown clearly in an
example above.

` `

display instructions from the current interactive session
Major Section: PROOF-CHECKER

Examples: comm (comm 10)Prints out instructions in reverse order. This is actually the same asGeneral Form: (comm &optional n)

`(commands n t)`

-- or, `(commands nil t)`

if `n`

is not supplied. As
explained in the documentation for `commands`

, the final argument of `t`

causes suppression of instructions occurring between so-called
``matching bookends,'' which we now explain.A ``begin bookend'' is an instruction of the form

(COMMENT :BEGIN x . y).Similarly, an ``end bookend'' is an instruction of the form

(COMMENT :END x' . y').The ``name'' of the first bookend is

`x`

and the ``name'' of the
second bookend is `x'`

. When such a pair of instructions occurs in
the current state-stack, we call them ``matching bookends'' provided
that they have the same name (i.e. `x`

equals `x'`

) and if no other
begin or end bookend with name `x`

occurs between them. The idea now
is that `comm`

hides matching bookends together with the instructions
they enclose. Here is a more precise explanation of this
``hiding''; probably there is no value in reading on!
A `comm`

instruction hides bookends in the following manner. (So does
a `comment`

instruction when its second optional argument is supplied
and non-`nil`

.) First, if the first argument `n`

is supplied and not
`nil`

, then we consider only the last `n`

instructions from the
state-stack; otherwise, we consider them all. Now the resulting
list of instructions is replaced by the result of applying the
following process to each pair of matching bookends: the pair is
removed, together with everything in between the begin and end
bookend of the pair, and all this is replaced by the ``instruction''

("***HIDING***" :COMMENT :BEGIN name ...)where

`(comment begin name ...)`

is the begin bookend of the pair.
Finally, after applying this process to each pair of matching
bookends, each begin bookend of the form `(comment begin name ...)`

that remains is replaced by
("***UNFINISHED***" :COMMENT :BEGIN name ...) .

` `

display instructions from the current interactive session
Major Section: PROOF-CHECKER

Examples: commands (commands 10 t)General Forms:

commands or (commands nil) Print out all the instructions (in the current state-stack) in reverse order, i.e. from the most recent instruction to the starting instruction.

(commands n) [n a positive integer] Print out the most recent n instructions (in the current state-stack), in reverse order.

(commands x abbreviate-flag) Same as above, but if abbreviate-flag is non-NIL, then do not display commands between ``matching bookends''. See documentation for comm for an explanation of matching bookends.

`n`

instructions in the state-stack,
then `(commands n)`

is the same as `commands`

(and also,
`(commands n abb)`

is the same as `(commands nil abb)`

).
` `

insert a comment
Major Section: PROOF-CHECKER

Example: (comment now begin difficult final goal)This instruction makes no change in the state except to insert theGeneral Form: (comment &rest x)

`comment`

instruction.
Some comments can be used to improve the display of commands; see
documentation for `comm`

.

` `

same as `contrapose`

Major Section: PROOF-CHECKER

see documentation for `contrapose`

` `

switch a hypothesis with the conclusion, negating both
Major Section: PROOF-CHECKER

Example: (contrapose 3)The (optional) argumentGeneral Form: (contrapose &optional n)

`n`

should be a positive integer that does
not exceed the number of hypotheses. Negate the current conclusion
and make it the `n`

th hypothesis, while negating the current `n`

th
hypothesis and making it the current conclusion. If no argument is
supplied then the effect is the same as for `(contrapose 1)`

.
**Note:** By ``negate'' we mean an operation that replaces `nil`

by `t`

, `x`

by `nil`

for any other explicit value `x`

, `(not x)`

by `x`

, and any other `x`

by `(not x)`

.

` `

move top-level hypotheses to the conclusion
Major Section: PROOF-CHECKER

Examples: demote -- demote all top-level hypotheses (demote 3 5) -- demote hypotheses 3 and 5For example, if the top-level hypotheses are

`x`

and `y`

and the
conclusion is `z`

, then after execution of `demote`

, the conclusion will
be `(implies (and x y) z)`

and there will be no (top-level)
hypotheses.

General Form: (demote &rest hyps-indices)Eliminate the indicated (top-level) hypotheses, but replace the conclusion

`conc`

with `(implies hyps conc)`

where `hyps`

is the
conjunction of the hypotheses that were eliminated. If no arguments
are supplied, then all hypotheses are demoted, i.e. `demote`

is the
same as `(demote 1 2 ... n)`

where `n`

is the number of top-level
hypotheses.
**Note**: You must be at the top of the conclusion in order to use
this command. Otherwise, first invoke `top`

. Also, `demote`

fails if
there are no top-level hypotheses or if indices are supplied that
are out of range.

` `

move to the indicated subterm
Major Section: PROOF-CHECKER

Examples: (DIVE 1) -- assign the new current subterm to be the first argument of the existing current subterm (DIVE 1 2) -- assign the new current subterm to be the result of first taking the 1st argument of the existing current subterm, and then the 2nd argument of thatFor example, if the current subterm is

(* (+ a b) c),then after

`(dive 1)`

it is
(+ a b).If after that, then

`(dive 2)`

is invoked, the new current subterm
will be
b.Instead of

`(dive 1)`

followed by `(dive 2)`

, the same current subterm
could be obtained by instead submitting the single instruction
`(dive 1 2)`

.

General Form: (dive &rest naturals-list)If

`naturals-list`

is a non-empty list `(n_1 ... n_k)`

of natural
numbers, let the new current subterm be the result of selecting the
`n_1`

-st argument of the current subterm, and then the `n_2`

-th subterm
of that, ..., finally the `n_k`

-th subterm.
**Note:** `Dive`

is related to the command `pp`

, in that the diving is done
according to raw (translated, internal form) syntax. Use the
command `dv`

if you want to dive according to the syntax displayed by
the command `p`

. Note that `(dv n)`

can be abbreviated by simply `n`

.

` `

run the given instructions
Major Section: PROOF-CHECKER

Example: (do-all induct p prove)Run the indicated instructions until there is a hard ``failure''. The instruction ``succeeds'' if and only if each instruction inGeneral Form: (do-all &rest instruction-list)

`instruction-list`

does. (See the documentation for `sequence`

for an
explanation of ``success'' and ``failure.'') As each instruction is
executed, the system will print the usual prompt followed by that
instruction, unless the global state variable
`print-prompt-and-instr-flg`

is `nil`

.
**Note:** If `do-all`

``fails'', then the failure is hard if and only if
the last instruction it runs has a hard ``failure''.

Obscure point: For the record, `(do-all ins_1 ins_2 ... ins_k)`

is
the same as `(sequence (ins_1 ins_2 ... ins_k))`

.

` `

run the given instructions, halting once there is a ``failure''
Major Section: PROOF-CHECKER

Example: (do-all-no-prompt induct p prove)General Form: (do-all-no-prompt &rest instruction-list)

`Do-all-no-prompt`

is the same as `do-all`

, except that the prompt and
instruction are not printed each time, regardless of the value of
`print-prompt-and-instr-flg`

. Also, restoring is disabled. See the
documentation for `do-all`

.
` `

run the given instructions, halting once there is a ``failure''
Major Section: PROOF-CHECKER

Example: (do-strict induct p prove)Run the indicated instructions until there is a (hard or soft) ``failure''. In factGeneral Form: (do-strict &rest instruction-list)

`do-strict`

is identical in effect to `do-all`

,
except that `do-all`

only halts once there is a hard ``failure''. See
the documentation for `do-all`

.
` `

drop top-level hypotheses
Major Section: PROOF-CHECKER

Examples: (drop 2 3) -- drop the second and third hypotheses drop -- drop all top-level hypothesesGeneral Forms: (drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.

drop -- Drop all the top-level hypotheses.

`drop`

will fail. If any of the indices is out of range, i.e. is not
an integer between one and the number of top-level hypotheses
`(inclusive)`

, then `(drop n1 n2 ...)`

will fail.
` `

move to the indicated subterm
Major Section: PROOF-CHECKER

Examples: (dv 1) -- assign the new current subterm to be the first argument of the existing current subterm (dv 1 2) -- assign the new current subterm to be the result of first taking the 1st argument of the existing current subterm, and then the 2nd argument of thatFor example, if the current subterm is

(* (+ a b) c),then after

`(dv 1)`

it is
(+ a b).If after that, then

`(dv 2)`

is invoked, the new current subterm
will be
b.Instead of

`(dv 1)`

followed by `(dv 2)`

, the same current subterm
could be obtained by instead submitting the single instruction
`(dv 1 2)`

.

General Form: (dv &rest naturals-list)If

`naturals-list`

is a non-empty list `(n_1 ... n_k)`

of natural
numbers, let the new current subterm be the result of selecting the
`n_1`

-st argument of the current subterm, and then the `n_2`

-th subterm
of that, ..., finally the `n_k`

-th subterm.
**Note:** `(dv n)`

may be abbreviated by simply `n`

, so we could have typed
`1`

instead of `(dv 1)`

in the first example above.

**Note:** See also `dive`

, which is related to the command `pp`

, in that
the diving is done according to raw (translated, internal form)
syntax. Use the command `dv`

if you want to dive according to the
syntax displayed by the command `p`

.

` `

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

Example and General Form: elim

Upon running the `elim`

command, the system will create a subgoal will
be created for each goal that would have been pushed for proof by
induction in an ordinary proof, where **only** elimination is used; not
even simplification is used!

` `

attempt an equality (or congruence-based) substitution
Major Section: PROOF-CHECKER

Examples: (equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the current subterm, if their equality is among the top-level hypotheses or the governors (equiv x t iff) -- replace x by t everywhere inside the current subterm, where only propositional equivalence needs to be maintained at each occurrence of xSubstitute new for old everywhere inside the current subterm, provided that either (relation old new) or (relation new old) is among the top-level hypotheses or the governors (possibly by way of backchaining and/or refinement; see below). If relation isGeneral form: (equiv old new &optional relation)

`nil`

or
is not supplied, then it defaults to `equal`

. See also the command `=`

,
which is much more flexible. Note that this command fails if no
substitution is actually made.
**Note:** No substitution takes place inside explicit values. So for
example, the instruction `(equiv 3 x)`

will cause `3`

to be replaced by
`x`

if the current subterm is, say, `(* 3 y)`

, but not if the current
subterm is `(* 4 y)`

even though `4 = (1+ 3)`

.

The following remarks are quite technical and mostly describe a
certain weak form of ``backchaining'' that has been implemented for
`equiv`

in order to support the `=`

command. In fact neither the term
`(relation old new)`

nor the term `(relation new old)`

needs to be
**explicitly** among the current ``assumptions'', i.e., the top-level
hypothesis or the governors. Rather, there need only be such an
assumption that ``tells us'' `(r old new)`

or `(r new old)`

, for **some**
equivalence relation `r`

that **refines** `relation`

. Here, ``tells us''
means that either one of the indicated terms is among those
assumptions, or else there is an assumption that is an implication
whose conclusion is one of the indicated terms and whose hypotheses
(gathered up by appropriately flattening the first argument of the
`implies`

term) are all among the current assumptions.

` `

exit after possibly saving the state
Major Section: PROOF-CHECKER

Example and General Form: ex

Same as `exit`

, except that first the instruction `save`

is executed.

If `save`

queries the user and is answered negatively, then the exit
is aborted.

` `

exit the interactive proof-checker
Major Section: PROOF-CHECKER

Examples: exit -- exit the interactive proof-checker (exit append-associativity) -- exit and create a defthm event named append-associativityThe commandGeneral Forms:

exit -- Exit without storing an event.

(exit event-name &optional rule-classes do-it-flg) Exit, and store an event.

`exit`

returns you to the ACL2 loop. At a later time,
`(verify)`

may be executed to get back into the same proof-checker
state, as long as there hasn't been an intervening use of the
proof-checker (otherwise see `save`

).
When given one or more arguments as shown above, `exit`

still returns
you to the ACL2 loop, but first, if the interactive proof is
complete, then it attempts create a `defthm`

event with the specified
`event-name`

and `rule-classes`

(which defaults to `(:rewrite)`

if not
supplied). The event will be printed to the terminal, and then
normally the user will be queried whether an event should really be
created. However, if the final optional argument `do-it-flg`

is
supplied and not `nil`

, then an event will be made without a query.

For example, the form

(exit top-pop-elim (:elim :rewrite) t)causes a

`defthm`

event named `top-pop-elim`

to be created with
rule-classes `(:elim :rewrite)`

, without a query to the user (because
of the argument `t`

).
**Note:** it is permitted for `event-name`

to be `nil`

. In that case, the
name of the event will be the name supplied during the original call
of `verify`

. (See the documentation for `verify`

and `commands`

.) Also
in that case, if `rule-classes`

is not supplied then it defaults to
the rule-classes supplied in the original call of `verify`

.

`Comments`

on ``success'' and ``failure''. An `exit`

instruction will
always ``fail'', so for example, if it appears as an argument of a
`do-strict`

instruction then none of the later (instruction) arguments
will be executed. Moreover, the ``failure'' will be ``hard'' if an
event is successfully created or if the instruction is simply `exit`

;
otherwise it will be ``soft''. See the documentation for `sequence`

for an explanation of hard and soft ``failures''. An obscure but
potentially important fact is that if the ``failure'' is hard, then
the error signal is a special signal that the top-level interactive
loop can interpret as a request to exit. Thus for example, a
sequencing command that turns an error triple `(mv erp val state)`

into `(mv t val state)`

would never cause an exit from the interactive
loop.

If the proof is not complete, then `(exit event-name ...)`

will not
cause an exit from the interactive loop. However, in that case it
will print out the original user-supplied goal (the one that was
supplied with the call to `verify`

) and the current list of
instructions.

` `

expand the current function call without simplification
Major Section: PROOF-CHECKER

Examples: expand -- expand and do not simplify.For example, if the current subterm is

`(append a b)`

, then after
`(expand t)`

the current subterm will be the term:
(if (true-listp x) (if x (cons (car x) (append (cdr x) y)) y) (apply 'binary-append (list x y)))regardless of the top-level hypotheses and the governors.

General Form: (expand &optional do-not-expand-lambda-flg new-goals-flg keep-all-guards-flg)Expand the function call at the current subterm, and do not simplify. The options have the following meanings:

do-not-expand-lambda-flg: default is nil; otherwise, the result should be a lambda expressionSee alsonew-goals-flg: default of nil means to introduce APPLY for guards

keep-all-guards-flg: default of nil means that the system should make a weak attempt to prove the guards from the current context

`x`

, which allows simplification.
` `

cause a failure
Major Section: PROOF-CHECKER

Examples: fail (fail t)This is probably only of interest to writers of macro commands. The only function ofGeneral Form: (fail &optional hard)

`fail`

is to fail to ``succeed''.
The full story is that `fail`

and `(fail nil)`

simply return
`(mv nil nil state)`

, while `(fail hard)`

returns `(mv hard nil state)`

if
`hard-flag`

is not `nil`

. See also `do-strict`

, `do-all`

, and `sequence`

.

` `

forward chain from an implication in the hyps
Major Section: PROOF-CHECKER

Example: (forwardchain 2) ; Second hypothesis should be of the form ; (IMPLIES hyp concl), and the result is to replace ; that hypothesis with concl.General Forms: (forwardchain hypothesis-number) (forwardchain hypothesis-number hints) (forwardchain hypothesis-number hints quiet-flg)

This command replaces the hypothesis corresponding to given index,
which should be of the form `(IMPLIES hyp concl)`

, with its
consequent `concl`

. In fact, the given hypothesis is dropped, and
the replacement hypothesis will appear as the final hypothesis after
this command is executed.

The prover must be able to prove the indicated hypothesis from the
other hypotheses, or else the command will fail. The `:hints`

argument is used in this prover call, and should have the usual
syntax of hints to the prover.

Output is suppressed if `quiet-flg`

is supplied and not `nil`

.