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')))
BY
(RepUR ``es-p-le-pred`` THEN Auto) }

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


Latex:


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


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




Home Index