---

Step * 1 of Lemma nth-stream-map


1. f : Top
2. n : ℤ
3. 0 = 0 ∈ ℤ
4. as : stream(Top)
5. s1 : Top
6. s2 : stream(Top)
7. as = <s1, s2> ∈ (Top × stream(Top))
⊢ f s1 ~ f s1
BY
{ Auto }

---

Latex:

---

Latex:

1.  f  :  Top
2.  n  :  \mBbbZ{}
3.  0  =  0
4.  as  :  stream(Top)
5.  s1  :  Top
6.  s2  :  stream(Top)
7.  as  =  <s1,  s2>
\mvdash{}  f  s1  \msim{}  f  s1


By

---

Latex:
Auto

---

Home Index