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