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