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