---

Step * 1 of Lemma decidable__exists-last-classrel-between3-sv


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''))))))))
BY
{ ((OrLeft THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌈e⌉]⋅
   THEN Auto
   THEN (InstLemma `decidable__exists-single-valued-classrel` [⌈Info⌉;⌈T⌉;⌈X⌉;⌈es⌉;⌈e⌉]⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN Assert ⌈False⌉⋅
   THEN Auto
   THEN D (-3)
   THEN Auto) }

---

Latex:



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.  \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''))))))
\mvdash{}  (\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'')))))))
\mvee{}  (\mneg{}(\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

((OrLeft  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `decidable\_\_exists-single-valued-classrel`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  (-3)
  THEN  Auto)

---

Home Index