---

Step * of Lemma decidable__exists-es-p-le-pred

∀es:EO. ∀[P:E ─→ ℙ]. ∀e:E. ((∀e:E. Dec(P e)) ⇒ Dec(∃a:E. (es-p-le-pred(es;P) e a)))
BY
{ (Auto
   THEN RepUR ``es-p-le-pred`` 0
   THEN Unfold `and` 0
   THEN Fold `cand` 0
   THEN Fold `existse-le` 0
   THEN Fold `alle-le` 0
   THEN Auto) }

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

---

Latex:


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


By

(Auto
  THEN  RepUR  ``es-p-le-pred``  0
  THEN  Unfold  `and`  0
  THEN  Fold  `cand`  0
  THEN  Fold  `existse-le`  0
  THEN  Fold  `alle-le`  0
  THEN  Auto)

---

Home Index