R-PRIME-RESTR : WFFOP

R-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


© 1988-99, Carnegie Mellon University.

TPS homepage