1\DOC NOT_EQ_SYM 2 3\TYPE {NOT_EQ_SYM : (thm -> thm)} 4 5\SYNOPSIS 6Swaps left-hand and right-hand sides of a negated equation. 7 8\KEYWORDS 9rule, symmetry, equality, negation. 10 11\DESCRIBE 12When applied to a theorem {A |- ~(t1 = t2)}, the inference rule {NOT_EQ_SYM} 13returns the theorem {A |- ~(t2 = t1)}. 14{ 15 A |- ~(t1 = t2) 16 ----------------- NOT_EQ_SYM 17 A |- ~(t2 = t1) 18} 19 20 21\FAILURE 22Fails unless the theorem's conclusion is a negated equation. 23 24\SEEALSO 25Conv.DEPTH_CONV, Thm.REFL, Thm.SYM. 26\ENDDOC 27