---

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


1. L : (Id × Top) List
2. n : ℕ
3. ¬↑first(n)
4. ∀n:ℕn. (n < ||L|| ⇒ (before(n) = filter(λn@0.loc(n@0) = loc(n);upto(n)) ∈ (ℕn List)))
5. n < ||L||@i
6. n ∈ E
7. (pred(n) <loc n)
8. (loc(pred(n)) = loc(n) ∈ Id) ∧ pred(n) < n
9. pred(n) ∈ ℕn
⊢ (before(pred(n)) @ [pred(n)]) = filter(λn@0.loc(n@0) = loc(n);upto(n)) ∈ (ℕn List)
BY
{ InstHyp [⌈pred(n)⌉] 4⋅ }

1
.....wf..... 
1. L : (Id × Top) List
2. n : ℕ
3. ¬↑first(n)
4. ∀n:ℕn. (n < ||L|| ⇒ (before(n) = filter(λn@0.loc(n@0) = loc(n);upto(n)) ∈ (ℕn List)))
5. n < ||L||@i
6. n ∈ E
7. (pred(n) <loc n)
8. (loc(pred(n)) = loc(n) ∈ Id) ∧ pred(n) < n
9. pred(n) ∈ ℕn
⊢ pred(n) ∈ ℕn

2
.....antecedent..... 
1. L : (Id × Top) List
2. n : ℕ
3. ¬↑first(n)
4. ∀n:ℕn. (n < ||L|| ⇒ (before(n) = filter(λn@0.loc(n@0) = loc(n);upto(n)) ∈ (ℕn List)))
5. n < ||L||@i
6. n ∈ E
7. (pred(n) <loc n)
8. (loc(pred(n)) = loc(n) ∈ Id) ∧ pred(n) < n
9. pred(n) ∈ ℕn
⊢ pred(n) < ||L||

3
1. L : (Id × Top) List
2. n : ℕ
3. ¬↑first(n)
4. ∀n:ℕn. (n < ||L|| ⇒ (before(n) = filter(λn@0.loc(n@0) = loc(n);upto(n)) ∈ (ℕn List)))
5. n < ||L||@i
6. n ∈ E
7. (pred(n) <loc n)
8. (loc(pred(n)) = loc(n) ∈ Id) ∧ pred(n) < n
9. pred(n) ∈ ℕn
10. before(pred(n)) = filter(λn@0.loc(n@0) = loc(pred(n));upto(pred(n))) ∈ (ℕpred(n) List)
⊢ (before(pred(n)) @ [pred(n)]) = filter(λn@0.loc(n@0) = loc(n);upto(n)) ∈ (ℕn List)

---

Latex:

---

Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  n  :  \mBbbN{}
3.  \mneg{}\muparrow{}first(n)
4.  \mforall{}n:\mBbbN{}n.  (n  <  ||L||  {}\mRightarrow{}  (before(n)  =  filter(\mlambda{}n@0.loc(n@0)  =  loc(n);upto(n))))
5.  n  <  ||L||@i
6.  n  \mmember{}  E
7.  (pred(n)  <loc  n)
8.  (loc(pred(n))  =  loc(n))  \mwedge{}  pred(n)  <  n
9.  pred(n)  \mmember{}  \mBbbN{}n
\mvdash{}  (before(pred(n))  @  [pred(n)])  =  filter(\mlambda{}n@0.loc(n@0)  =  loc(n);upto(n))


By

---

Latex:
InstHyp  [\mkleeneopen{}pred(n)\mkleeneclose{}]  4\mcdot{}

---

Home Index