Nuprl Definition : chrem

chrem(a;r;b;s) ==
  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,%13 = rec r p 
                                     in let a,b,x1,y1,%18,%20,%21 = %13 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(|r|) 
            |s| 
  in let x1,x2,x3,x4,x5,x5,y = y in 
      if x=0
      then if a=b then inl a else (inr (λx.Ax) )
      else let x4,r1 = divrem(b - a; x) 
           in if r1=0
              then eval z = a + if (r) < (0)  then ((-1) * x3) * x4 * r  else ((1 * x3) * x4 * r) in
                   inl z
              else (inr (λx.Ax) )


Definitions occuring in Statement :  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>,  inr: inr x ,  inl: inl x,  divrem: divrem(n; m),  multiply: n * m,  subtract: n - m,  add: n + m,  minus: -n,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  genrec-ap: genrec-ap,  apply: f a,  pair: <a, b>,  absval: |i|,  spreadn: spread7,  spread: spread def,  divrem: divrem(n; m),  subtract: n - m,  int_eq: if a=b then c else d,  callbyvalue: callbyvalue,  add: n + m,  less: if (a) < (b)  then c  else d,  minus: -n,  natural_number: $n,  multiply: n * m,  inl: inl x,  inr: inr x ,  lambda: λx.A[x],  axiom: Ax
FDL editor aliases :  chrem
Latex:
chrem(a;r;b;s)  ==
    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,\%13  =  rec  r  p 
                                                                          in  let  a,b,x1,y1,\%18,\%20,\%21  =  \%13  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(|r|) 
                        |s| 
    in  let  x1,x2,x3,x4,x5,x5,y  =  y  in 
            if  x=0
            then  if  a=b  then  inl  a  else  (inr  (\mlambda{}x.Ax)  )
            else  let  x4,r1  =  divrem(b  -  a;  x) 
                      in  if  r1=0
                            then  eval  z  =  a  +  if  (r)  <  (0)    then  ((-1)  *  x3)  *  x4  *  r    else  ((1  *  x3)  *  x4  *  r)  in
                                      inl  z
                            else  (inr  (\mlambda{}x.Ax)  )


Date html generated: 2020_05_20-AM-08_13_33
Last ObjectModification: 2019_11_27-PM-03_14_48

Theory : general


Home Index