---

Step * of Lemma tl-stream-zip

∀[f:Top]. ∀[as,bs:stream(Top)].  (s-tl(stream-zip(f;as;bs)) ~ stream-zip(f;s-tl(as);s-tl(bs)))
BY
{ (Auto THEN RW (AddrC [1] (RecUnfoldC `stream-zip`)) 0) }

1
1. f : Top
2. as : stream(Top)
3. bs : stream(Top)
⊢ s-tl(let a,as' = as 
       in let b,bs' = bs 
          in <f a b, stream-zip(f;as';bs')>) ~ stream-zip(f;s-tl(as);s-tl(bs))

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[as,bs:stream(Top)].    (s-tl(stream-zip(f;as;bs))  \msim{}  stream-zip(f;s-tl(as);s-tl(bs)))


By

---

Latex:
(Auto  THEN  RW  (AddrC  [1]  (RecUnfoldC  `stream-zip`))  0)

---

Home Index