Rule to replace an implication by a disjunction.

The command format for IMP-DISJ-R is:

<n>IMP-DISJ-R D1 D2 A B D1-HYPS D2-HYPS

"LINE" "LINE" "GWFF" "GWFF" "LINELIST" "LINELIST"

The arguments have the following meaning:

D1 : Line with Implication

D2 : Line with Disjunction

A : Antecedent of Implication

B : Succedent of Implication

D1-HYPS : Hypotheses

D2-HYPS : Hypotheses

Its priority is NIL

© 1988-99, Carnegie Mellon University.