---

Step * 1 of Lemma es-interface-le-pred

.....decidable?..... 
1. [Info] : Type
2. [P] : es:EO+(Info) ─→ E ─→ ℙ
3. ∀es:EO+(Info). ∀e:E.  Dec(P es e)@i'
4. es : EO+(Info)@i'
5. e : E@i
⊢ Dec(∃a:{e:E| P es e} . (es-p-le-pred(es;P es) e a))
BY
{ (Assert ⌈Dec(∃a:E. (es-p-le-pred(es;P es) e a))⌉⋅ THEN Auto THEN Repeat (ParallelLast)) }

1
.....wf..... 
1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ ℙ
3. ∀es:EO+(Info). ∀e:E.  Dec(P es e)@i'
4. es : EO+(Info)@i'
5. e : E@i
6. a : E
7. es-p-le-pred(es;P es) e a
⊢ a ∈ {e:E| P es e} 

---

Latex:

---

Latex:
.....decidable?..... 
1.  [Info]  :  Type
2.  [P]  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(P  es  e)@i'
4.  es  :  EO+(Info)@i'
5.  e  :  E@i
\mvdash{}  Dec(\mexists{}a:\{e:E|  P  es  e\}  .  (es-p-le-pred(es;P  es)  e  a))


By

---

Latex:
(Assert  \mkleeneopen{}Dec(\mexists{}a:E.  (es-p-le-pred(es;P  es)  e  a))\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Repeat  (ParallelLast))

---

Home Index