---

Step * of Lemma es-init-le-iff

∀es:EO. ∀e,e':E.  (es-init(es;e) ≤loc e'  ⇐⇒ loc(e') = loc(e) ∈ Id)
BY
{ (Auto THEN (FLemma `es-init-eq` [-1] THEN Auto) THEN RevHypSubst (-1) 0 THEN Auto) }

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

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (es-init(es;e)  \mleq{}loc  e'    \mLeftarrow{}{}\mRightarrow{}  loc(e')  =  loc(e))


By

(Auto  THEN  (FLemma  `es-init-eq`  [-1]  THEN  Auto)  THEN  RevHypSubst  (-1)  0  THEN  Auto)

---

Home Index