Nuprl Definition : find-xover-print

find-xover-print(f;m;n;step) ==
  fix((λfind-xover,m,n,step. eval s = evalall(nat-to-str(n)) in
                             print_line(s;
                                        if f n
                                        then <n, m>
                                        else eval step' = 2 * step in
                                             eval k = n + step in
                                               find-xover n k step'
                                        fi ))) 
  m 
  n 
  step


Definitions occuring in Statement :  nat-to-str: nat-to-str(n),  evalall: evalall(t),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  evalall: evalall(t),  nat-to-str: nat-to-str(n),  ifthenelse: if b then t else f fi ,  pair: <a, b>,  multiply: n * m,  natural_number: $n,  callbyvalue: callbyvalue,  add: n + m,  apply: f a
FDL editor aliases :  find-xover-print
Latex:
find-xover-print(f;m;n;step)  ==
    fix((\mlambda{}find-xover,m,n,step.  eval  s  =  evalall(nat-to-str(n))  in
                                                          print\_line(s;
                                                                                if  f  n
                                                                                then  <n,  m>
                                                                                else  eval  step'  =  2  *  step  in
                                                                                          eval  k  =  n  +  step  in
                                                                                              find-xover  n  k  step'
                                                                                fi  ))) 
    m 
    n 
    step


Date html generated: 2016_05_14-PM-03_36_05
Last ObjectModification: 2015_09_22-PM-06_01_21

Theory : decidable!equality


Home Index