SUBST-OCCS : WFFOPSUBST-OCCS is a wff operation.
Checks to see if wff2 is the result of replacing some
occurrences of term1 in wff1 with term2. The pvs must not be
bound at such occurrences of term1.
The calling scheme for SUBST-OCCS is:
(SUBST-OCCS TERM1 WFF1 TERM2 WFF2 PVS)
"GWFF" "GWFF" "GWFF" "GWFF" "GVARLIST"
The result is of type BOOLEAN.
The arguments have the following meaning:
TERM1 : old term
WFF1 : old wff
TERM2 : new term
WFF2 : new wff
PVS : variables to be free in occurrence
TPS documentation homepage