---

Step * of Lemma nth-better-fibs

∀n:ℕ. (s-nth(n;better-fibs()) = fib(n) ∈ ℤ)
BY
{ (Auto THEN Unfold `better-fibs` 0 THEN (RWO "nth-stream-map" 0 THENM Reduce 0) THEN Try (Complete (Auto))) }

1
.....wf..... 
1. n : ℕ
⊢ mk-stream(λp.let a,b = p 
               in eval c = a + b in
                  <b, c>;<1, 1>) ∈ stream(Top)

2
1. n : ℕ
⊢ (fst(s-nth(n;mk-stream(λp.let a,b = p in eval c = a + b in <b, c>;<1, 1>)))) = fib(n) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (s-nth(n;better-fibs())  =  fib(n))


By

---

Latex:
(Auto
  THEN  Unfold  `better-fibs`  0
  THEN  (RWO  "nth-stream-map"  0  THENM  Reduce  0)
  THEN  Try  (Complete  (Auto)))

---

Home Index