---

Step * 1 of Lemma global-eo-before


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)
BY
{ (CompNatInd (-2) THEN (D 0 THENA Auto)) }

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

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  n  :  \mBbbN{}@i
3.  n  <  ||L||@i
\mvdash{}  before(n)  =  filter(\mlambda{}n@0.loc(n@0)  =  loc(n);upto(n))


By

---

Latex:
(CompNatInd  (-2)  THEN  (D  0  THENA  Auto))

---

Home Index