Rule to replace an implication by a disjunction.

The command format for IMP-DISJ-L is:

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

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

The arguments have the following meaning:

D1 : Line with Implication

D2 : Line with Disjunction

B : Succedent of Implication

A : Antecedent of Implication

D1-HYPS : Hypotheses

D2-HYPS : Hypotheses

Its priority is NIL

© 1988-99, Carnegie Mellon University.