---

Step * 2 of Lemma es-causl-swellfnd-base

.....wf..... 
1. es : EO@i'
2. ∀x,y:es-base-E(es).  ((x < y) ⇒ es-rank(es;x) < es-rank(es;y))
3. f : es-base-E(es) ─→ ℕ
⊢ ∀e,e':es-base-E(es).  ((e < e') ⇒ f e < f e') ∈ ℙ
BY
{ (RepeatFor 2 (MemCD) THEN Try ((InstLemma `es-causl-wf-base` [⌈es⌉;⌈e⌉;⌈e'⌉]⋅ THEN Auto)) THEN Auto) }

---

Latex:


.....wf..... 
1.  es  :  EO@i'
2.  \mforall{}x,y:es-base-E(es).    ((x  <  y)  {}\mRightarrow{}  es-rank(es;x)  <  es-rank(es;y))
3.  f  :  es-base-E(es)  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \mforall{}e,e':es-base-E(es).    ((e  <  e')  {}\mRightarrow{}  f  e  <  f  e')  \mmember{}  \mBbbP{}


By

(RepeatFor  2  (MemCD)  THEN  Try  ((InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THEN  Auto))  THEN  Auto)

---

Home Index