### 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`

.