WFFEQ-AB-BETA : WFFOP

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

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