Nuprl Definition : pa-inv

pa-inv(p;x) ==
  let n,a = x 
  in if (n =z 0)
     then eval k = mu(λi.(¬b(a (i + 1) =z 0))) in
          let j,b = p-unitize(p;a;k + 1) 
          in <j, p-inv(p;b)>
     else <0, p^n(p) * p-inv(p;a)>
     fi 


Definitions occuring in Statement :  p-unitize: p-unitize(p;a;n),  p-inv: p-inv(p;a),  p-int: k(p),  p-mul: x * y,  fastexp: i^n,  mu: mu(f),  callbyvalue: callbyvalue,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  callbyvalue: callbyvalue,  mu: mu(f),  lambda: λx.A[x],  bnot: ¬bb,  eq_int: (i =z j),  apply: f a,  spread: spread def,  p-unitize: p-unitize(p;a;n),  add: n + m,  pair: <a, b>,  natural_number: $n,  p-mul: x * y,  p-int: k(p),  fastexp: i^n,  p-inv: p-inv(p;a)
FDL editor aliases :  pa-inv
Latex:
pa-inv(p;x)  ==
    let  n,a  =  x 
    in  if  (n  =\msubz{}  0)
          then  eval  k  =  mu(\mlambda{}i.(\mneg{}\msubb{}(a  (i  +  1)  =\msubz{}  0)))  in
                    let  j,b  =  p-unitize(p;a;k  +  1) 
                    in  <j,  p-inv(p;b)>
          else  ɘ,  p\^{}n(p)  *  p-inv(p;a)>
          fi 


Date html generated: 2018_05_21-PM-03_28_41
Last ObjectModification: 2018_02_05-AM-11_17_07

Theory : rings_1


Home Index