Nuprl Definition : aa_3n_plus_1_ctr

aa_3n_plus_1_ctr(m) ==
  fix((f,n. if (n = 1) then <0, 0>
            if (n rem 2 = 0) then aa_capply(f (n  2);t.(1 + t))
            else aa_capply(f (1 + (3 * n));t.t)
            fi )) 
  m


Definitions occuring in Statement :  aa_capply: aa_capply(p;l),  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: x.A[x],  pair: <a, b>,  remainder: n rem m,  divide: n  m,  multiply: n * m,  add: n + m,  natural_number: $n
FDL editor aliases :  aa_3n_plus_1_ctr
aa\_3n\_plus\_1\_ctr(m)  ==
    fix((\mlambda{}f,n.  if  (n  =\msubz{}  1)  then  ɘ,  0>
                        if  (n  rem  2  =\msubz{}  0)  then  aa\_capply(f  (n  \mdiv{}  2);\mlambda{}t.(1  +  t))
                        else  aa\_capply(f  (1  +  (3  *  n));\mlambda{}t.t)
                        fi  )) 
    m


Date html generated: 2013_03_20-AM-09_57_14
Last ObjectModification: 2012_11_27-AM-10_33_48

Home Index