ACL2-PC::BK

(atomic macro) move backward one argument in the enclosing term
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
bk
For 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.