---

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


1. [Info] : Type
2. [A] : Type
3. [P] : eo:EO+(Info) ─→ E ─→ A ─→ ℙ
4. f : eo:EO+(Info) ─→ e:E ─→ (a:A × P[eo;e;a] + (¬(a:A × P[eo;e;a])))@i'
5. eo : EO+(Info)@i'
6. e : E@i
7. x : a:A × P[eo;e;a]@i
8. (f eo e) = (inl x) ∈ (a:A × P[eo;e;a] + (¬(a:A × P[eo;e;a])))@i
9. True ⇐ ∃a:A. P[eo;e;a]
10. True
11. ∃a:A. P[eo;e;a]
⊢ P[eo;e;fst(x)]
BY
{ (DVar `x' THEN Reduce 0 THEN Auto) }

---

Latex:



1.  [Info]  :  Type
2.  [A]  :  Type
3.  [P]  :  eo:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  f  :  eo:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  (a:A  \mtimes{}  P[eo;e;a]  +  (\mneg{}(a:A  \mtimes{}  P[eo;e;a])))@i'
5.  eo  :  EO+(Info)@i'
6.  e  :  E@i
7.  x  :  a:A  \mtimes{}  P[eo;e;a]@i
8.  (f  eo  e)  =  (inl  x)@i
9.  True  \mLeftarrow{}{}  \mexists{}a:A.  P[eo;e;a]
10.  True
11.  \mexists{}a:A.  P[eo;e;a]
\mvdash{}  P[eo;e;fst(x)]


By

(DVar  `x'  THEN  Reduce  0  THEN  Auto)

---

Home Index