` `

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

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.