Nuprl Definition : p-inv

p-inv(p;a) ==
  λn.eval pn = p^n in
     eval an = a n in
       let x,y = letrec rec(p)=λq.if p=0
                                  then <q, 0, 1, 1, 1, Ax, Ax, Ax>
                                  else let x,y = divrem(q; p) 
                                       in eval r = y in
                                          let g,t = rec r p 
                                          in let a,b,x1,y1,_,_,_@0 = t in 
                                              eval q' = x in
                                              eval b' = (b * q') + a in
                                              eval x' = y1 - x1 * q' in
                                                <g, b, b', x', x1, Ax, Ax, Ax> in
                  rec(|a n|) 
                 pn 
       in let x1,x2,x3,x4,x5,x5,y = y in 
           eval r = 1 * x3 rem pn in
           if (r) < (0)  then pn + r  else r


Definitions occuring in Statement :  exp: i^n,  genrec-ap: genrec-ap,  absval: |i|,  callbyvalue: callbyvalue,  spreadn: spread7,  less: if (a) < (b)  then c  else d,  int_eq: if a=b then c else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  remainder: n rem m,  divrem: divrem(n; m),  multiply: n * m,  subtract: n - m,  add: n + m,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  exp: i^n,  genrec-ap: genrec-ap,  lambda: λx.A[x],  int_eq: if a=b then c else d,  divrem: divrem(n; m),  spread: spread def,  subtract: n - m,  pair: <a, b>,  axiom: Ax,  absval: |i|,  apply: f a,  spreadn: spread7,  callbyvalue: callbyvalue,  remainder: n rem m,  multiply: n * m,  less: if (a) < (b)  then c  else d,  natural_number: $n,  add: n + m
FDL editor aliases :  p-inv
Latex:
p-inv(p;a)  ==
    \mlambda{}n.eval  pn  =  p\^{}n  in
          eval  an  =  a  n  in
              let  x,y  =  letrec  rec(p)=\mlambda{}q.if  p=0
                                                                    then  <q,  0,  1,  1,  1,  Ax,  Ax,  Ax>
                                                                    else  let  x,y  =  divrem(q;  p) 
                                                                              in  eval  r  =  y  in
                                                                                    let  g,t  =  rec  r  p 
                                                                                    in  let  a,b,x1,y1,$_{}$,$_{\000C}$,$_{@0}$  =  t  in 
                                                                                            eval  q'  =  x  in
                                                                                            eval  b'  =  (b  *  q')  +  a  in
                                                                                            eval  x'  =  y1  -  x1  *  q'  in
                                                                                                <g,  b,  b',  x',  x1,  Ax,  Ax,  Ax>  in
                                    rec(|a  n|) 
                                  pn 
              in  let  x1,x2,x3,x4,x5,x5,y  =  y  in 
                      eval  r  =  1  *  x3  rem  pn  in
                      if  (r)  <  (0)    then  pn  +  r    else  r


Date html generated: 2019_10_15-AM-10_34_52
Last ObjectModification: 2019_06_24-PM-00_54_55

Theory : rings_1


Home Index