---

Step * of Lemma decidable__exists-last-classrel-between3-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))
               ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e'')))))))))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `decidable__exists-last-classrel-between3` [⌜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. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e''))))))
⊢ (∃e:E
    ((e1 <loc e) ∧ e ≤loc e2  ∧ (∃v:T. v ∈ X(e)) ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e'')))))))
∨ (¬(∃e:E
      ((e1 <loc e)
      ∧ e ≤loc e2 
      ∧ (∃v:T. v ∈ X(e))
      ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ 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. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e'')))))))
⊢ (∃e:E
    ((e1 <loc e) ∧ e ≤loc e2  ∧ (∃v:T. v ∈ X(e)) ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e'')))))))
∨ (¬(∃e:E
      ((e1 <loc e)
      ∧ e ≤loc e2 
      ∧ (∃v:T. v ∈ X(e))
      ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e''))))))))

---

Latex:

---

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  <loc  e)
                              \mwedge{}  e  \mleq{}loc  e2 
                              \mwedge{}  (\mexists{}v:T.  v  \mmember{}  X(e))
                              \mwedge{}  (\mforall{}e'':E.  ((e  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e2    {}\mRightarrow{}  (\mforall{}x:T.  (\mneg{}x  \mmember{}  X(e'')))))))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `decidable\_\_exists-last-classrel-between3`  [\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