---

Step * 1 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||)))
4. b : Top
⊢ [b / map(λi.b;upto(||v||))] ~ [b / map(λx.b;upto((||v|| + 1) - 1))]
BY
{ Auto }

---

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||)))
4.  b  :  Top
\mvdash{}  [b  /  map(\mlambda{}i.b;upto(||v||))]  \msim{}  [b  /  map(\mlambda{}x.b;upto((||v||  +  1)  -  1))]


By

---

Latex:
Auto

---

Home Index