---

Step * 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)
⊢ (pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es))
BY
{ ((InstLemma `es-causl-wf-base` [⌈es⌉]⋅ THENA Auto) THEN OrRight THEN 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)
5. ∀[e,e':es-base-E(es)].  ((e < e') ∈ ℙ)
⊢ pred1(e) = e ∈ es-base-E(es)

---

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)
\mvdash{}  (pred1(e)  <  e)  \mvee{}  (pred1(e)  =  e)


By

((InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  OrRight  THEN  Auto)

---

Home Index