---

Step * of Lemma decidable__es-p-le-pred

∀es:EO. ∀[P:E ─→ ℙ]. ((∀e:E. Dec(P e)) ⇒ (∀e,e':E.  Dec(es-p-le-pred(es;P) e e')))
BY
{ (RepUR ``es-p-le-pred`` 0 THEN Auto) }

1
.....decidable?..... 
1. es : EO@i'
2. [P] : E ─→ ℙ
3. ∀e:E. Dec(P e)@i
4. e : E@i
5. e' : E@i
⊢ Dec(e' ≤loc e  ∧ (P e') ∧ (∀e'':E. (e'' ≤loc e  ⇒ (e' <loc e'') ⇒ (¬(P e'')))))

---

Latex:


\mforall{}es:EO.  \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}e:E.  Dec(P  e))  {}\mRightarrow{}  (\mforall{}e,e':E.    Dec(es-p-le-pred(es;P)  e  e')))


By

(RepUR  ``es-p-le-pred``  0  THEN  Auto)

---

Home Index