---

Step * 1 1 of Lemma member-es-interval


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
⊢ ((ev <loc e') ∨ (ev = e' ∈ E) ∨ False) ∧ e ≤loc ev  ⇐⇒ e ≤loc ev  ∧ ev ≤loc e' 
BY
{ (Auto
   THEN SplitOrHyps
   THEN Auto
   THEN Try ((Unfold `es-le` 0 THEN ((OrLeft THEN Complete (Auto)) ORELSE (OrRight THEN Complete (Auto)))))) }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
5. e ≤loc ev @i
6. ev ≤loc e' @i
⊢ (ev <loc e') ∨ (ev = e' ∈ E) ∨ False

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  ev  :  E@i
\mvdash{}  ((ev  <loc  e')  \mvee{}  (ev  =  e')  \mvee{}  False)  \mwedge{}  e  \mleq{}loc  ev    \mLeftarrow{}{}\mRightarrow{}  e  \mleq{}loc  ev    \mwedge{}  ev  \mleq{}loc  e' 


By

(Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  ((Unfold  `es-le`  0
                        THEN  ((OrLeft  THEN  Complete  (Auto))  ORELSE  (OrRight  THEN  Complete  (Auto)))
                        )))

---

Home Index