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.