Book Theorem:

A(A) = B(A) IMPLIES B = A

Symmetry of Equality.

(P1) H !A(A) = B(A)

*(P2) H !B(A) = A(A) Sym=: P1

Transformation: (P2 ss) ==> (P1 ss)

Rule of Symmetry of Equality.

The command format for SYM= is:

<n>SYM= P2 P1 A B P2-HYPS P1-HYPS

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

The arguments have the following meaning:

P2 : Higher Line

P1 : Lower Line

A : Left Hand Side of Lower Equality

B : Right Hand Side of Lower Equality

P2-HYPS : Hypotheses

P1-HYPS : Hypotheses

Its priority is NIL

© 1988-99, Carnegie Mellon University.