---

Step * 1 of Lemma fibs-equal-map


1. n : ℕ@i
⊢ s-nth(n;fibs()) = s-nth(n;stream-map(λn.fib(n);nats())) ∈ ℕ
BY
{ (RWW "nth-fibs nth-stream-map nth-nats" 0 THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}@i
\mvdash{}  s-nth(n;fibs())  =  s-nth(n;stream-map(\mlambda{}n.fib(n);nats()))


By

---

Latex:
(RWW  "nth-fibs  nth-stream-map  nth-nats"  0  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index