Nuprl Definition : expfact

expfact(n;x;p;b)
==r if p ≤z b then n else eval n' = n + 1 in eval p' = x * p in eval b' = n' * b in   expfact(n';x;p';b') fi 
expfact(n;x;p;b) ==
  fix((λexpfact,n,p,b. if p ≤z b
                      then n
                      else eval n' = n + 1 in
                           eval p' = x * p in
                           eval b' = n' * b in
                             expfact n' p' b'
                      fi )) 
  n 
  p 
  b


Definitions occuring in Statement :  le_int: i ≤z j,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  le_int: i ≤z j,  add: n + m,  natural_number: $n,  callbyvalue: callbyvalue,  multiply: n * m,  apply: f a
FDL editor aliases :  expfact
Latex:
expfact(n;x;p;b)
==r  if  p  \mleq{}z  b
        then  n
        else  eval  n'  =  n  +  1  in
                  eval  p'  =  x  *  p  in
                  eval  b'  =  n'  *  b  in
                      expfact(n';x;p';b')
        fi 

Latex:
expfact(n;x;p;b)  ==
    fix((\mlambda{}expfact,n,p,b.  if  p  \mleq{}z  b
                                            then  n
                                            else  eval  n'  =  n  +  1  in
                                                      eval  p'  =  x  *  p  in
                                                      eval  b'  =  n'  *  b  in
                                                          expfact  n'  p'  b'
                                            fi  )) 
    n 
    p 
    b


Date html generated: 2016_05_15-PM-04_06_39
Last ObjectModification: 2015_09_23-AM-07_46_33

Theory : general


Home Index