WFFEQ-AB-BETA : WFFOPWFFEQ-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)
The result is of type BOOLEAN.
The arguments have the following meaning:
WFF1 : old wff
WFF2 : new wff
TPS documentation homepage