---

Step * of Lemma global-eo-before

∀[L:(Id × Top) List]. ∀[e:E].  (before(e) ~ filter(λn.loc(n) = loc(e);upto(e)))
BY
{ (RWO "global-eo-E-sq" 0 THEN Auto THEN (GenConcl ⌜e = n ∈ {n:ℕ| n < ||L||} ⌝⋅ THENA Auto) THEN ThinVar `e' THEN D -1) \000C}

1
1. L : (Id × Top) List
2. n : ℕ@i
3. n < ||L||@i
⊢ before(n) = filter(λn@0.loc(n@0) = loc(n);upto(n)) ∈ (ℕn List)

---

Latex:

---

Latex:
\mforall{}[L:(Id  \mtimes{}  Top)  List].  \mforall{}[e:E].    (before(e)  \msim{}  filter(\mlambda{}n.loc(n)  =  loc(e);upto(e)))


By

---

Latex:
(RWO  "global-eo-E-sq"  0  THEN  Auto  THEN  (GenConcl  \mkleeneopen{}e  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `e'  THEN  D  -1)

---

Home Index