up, dive, nx, and bk.
move to the top of the goal
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: topFor 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.