### Nuprl Definition : regularize

regularize(k;f) ==
λn.if regular-upto(k;n;f)
then n
else eval mu(λn.(¬bregular-upto(k;n;f))) in
eval seq-min-upper(k;m;f) in
((n ((f j) (2 k))) ÷ k)
fi

Definitions occuring in Statement :  seq-min-upper: seq-min-upper(k;n;f) regular-upto: regular-upto(k;n;f) mu: mu(f) callbyvalue: callbyvalue bnot: ¬bb ifthenelse: if then else fi  apply: a lambda: λx.A[x] divide: n ÷ m multiply: m subtract: m add: m natural_number: \$n
Definitions occuring in definition :  multiply: m natural_number: \$n apply: a add: m divide: n ÷ m seq-min-upper: seq-min-upper(k;n;f) callbyvalue: callbyvalue regular-upto: regular-upto(k;n;f) bnot: ¬bb lambda: λx.A[x] mu: mu(f) subtract: m ifthenelse: if then else fi
FDL editor aliases :  regularize

Latex:
regularize(k;f)  ==
\mlambda{}n.if  regular-upto(k;n;f)
then  f  n
else  eval  m  =  mu(\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f)))  -  1  in
eval  j  =  seq-min-upper(k;m;f)  in
k  *  ((n  *  ((f  j)  +  (2  *  k)))  \mdiv{}  j  *  k)
fi

Date html generated: 2017_10_03-AM-09_07_15
Last ObjectModification: 2017_09_11-PM-04_11_19

Theory : reals

Home Index