Nuprl Definition : aa_3n_plus_1_depth_pi
aa_3n_plus_1_depth_pi(m) ==
  fix((
f,n. if (n =
 1) then <0, 0>
            if (n rem 2 =
 0) then <1 + (fst((f (n 
 2)))), 1 + (snd((f (n 
 2))))>
            else <fst((f (1 + (3 * n)))), 1 + (snd((f (1 + (3 * n)))))>
            fi )) 
  m
Definitions occuring in Statement : 
eq_int: (i =
 j), 
ifthenelse: if b then t else f fi , 
pi1: fst(t), 
pi2: snd(t), 
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_depth_pi
aa\_3n\_plus\_1\_depth\_pi(m)  ==
    fix((\mlambda{}f,n.  if  (n  =\msubz{}  1)  then  ɘ,  0>
                        if  (n  rem  2  =\msubz{}  0)  then  ə  +  (fst((f  (n  \mdiv{}  2)))),  1  +  (snd((f  (n  \mdiv{}  2))))>
                        else  <fst((f  (1  +  (3  *  n)))),  1  +  (snd((f  (1  +  (3  *  n)))))>
                        fi  )) 
    m
Date html generated:
2013_03_20-AM-09_55_26
Last ObjectModification:
2012_11_27-AM-10_33_37
Home
Index