---

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

.....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)))
BY
{ ((Assert ∃a:A. ((↑e ∈b X) ∧ (a = X(e) ∈ A)) ⇐⇒ ↑e ∈b X BY
          (Auto THEN ExRepD THEN Auto THEN InstConcl [⌈X(e)⌉]⋅ THEN Auto))
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:


.....decidable?..... 
1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  A  :  Type@i'
4.  X  :  EClass(A)@i'
5.  e  :  E@i
\mvdash{}  Dec(\mexists{}a:A.  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (a  =  X(e))))


By

((Assert  \mexists{}a:A.  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (a  =  X(e)))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  X  BY
                (Auto  THEN  ExRepD  THEN  Auto  THEN  InstConcl  [\mkleeneopen{}X(e)\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index