---

Step * of Lemma genfact-unbounded-ext

∀f:ℕ+ ⟶ ℤ. ∀b:ℕ+. ∀N:ℤ.  (∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]) supposing ∀m:ℕ+. 1 < f[m]
BY
{ Extract of Obid: genfact-unbounded
  not unfolding  recdefs
  finishing with Auto
  normalizes to:
  
  λf,b,N. eval M = N in
          letrec g(k)=λx.if (x) < (M)  then eval k' = k + 1 in eval z = f k' in eval x' = z * x in   g k' x'  else k in
           g(0) 
          b }

---

Latex:

---

Latex:
\mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b:\mBbbN{}\msupplus{}.  \mforall{}N:\mBbbZ{}.    (\mexists{}n:\mBbbN{}  [(N  \mleq{}  genfact(n;b;m.f[m]))])  supposing  \mforall{}m:\mBbbN{}\msupplus{}.  1  <  f[m]


By

---

Latex:
Extract  of  Obid:  genfact-unbounded
not  unfolding    recdefs
finishing  with  Auto
normalizes  to:

\mlambda{}f,b,N.  eval  M  =  N  in
                letrec  g(k)=\mlambda{}x.if  (x)  <  (M)
                                                    then  eval  k'  =  k  +  1  in
                                                              eval  z  =  f  k'  in
                                                              eval  x'  =  z  *  x  in
                                                                  g  k'  x'
                                                    else  k  in
                  g(0) 
                b

---

Home Index