---

Step * 1 of Lemma decidable-implies-es-interface


1. [Info] : Type
2. [A] : Type
3. [P] : eo:EO+(Info) ─→ E ─→ A ─→ ℙ
4. f : eo:EO+(Info) ─→ e:E ─→ (a:A × P[eo;e;a] + (¬(a:A × P[eo;e;a])))@i'
⊢ ∀eo:EO+(Info). ∀e:E.
    ((↑e ∈b λeo,e. case f eo e of inl(p) => {fst(p)} | inr(z) => {} ⇐⇒ ∃a:A. P[eo;e;a])
    ∧ P[eo;e;λeo,e. case f eo e of inl(p) => {fst(p)} | inr(z) => {}(e)] 
      supposing ↑e ∈b λeo,e. case f eo e of inl(p) => {fst(p)} | inr(z) => {})
BY
{ ((RepeatFor 2 ((D 0 THENA Auto)) THEN RepUR ``in-eclass eclass-val`` 0)⋅
   THEN GenConclAtAddr [1;1;1;1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

1
1. [Info] : Type
2. [A] : Type
3. [P] : eo:EO+(Info) ─→ E ─→ A ─→ ℙ
4. f : eo:EO+(Info) ─→ e:E ─→ (a:A × P[eo;e;a] + (¬(a:A × P[eo;e;a])))@i'
5. eo : EO+(Info)@i'
6. e : E@i
7. x : a:A × P[eo;e;a]@i
8. (f eo e) = (inl x) ∈ (a:A × P[eo;e;a] + (¬(a:A × P[eo;e;a])))@i
9. True ⇐ ∃a:A. P[eo;e;a]
10. True
11. ∃a:A. P[eo;e;a]
⊢ P[eo;e;fst(x)]

---

Latex:



1.  [Info]  :  Type
2.  [A]  :  Type
3.  [P]  :  eo:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  f  :  eo:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  (a:A  \mtimes{}  P[eo;e;a]  +  (\mneg{}(a:A  \mtimes{}  P[eo;e;a])))@i'
\mvdash{}  \mforall{}eo:EO+(Info).  \mforall{}e:E.
        ((\muparrow{}e  \mmember{}\msubb{}  \mlambda{}eo,e.  case  f  eo  e  of  inl(p)  =>  \{fst(p)\}  |  inr(z)  =>  \{\}  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A.  P[eo;e;a])
        \mwedge{}  P[eo;e;\mlambda{}eo,e.  case  f  eo  e  of  inl(p)  =>  \{fst(p)\}  |  inr(z)  =>  \{\}(e)] 
            supposing  \muparrow{}e  \mmember{}\msubb{}  \mlambda{}eo,e.  case  f  eo  e  of  inl(p)  =>  \{fst(p)\}  |  inr(z)  =>  \{\})


By

((RepeatFor  2  ((D  0  THENA  Auto))  THEN  RepUR  ``in-eclass  eclass-val``  0)\mcdot{}
  THEN  GenConclAtAddr  [1;1;1;1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index