Step * 1 1 of Lemma nth-fibs


1. {1...}
2. 1 ≠ 0
3. ∀n:ℕn. (s-nth(n;fibs()) fib(n) ∈ ℤ)
⊢ (s-nth(n 1;fibs()) s-nth(n 1;s-tl(fibs()))) (fib(n 1) fib(n 2)) ∈ ℤ
BY
(Subst' fib(n 1) fib(n 2) fib(n 2) fib(n 1) THEN Auto THEN EqCD) }

1
.....subterm..... T:t
1:n
1. {1...}
2. 1 ≠ 0
3. ∀n:ℕn. (s-nth(n;fibs()) fib(n) ∈ ℤ)
⊢ s-nth(n 1;fibs()) fib(n 2) ∈ ℤ

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


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


By


Latex:
(Subst'  fib(n  -  1)  +  fib(n  -  2)  \msim{}  fib(n  -  2)  +  fib(n  -  1)  0  THEN  Auto  THEN  EqCD)




Home Index