---

Step * 2 of Lemma decidable__exists-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. ((e1 <loc e) ∧ e ≤loc e2  ∧ (∃v:T. v ∈ X(e)))) ∨ (¬(∃e:E. ((e1 <loc e) ∧ e ≤loc e2  ∧ (∃v:T. v ∈ X(e)))))
BY
{ ((OrRight THENA Auto) THEN (D 0 THENA Auto) THEN D (-2) THEN ExRepD THEN InstConcl [⌈e⌉]⋅ 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.  \mneg{}(\mexists{}e:E.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  (\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))))
\mvdash{}  (\mexists{}e:E.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  (\mexists{}v:T.  v  \mmember{}  X(e))))
\mvee{}  (\mneg{}(\mexists{}e:E.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  (\mexists{}v:T.  v  \mmember{}  X(e)))))


By

((OrRight  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  D  (-2)  THEN  ExRepD  THEN  InstConcl  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index