R-PRIME-RESTR : WFFOPR-PRIME-RESTR is a wff operation.
Verifies that wff2 follows from wff1 by Rule R' using equality term1=term2.
The calling scheme for R-PRIME-RESTR is:
(R-PRIME-RESTR 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