---

Step * 1 of Lemma es-loc-init


1. es : EO
2. e : E
3. es-init(es;e) ≤loc e 
⊢ loc(es-init(es;e)) = loc(e) ∈ Id
BY
{ (D (-1) THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  es-init(es;e)  \mleq{}loc  e 
\mvdash{}  loc(es-init(es;e))  =  loc(e)


By

(D  (-1)  THEN  Auto)

---

Home Index