### ACL2-PC::=

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

General Form:
(= &optional x y &rest keyword-args)
```
If terms `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.

Remarks: (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.