---

Step * of Lemma es-base-pred-less

∀es:EO. ∀e:es-base-E(es).  ((¬↑(es-eq(es) pred1(e) e)) ⇒ (pred1(e) < e))
BY
{ ((D 0 THENA Auto) THEN InstLemma `es-eq-wf-base` [⌈es⌉]⋅ THEN Auto) }

1
1. es : EO@i'
2. es-eq(es) ∈ EqDecider(es-base-E(es))
3. e : es-base-E(es)@i
4. ¬↑(es-eq(es) pred1(e) e)@i
⊢ (pred1(e) < e)

---

Latex:


\mforall{}es:EO.  \mforall{}e:es-base-E(es).    ((\mneg{}\muparrow{}(es-eq(es)  pred1(e)  e))  {}\mRightarrow{}  (pred1(e)  <  e))


By

((D  0  THENA  Auto)  THEN  InstLemma  `es-eq-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index