Nuprl Definition : bpa-norm

bpa-norm(p;x) ==
  let n,a = x 
  in if (n =z 0) then <0, a>
     if (a n =z 0) then <0, p-shift(p;a;n)>
     else let k,b = p-unitize(p;a;n) 
          in <n - k, b>
     fi 


Definitions occuring in Statement :  p-unitize: p-unitize(p;a;n),  p-shift: p-shift(p;a;k),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  spread: spread def,  pair: <a, b>,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  natural_number: $n,  p-shift: p-shift(p;a;k),  spread: spread def,  p-unitize: p-unitize(p;a;n),  pair: <a, b>,  subtract: n - m
FDL editor aliases :  bpa-norm
Latex:
bpa-norm(p;x)  ==
    let  n,a  =  x 
    in  if  (n  =\msubz{}  0)  then  ɘ,  a>
          if  (a  n  =\msubz{}  0)  then  ɘ,  p-shift(p;a;n)>
          else  let  k,b  =  p-unitize(p;a;n) 
                    in  <n  -  k,  b>
          fi 


Date html generated: 2018_05_21-PM-03_25_09
Last ObjectModification: 2018_02_01-PM-07_14_31

Theory : rings_1


Home Index