ACL2-PC::X

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

Note (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) (equal 3 3) 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`.