---

Step * of Lemma global-eo-info-le-before

∀[L:(Id × Top) List]. ∀[e:E].  (map(λe.info(e);≤loc(e)) ~ map(λx.(snd(x));filter(λx.fst(x) = loc(e);firstn(e + 1;L))))
BY
{ (Intros
   THEN ((RWO "global-eo-E-sq" 0 THEN Auto)
        ORELSE (UseWitness ⌜Ax⌝⋅
                THEN MemCD
                THEN Unfold `es-le-before` 0
                THEN (RWO "map_append_sq" 0 THENA Auto)
                THEN Reduce 0
                THEN (RWO "global-eo-info-before" 0 THENA Auto))
        )
   ) }

1
1. L : (Id × Top) List
2. e : E
⊢ map(λx.(snd(x));filter(λx.fst(x) = loc(e);firstn(e;L))) @ [info(e)] 
~ map(λx.(snd(x));filter(λx.fst(x) = loc(e);firstn(e + 1;L)))

---

Latex:

---

Latex:
\mforall{}[L:(Id  \mtimes{}  Top)  List].  \mforall{}[e:E].
    (map(\mlambda{}e.info(e);\mleq{}loc(e))  \msim{}  map(\mlambda{}x.(snd(x));filter(\mlambda{}x.fst(x)  =  loc(e);firstn(e  +  1;L))))


By

---

Latex:
(Intros
  THEN  ((RWO  "global-eo-E-sq"  0  THEN  Auto)
            ORELSE  (UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
                            THEN  MemCD
                            THEN  Unfold  `es-le-before`  0
                            THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (RWO  "global-eo-info-before"  0  THENA  Auto))
            )
  )

---

Home Index