### ACL2-PC::NX

(atomic macro)
` `

move forward one argument in the enclosing term
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form:
nx

For example, if the conclusion is `(= x (* (- y) z))`

and the
current subterm is `x`

, then after executing `nx`

, the current
subterm will be `(* (- y) z)`

.
This is the same as `up`

followed by `(dive n+1)`

, where `n`

is the
position of the current subterm in its parent term in the
conclusion. Thus in particular, the `nx`

command fails if one is
already at the top of the conclusion.

See also `up`

, `dive`

, `top`

, and `bk`

.