---

Step * 2 1 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. 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]))
BY
{ (RecUnfold `firstn` 0 THEN Reduce 0 THEN AutoSplit THEN (RWO "data-stream-cons" 0 THENA Auto) THEN EqCD) }

---

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.  u  :  Top
5.  v  :  Top  List
6.  P  :  Top
\mvdash{}  firstn(n;[snd(P(u))  /  data-stream(fst(P(u));v)])  \msim{}  data-stream(P;firstn(n;[u  /  v]))


By

---

Latex:
(RecUnfold  `firstn`  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (RWO  "data-stream-cons"  0  THENA  Auto)
  THEN  EqCD)

---

Home Index