---

Step * of Lemma es-locl-wellfnd

∀es:EO. WellFnd{i}(E;x,y.(x <loc y))
BY
{ (Auto
   THEN BLemma `strongwf-implies`
   THEN Auto
   THEN (InstLemma `es-causl-swellfnd` [⌈es⌉]⋅ THENA Auto)⋅
   THEN RepeatFor 5 (ParallelLast)
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  WellFnd\{i\}(E;x,y.(x  <loc  y))


By

(Auto
  THEN  BLemma  `strongwf-implies`
  THEN  Auto
  THEN  (InstLemma  `es-causl-swellfnd`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  RepeatFor  5  (ParallelLast)
  THEN  Auto)

---

Home Index