---

Step * 1 of Lemma data-stream-append


1. u : Top
2. v : Top List
3. ∀[as2:Top List]. ∀[P:Top].  (data-stream(P;v @ as2) ~ data-stream(P;v) @ data-stream(P*(v);as2))
4. as2 : Top List
5. P : Top
⊢ data-stream(P;[u / (v @ as2)]) ~ data-stream(P;[u / v]) @ data-stream(fst(P(u))*(v);as2)
BY
{ ((RWO "data-stream-cons" 0 THENM (Reduce 0 THEN EqCD)) THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[as2:Top  List].  \mforall{}[P:Top].    (data-stream(P;v  @  as2)  \msim{}  data-stream(P;v)  @  data-stream(P*(v);as2))
4.  as2  :  Top  List
5.  P  :  Top
\mvdash{}  data-stream(P;[u  /  (v  @  as2)])  \msim{}  data-stream(P;[u  /  v])  @  data-stream(fst(P(u))*(v);as2)


By

---

Latex:
((RWO  "data-stream-cons"  0  THENM  (Reduce  0  THEN  EqCD))  THEN  Auto)

---

Home Index