---

Step * 1 of Lemma nth-fibs


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)) ∈ ℤ
BY
{ ((RWO "nth-stream-zip" 0⋅ THENA Auto) THEN Reduce 0) }

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

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  n  -  1  \mneq{}  0
3.  \mforall{}n:\mBbbN{}n.  (s-nth(n;fibs())  =  fib(n))
\mvdash{}  s-nth(n  -  1  -  1;stream-zip(\mlambda{}x,y.  (x  +  y);fibs();s-tl(fibs())))  =  (fib(n  -  1)  +  fib(n  -  2))


By

---

Latex:
((RWO  "nth-stream-zip"  0\mcdot{}  THENA  Auto)  THEN  Reduce  0)

---

Home Index