---

Step * 2 1 of Lemma data-stream-cons


1. L : Top List
2. a : Top
3. P : Top
4. u : ℕ||L||
5. v : ℕ||L|| List
6. map(λx.(snd(P*(firstn(x + 1;[a / L]))([a / L][x + 1])));v) ~ map(λi.(snd(fst(P(a))*(firstn(i;L))(L[i])));v)
⊢ P*(firstn(u + 1;[a / L])) ~ fst(P(a))*(firstn(u;L))
BY
{ Subst ⌈firstn(u + 1;[a / L]) ~ [a / firstn(u;L)]⌉ 0⋅ }

1
.....equality..... 
1. L : Top List
2. a : Top
3. P : Top
4. u : ℕ||L||
5. v : ℕ||L|| List
6. map(λx.(snd(P*(firstn(x + 1;[a / L]))([a / L][x + 1])));v) ~ map(λi.(snd(fst(P(a))*(firstn(i;L))(L[i])));v)
⊢ firstn(u + 1;[a / L]) ~ [a / firstn(u;L)]

2
1. L : Top List
2. a : Top
3. P : Top
4. u : ℕ||L||
5. v : ℕ||L|| List
6. map(λx.(snd(P*(firstn(x + 1;[a / L]))([a / L][x + 1])));v) ~ map(λi.(snd(fst(P(a))*(firstn(i;L))(L[i])));v)
⊢ P*([a / firstn(u;L)]) ~ fst(P(a))*(firstn(u;L))

---

Latex:

---

Latex:

1.  L  :  Top  List
2.  a  :  Top
3.  P  :  Top
4.  u  :  \mBbbN{}||L||
5.  v  :  \mBbbN{}||L||  List
6.  map(\mlambda{}x.(snd(P*(firstn(x  +  1;[a  /  L]))([a  /  L][x  +  1])));v) 
\msim{}  map(\mlambda{}i.(snd(fst(P(a))*(firstn(i;L))(L[i])));v)
\mvdash{}  P*(firstn(u  +  1;[a  /  L]))  \msim{}  fst(P(a))*(firstn(u;L))


By

---

Latex:
Subst  \mkleeneopen{}firstn(u  +  1;[a  /  L])  \msim{}  [a  /  firstn(u;L)]\mkleeneclose{}  0\mcdot{}

---

Home Index