---

Step * 2 of Lemma nth-stream-map


1. f : Top
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. ∀[as:stream(Top)]. (s-nth(n - 1;stream-map(f;as)) ~ f s-nth(n - 1;as))
6. as : stream(Top)
7. s1 : Top
8. s2 : stream(Top)
9. as = <s1, s2> ∈ (Top × stream(Top))
⊢ eval m = n - 1 in
  s-nth(m;stream-map(f;s2)) ~ f eval m = n - 1 in s-nth(m;s2)
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:stream(Top)].  (s-nth(n  -  1;stream-map(f;as))  \msim{}  f  s-nth(n  -  1;as))
6.  as  :  stream(Top)
7.  s1  :  Top
8.  s2  :  stream(Top)
9.  as  =  <s1,  s2>
\mvdash{}  eval  m  =  n  -  1  in
    s-nth(m;stream-map(f;s2))  \msim{}  f  eval  m  =  n  -  1  in  s-nth(m;s2)


By

---

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

---

Home Index