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
up in order to get to the top of the conclusion. The
command fails if one is already at the top of the conclusion.