` `

expand and (maybe) simplify function call at the current subterm
Major Section: PROOF-CHECKER-COMMANDS

Examples: x -- expand and simplify.For example, if the current subterm is (append a b), then after

`x`

the current subterm will probably be (cons (car a) (append (cdr a)
b)) if (consp a) and (true-listp a) are among the top-level
hypotheses and governors. If there are no top-level hypotheses and
governors, then after `x`

the current subterm will probably be:
(if (true-listp x) (if x (cons (car x) (append (cdr x) y)) y) (apply 'binary-append (list x y))). General Form: (X &key rewrite normalize backchain-limit in-theory hands-off expand)Expand the function call at the current subterm, and simplify using the same conventions as with the

`s`

command (see documentation
for `s`

).Unlike `s`

, it is permitted to set both `:rewrite`

and `:normalize`

to
`nil`

, which will result in no simplification; see `x-dumb`

.

**Remark** (obscure): On rare occasions the current address may be
affected by the use of `x`

. For example, suppose we have the
definition

(defun g (x) (if (consp x) x 3))and then we enter the proof-checker with

(verify (if (integerp x) (equal (g x) 3) t)) .Then after invoking the instruction

`(dive 2 1)`

, so that the
current subterm is `(g x)`

, followed by the instruction `x`

, we would
expect the conclusion to be `(if (integerp x) (equal 3 3) t)`

.
However, the system actually replaces `(equal 3 3)`

with `t`

(because we
use the ACL2 term-forming primitives), and hence the conclusion is actually
`(if (integerp x) t t)`

. Therefore, the current address is put at `(2)`

rather than `(2 1)`

. In such cases, a warning ```NOTE`

'' will be printed
to the terminal.The other primitive commands to which the above ``truncation'' note
applies are `equiv`

, `rewrite`

, and `s`

.