up, dive, top, and bk.
move forward one argument in the enclosing term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: nxFor 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.