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
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.