Nuprl Definition : gcd-reduce-eq-constraints

Each equality constraint is a list [c,a1,a2,...] and represents the
constraint  c + a1*v1 + a2*v2 + ....  = 0 (on variables v1, v2, ...).
If g = gcd(a1,a2,...) is greater than 1, then if c is not divisible by g
then the constraint is unsatisfiable.
Otherwise we can divide c and all the a1,a2,... by g and preserve
satisfiability.⋅
gcd-reduce-eq-constraints(sat;LL) ==
  accumulate_abort(L,Ls.let h,t = L 
                        in if t = Ax then if h=0  then inl [L / Ls]  else (inr ⋅ )
                           otherwise eval g = |gcd-list(t)| in
                                     if (1) < (g)
                                        then if h rem g=0
                                                then eval L' = eager-map(λx.(x ÷ g);L) in
                                                     inl [L' / Ls]
                                                else (inr ⋅ )
                                        else (inl [L / Ls]);inl sat;LL)


Definitions occuring in Statement :  gcd-list: gcd-list(L),  accumulate_abort: accumulate_abort(x,sofar.F[x; sofar];s;L),  eager-map: eager-map(f;as),  cons: [a / b],  absval: |i|,  callbyvalue: callbyvalue,  it: ⋅,  isaxiom: if z = Ax then a otherwise b,  less: if (a) < (b)  then c  else d,  int_eq: if a=b  then c  else d,  lambda: λx.A[x],  spread: spread def,  inr: inr x ,  inl: inl x,  remainder: n rem m,  divide: n ÷ m,  natural_number: $n
Definitions occuring in definition :  accumulate_abort: accumulate_abort(x,sofar.F[x; sofar];s;L),  spread: spread def,  isaxiom: if z = Ax then a otherwise b,  absval: |i|,  gcd-list: gcd-list(L),  less: if (a) < (b)  then c  else d,  int_eq: if a=b  then c  else d,  remainder: n rem m,  natural_number: $n,  callbyvalue: callbyvalue,  eager-map: eager-map(f;as),  lambda: λx.A[x],  divide: n ÷ m,  inr: inr x ,  it: ⋅,  cons: [a / b],  inl: inl x
FDL editor aliases :  gcd-reduce-eq-constraints
Latex:
gcd-reduce-eq-constraints(sat;LL)  ==
    accumulate\_abort(L,Ls.let  h,t  =  L 
                                                in  if  t  =  Ax  then  if  h=0    then  inl  [L  /  Ls]    else  (inr  \mcdot{}  )
                                                      otherwise  eval  g  =  |gcd-list(t)|  in
                                                                          if  (1)  <  (g)
                                                                                then  if  h  rem  g=0
                                                                                                then  eval  L'  =  eager-map(\mlambda{}x.(x  \mdiv{}  g);L)  in
                                                                                                          inl  [L'  /  Ls]
                                                                                                else  (inr  \mcdot{}  )
                                                                                else  (inl  [L  /  Ls]);inl  sat;LL)


Date html generated: 2016_07_08-PM-04_48_10
Last ObjectModification: 2015_12_14-PM-06_31_26

Theory : omega


Home Index