UNIFORM-SEARCH-L : MEXPRUNIFORM-SEARCH-L is a top-level command.
Enter the test top level to search for any mode that will prove
a given lemma. (Compare DIY-L) The mode provided by the user should list flag
settings that are not to be varied, and the searchlist provided by the user should
list all of the flags to be varied. The default settings for the mode and
searchlist are UNIFORM-SEARCH-MODE and UNIFORM-SEARCH-2.
If you opt for the searchlist to be automatically modified, TPS will inspect
the given wff to check whether it is first order, whether it contains any
definitions, whether it contains any equalities (and if so whether the LEIBNIZ
and ALL instantiations are different), and whether it has any possible primitive
substitutions, and will then remove or modify any unnecessary flags from the
searchlist (respectively, unification bounds will be deleted, REWRITE-DEFNS will
be deleted, REWRITE-EQUALITIES will be deleted or modified, and DEFAULT-MS will
be changed to a search without option sets).
After entering the test top level with this command, type GO ! to start
searching for a successful mode.
The command format for UNIFORM-SEARCH-L is:
<n>UNIFORM-SEARCH-L GOAL SUPPORT LINE-RANGE WINDOW MODE SLIST MODIFY
"PLINE" "EXISTING-LINELIST" "LINE-RANGE" "YESNO" "SYMBOL" "SYMBOL" "YESNO"
The arguments have the following meaning:
GOAL : Planned Line
SUPPORT : Support Lines
LINE-RANGE : Line range for new lines?
WINDOW : Open Vpform Window?
MODE : Mode
SLIST : Searchlist
MODIFY : Automatically modify searchlist?
TPS documentation homepage