---

Step * 1 1 of Lemma decidable__exists-classrel-between3


1. [Info] : Type
2. [T] : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. e1 : E@i
6. e2 : E@i
7. loc(e1) = loc(e2) ∈ Id
8. ∃e∈(e1,e2].↓∃v:T. v ∈ X(e)
⊢ Dec(∃e:E. ((e1 <loc e) ∧ e ≤loc e2  ∧ (↓∃v:T. v ∈ X(e))))
BY
{ (OrLeft THEN Auto THEN Unfold `existse-between3` (-1) THEN ExRepD THEN Auto) }

---

Latex:



1.  [Info]  :  Type
2.  [T]  :  Type
3.  X  :  EClass(T)@i'
4.  es  :  EO+(Info)@i'
5.  e1  :  E@i
6.  e2  :  E@i
7.  loc(e1)  =  loc(e2)
8.  \mexists{}e\mmember{}(e1,e2].\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e)
\mvdash{}  Dec(\mexists{}e:E.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  (\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))))


By

(OrLeft  THEN  Auto  THEN  Unfold  `existse-between3`  (-1)  THEN  ExRepD  THEN  Auto)

---

Home Index