---

Step * of Lemma fast-fib

∀n:ℕ. (∃m:ℕ [(m = fib(n) ∈ ℕ)])
BY
{ xxxAssert ⌜∀n:ℕ. ∀a,b:ℤ.
               (∃c:ℤ [(∀m:ℕ
                         ((a = fib(m + 1) ∈ ℤ)
                         ⇒ (b = fib(m) ∈ ℤ)
                         ⇒ (c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ)))])⌝
⋅xxx }

1
.....assertion..... 
∀n:ℕ. ∀a,b:ℤ.
  (∃c:ℤ [(∀m:ℕ. ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ)))])

2
1. ∀n:ℕ. ∀a,b:ℤ.
     (∃c:ℤ [(∀m:ℕ. ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ)))])
⊢ ∀n:ℕ. (∃m:ℕ [(m = fib(n) ∈ ℕ)])

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}m:\mBbbN{}  [(m  =  fib(n))])


By

---

Latex:
xxxAssert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbZ{}.
                          (\mexists{}c:\mBbbZ{}  [(\mforall{}m:\mBbbN{}
                                              ((a  =  fib(m  +  1))
                                              {}\mRightarrow{}  (b  =  fib(m))
                                              {}\mRightarrow{}  (c  =  if  0  \mleq{}z  n  then  fib(n  +  m)  else  fib(m)  fi  )))])\mkleeneclose{}
\mcdot{}xxx

---

Home Index