---

Step * 2 of Lemma nth-stream-zip


1. f : Top
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. ∀[as,bs:stream(Top)].  (s-nth(n - 1;stream-zip(f;as;bs)) ~ f s-nth(n - 1;as) s-nth(n - 1;bs))
6. as : stream(Top)
7. bs : stream(Top)
8. s1 : Top
9. s2 : stream(Top)
10. as = <s1, s2> ∈ (Top × stream(Top))
11. s3 : Top
12. s4 : stream(Top)
13. bs = <s3, s4> ∈ (Top × stream(Top))
⊢ eval m = n - 1 in
  s-nth(m;stream-zip(f;s2;s4)) ~ f eval m = n - 1 in s-nth(m;s2) eval m = n - 1 in s-nth(m;s4)
BY
{ ((CallByValueReduce 0 THEN Auto) THENA Auto) }

---

Latex:

---

Latex:

1.  f  :  Top
2.  n  :  \mBbbZ{}
3.  n  \mneq{}  0
4.  0  <  n
5.  \mforall{}[as,bs:stream(Top)].    (s-nth(n  -  1;stream-zip(f;as;bs))  \msim{}  f  s-nth(n  -  1;as)  s-nth(n  -  1;bs))
6.  as  :  stream(Top)
7.  bs  :  stream(Top)
8.  s1  :  Top
9.  s2  :  stream(Top)
10.  as  =  <s1,  s2>
11.  s3  :  Top
12.  s4  :  stream(Top)
13.  bs  =  <s3,  s4>
\mvdash{}  eval  m  =  n  -  1  in
    s-nth(m;stream-zip(f;s2;s4))  \msim{}  f  eval  m  =  n  -  1  in  s-nth(m;s2)  eval  m  =  n  -  1  in  s-nth(m;s4)


By

---

Latex:
((CallByValueReduce  0  THEN  Auto)  THENA  Auto)

---

Home Index