---

Step * of Lemma es-base-pred-le

∀es:EO. ∀e:es-base-E(es).  ((pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es)))
BY
{ (Auto THEN ((InstLemma `es-eq-wf-base` [⌈es⌉]⋅ THENA Auto) THEN (Decide ↑(es-eq(es) pred1(e) e)⋅ THENA Auto))) }

1
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)
⊢ (pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es))

2
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)
⊢ (pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es))

---

Latex:


\mforall{}es:EO.  \mforall{}e:es-base-E(es).    ((pred1(e)  <  e)  \mvee{}  (pred1(e)  =  e))


By

(Auto
  THEN  ((InstLemma  `es-eq-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (Decide  \muparrow{}(es-eq(es)  pred1(e)  e)\mcdot{}  THENA  Auto)
              )
  )

---

Home Index