---

Step * of Lemma constant-data-stream

∀[L:Top List]. ∀[b:Top].  (data-stream(constant-dataflow(b);L) ~ map(λi.b;upto(||L||)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN ((RWO "data-stream-cons" 0 THENM Reduce 0) THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)) }

1
1. u : Top
2. v : Top List
3. ∀[b:Top]. (data-stream(constant-dataflow(b);v) ~ map(λi.b;upto(||v||)))
⊢ ∀[b:Top]. ([b / map(λi.b;upto(||v||))] ~ map(λi.b;upto(||v|| + 1)))

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[b:Top].    (data-stream(constant-dataflow(b);L)  \msim{}  map(\mlambda{}i.b;upto(||L||)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  ((RWO  "data-stream-cons"  0  THENM  Reduce  0)  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index