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