Nuprl Definition : expfact

expfact(n;x;p;b)
==r if p ≤then else eval n' in eval p' in eval b' n' in   expfact(n';x;p';b') fi 

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



Definitions occuring in Statement :  callbyvalue: callbyvalue le_int: i ≤j ifthenelse: if then else fi  apply: a fix: fix(F) lambda: λx.A[x] multiply: m add: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] ifthenelse: if then else fi  le_int: i ≤j add: m natural_number: $n callbyvalue: callbyvalue multiply: m apply: 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: 2018_05_21-PM-01_02_07
Last ObjectModification: 2018_01_28-PM-02_12_31

Theory : num_thy_1


Home Index