---

Step * of Lemma nth-stream-map

∀[f:Top]. ∀[n:ℕ]. ∀[as:stream(Top)].  (s-nth(n;stream-map(f;as)) ~ f s-nth(n;as))
BY
{ (InductionOnNat
   THEN RecUnfold `s-nth` 0
   THEN RecUnfold `stream-map` 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) }

1
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

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

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `s-nth`  0
  THEN  RecUnfold  `stream-map`  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)

---

Home Index