SAME-MODULO-EQUALITY : WFFOPSAME-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