---

Step * of Lemma data-stream-append

∀[as1,as2:Top List]. ∀[P:Top].  (data-stream(P;as1 @ as2) ~ data-stream(P;as1) @ data-stream(P*(as1);as2))
BY
{ (InductionOnList THEN Reduce 0 THEN (UnivCD THENA Auto) THEN Try (Trivial)) }

1
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)

---

Latex:

---

Latex:
\mforall{}[as1,as2:Top  List].  \mforall{}[P:Top].
    (data-stream(P;as1  @  as2)  \msim{}  data-stream(P;as1)  @  data-stream(P*(as1);as2))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  (UnivCD  THENA  Auto)  THEN  Try  (Trivial))

---

Home Index