---

Step * of Lemma nth-fibs

∀n:ℕ. (s-nth(n;fibs()) = fib(n) ∈ ℤ)
BY
{ (CompleteInductionOnNat
   THEN Auto
   THEN RecUnfold `fibs` 0
   THEN RecUnfold `fib` 0
   THEN RepeatFor 2 ((RecUnfold `s-nth` 0 THEN Reduce 0))
   THEN RepeatFor 2 ((AutoSplit THEN Try ((CallByValueReduce 0 THENA Auto))))) }

1
1. n : {1...}
2. n - 1 ≠ 0
3. ∀n:ℕn. (s-nth(n;fibs()) = fib(n) ∈ ℤ)
⊢ s-nth(n - 1 - 1;stream-zip(λx,y. (x + y);fibs();s-tl(fibs()))) = (fib(n - 1) + fib(n - 2)) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(CompleteInductionOnNat
  THEN  Auto
  THEN  RecUnfold  `fibs`  0
  THEN  RecUnfold  `fib`  0
  THEN  RepeatFor  2  ((RecUnfold  `s-nth`  0  THEN  Reduce  0))
  THEN  RepeatFor  2  ((AutoSplit  THEN  Try  ((CallByValueReduce  0  THENA  Auto)))))

---

Home Index