---

Step * 1 of Lemma constant-data-stream


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)))
BY
{ ((D 0 THENA Auto)
   THEN (RW (AddrC [2;2] (LemmaC `upto_decomp2`)) 0 THENA Auto')
   THEN Reduce 0
   THEN ((RWO "map-map" 0 THENM RepUR ``compose`` 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||)))
4. b : Top
⊢ [b / map(λi.b;upto(||v||))] ~ [b / map(λx.b;upto((||v|| + 1) - 1))]

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[b:Top].  (data-stream(constant-dataflow(b);v)  \msim{}  map(\mlambda{}i.b;upto(||v||)))
\mvdash{}  \mforall{}[b:Top].  ([b  /  map(\mlambda{}i.b;upto(||v||))]  \msim{}  map(\mlambda{}i.b;upto(||v||  +  1)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (RW  (AddrC  [2;2]  (LemmaC  `upto\_decomp2`))  0  THENA  Auto')
  THEN  Reduce  0
  THEN  ((RWO  "map-map"  0  THENM  RepUR  ``compose``  0)  THENA  Auto))

---

Home Index