---

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

.....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)) ∈ 𝕌'
BY
{ 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. X : es:EO+(Info) ─→ e:E ─→ bag(A[es;e])
6. es : EO+(Info)@i'
7. e : E@i
8. (↑(#(X es e) =z 1)) ⇐ ∃a:A[es;e]. R[es;e;a]
9. ↑(#(X es e) =z 1)
10. ∃a:A[es;e]. R[es;e;a]
⊢ single-valued-bag(X es e;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'
5. X : es:EO+(Info) ─→ e:E ─→ bag(A[es;e])
6. es : EO+(Info)@i'
7. e : E@i
8. (↑(#(X es e) =z 1)) ⇐ ∃a:A[es;e]. R[es;e;a]
9. ↑(#(X es e) =z 1)
10. single-valued-bag(X es e;A[es;e])
11. ∃a:A[es;e]. R[es;e;a]
⊢ 0 < #(X es e)

---

Latex:

---

Latex:
.....wf..... 
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'
5.  X  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A[es;e])
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.
        ((\muparrow{}(\#(X  es  e)  =\msubz{}  1)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A[es;e].  R[es;e;a])
        \mwedge{}  R[es;e;only(X  es  e)]  supposing  \muparrow{}(\#(X  es  e)  =\msubz{}  1))  \mmember{}  \mBbbU{}'


By

---

Latex:
Auto

---

Home Index