SUBST-SOME-OCCURRENCES : WFFOPSUBST-SOME-OCCURRENCES is a wff operation.
Checks to see if wff2 is the result of replacing some
occurrences of term1 in wff1 with term2.
The calling scheme for SUBST-SOME-OCCURRENCES is:
(SUBST-SOME-OCCURRENCES TERM1 WFF1 TERM2 WFF2)
"GWFF" "GWFF" "GWFF" "GWFF"
The result is of type BOOLEAN.
The arguments have the following meaning:
TERM1 : old term
WFF1 : old wff
TERM2 : new term
WFF2 : new wff
TPS documentation homepage