Nuprl Definition : cubic_converge2

cubic_converge2(a;b;k;m)
==r if a * m ≤z b
    then 0
    else if m=2  then k  else eval r = iroot(3;m) + 1 in eval n = cubic_converge2(a;b;k;r) in   n + 1
    fi 
cubic_converge2(a;b;k;m) ==
  fix((λcubic_converge2,m. if a * m ≤z b
                          then 0
                          else if m=2  then k  else eval r = iroot(3;m) + 1 in eval n = cubic_converge2 r in   n + 1
                          fi )) 
  m


Definitions occuring in Statement :  le_int: i ≤z j,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n,  iroot: iroot(n;x)
Definitions occuring in definition :  natural_number: $n,  add: n + m,  apply: f a,  callbyvalue: callbyvalue,  iroot: iroot(n;x),  int_eq: if a=b  then c  else d,  multiply: n * m,  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  fix: fix(F)
FDL editor aliases :  cubic_converge2
Latex:
cubic\_converge2(a;b;k;m)
==r  if  a  *  m  \mleq{}z  b
        then  0
        else  if  m=2
                        then  k
                        else  eval  r  =  iroot(3;m)  +  1  in
                                  eval  n  =  cubic\_converge2(a;b;k;r)  in
                                      n  +  1
        fi 

Latex:
cubic\_converge2(a;b;k;m)  ==
    fix((\mlambda{}cubic$_{converge2}$,m.  if  a  *  m  \mleq{}z  b
                                                  then  0
                                                  else  if  m=2
                                                                  then  k
                                                                  else  eval  r  =  iroot(3;m)  +  1  in
                                                                            eval  n  =  cubic$_{converge2}$  r  in
                                                                                n  +  1
                                                  fi  )) 
    m


Date html generated: 2016_10_26-PM-00_22_21
Last ObjectModification: 2016_10_10-PM-04_02_09

Theory : reals_2


Home Index