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 : callbyvalue: callbyvalue, le_int: i ≤z j, 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: 2018_05_21-PM-01_02_07 Last ObjectModification: 2018_01_28-PM-02_12_31 Theory : num_thy_1 Home Index