### ACL2-PC::TOP

(atomic macro)
` `

move to the top of the goal
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form:
top

For example, if the conclusion is `(= x (* (- y) z))`

and the
current subterm is `y`

, then after executing `top`

, the current subterm
will be the same as the conclusion, i.e., `(= x (* (- y) z))`

.
`Top`

is the same as `(up n)`

, where `n`

is the number of times one needs
to execute `up`

in order to get to the top of the conclusion. The `top`

command fails if one is already at the top of the conclusion.

See also `up`

, `dive`

, `nx`

, and `bk`

.