---

Step * 1 2 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. 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))
BY
{ (Reduce 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (GenConcl ⌈(f es e) = d ∈ Dec(∃a:A[es;e]. R[es;e;a])⌉⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

1
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. es : EO+(Info)@i'
6. e : E@i
7. x : ∃a:A[es;e]. R[es;e;a]@i
8. (f es e) = (inl x) ∈ Dec(∃a:A[es;e]. R[es;e;a])@i
9. True ⇐ ∃a:A[es;e]. R[es;e;a]
10. True
11. ∃a:A[es;e]. R[es;e;a]
⊢ R[es;e;fst(x)]

---

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.  f  :  \mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(\mexists{}a:A[es;e].  R[es;e;a])@i'
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.
        ((\muparrow{}(\#((\mlambda{}es,e.  case  f  es  e  of  inl(p)  =>  \{fst(p)\}  |  inr(p)  =>  \{\})  es  e)  =\msubz{}  1)
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A[es;e].  R[es;e;a])
        \mwedge{}  R[es;e;only((\mlambda{}es,e.  case  f  es  e  of  inl(p)  =>  \{fst(p)\}  |  inr(p)  =>  \{\})  es  e)] 
            supposing  \muparrow{}(\#((\mlambda{}es,e.  case  f  es  e  of  inl(p)  =>  \{fst(p)\}  |  inr(p)  =>  \{\})  es  e)  =\msubz{}  1))


By

---

Latex:
(Reduce  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}(f  es  e)  =  d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index