FIND-LINE : MEXPRFIND-LINE is a top-level command.
Find all lines matching a certain wff, up to
alphabetic change of bound variables and (possibly)
alphabetic change of a given list of free variables.
Optionally, you can treat the remaining free variables
as matching any given term (as you might do if you were
asserting an axiom).
e.g. (suppose P is an abbreviation or constant):
FIND-LINE "P a" () NO finds all lines that say "P a"
FIND-LINE "P a" ("a") NO also finds "P x" and "P y"
FIND-LINE "P a" () YES finds all the above, plus
"P [COMPOSE f g]"
FIND-LINE "a x" ("x") YES finds all lines of the form
The command format for FIND-LINE is:
<n>FIND-LINE WFF VARS META
"GWFF0" "GVARLIST" "YESNO"
The arguments have the following meaning:
WFF : Wff to look for
VARS : Free variables that may be alphabetically changed
META : Treat remaining free vars as subterms?
TPS documentation homepage