Nuprl Definition : genfact-inv

genfact-inv(N;b;m.f[m]) ==
  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


Definitions occuring in Statement :  genrec-ap: genrec-ap,  callbyvalue: callbyvalue,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  genrec-ap: genrec-ap,  lambda: λx.A[x],  less: if (a) < (b)  then c  else d,  add: n + m,  callbyvalue: callbyvalue,  multiply: n * m,  apply: f a,  natural_number: $n
FDL editor aliases :  genfact-inv
Latex:
genfact-inv(N;b;m.f[m])  ==
    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


Date html generated: 2019_06_20-PM-02_25_57
Last ObjectModification: 2019_02_11-PM-00_12_56

Theory : num_thy_1


Home Index