---

Step * of Lemma es-init-locl

∀es:EO. ∀e:E.  ((¬↑first(e)) ⇒ (es-init(es;e) <loc e))
BY
{ (Auto
   THEN (Assert ⌜es-init(es;e) ≤loc e ⌝⋅ THENA (RWO "es-init-le" 0 THEN Auto))
   THEN D (-1)
   THEN Auto
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN RWO "es-init-identity" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e:E.    ((\mneg{}\muparrow{}first(e))  {}\mRightarrow{}  (es-init(es;e)  <loc  e))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}es-init(es;e)  \mleq{}loc  e  \mkleeneclose{}\mcdot{}  THENA  (RWO  "es-init-le"  0  THEN  Auto))
  THEN  D  (-1)
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  RWO  "es-init-identity"  (-1)
  THEN  Auto)

---

Home Index