---

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