---

Step * 1 of Lemma nth-stream-zip


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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index