---

Step * of Lemma length-data-stream

∀[L:Top List]. ∀[P:Top].  (||data-stream(P;L)|| ~ ||L||)
BY
{ ((UnivCD THENA Auto) THEN Unfold `data-stream` 0 THEN RWW "length-map length_upto" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[P:Top].    (||data-stream(P;L)||  \msim{}  ||L||)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `data-stream`  0  THEN  RWW  "length-map  length\_upto"  0  THEN  Auto)

---

Home Index