---

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


1. [Info] : Type
2. [A] : es:EO+(Info) ─→ e:E ─→ Type
3. [R] : es:EO+(Info) ─→ e:E ─→ A[es;e] ─→ ℙ
4. ∀es:EO+(Info). ∀e:E.  Dec(∃a:A[es;e]. R[es;e;a])@i'
⊢ ∃X:EClass(A[es;e]). ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X ⇐⇒ ∃a:A[es;e]. R[es;e;a]) ∧ R[es;e;X(e)] supposing ↑e ∈b X)
BY
{ ((RenameVar `f' (-1) THEN RepUR ``eclass in-eclass eclass-val`` 0)⋅
   THEN At ⌈𝕌'⌉ (InstConcl [⌈λes,e. case f es e of inl(p) => {fst(p)} | inr(p) => {}⌉])⋅
   ) }

1
.....wf..... 
1. Info : Type
2. A : es:EO+(Info) ─→ e:E ─→ Type
3. R : es:EO+(Info) ─→ e:E ─→ A[es;e] ─→ ℙ
4. f : ∀es:EO+(Info). ∀e:E.  Dec(∃a:A[es;e]. R[es;e;a])@i'
⊢ λes,e. case f es e of inl(p) => {fst(p)} | inr(p) => {} ∈ es:EO+(Info) ─→ e:E ─→ bag(A[es;e])

2
1. [Info] : Type
2. [A] : es:EO+(Info) ─→ e:E ─→ Type
3. [R] : es:EO+(Info) ─→ e:E ─→ A[es;e] ─→ ℙ
4. f : ∀es:EO+(Info). ∀e:E.  Dec(∃a:A[es;e]. R[es;e;a])@i'
⊢ ∀es:EO+(Info). ∀e:E.
    ((↑(#((λes,e. case f es e of inl(p) => {fst(p)} | inr(p) => {}) es e) =z 1) ⇐⇒ ∃a:A[es;e]. R[es;e;a])
    ∧ R[es;e;only((λes,e. case f es e of inl(p) => {fst(p)} | inr(p) => {}) es e)] 
      supposing ↑(#((λes,e. case f es e of inl(p) => {fst(p)} | inr(p) => {}) es e) =z 1))

3
.....wf..... 
1. Info : Type
2. A : es:EO+(Info) ─→ e:E ─→ Type
3. R : es:EO+(Info) ─→ e:E ─→ A[es;e] ─→ ℙ
4. f : ∀es:EO+(Info). ∀e:E.  Dec(∃a:A[es;e]. R[es;e;a])@i'
5. X : es:EO+(Info) ─→ e:E ─→ bag(A[es;e])
⊢ ∀es:EO+(Info). ∀e:E.
    ((↑(#(X es e) =z 1) ⇐⇒ ∃a:A[es;e]. R[es;e;a]) ∧ R[es;e;only(X es e)] supposing ↑(#(X es e) =z 1)) ∈ 𝕌'

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  [A]  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  Type
3.  [R]  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  A[es;e]  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(\mexists{}a:A[es;e].  R[es;e;a])@i'
\mvdash{}  \mexists{}X:EClass(A[es;e])
      \mforall{}es:EO+(Info).  \mforall{}e:E.    ((\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A[es;e].  R[es;e;a])  \mwedge{}  R[es;e;X(e)]  supposing  \muparrow{}e  \mmember{}\msubb{}  X)


By

---

Latex:
((RenameVar  `f'  (-1)  THEN  RepUR  ``eclass  in-eclass  eclass-val``  0)\mcdot{}
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (InstConcl  [\mkleeneopen{}\mlambda{}es,e.  case  f  es  e  of  inl(p)  =>  \{fst(p)\}  |  inr(p)  =>  \{\}\mkleeneclose{}])\mcdot{}
  )

---

Home Index