Nuprl Definition : factorit

factorit(x;b;tried;facs) ==
  fix((λfactorit,x,b,tried,facs. if x <z b * b then if x <z 2 then facs else [x / facs] fi 
                                if (∃p∈tried.(b rem p =z 0))_b then eval b' = b + 1 in factorit x b' tried facs
                                if (x rem b =z 0) then eval x' = x ÷ b in factorit x' b tried [b / facs]
                                else eval b' = b + 1 in
                                     factorit x b' [b / tried] facs
                                fi )) 
  x 
  b 
  tried 
  facs


Definitions occuring in Statement :  bl-exists: (∃x∈L.P[x])_b,  cons: [a / b],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  remainder: n rem m,  divide: n ÷ m,  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  lt_int: i <z j,  bl-exists: (∃x∈L.P[x])_b,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  remainder: n rem m,  divide: n ÷ m,  callbyvalue: callbyvalue,  add: n + m,  natural_number: $n,  apply: f a,  cons: [a / b]
FDL editor aliases :  factorit
Latex:
factorit(x;b;tried;facs)  ==
    fix((\mlambda{}factorit,x,b,tried,facs.  if  x  <z  b  *  b  then  if  x  <z  2  then  facs  else  [x  /  facs]  fi 
                                                                if  (\mexists{}p\mmember{}tried.(b  rem  p  =\msubz{}  0))\_b
                                                                    then  eval  b'  =  b  +  1  in
                                                                              factorit  x  b'  tried  facs
                                                                if  (x  rem  b  =\msubz{}  0)
                                                                    then  eval  x'  =  x  \mdiv{}  b  in
                                                                              factorit  x'  b  tried  [b  /  facs]
                                                                else  eval  b'  =  b  +  1  in
                                                                          factorit  x  b'  [b  /  tried]  facs
                                                                fi  )) 
    x 
    b 
    tried 
    facs


Date html generated: 2016_05_15-PM-04_00_34
Last ObjectModification: 2015_09_23-AM-07_45_56

Theory : general


Home Index