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.