LEXPD : WFFOPLEXPD is a wff operation.
Converts the wff into the application of a function to the term.
The function is formed by replacing given valid occurrences of a term
with the variable and binding the result.
The calling scheme for LEXPD is:
(LEXPD VAR TERM INWFF OCCURS)
"GVAR" "GWFF" "GWFF" "OCC-LIST"
The result is of type GWFF.
The arguments have the following meaning:
VAR : lambda variable
TERM : term to be extracted
INWFF : contracted form
OCCURS : occurrences to be extracted
TPS documentation homepage