Nuprl Definition : rinv

rinv(x) ==
  eval n = mu-ge(λn.eval k = x n in
                    4 <z |k|;1) in
  if (n =z 1)
  then accelerate(5;reg-seq-inv(x))
  else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;x)))
  fi 


Definitions occuring in Statement :  reg-seq-adjust: reg-seq-adjust(n;x),  reg-seq-inv: reg-seq-inv(x),  accelerate: accelerate(k;f),  mu-ge: mu-ge(f;n),  absval: |i|,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  mu-ge: mu-ge(f;n),  lambda: λx.A[x],  callbyvalue: callbyvalue,  apply: f a,  lt_int: i <z j,  absval: |i|,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  accelerate: accelerate(k;f),  add: n + m,  multiply: n * m,  natural_number: $n,  reg-seq-inv: reg-seq-inv(x),  reg-seq-adjust: reg-seq-adjust(n;x)
FDL editor aliases :  rinv rinv
Latex:
rinv(x)  ==
    eval  n  =  mu-ge(\mlambda{}n.eval  k  =  x  n  in
                                        4  <z  |k|;1)  in
    if  (n  =\msubz{}  1)
    then  accelerate(5;reg-seq-inv(x))
    else  accelerate(4  *  ((4  *  n  *  n)  +  1);reg-seq-inv(reg-seq-adjust(n;x)))
    fi 


Date html generated: 2016_05_18-AM-06_53_58
Last ObjectModification: 2015_09_23-AM-09_00_50

Theory : reals


Home Index