---

Step * of Lemma less-fast-fib-ext

∀n:ℕ. {m:ℕ| m = fib(n) ∈ ℕ} 
BY
{ Extract of Obid: less-fast-fib
  not unfolding  primrec
  finishing with Auto
  normalizes to:
  
  λn.(primrec(n;λa,b. a;λi,x,a,b. (x (a + b) a)) 1 0)
THEN skip{The extract, slowfib(n), takes 4n+7+fib(n+1) steps to compute fib(n).} }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \{m:\mBbbN{}|  m  =  fib(n)\} 


By

---

Latex:
Extract  of  Obid:  less-fast-fib
not  unfolding    primrec
finishing  with  Auto
normalizes  to:

\mlambda{}n.(primrec(n;\mlambda{}a,b.  a;\mlambda{}i,x,a,b.  (x  (a  +  b)  a))  1  0)
THEN  skip\{The  extract,  slowfib(n),  takes  4n+7+fib(n+1)  steps  to  compute  fib(n).\}

---

Home Index