---

Step * of Lemma decidable__exists-last-classrel-between3

∀[Info,T:Type].
  ∀X:EClass(T). ∀es:EO+(Info). ∀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 (Decide loc(e1) = loc(e2) ∈ Id THENA Auto)) }

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
⊢ 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'')))))))

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)
⊢ 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'')))))))

---

Latex:


\mforall{}[Info,T:Type].
    \mforall{}X:EClass(T).  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.
        Dec(\mexists{}e:E
                  ((e1  <loc  e)
                  \mwedge{}  e  \mleq{}loc  e2 
                  \mwedge{}  (\mdownarrow{}\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

((UnivCD  THENA  Auto)  THEN  (Decide  loc(e1)  =  loc(e2)  THENA  Auto))

---

Home Index