---

Step * of Lemma nth-stream-zip

∀[f:Top]. ∀[n:ℕ]. ∀[as,bs:stream(Top)].  (s-nth(n;stream-zip(f;as;bs)) ~ f s-nth(n;as) s-nth(n;bs))
BY
{ (InductionOnNat
   THEN RecUnfold `s-nth` 0
   THEN RecUnfold `stream-zip` 0
   THEN AutoSplit
   THEN Auto
   THEN (GenConcl ⌜as = ss ∈ (Top × stream(Top))⌝⋅⋅
         THENA (Auto THEN DoSubsume THEN Auto THEN InstLemma `stream-ext` [⌜Top⌝]⋅ THEN Auto)
         )
   THEN D -2
   THEN Reduce 0
   THEN (GenConcl ⌜bs = ss ∈ (Top × stream(Top))⌝⋅⋅
         THENA (Auto THEN DoSubsume THEN Auto THEN InstLemma `stream-ext` [⌜Top⌝]⋅ THEN Auto)
         )
   THEN D -2
   THEN Reduce 0) }

1
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

2
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)

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `s-nth`  0
  THEN  RecUnfold  `stream-zip`  0
  THEN  AutoSplit
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}as  =  ss\mkleeneclose{}\mcdot{}\mcdot{}
              THENA  (Auto  THEN  DoSubsume  THEN  Auto  THEN  InstLemma  `stream-ext`  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  D  -2
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}bs  =  ss\mkleeneclose{}\mcdot{}\mcdot{}
              THENA  (Auto  THEN  DoSubsume  THEN  Auto  THEN  InstLemma  `stream-ext`  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  D  -2
  THEN  Reduce  0)

---

Home Index