---

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


1. es : EO@i'
2. e : es-base-E(es)@i
3. es-eq(es) ∈ EqDecider(es-base-E(es))
4. ↑(es-eq(es) pred1(e) e)
5. ∀[e,e':es-base-E(es)].  ((e < e') ∈ ℙ)
⊢ pred1(e) = e ∈ es-base-E(es)
BY
{ (Fold `es-eq-E` (-2) THEN RWO "assert-es-eq-E-base<" (-2) THEN Auto)⋅ }

---

Latex:



1.  es  :  EO@i'
2.  e  :  es-base-E(es)@i
3.  es-eq(es)  \mmember{}  EqDecider(es-base-E(es))
4.  \muparrow{}(es-eq(es)  pred1(e)  e)
5.  \mforall{}[e,e':es-base-E(es)].    ((e  <  e')  \mmember{}  \mBbbP{})
\mvdash{}  pred1(e)  =  e


By

(Fold  `es-eq-E`  (-2)  THEN  RWO  "assert-es-eq-E-base<"  (-2)  THEN  Auto)\mcdot{}

---

Home Index