GO2 : MEXPRGO2 is a top-level command.
Apply all possible invertible tactics, until no more are possible.
This is equivalent to typing USE-TACTIC GO2-TAC NAT-DED.
The amount of output to the main window and the proofwindows is
determined by the flag ETREE-NAT-VERBOSE.
The command format for GO2 is:
The arguments have the following meaning:
TACMODE : Mode
TPS documentation homepage