---

Step * 2 of Lemma nth-better-fibs


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) ∈ ℤ
BY
{ Subst' <1, 1> ~ <fib(0), fib(0 + 1)> 0 }

1
.....equality..... 
1. n : ℕ
⊢ <1, 1> ~ <fib(0), fib(0 + 1)>

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  (fst(s-nth(n;mk-stream(\mlambda{}p.let  a,b  =  p  in  eval  c  =  a  +  b  in  <b,  c>ə,  1>))))  =  fib(n)


By

---

Latex:
Subst'  ə,  1>  \msim{}  <fib(0),  fib(0  +  1)>  0

---

Home Index