### ACL2-PC::UP

(primitive)
` `

move to the parent (or some ancestor) of the current subterm
Major Section: PROOF-CHECKER-COMMANDS

Examples: if the conclusion is (= x (* (- y) z)) and the
current subterm is y, then we have:
up or (up 1) -- the current subterm becomes (- y)
(up 2) -- the current subterm becomes (* (- y) z)
(up 3) -- the current subterm becomes the entire conclusion
(up 4) -- no change; can't go up that many levels
General Form:
(up &optional n)

Move up `n`

levels in the conclusion from the current subterm, where `n`

is a positive integer. If `n`

is not supplied or is `nil`

, then move up
1 level, i.e., treat the instruction as `(up 1)`

.
See also `dive`

, `top`

, `nx`

, and `bk`

.