---

Step * 1 of Lemma decidable__exists-classrel-between1


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
⊢ Dec(∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (↓∃v:T. v ∈ X(e))))
BY
{ ((InstLemma `decidable__existse-between1` [⌈es⌉;⌈e1⌉;⌈e2⌉;⌈λ2e.↓∃v:T. v ∈ X(e)⌉]⋅ THENA (Auto THEN D 0 THEN Auto))
   THEN D (-1)
   ) }

1
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))))

2
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))))

---

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)
\mvdash{}  Dec(\mexists{}e:E.  (e1  \mleq{}loc  e    \mwedge{}  (e  <loc  e2)  \mwedge{}  (\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))))


By

((InstLemma  `decidable\_\_existse-between1`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}e.\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e)\mkleeneclose{}]\mcdot{}
    THENA  (Auto  THEN  D  0  THEN  Auto)
    )
  THEN  D  (-1)
  )

---

Home Index