---

Step * 1 1 of Lemma select-data-stream


1. L : Top List
2. P : Top
3. i : ℕ
4. i < ||L||
⊢ snd(P*(firstn(upto(||L||)[i];L))(L[upto(||L||)[i]])) ~ snd(P*(firstn(i;L))(L[i]))
BY
{ Subst ⌈upto(||L||)[i] ~ i⌉ 0⋅ }

1
.....equality..... 
1. L : Top List
2. P : Top
3. i : ℕ
4. i < ||L||
⊢ upto(||L||)[i] ~ i

2
1. L : Top List
2. P : Top
3. i : ℕ
4. i < ||L||
⊢ snd(P*(firstn(i;L))(L[i])) ~ snd(P*(firstn(i;L))(L[i]))

---

Latex:

---

Latex:

1.  L  :  Top  List
2.  P  :  Top
3.  i  :  \mBbbN{}
4.  i  <  ||L||
\mvdash{}  snd(P*(firstn(upto(||L||)[i];L))(L[upto(||L||)[i]]))  \msim{}  snd(P*(firstn(i;L))(L[i]))


By

---

Latex:
Subst  \mkleeneopen{}upto(||L||)[i]  \msim{}  i\mkleeneclose{}  0\mcdot{}

---

Home Index