---

Step * of Lemma null-data-stream

∀[L:Top List]. ∀[P:Top].  (null(data-stream(P;L)) ~ null(L))
BY
{ ((UnivCD THENA Auto)
   THEN D 1
   THEN RepUR ``data-stream`` 0
   THEN Auto
   THEN (RWW "upto_add_1 map_append_sq null_append" 0 THENM (Reduce 0 THEN RWO "band_ff_simp" 0))
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  1
  THEN  RepUR  ``data-stream``  0
  THEN  Auto
  THEN  (RWW  "upto\_add\_1  map\_append\_sq  null\_append"  0  THENM  (Reduce  0  THEN  RWO  "band\_ff\_simp"  0))
  THEN  Auto)

---

Home Index