---

Step * of Lemma decidable-implies-es-interface

∀[Info,A:Type]. ∀[P:eo:EO+(Info) ─→ E ─→ A ─→ ℙ].
  ((∀eo:EO+(Info). ∀e:E.  Dec(∃a:A. P[eo;e;a]))
  ⇒ (∃X:EClass(A). ∀eo:EO+(Info). ∀e:E.  ((↑e ∈b X ⇐⇒ ∃a:A. P[eo;e;a]) ∧ P[eo;e;X(e)] supposing ↑e ∈b X)))
BY
{ ((Auto THEN RepUR ``all decidable or exists`` -1 THEN RenameVar `f' (-1))
   THEN InstConcl [⌈λeo,e. case f eo e of inl(p) => {fst(p)} | inr(z) => {}⌉]⋅
   THEN Try (Complete (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'
⊢ ∀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) => {})

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[P:eo:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}eo:EO+(Info).  \mforall{}e:E.    Dec(\mexists{}a:A.  P[eo;e;a]))
    {}\mRightarrow{}  (\mexists{}X:EClass(A)
              \mforall{}eo:EO+(Info).  \mforall{}e:E.    ((\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A.  P[eo;e;a])  \mwedge{}  P[eo;e;X(e)]  supposing  \muparrow{}e  \mmember{}\msubb{}  X)))


By

((Auto  THEN  RepUR  ``all  decidable  or  exists``  -1  THEN  RenameVar  `f'  (-1))
  THEN  InstConcl  [\mkleeneopen{}\mlambda{}eo,e.  case  f  eo  e  of  inl(p)  =>  \{fst(p)\}  |  inr(z)  =>  \{\}\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index