---

Step * of Lemma es-loc-init

∀[es:EO]. ∀[e:E].  (loc(es-init(es;e)) ~ loc(e))
BY
{ (Auto THEN AssertBY es-init(es;e) ≤loc e  (RWO "es-init-le" 0 THEN Auto)⋅ THEN Auto) }

1
1. es : EO
2. e : E
3. es-init(es;e) ≤loc e 
⊢ loc(es-init(es;e)) = loc(e) ∈ Id

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (loc(es-init(es;e))  \msim{}  loc(e))


By

(Auto  THEN  AssertBY  es-init(es;e)  \mleq{}loc  e    (RWO  "es-init-le"  0  THEN  Auto)\mcdot{}  THEN  Auto)

---

Home Index