ACL2-PC_colon__colon_BK.html -- ACL2 Version 3.1

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.