---

Step * of Lemma decidable__exists-classrel-between1-sv

∀[Info,T:Type].
  ∀X:EClass(T). ∀es:EO+(Info).
    (single-valued-classrel(es;X;T) ⇒ (∀e1,e2:E.  Dec(∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (∃v:T. v ∈ X(e))))))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `decidable__exists-classrel-between1` [⌈Info⌉;⌈T⌉;⌈X⌉;⌈es⌉;⌈e1⌉;⌈e2⌉]⋅ THENA Auto)
   THEN D (-1)
   THEN Unfold `decidable` 0) }

1
1. [Info] : Type
2. [T] : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. single-valued-classrel(es;X;T)@i
6. e1 : E@i
7. e2 : E@i
8. ∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (↓∃v:T. v ∈ X(e)))
⊢ (∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (∃v:T. v ∈ X(e)))) ∨ (¬(∃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. single-valued-classrel(es;X;T)@i
6. e1 : E@i
7. e2 : E@i
8. ¬(∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (↓∃v:T. v ∈ X(e))))
⊢ (∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (∃v:T. v ∈ X(e)))) ∨ (¬(∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (∃v:T. v ∈ X(e)))))

---

Latex:


\mforall{}[Info,T:Type].
    \mforall{}X:EClass(T).  \mforall{}es:EO+(Info).
        (single-valued-classrel(es;X;T)
        {}\mRightarrow{}  (\mforall{}e1,e2:E.    Dec(\mexists{}e:E.  (e1  \mleq{}loc  e    \mwedge{}  (e  <loc  e2)  \mwedge{}  (\mexists{}v:T.  v  \mmember{}  X(e))))))


By

((UnivCD  THENA  Auto)
  THEN  (InstLemma  `decidable\_\_exists-classrel-between1`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Unfold  `decidable`  0)

---

Home Index