---

Step * of Lemma es-causl-swellfnd-base

∀es:EO. SWellFounded((e < e'))
BY
{ (InstLemma `event_ordering_properties` []⋅
   THEN ParallelLast
   THEN D -1
   THEN Thin (-1)
   THEN Thin 1
   THEN With ⌈λx.es-rank(es;x)⌉ (D 0)⋅
   THEN Reduce 0
   THEN Try (Trivial)) }

1
.....wf..... 
1. es : EO@i'
2. ∀x,y:es-base-E(es).  ((x < y) ⇒ es-rank(es;x) < es-rank(es;y))
⊢ λx.es-rank(es;x) ∈ es-base-E(es) ─→ ℕ

2
.....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') ∈ ℙ

---

Latex:


\mforall{}es:EO.  SWellFounded((e  <  e'))


By

(InstLemma  `event\_ordering\_properties`  []\mcdot{}
  THEN  ParallelLast
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  Thin  1
  THEN  With  \mkleeneopen{}\mlambda{}x.es-rank(es;x)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Reduce  0
  THEN  Try  (Trivial))

---

Home Index