up, dive, top, and bk.
move backward one argument in the enclosing term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: bkFor example, if the conclusion is
(= x (* (- y) z)) and the current
subterm is (* (- y) z), then after executing bk, the current subterm
will be x.
Move to the previous argument of the enclosing term.
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.