---

Step * 1 1 2 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;s-tl(fibs())) = s-nth(n - 1;fibs()) ∈ ℤ
BY
{ RW (AddrC [3] (RecUnfoldTopAbC)) 0⋅ }

1
1. n : {1...}
2. n - 1 ≠ 0
3. ∀n:ℕn. (s-nth(n;fibs()) = fib(n) ∈ ℤ)
⊢ s-nth(n - 1 - 1;s-tl(fibs()))
= let a,s' = fibs() 
  in if (n - 1 =z 0) then a else eval m = n - 1 - 1 in s-nth(m;s') fi 
∈ ℤ

---

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;s-tl(fibs()))  =  s-nth(n  -  1;fibs())


By

---

Latex:
RW  (AddrC  [3]  (RecUnfoldTopAbC))  0\mcdot{}

---

Home Index