---

Step * of Lemma hd-stream-zip

∀[f:Top]. ∀[as,bs:stream(Top)].  (s-hd(stream-zip(f;as;bs)) ~ f s-hd(as) s-hd(bs))
BY
{ (Auto
   THEN (InstLemma `nth-stream-zip` [⌜f⌝;⌜0⌝;⌜as⌝;⌜bs⌝]⋅ THENA Auto)
   THEN RecUnfold `s-nth` (-1)
   THEN Reduce (-1)
   THEN Fold `pi1` (-1)
   THEN Fold `s-hd` (-1)
   THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `nth-stream-zip`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RecUnfold  `s-nth`  (-1)
  THEN  Reduce  (-1)
  THEN  Fold  `pi1`  (-1)
  THEN  Fold  `s-hd`  (-1)
  THEN  Trivial)

---

Home Index