PUSH-UP : INFO

PUSH-UP is a flag setting or other piece of information.
A setting for TEST-NEXT-SEARCH-FN.
This setting is used internally by the PUSH-UP command.

TPS documentation homepage


PUSH-UP : TESTCMD

PUSH-UP is a test-top command.
This command effectively runs PUSH-UP until it finds
a mode that works, and then stops.
Before using this command, use the MODE command to
set up a mode in which the current theorem can not be proven. Also
check the value of the TEST-INCREASE-TIME flag (it should probably
not be zero).
Then PUSH-UP will systematically vary the values of the flags
listed in the TEST-EASIER-IF-* flags, using the PUSH-UP search
function (see the help message for TEST-NEXT-SEARCH-FN).
The value of TEST-NEXT-SEARCH-FN will be changed to PUSH-UP.

Note that this is NOT the same as PUSH-UP-2, since it automatically
generates a searchlist rather than relying on the user to provide one
 
The command format for PUSH-UP is:

<TEST>PUSH-UP MODENAME TESTWIN
"SYMBOL" "YESNO"

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage