---

Step * of Lemma data-stream-cons

∀[L:Top List]. ∀[a,P:Top].  (data-stream(P;[a / L]) ~ [snd(P(a)) / data-stream(fst(P(a));L)])
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `data-stream` 0
   THEN Subst' upto(||[a / L]||) ~ [0 / map(λi.(i + 1);upto(||L||))] 0) }

1
.....equality..... 
1. L : Top List
2. a : Top
3. P : Top
⊢ upto(||[a / L]||) ~ [0 / map(λi.(i + 1);upto(||L||))]

2
1. L : Top List
2. a : Top
3. P : Top
⊢ map(λi.(snd(P*(firstn(i;[a / L]))([a / L][i])));[0 / map(λi.(i + 1);upto(||L||))]) 
~ [snd(P(a)) / map(λi.(snd(fst(P(a))*(firstn(i;L))(L[i])));upto(||L||))]

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[a,P:Top].    (data-stream(P;[a  /  L])  \msim{}  [snd(P(a))  /  data-stream(fst(P(a));L)])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `data-stream`  0
  THEN  Subst'  upto(||[a  /  L]||)  \msim{}  [0  /  map(\mlambda{}i.(i  +  1);upto(||L||))]  0)

---

Home Index