Recursively apply the following laws to a wff:

A and (A or B), (A or B) and A --> A or B

A and (B or A), (B or A) and A --> B or A

A or (A and B), (A and B) or A --> A

(B and A) or A, (B and A) or A --> A.

The command format for ASRB* is:

<Ed>ASRB* <<GWFF>>

<<GWFF>>

The result replaces the current wff.

© 1988-99, Carnegie Mellon University.