Nuprl Definition : exp-ratio

exp-ratio(a;b;n;p;q)

==r if p <z q then n else eval n' = n + 1 in eval p' = a * p in eval q' = b * q in   exp-ratio(a;b;n';p';q') fi

exp-ratio(a;b;n;p;q) ==
  fix((λexp-ratio,n,p,q. if p <z q
                        then n
                        else eval n' = n + 1 in
                             eval p' = a * p in
                             eval q' = b * q in
                               exp-ratio n' p' q'
                        fi ))
  n
  p
  q

Definitions occuring in Statement : callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , lt_int: i <z j, 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 , lt_int: i <z j, add: n + m, natural_number: $n, callbyvalue: callbyvalue, multiply: n * m, apply: f a
FDL editor aliases : exp-ratio

Latex:
exp-ratio(a;b;n;p;q) ==r if p <z q then n else eval n' = n + 1 in eval p' = a * p in eval q' = b * q in exp-ratio(a;b;n';p';q') fi

Latex:
exp-ratio(a;b;n;p;q) == fix((\mlambda{}exp-ratio,n,p,q. if p <z q then n else eval n' = n + 1 in eval p' = a * p in eval q' = b * q in exp-ratio n' p' q' fi )) n p q Date html generated: 2018_05_21-PM-01_02_47 Last ObjectModification: 2018_01_28-PM-02_12_45 Theory : num_thy_1 Home Index