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.