---

Step * of Lemma es-causl-wf-base

∀[the_es:EO]. ∀[e,e':es-base-E(the_es)].  ((e < e') ∈ ℙ)
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN All (Unfold `es-base-E`)
   THEN (D 1 THEN (DRecord 1 THENA Auto) THEN ProveWfLemma)⋅)⋅ }

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e,e':es-base-E(the$_{es}$)].    ((e  <  e')  \000C\mmember{}  \mBbbP{})


By

(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  All  (Unfold  `es-base-E`)
  THEN  (D  1  THEN  (DRecord  1  THENA  Auto)  THEN  ProveWfLemma)\mcdot{})\mcdot{}

---

Home Index