---

Step * 1 1 1 1 1 1 1 of Lemma global-eo-before


1. L : (Id × Top) List
2. n : ℕ
3. ∀n:ℕn. (n < ||L|| ⇒ (before(n) = filter(λn@0.fst(L[n@0]) = fst(L[n]);upto(n)) ∈ (ℕn List)))
4. n < ||L||@i
5. n ∈ E
6. ↑(∀x∈upto(n).¬bfst(L[x]) = fst(L[n]))_b
⊢ (∀x∈upto(n).¬↑fst(L[x]) = fst(L[n]))
BY
{ (RWO "assert-bl-all" (-1) THEN Auto) }

1
1. L : (Id × Top) List
2. n : ℕ
3. ∀n:ℕn. (n < ||L|| ⇒ (before(n) = filter(λn@0.fst(L[n@0]) = fst(L[n]);upto(n)) ∈ (ℕn List)))
4. n < ||L||@i
5. n ∈ E
6. (∀x∈upto(n).↑¬bfst(L[x]) = fst(L[n]))
⊢ (∀x∈upto(n).¬↑fst(L[x]) = fst(L[n]))

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n.  (n  <  ||L||  {}\mRightarrow{}  (before(n)  =  filter(\mlambda{}n@0.fst(L[n@0])  =  fst(L[n]);upto(n))))
4.  n  <  ||L||@i
5.  n  \mmember{}  E
6.  \muparrow{}(\mforall{}x\mmember{}upto(n).\mneg{}\msubb{}fst(L[x])  =  fst(L[n]))\_b
\mvdash{}  (\mforall{}x\mmember{}upto(n).\mneg{}\muparrow{}fst(L[x])  =  fst(L[n]))


By

---

Latex:
(RWO  "assert-bl-all"  (-1)  THEN  Auto)

---

Home Index