---

Step * 2 1 2 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*([a / firstn(u;L)]) ~ fst(P(a))*(firstn(u;L))
BY
{ (Reduce 0 THEN Auto) }

---

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*([a  /  firstn(u;L)])  \msim{}  fst(P(a))*(firstn(u;L))


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index