---

Step * of Lemma fast-fib-ext

∀n:ℕ. (∃m:{ℕ| (m = fib(n) ∈ ℕ)})
BY
{ Extract of Obid: fast-fib
  normalizes to:
  
  λn.(letrec rec(n)=λa,b. if n=0  then b  else eval s = a + b in eval n' = n - 1 in   rec n' s a in rec(n) 1 1)
  
  not unfolding  
  finishing with Auto }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  fast-fib
normalizes  to:

\mlambda{}n.(letrec  rec(n)=\mlambda{}a,b.  if  n=0    then  b    else  eval  s  =  a  +  b  in  eval  n'  =  n  -  1  in      rec  n'  s  a  in
          rec(n) 
        1 
        1)

not  unfolding   
finishing  with  Auto

---

Home Index