---

Step * 2 of Lemma firstn-data-stream


1. n : ℤ
2. 0 < n
3. ∀[L:Top List]. ∀[P:Top].  (firstn(n - 1;data-stream(P;L)) ~ data-stream(P;firstn(n - 1;L)))
4. L : Top List
5. P : Top
⊢ firstn(n;data-stream(P;L)) ~ data-stream(P;firstn(n;L))
BY
{ (D -2 THEN Reduce 0 THEN Try (Trivial) THEN (RWO "data-stream-cons" 0 THENA Auto)) }

1
1. n : ℤ
2. 0 < n
3. ∀[L:Top List]. ∀[P:Top].  (firstn(n - 1;data-stream(P;L)) ~ data-stream(P;firstn(n - 1;L)))
4. u : Top
5. v : Top List
6. P : Top
⊢ firstn(n;[snd(P(u)) / data-stream(fst(P(u));v)]) ~ data-stream(P;firstn(n;[u / v]))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[L:Top  List].  \mforall{}[P:Top].    (firstn(n  -  1;data-stream(P;L))  \msim{}  data-stream(P;firstn(n  -  1;L)))
4.  L  :  Top  List
5.  P  :  Top
\mvdash{}  firstn(n;data-stream(P;L))  \msim{}  data-stream(P;firstn(n;L))


By

---

Latex:
(D  -2  THEN  Reduce  0  THEN  Try  (Trivial)  THEN  (RWO  "data-stream-cons"  0  THENA  Auto))

---

Home Index