---

Step * of Lemma es-interface-implies-decidable

∀[Info:Type]
  ∀es:EO+(Info). ∀A:Type. ∀X:EClass(A).
    ∃P:E ─→ A ─→ ℙ. ((∀e:E. Dec(∃a:A. P[e;a])) ∧ (∀e:E. ((↑e ∈b X ⇐⇒ ∃a:A. P[e;a]) ∧ P[e;X(e)] supposing ↑e ∈b X)))
BY
{ (Auto THEN InstConcl [⌈λe,a. ((↑e ∈b X) ∧ (a = X(e) ∈ A))⌉]⋅ THEN All (RepUR ``so_apply``)⋅ THEN Auto) }

1
.....decidable?..... 
1. [Info] : Type
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : EClass(A)@i'
5. e : E@i
⊢ Dec(∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A)))

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : EClass(A)@i'
5. ∀e:E. Dec(∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A)))
6. e : E@i
7. ↑e ∈b X@i
⊢ ∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A))

3
1. Info : Type
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : EClass(A)@i'
5. ∀e:E. Dec(∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A)))
6. e : E@i
7. ∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A))@i
⊢ ↑e ∈b X

---

Latex:


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


By

(Auto  THEN  InstConcl  [\mkleeneopen{}\mlambda{}e,a.  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (a  =  X(e)))\mkleeneclose{}]\mcdot{}  THEN  All  (RepUR  ``so\_apply``)\mcdot{}  THEN  Auto)

---

Home Index