---

Step * 1 of Lemma firstn-data-stream


1. n : ℤ
2. L : Top List
3. P : Top
⊢ firstn(0;data-stream(P;L)) ~ data-stream(P;firstn(0;L))
BY
{ (RWO "first0" 0 THEN Reduce 0 THEN Try (Complete (Auto)) THEN Unfold `data-stream` 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "first0"  0  THEN  Reduce  0  THEN  Try  (Complete  (Auto))  THEN  Unfold  `data-stream`  0  THEN  Auto)

---

Home Index