WFFEQ-AB-LAMBDA : WFFOP

WFFEQ-AB-LAMBDA is a wff operation.
Verifies that wff1 and wff2 are equal up to
lambda-normalization and alphabetic change of bound variables.
Uses both eta and beta rules (compare WFFEQ-AB-ETA and WFFEQ-AB-BETA).
 
The calling scheme for WFFEQ-AB-LAMBDA is:

(WFFEQ-AB-LAMBDA 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