Rule to convert equality at type o into an equivalence.

The command format for EXT=0 is:

<n>EXT=0 P2 P1 R P P2-HYPS P1-HYPS

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

The arguments have the following meaning:

P2 : Line with Equality

P1 : Line with Equivalence

R : Right Equivalent

P : Left Equivalent

P2-HYPS : Hypotheses

P1-HYPS : Hypotheses

Its priority is 1

© 1988-99, Carnegie Mellon University.