1\DOC GSYM 2 3\TYPE {GSYM : thm -> thm} 4 5\SYNOPSIS 6Reverses the first equation(s) encountered in a top-down search. 7 8\KEYWORDS 9rule, symmetry, equality. 10 11\DESCRIBE 12The inference rule {GSYM} reverses the first equation(s) encountered in a 13top-down search of the conclusion of the argument theorem. An equation will be 14reversed iff it is not a proper subterm of another equation. If a theorem 15contains no equations, it will be returned unchanged. 16{ 17 A |- ..(s1 = s2)...(t1 = t2).. 18 -------------------------------- GSYM 19 A |- ..(s2 = s1)...(t2 = t1).. 20} 21 22 23\FAILURE 24Never fails, and never loops infinitely. 25 26\EXAMPLE 27{ 28- arithmeticTheory.ADD; 29> val it = |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n)) : thm 30 31- GSYM arithmeticTheory.ADD; 32> val it = |- (!n. n = 0 + n) /\ (!m n. SUC(m + n) = (SUC m) + n) : thm 33} 34 35 36\SEEALSO 37Drule.NOT_EQ_SYM, Thm.REFL, Thm.SYM. 38\ENDDOC 39