WFFEQ-AB-ETA : WFFOP

WFFEQ-AB-ETA is a wff operation.
Verifies that wff1 and wff2 are equal up to
lambda-normalization with eta rule only, and alphabetic change of
bound variables. (Compare WFFEQ-AB-BETA, WFFEQ-AB-LAMBDA.)
 
The calling scheme for WFFEQ-AB-ETA is:

(WFFEQ-AB-ETA WFF1 WFF2)
"GWFF" "GWFF"


The result is of type BOOLEAN.

The arguments have the following meaning:
WFF1 : old wff
WFF2 : new wff

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage