Apply commutativity laws to a formula:

A and B --> B and A

A or B --> B or A

A implies B --> not B implies not A

A equiv B --> B equiv A.

The calling scheme for WFF-COMMUTATIVE is:

(WFF-COMMUTATIVE GWFF)

"GWFF"

The result is of type GWFF.

The arguments have the following meaning:

GWFF : Wff

© 1988-99, Carnegie Mellon University.