---

Step * of Lemma es-before-partition

∀[es:EO]. ∀[e,e':E].  before(e) = (≤loc(e') @ (e', e)) ∈ (E List) supposing (e' <loc e)
BY
{ (InstLemma `es-le-before-partition` [] THEN (RepeatFor 4 (ParallelLast') THENA Auto)) }

1
1. es : EO
2. e : E
3. e' : E
4. (e' <loc e)
5. ≤loc(e) = (before(e') @ [e', e]) ∈ (E List)
⊢ before(e) = (≤loc(e') @ (e', e)) ∈ (E List)

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    before(e)  =  (\mleq{}loc(e')  @  (e',  e))  supposing  (e'  <loc  e)


By

(InstLemma  `es-le-before-partition`  []  THEN  (RepeatFor  4  (ParallelLast')  THENA  Auto))

---

Home Index