SAME-MODULO-EQUALITY : WFFOP

SAME-MODULO-EQUALITY is a wff operation.
Verifies that wff2 follows from wff1 by Rule R' (possibly
iterated) using equality term1=term2.
 
The calling scheme for SAME-MODULO-EQUALITY is:

(SAME-MODULO-EQUALITY WFF1 WFF2 TERM1 TERM2)
"GWFF" "GWFF" "GWFF" "GWFF"


The result is of type BOOLEAN.

The arguments have the following meaning:
WFF1 : old wff
WFF2 : new wff
TERM1 : first term
TERM2 : equal term

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage