Step
*
1
of Lemma
es-le-trans
1. the_es : EO@i'
2. a : E@i
3. b : E@i
4. c : E@i
5. (a <loc b) ∨ (a = b ∈ E)@i
6. (b <loc c) ∨ (b = c ∈ E)@i
7. Trans(E;x,y.(x <loc y))
⊢ (a <loc c) ∨ (a = c ∈ E)
BY
{ ((SplitOrHyps
THENL [(OrLeft THENM UseTrans ⌈b⌉⋅); (OrLeft THENM (HypSubst (-3) 0)); (OrLeft THENM (HypSubst (-2) (-3))); OrRight]
)
THEN Auto
) }
Latex:
1. the$_{es}$ : EO@i'
2. a : E@i
3. b : E@i
4. c : E@i
5. (a <loc b) \mvee{} (a = b)@i
6. (b <loc c) \mvee{} (b = c)@i
7. Trans(E;x,y.(x <loc y))
\mvdash{} (a <loc c) \mvee{} (a = c)
By
((SplitOrHyps
THENL [(OrLeft THENM UseTrans \mkleeneopen{}b\mkleeneclose{}\mcdot{})
; (OrLeft THENM (HypSubst (-3) 0))
; (OrLeft THENM (HypSubst (-2) (-3)))
; OrRight]
)
THEN Auto
)
Home
Index