---

Step * of Lemma global-eo-info-before

∀[L:(Id × Top) List]. ∀[e:E].  (map(λe.info(e);before(e)) ~ map(λx.(snd(x));filter(λx.fst(x) = loc(e);firstn(e;L))))
BY
{ (Intros
   THEN ((RWO "global-eo-E-sq" 0 THEN Auto) ORELSE (UseWitness ⌜Ax⌝⋅ THEN MemCD))
   THEN (RWO "global-eo-before" 0 THENA Auto)
   THEN (RWO "global-eo-E-sq" (-1) THENA Auto)
   THEN (RWO  "firstn_map_upto" 0 THENA Auto)
   THEN (Subst' imin(||L||;e) ~ e 0 THENA (Auto THEN RWO "imin_unfold" 0 THEN Auto))) }

1
1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
⊢ map(λe.info(e);filter(λn.loc(n) = loc(e);upto(e))) ~ map(λx.(snd(x));filter(λx.fst(x) = loc(e);map(λi.L[i];upto(e))))

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  ((RWO  "global-eo-E-sq"  0  THEN  Auto)  ORELSE  (UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  MemCD))
  THEN  (RWO  "global-eo-before"  0  THENA  Auto)
  THEN  (RWO  "global-eo-E-sq"  (-1)  THENA  Auto)
  THEN  (RWO    "firstn\_map\_upto"  0  THENA  Auto)
  THEN  (Subst'  imin(||L||;e)  \msim{}  e  0  THENA  (Auto  THEN  RWO  "imin\_unfold"  0  THEN  Auto)))

---

Home Index