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
37
38
39
40
|
\DOC TRANS
\TYPE {$TRANS : (thm -> thm -> thm)}
\SYNOPSIS
Uses transitivity of equality on two equational theorems.
\KEYWORDS
rule, transitivity, equality.
\DESCRIBE
When applied to a theorem {A1 |- t1 = t2} and a theorem {A2 |- t2 = t3}, the
inference rule {TRANS} returns the theorem {A1 u A2 |- t1 = t3}. Note that
{TRANS} can also be used as a infix (see example below).
{
A1 |- t1 = t2 A2 |- t2 = t3
------------------------------- TRANS
A1 u A2 |- t1 = t3
}
\FAILURE
Fails unless the theorems are equational, with the right side of the first
being the same as the left side of the second.
\EXAMPLE
The following shows identical uses of {TRANS}, one as a prefix, one an infix.
{
#let t1 = ASSUME "a:bool = b" and t2 = ASSUME "b:bool = c";;
t1 = . |- a = b
t2 = . |- b = c
#TRANS t1 t2;;
.. |- a = c
#t1 TRANS t2;;
.. |- a = c
}
\SEEALSO
EQ_MP, IMP_TRANS, REFL, SYM.
\ENDDOC
|
