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