---

Step * 2 1 1 1 1 of Lemma less-fast-fib


1. f : n:ℕ
⟶ a:ℕ
⟶ b:ℕ
⟶ {m:ℕ| 
    k:ℕ ⟶ ((a = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (b = 0 ∈ ℤ)) ⇒ (0 < k ⇒ (b = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(n + k) ∈ ℕ))} 
2. n : ℕ@i
3. (f n 1 0)
= (f n 1 0)
∈ {m:ℕ| 
   k:ℕ ⟶ ((1 = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (0 = 0 ∈ ℤ)) ⇒ (0 < k ⇒ (0 = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(n + k) ∈ ℕ))} 
4. m : ℕ@i
5. ∀k:ℕ. ((1 = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (0 ∈ ℤ)) ⇒ (0 < k ⇒ (0 = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(n + k) ∈ ℕ))
⊢ m = fib(n) ∈ ℕ
BY
{ (InstHyp [⌜0⌝] (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  n:\mBbbN{}
{}\mrightarrow{}  a:\mBbbN{}
{}\mrightarrow{}  b:\mBbbN{}
{}\mrightarrow{}  \{m:\mBbbN{}| 
        k:\mBbbN{}  {}\mrightarrow{}  ((a  =  fib(k))
                      {}\mRightarrow{}  ((k  \mleq{}  0)  {}\mRightarrow{}  (b  =  0))
                      {}\mRightarrow{}  (0  <  k  {}\mRightarrow{}  (b  =  fib(k  -  1)))
                      {}\mRightarrow{}  (m  =  fib(n  +  k)))\} 
2.  n  :  \mBbbN{}@i
3.  (f  n  1  0)  =  (f  n  1  0)
4.  m  :  \mBbbN{}@i
5.  \mforall{}k:\mBbbN{}.  ((1  =  fib(k))  {}\mRightarrow{}  ((k  \mleq{}  0)  {}\mRightarrow{}  (0  \mmember{}  \mBbbZ{}))  {}\mRightarrow{}  (0  <  k  {}\mRightarrow{}  (0  =  fib(k  -  1)))  {}\mRightarrow{}  (m  =  fib(n  +  k)))
\mvdash{}  m  =  fib(n)


By

---

Latex:
(InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index