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