src/HOL/Integ/reflected_presburger.ML
author chaieb
Wed Sep 14 17:25:52 2005 +0200 (2005-09-14)
changeset 17378 105519771c67
child 17390 df2b53a66937
permissions -rw-r--r--
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
comm_ring : a reflected Method for proving equalities in a commutative ring
     1 (* $Id$ *)
     2 
     3     (* Caution: This file should not be modified. *)
     4     (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
     5 fun nat i = if i < 0 then 0 else i;
     6 structure Generated =
     7 struct
     8 
     9 datatype intterm = Cst of int | Var of int | Neg of intterm
    10   | Add of intterm * intterm | Sub of intterm * intterm
    11   | Mult of intterm * intterm;
    12 
    13 datatype QF = Lt of intterm * intterm | Gt of intterm * intterm
    14   | Le of intterm * intterm | Ge of intterm * intterm | Eq of intterm * intterm
    15   | Divides of intterm * intterm | T | F | NOT of QF | And of QF * QF
    16   | Or of QF * QF | Imp of QF * QF | Equ of QF * QF | QAll of QF | QEx of QF;
    17 
    18 datatype 'a option = None | Some of 'a;
    19 
    20 fun lift_un c None = None
    21   | lift_un c (Some p) = Some (c p);
    22 
    23 fun lift_bin (c, (Some a, Some b)) = Some (c a b)
    24   | lift_bin (c, (None, y)) = None
    25   | lift_bin (c, (Some y, None)) = None;
    26 
    27 fun lift_qe qe None = None
    28   | lift_qe qe (Some p) = qe p;
    29 
    30 fun qelim (qe, QAll p) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe, p))))
    31   | qelim (qe, QEx p) = lift_qe qe (qelim (qe, p))
    32   | qelim (qe, And (p, q)) =
    33     lift_bin ((fn x => fn xa => And (x, xa)), (qelim (qe, p), qelim (qe, q)))
    34   | qelim (qe, Or (p, q)) =
    35     lift_bin ((fn x => fn xa => Or (x, xa)), (qelim (qe, p), qelim (qe, q)))
    36   | qelim (qe, Imp (p, q)) =
    37     lift_bin ((fn x => fn xa => Imp (x, xa)), (qelim (qe, p), qelim (qe, q)))
    38   | qelim (qe, Equ (p, q)) =
    39     lift_bin ((fn x => fn xa => Equ (x, xa)), (qelim (qe, p), qelim (qe, q)))
    40   | qelim (qe, NOT p) = lift_un NOT (qelim (qe, p))
    41   | qelim (qe, Lt (w, x)) = Some (Lt (w, x))
    42   | qelim (qe, Gt (y, z)) = Some (Gt (y, z))
    43   | qelim (qe, Le (aa, ab)) = Some (Le (aa, ab))
    44   | qelim (qe, Ge (ac, ad)) = Some (Ge (ac, ad))
    45   | qelim (qe, Eq (ae, af)) = Some (Eq (ae, af))
    46   | qelim (qe, Divides (ag, ah)) = Some (Divides (ag, ah))
    47   | qelim (qe, T) = Some T
    48   | qelim (qe, F) = Some F;
    49 
    50 fun lin_mul (c, Cst i) = Cst (c * i)
    51   | lin_mul (c, Add (Mult (Cst c', Var n), r)) =
    52     (if (c = 0) then Cst 0
    53       else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
    54 
    55 fun op_60_def0 m n = ((m) < (n));
    56 
    57 fun op_60_61_def0 m n = not (op_60_def0 n m);
    58 
    59 fun lin_add (Add (Mult (Cst c1, Var n1), r1), Add (Mult (Cst c2, Var n2), r2)) =
    60     (if (n1 = n2)
    61       then let val c = Cst (c1 + c2)
    62            in (if ((c1 + c2) = 0) then lin_add (r1, r2)
    63                 else Add (Mult (c, Var n1), lin_add (r1, r2)))
    64            end
    65       else (if op_60_61_def0 n1 n2
    66              then Add (Mult (Cst c1, Var n1),
    67                         lin_add (r1, Add (Mult (Cst c2, Var n2), r2)))
    68              else Add (Mult (Cst c2, Var n2),
    69                         lin_add (Add (Mult (Cst c1, Var n1), r1), r2))))
    70   | lin_add (Add (Mult (Cst c1, Var n1), r1), Cst b) =
    71     Add (Mult (Cst c1, Var n1), lin_add (r1, Cst b))
    72   | lin_add (Cst x, Add (Mult (Cst c2, Var n2), r2)) =
    73     Add (Mult (Cst c2, Var n2), lin_add (Cst x, r2))
    74   | lin_add (Cst b1, Cst b2) = Cst (b1 + b2);
    75 
    76 fun lin_neg i = lin_mul (~1, i);
    77 
    78 fun linearize (Cst b) = Some (Cst b)
    79   | linearize (Var n) = Some (Add (Mult (Cst 1, Var n), Cst 0))
    80   | linearize (Neg i) = lift_un lin_neg (linearize i)
    81   | linearize (Add (i, j)) =
    82     lift_bin ((fn x => fn y => lin_add (x, y)), (linearize i, linearize j))
    83   | linearize (Sub (i, j)) =
    84     lift_bin
    85       ((fn x => fn y => lin_add (x, lin_neg y)), (linearize i, linearize j))
    86   | linearize (Mult (i, j)) =
    87     (case linearize i of None => None
    88       | Some x =>
    89           (case x of
    90             Cst xa =>
    91               (case linearize j of None => None
    92                 | Some x => Some (lin_mul (xa, x)))
    93             | Var xa =>
    94                 (case linearize j of None => None
    95                   | Some xa =>
    96                       (case xa of Cst xa => Some (lin_mul (xa, x))
    97                         | Var xa => None | Neg xa => None | Add (xa, xb) => None
    98                         | Sub (xa, xb) => None | Mult (xa, xb) => None))
    99             | Neg xa =>
   100                 (case linearize j of None => None
   101                   | Some xa =>
   102                       (case xa of Cst xa => Some (lin_mul (xa, x))
   103                         | Var xa => None | Neg xa => None | Add (xa, xb) => None
   104                         | Sub (xa, xb) => None | Mult (xa, xb) => None))
   105             | Add (xa, xb) =>
   106                 (case linearize j of None => None
   107                   | Some xa =>
   108                       (case xa of Cst xa => Some (lin_mul (xa, x))
   109                         | Var xa => None | Neg xa => None | Add (xa, xb) => None
   110                         | Sub (xa, xb) => None | Mult (xa, xb) => None))
   111             | Sub (xa, xb) =>
   112                 (case linearize j of None => None
   113                   | Some xa =>
   114                       (case xa of Cst xa => Some (lin_mul (xa, x))
   115                         | Var xa => None | Neg xa => None | Add (xa, xb) => None
   116                         | Sub (xa, xb) => None | Mult (xa, xb) => None))
   117             | Mult (xa, xb) =>
   118                 (case linearize j of None => None
   119                   | Some xa =>
   120                       (case xa of Cst xa => Some (lin_mul (xa, x))
   121                         | Var xa => None | Neg xa => None | Add (xa, xb) => None
   122                         | Sub (xa, xb) => None | Mult (xa, xb) => None))));
   123 
   124 fun linform (Le (it1, it2)) =
   125     lift_bin
   126       ((fn x => fn y => Le (lin_add (x, lin_neg y), Cst 0)),
   127         (linearize it1, linearize it2))
   128   | linform (Eq (it1, it2)) =
   129     lift_bin
   130       ((fn x => fn y => Eq (lin_add (x, lin_neg y), Cst 0)),
   131         (linearize it1, linearize it2))
   132   | linform (Divides (d, t)) =
   133     (case linearize d of None => None
   134       | Some x =>
   135           (case x of
   136             Cst xa =>
   137               (if (xa = 0) then None
   138                 else (case linearize t of None => None
   139                        | Some xa => Some (Divides (x, xa))))
   140             | Var xa => None | Neg xa => None | Add (xa, xb) => None
   141             | Sub (xa, xb) => None | Mult (xa, xb) => None))
   142   | linform T = Some T
   143   | linform F = Some F
   144   | linform (NOT p) = lift_un NOT (linform p)
   145   | linform (And (p, q)) =
   146     lift_bin ((fn f => fn g => And (f, g)), (linform p, linform q))
   147   | linform (Or (p, q)) =
   148     lift_bin ((fn f => fn g => Or (f, g)), (linform p, linform q));
   149 
   150 fun nnf (Lt (it1, it2)) = Le (Sub (it1, it2), Cst (~ 1))
   151   | nnf (Gt (it1, it2)) = Le (Sub (it2, it1), Cst (~ 1))
   152   | nnf (Le (it1, it2)) = Le (it1, it2)
   153   | nnf (Ge (it1, it2)) = Le (it2, it1)
   154   | nnf (Eq (it1, it2)) = Eq (it2, it1)
   155   | nnf (Divides (d, t)) = Divides (d, t)
   156   | nnf T = T
   157   | nnf F = F
   158   | nnf (And (p, q)) = And (nnf p, nnf q)
   159   | nnf (Or (p, q)) = Or (nnf p, nnf q)
   160   | nnf (Imp (p, q)) = Or (nnf (NOT p), nnf q)
   161   | nnf (Equ (p, q)) = Or (And (nnf p, nnf q), And (nnf (NOT p), nnf (NOT q)))
   162   | nnf (NOT (Lt (it1, it2))) = Le (it2, it1)
   163   | nnf (NOT (Gt (it1, it2))) = Le (it1, it2)
   164   | nnf (NOT (Le (it1, it2))) = Le (Sub (it2, it1), Cst (~ 1))
   165   | nnf (NOT (Ge (it1, it2))) = Le (Sub (it1, it2), Cst (~ 1))
   166   | nnf (NOT (Eq (it1, it2))) = NOT (Eq (it1, it2))
   167   | nnf (NOT (Divides (d, t))) = NOT (Divides (d, t))
   168   | nnf (NOT T) = F
   169   | nnf (NOT F) = T
   170   | nnf (NOT (NOT p)) = nnf p
   171   | nnf (NOT (And (p, q))) = Or (nnf (NOT p), nnf (NOT q))
   172   | nnf (NOT (Or (p, q))) = And (nnf (NOT p), nnf (NOT q))
   173   | nnf (NOT (Imp (p, q))) = And (nnf p, nnf (NOT q))
   174   | nnf (NOT (Equ (p, q))) =
   175     Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
   176 
   177 fun op_45_def2 z w = (z + ~ w);
   178 
   179 fun op_45_def0 m n = nat (op_45_def2 (m) (n));
   180 
   181 val id_1_def0 : int = (0 + 1);
   182 
   183 fun decrvarsI (Cst i) = Cst i
   184   | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
   185   | decrvarsI (Neg a) = Neg (decrvarsI a)
   186   | decrvarsI (Add (a, b)) = Add (decrvarsI a, decrvarsI b)
   187   | decrvarsI (Sub (a, b)) = Sub (decrvarsI a, decrvarsI b)
   188   | decrvarsI (Mult (a, b)) = Mult (decrvarsI a, decrvarsI b);
   189 
   190 fun decrvars (Lt (a, b)) = Lt (decrvarsI a, decrvarsI b)
   191   | decrvars (Gt (a, b)) = Gt (decrvarsI a, decrvarsI b)
   192   | decrvars (Le (a, b)) = Le (decrvarsI a, decrvarsI b)
   193   | decrvars (Ge (a, b)) = Ge (decrvarsI a, decrvarsI b)
   194   | decrvars (Eq (a, b)) = Eq (decrvarsI a, decrvarsI b)
   195   | decrvars (Divides (a, b)) = Divides (decrvarsI a, decrvarsI b)
   196   | decrvars T = T
   197   | decrvars F = F
   198   | decrvars (NOT p) = NOT (decrvars p)
   199   | decrvars (And (p, q)) = And (decrvars p, decrvars q)
   200   | decrvars (Or (p, q)) = Or (decrvars p, decrvars q)
   201   | decrvars (Imp (p, q)) = Imp (decrvars p, decrvars q)
   202   | decrvars (Equ (p, q)) = Equ (decrvars p, decrvars q);
   203 
   204 fun op_64 [] ys = ys
   205   | op_64 (x :: xs) ys = (x :: op_64 xs ys);
   206 
   207 fun map f [] = []
   208   | map f (x :: xs) = (f x :: map f xs);
   209 
   210 fun iupto (i, j) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
   211 
   212 fun all_sums (j, []) = []
   213   | all_sums (j, (i :: is)) =
   214     op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
   215 
   216 fun split x = (fn p => x (fst p) (snd p));
   217 
   218 fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
   219 
   220 fun adjust b =
   221   (fn (q, r) =>
   222     (if (0 <= op_45_def2 r b) then (((2 * q) + 1), op_45_def2 r b)
   223       else ((2 * q), r)));
   224 
   225 fun negDivAlg (a, b) =
   226     (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
   227       else adjust b (negDivAlg (a, (2 * b))));
   228 
   229 fun posDivAlg (a, b) =
   230     (if ((a < b) orelse (b <= 0)) then (0, a)
   231       else adjust b (posDivAlg (a, (2 * b))));
   232 
   233 fun divAlg x =
   234   split (fn a => fn b =>
   235           (if (0 <= a)
   236             then (if (0 <= b) then posDivAlg (a, b)
   237                    else (if (a = 0) then (0, 0)
   238                           else negateSnd (negDivAlg (~ a, ~ b))))
   239             else (if (0 < b) then negDivAlg (a, b)
   240                    else negateSnd (posDivAlg (~ a, ~ b)))))
   241     x;
   242 
   243 fun op_mod_def1 a b = snd (divAlg (a, b));
   244 
   245 fun op_dvd m n = (op_mod_def1 n m = 0);
   246 
   247 fun psimpl (Le (l, r)) =
   248     (case lift_bin
   249             ((fn x => fn y => lin_add (x, lin_neg y)),
   250               (linearize l, linearize r)) of
   251       None => Le (l, r)
   252       | Some x =>
   253           (case x of Cst xa => (if (xa <= 0) then T else F)
   254             | Var xa => Le (x, Cst 0) | Neg xa => Le (x, Cst 0)
   255             | Add (xa, xb) => Le (x, Cst 0) | Sub (xa, xb) => Le (x, Cst 0)
   256             | Mult (xa, xb) => Le (x, Cst 0)))
   257   | psimpl (Eq (l, r)) =
   258     (case lift_bin
   259             ((fn x => fn y => lin_add (x, lin_neg y)),
   260               (linearize l, linearize r)) of
   261       None => Eq (l, r)
   262       | Some x =>
   263           (case x of Cst xa => (if (xa = 0) then T else F)
   264             | Var xa => Eq (x, Cst 0) | Neg xa => Eq (x, Cst 0)
   265             | Add (xa, xb) => Eq (x, Cst 0) | Sub (xa, xb) => Eq (x, Cst 0)
   266             | Mult (xa, xb) => Eq (x, Cst 0)))
   267   | psimpl (Divides (Cst d, t)) =
   268     (case linearize t of None => Divides (Cst d, t)
   269       | Some x =>
   270           (case x of Cst xa => (if op_dvd d xa then T else F)
   271             | Var xa => Divides (Cst d, x) | Neg xa => Divides (Cst d, x)
   272             | Add (xa, xb) => Divides (Cst d, x)
   273             | Sub (xa, xb) => Divides (Cst d, x)
   274             | Mult (xa, xb) => Divides (Cst d, x)))
   275   | psimpl (Equ (p, q)) =
   276     let val p' = psimpl p; val q' = psimpl q
   277     in (case p' of
   278          Lt (x, xa) =>
   279            (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   280              | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   281              | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   282              | T => p' | F => NOT p' | NOT x => Equ (p', q')
   283              | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   284              | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   285              | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   286          | Gt (x, xa) =>
   287              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   288                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   289                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   290                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   291                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   292                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   293                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   294          | Le (x, xa) =>
   295              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   296                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   297                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   298                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   299                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   300                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   301                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   302          | Ge (x, xa) =>
   303              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   304                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   305                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   306                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   307                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   308                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   309                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   310          | Eq (x, xa) =>
   311              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   312                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   313                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   314                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   315                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   316                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   317                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   318          | Divides (x, xa) =>
   319              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   320                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   321                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   322                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   323                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   324                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   325                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   326          | T => q'
   327          | F => (case q' of Lt (x, xa) => NOT q' | Gt (x, xa) => NOT q'
   328                   | Le (x, xa) => NOT q' | Ge (x, xa) => NOT q'
   329                   | Eq (x, xa) => NOT q' | Divides (x, xa) => NOT q' | T => F
   330                   | F => T | NOT x => x | And (x, xa) => NOT q'
   331                   | Or (x, xa) => NOT q' | Imp (x, xa) => NOT q'
   332                   | Equ (x, xa) => NOT q' | QAll x => NOT q' | QEx x => NOT q')
   333          | NOT x =>
   334              (case q' of Lt (xa, xb) => Equ (p', q')
   335                | Gt (xa, xb) => Equ (p', q') | Le (xa, xb) => Equ (p', q')
   336                | Ge (xa, xb) => Equ (p', q') | Eq (xa, xb) => Equ (p', q')
   337                | Divides (xa, xb) => Equ (p', q') | T => p' | F => x
   338                | NOT xa => Equ (x, xa) | And (xa, xb) => Equ (p', q')
   339                | Or (xa, xb) => Equ (p', q') | Imp (xa, xb) => Equ (p', q')
   340                | Equ (xa, xb) => Equ (p', q') | QAll xa => Equ (p', q')
   341                | QEx xa => Equ (p', q'))
   342          | And (x, xa) =>
   343              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   344                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   345                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   346                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   347                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   348                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   349                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   350          | Or (x, xa) =>
   351              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   352                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   353                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   354                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   355                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   356                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   357                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   358          | Imp (x, xa) =>
   359              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   360                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   361                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   362                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   363                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   364                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   365                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   366          | Equ (x, xa) =>
   367              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   368                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   369                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   370                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   371                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   372                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   373                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   374          | QAll x =>
   375              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   376                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   377                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   378                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   379                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   380                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   381                | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   382          | QEx x =>
   383              (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   384                | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   385                | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   386                | T => p' | F => NOT p' | NOT x => Equ (p', q')
   387                | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   388                | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   389                | QAll x => Equ (p', q') | QEx x => Equ (p', q')))
   390     end
   391   | psimpl (NOT p) =
   392     let val p' = psimpl p
   393     in (case p' of Lt (x, xa) => NOT p' | Gt (x, xa) => NOT p'
   394          | Le (x, xa) => NOT p' | Ge (x, xa) => NOT p' | Eq (x, xa) => NOT p'
   395          | Divides (x, xa) => NOT p' | T => F | F => T | NOT x => x
   396          | And (x, xa) => NOT p' | Or (x, xa) => NOT p' | Imp (x, xa) => NOT p'
   397          | Equ (x, xa) => NOT p' | QAll x => NOT p' | QEx x => NOT p')
   398     end
   399   | psimpl (Lt (u, v)) = Lt (u, v)
   400   | psimpl (Gt (w, x)) = Gt (w, x)
   401   | psimpl (Ge (aa, ab)) = Ge (aa, ab)
   402   | psimpl (Divides (Var bp, af)) = Divides (Var bp, af)
   403   | psimpl (Divides (Neg bq, af)) = Divides (Neg bq, af)
   404   | psimpl (Divides (Add (br, bs), af)) = Divides (Add (br, bs), af)
   405   | psimpl (Divides (Sub (bt, bu), af)) = Divides (Sub (bt, bu), af)
   406   | psimpl (Divides (Mult (bv, bw), af)) = Divides (Mult (bv, bw), af)
   407   | psimpl T = T
   408   | psimpl F = F
   409   | psimpl (QAll ap) = QAll ap
   410   | psimpl (QEx aq) = QEx aq
   411   | psimpl (And (p, q)) =
   412     let val p' = psimpl p
   413     in (case p' of
   414          Lt (x, xa) =>
   415            let val q' = psimpl q
   416            in (case q' of Lt (x, xa) => And (p', q')
   417                 | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   418                 | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   419                 | Divides (x, xa) => And (p', q') | T => p' | F => F
   420                 | NOT x => And (p', q') | And (x, xa) => And (p', q')
   421                 | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   422                 | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   423                 | QEx x => And (p', q'))
   424            end
   425          | Gt (x, xa) =>
   426              let val q' = psimpl q
   427              in (case q' of Lt (x, xa) => And (p', q')
   428                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   429                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   430                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   431                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   432                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   433                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   434                   | QEx x => And (p', q'))
   435              end
   436          | Le (x, xa) =>
   437              let val q' = psimpl q
   438              in (case q' of Lt (x, xa) => And (p', q')
   439                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   440                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   441                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   442                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   443                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   444                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   445                   | QEx x => And (p', q'))
   446              end
   447          | Ge (x, xa) =>
   448              let val q' = psimpl q
   449              in (case q' of Lt (x, xa) => And (p', q')
   450                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   451                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   452                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   453                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   454                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   455                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   456                   | QEx x => And (p', q'))
   457              end
   458          | Eq (x, xa) =>
   459              let val q' = psimpl q
   460              in (case q' of Lt (x, xa) => And (p', q')
   461                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   462                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   463                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   464                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   465                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   466                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   467                   | QEx x => And (p', q'))
   468              end
   469          | Divides (x, xa) =>
   470              let val q' = psimpl q
   471              in (case q' of Lt (x, xa) => And (p', q')
   472                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   473                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   474                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   475                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   476                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   477                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   478                   | QEx x => And (p', q'))
   479              end
   480          | T => psimpl q | F => F
   481          | NOT x =>
   482              let val q' = psimpl q
   483              in (case q' of Lt (x, xa) => And (p', q')
   484                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   485                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   486                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   487                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   488                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   489                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   490                   | QEx x => And (p', q'))
   491              end
   492          | And (x, xa) =>
   493              let val q' = psimpl q
   494              in (case q' of Lt (x, xa) => And (p', q')
   495                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   496                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   497                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   498                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   499                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   500                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   501                   | QEx x => And (p', q'))
   502              end
   503          | Or (x, xa) =>
   504              let val q' = psimpl q
   505              in (case q' of Lt (x, xa) => And (p', q')
   506                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   507                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   508                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   509                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   510                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   511                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   512                   | QEx x => And (p', q'))
   513              end
   514          | Imp (x, xa) =>
   515              let val q' = psimpl q
   516              in (case q' of Lt (x, xa) => And (p', q')
   517                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   518                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   519                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   520                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   521                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   522                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   523                   | QEx x => And (p', q'))
   524              end
   525          | Equ (x, xa) =>
   526              let val q' = psimpl q
   527              in (case q' of Lt (x, xa) => And (p', q')
   528                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   529                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   530                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   531                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   532                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   533                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   534                   | QEx x => And (p', q'))
   535              end
   536          | QAll x =>
   537              let val q' = psimpl q
   538              in (case q' of Lt (x, xa) => And (p', q')
   539                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   540                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   541                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   542                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   543                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   544                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   545                   | QEx x => And (p', q'))
   546              end
   547          | QEx x =>
   548              let val q' = psimpl q
   549              in (case q' of Lt (x, xa) => And (p', q')
   550                   | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   551                   | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   552                   | Divides (x, xa) => And (p', q') | T => p' | F => F
   553                   | NOT x => And (p', q') | And (x, xa) => And (p', q')
   554                   | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   555                   | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   556                   | QEx x => And (p', q'))
   557              end)
   558     end
   559   | psimpl (Or (p, q)) =
   560     let val p' = psimpl p
   561     in (case p' of
   562          Lt (x, xa) =>
   563            let val q' = psimpl q
   564            in (case q' of Lt (x, xa) => Or (p', q') | Gt (x, xa) => Or (p', q')
   565                 | Le (x, xa) => Or (p', q') | Ge (x, xa) => Or (p', q')
   566                 | Eq (x, xa) => Or (p', q') | Divides (x, xa) => Or (p', q')
   567                 | T => T | F => p' | NOT x => Or (p', q')
   568                 | And (x, xa) => Or (p', q') | Or (x, xa) => Or (p', q')
   569                 | Imp (x, xa) => Or (p', q') | Equ (x, xa) => Or (p', q')
   570                 | QAll x => Or (p', q') | QEx x => Or (p', q'))
   571            end
   572          | Gt (x, xa) =>
   573              let val q' = psimpl q
   574              in (case q' of Lt (x, xa) => Or (p', q')
   575                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   576                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   577                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   578                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   579                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   580                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   581                   | QEx x => Or (p', q'))
   582              end
   583          | Le (x, xa) =>
   584              let val q' = psimpl q
   585              in (case q' of Lt (x, xa) => Or (p', q')
   586                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   587                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   588                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   589                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   590                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   591                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   592                   | QEx x => Or (p', q'))
   593              end
   594          | Ge (x, xa) =>
   595              let val q' = psimpl q
   596              in (case q' of Lt (x, xa) => Or (p', q')
   597                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   598                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   599                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   600                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   601                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   602                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   603                   | QEx x => Or (p', q'))
   604              end
   605          | Eq (x, xa) =>
   606              let val q' = psimpl q
   607              in (case q' of Lt (x, xa) => Or (p', q')
   608                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   609                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   610                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   611                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   612                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   613                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   614                   | QEx x => Or (p', q'))
   615              end
   616          | Divides (x, xa) =>
   617              let val q' = psimpl q
   618              in (case q' of Lt (x, xa) => Or (p', q')
   619                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   620                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   621                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   622                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   623                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   624                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   625                   | QEx x => Or (p', q'))
   626              end
   627          | T => T | F => psimpl q
   628          | NOT x =>
   629              let val q' = psimpl q
   630              in (case q' of Lt (x, xa) => Or (p', q')
   631                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   632                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   633                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   634                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   635                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   636                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   637                   | QEx x => Or (p', q'))
   638              end
   639          | And (x, xa) =>
   640              let val q' = psimpl q
   641              in (case q' of Lt (x, xa) => Or (p', q')
   642                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   643                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   644                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   645                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   646                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   647                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   648                   | QEx x => Or (p', q'))
   649              end
   650          | Or (x, xa) =>
   651              let val q' = psimpl q
   652              in (case q' of Lt (x, xa) => Or (p', q')
   653                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   654                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   655                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   656                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   657                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   658                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   659                   | QEx x => Or (p', q'))
   660              end
   661          | Imp (x, xa) =>
   662              let val q' = psimpl q
   663              in (case q' of Lt (x, xa) => Or (p', q')
   664                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   665                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   666                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   667                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   668                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   669                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   670                   | QEx x => Or (p', q'))
   671              end
   672          | Equ (x, xa) =>
   673              let val q' = psimpl q
   674              in (case q' of Lt (x, xa) => Or (p', q')
   675                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   676                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   677                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   678                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   679                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   680                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   681                   | QEx x => Or (p', q'))
   682              end
   683          | QAll x =>
   684              let val q' = psimpl q
   685              in (case q' of Lt (x, xa) => Or (p', q')
   686                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   687                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   688                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   689                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   690                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   691                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   692                   | QEx x => Or (p', q'))
   693              end
   694          | QEx x =>
   695              let val q' = psimpl q
   696              in (case q' of Lt (x, xa) => Or (p', q')
   697                   | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   698                   | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   699                   | Divides (x, xa) => Or (p', q') | T => T | F => p'
   700                   | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   701                   | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   702                   | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   703                   | QEx x => Or (p', q'))
   704              end)
   705     end
   706   | psimpl (Imp (p, q)) =
   707     let val p' = psimpl p
   708     in (case p' of
   709          Lt (x, xa) =>
   710            let val q' = psimpl q
   711            in (case q' of Lt (x, xa) => Imp (p', q')
   712                 | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   713                 | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   714                 | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   715                 | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   716                 | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   717                 | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   718                 | QEx x => Imp (p', q'))
   719            end
   720          | Gt (x, xa) =>
   721              let val q' = psimpl q
   722              in (case q' of Lt (x, xa) => Imp (p', q')
   723                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   724                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   725                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   726                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   727                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   728                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   729                   | QEx x => Imp (p', q'))
   730              end
   731          | Le (x, xa) =>
   732              let val q' = psimpl q
   733              in (case q' of Lt (x, xa) => Imp (p', q')
   734                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   735                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   736                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   737                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   738                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   739                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   740                   | QEx x => Imp (p', q'))
   741              end
   742          | Ge (x, xa) =>
   743              let val q' = psimpl q
   744              in (case q' of Lt (x, xa) => Imp (p', q')
   745                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   746                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   747                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   748                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   749                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   750                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   751                   | QEx x => Imp (p', q'))
   752              end
   753          | Eq (x, xa) =>
   754              let val q' = psimpl q
   755              in (case q' of Lt (x, xa) => Imp (p', q')
   756                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   757                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   758                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   759                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   760                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   761                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   762                   | QEx x => Imp (p', q'))
   763              end
   764          | Divides (x, xa) =>
   765              let val q' = psimpl q
   766              in (case q' of Lt (x, xa) => Imp (p', q')
   767                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   768                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   769                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   770                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   771                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   772                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   773                   | QEx x => Imp (p', q'))
   774              end
   775          | T => psimpl q | F => T
   776          | NOT x =>
   777              let val q' = psimpl q
   778              in (case q' of Lt (xa, xb) => Or (x, q')
   779                   | Gt (xa, xb) => Or (x, q') | Le (xa, xb) => Or (x, q')
   780                   | Ge (xa, xb) => Or (x, q') | Eq (xa, xb) => Or (x, q')
   781                   | Divides (xa, xb) => Or (x, q') | T => T | F => x
   782                   | NOT xa => Or (x, q') | And (xa, xb) => Or (x, q')
   783                   | Or (xa, xb) => Or (x, q') | Imp (xa, xb) => Or (x, q')
   784                   | Equ (xa, xb) => Or (x, q') | QAll xa => Or (x, q')
   785                   | QEx xa => Or (x, q'))
   786              end
   787          | And (x, xa) =>
   788              let val q' = psimpl q
   789              in (case q' of Lt (x, xa) => Imp (p', q')
   790                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   791                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   792                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   793                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   794                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   795                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   796                   | QEx x => Imp (p', q'))
   797              end
   798          | Or (x, xa) =>
   799              let val q' = psimpl q
   800              in (case q' of Lt (x, xa) => Imp (p', q')
   801                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   802                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   803                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   804                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   805                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   806                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   807                   | QEx x => Imp (p', q'))
   808              end
   809          | Imp (x, xa) =>
   810              let val q' = psimpl q
   811              in (case q' of Lt (x, xa) => Imp (p', q')
   812                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   813                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   814                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   815                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   816                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   817                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   818                   | QEx x => Imp (p', q'))
   819              end
   820          | Equ (x, xa) =>
   821              let val q' = psimpl q
   822              in (case q' of Lt (x, xa) => Imp (p', q')
   823                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   824                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   825                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   826                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   827                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   828                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   829                   | QEx x => Imp (p', q'))
   830              end
   831          | QAll x =>
   832              let val q' = psimpl q
   833              in (case q' of Lt (x, xa) => Imp (p', q')
   834                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   835                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   836                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   837                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   838                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   839                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   840                   | QEx x => Imp (p', q'))
   841              end
   842          | QEx x =>
   843              let val q' = psimpl q
   844              in (case q' of Lt (x, xa) => Imp (p', q')
   845                   | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   846                   | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   847                   | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   848                   | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   849                   | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   850                   | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   851                   | QEx x => Imp (p', q'))
   852              end)
   853     end;
   854 
   855 fun subst_it i (Cst b) = Cst b
   856   | subst_it i (Var n) = (if (n = 0) then i else Var n)
   857   | subst_it i (Neg it) = Neg (subst_it i it)
   858   | subst_it i (Add (it1, it2)) = Add (subst_it i it1, subst_it i it2)
   859   | subst_it i (Sub (it1, it2)) = Sub (subst_it i it1, subst_it i it2)
   860   | subst_it i (Mult (it1, it2)) = Mult (subst_it i it1, subst_it i it2);
   861 
   862 fun subst_p i (Le (it1, it2)) = Le (subst_it i it1, subst_it i it2)
   863   | subst_p i (Lt (it1, it2)) = Lt (subst_it i it1, subst_it i it2)
   864   | subst_p i (Ge (it1, it2)) = Ge (subst_it i it1, subst_it i it2)
   865   | subst_p i (Gt (it1, it2)) = Gt (subst_it i it1, subst_it i it2)
   866   | subst_p i (Eq (it1, it2)) = Eq (subst_it i it1, subst_it i it2)
   867   | subst_p i (Divides (d, t)) = Divides (subst_it i d, subst_it i t)
   868   | subst_p i T = T
   869   | subst_p i F = F
   870   | subst_p i (And (p, q)) = And (subst_p i p, subst_p i q)
   871   | subst_p i (Or (p, q)) = Or (subst_p i p, subst_p i q)
   872   | subst_p i (Imp (p, q)) = Imp (subst_p i p, subst_p i q)
   873   | subst_p i (Equ (p, q)) = Equ (subst_p i p, subst_p i q)
   874   | subst_p i (NOT p) = NOT (subst_p i p);
   875 
   876 fun explode_disj ([], p) = F
   877   | explode_disj ((i :: is), p) =
   878     let val pi = psimpl (subst_p i p)
   879     in (case pi of
   880          Lt (x, xa) =>
   881            let val r = explode_disj (is, p)
   882            in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   883                 | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   884                 | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   885                 | T => T | F => pi | NOT x => Or (pi, r)
   886                 | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   887                 | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   888                 | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   889            end
   890          | Gt (x, xa) =>
   891              let val r = explode_disj (is, p)
   892              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   893                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   894                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   895                   | T => T | F => pi | NOT x => Or (pi, r)
   896                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   897                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   898                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   899              end
   900          | Le (x, xa) =>
   901              let val r = explode_disj (is, p)
   902              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   903                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   904                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   905                   | T => T | F => pi | NOT x => Or (pi, r)
   906                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   907                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   908                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   909              end
   910          | Ge (x, xa) =>
   911              let val r = explode_disj (is, p)
   912              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   913                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   914                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   915                   | T => T | F => pi | NOT x => Or (pi, r)
   916                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   917                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   918                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   919              end
   920          | Eq (x, xa) =>
   921              let val r = explode_disj (is, p)
   922              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   923                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   924                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   925                   | T => T | F => pi | NOT x => Or (pi, r)
   926                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   927                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   928                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   929              end
   930          | Divides (x, xa) =>
   931              let val r = explode_disj (is, p)
   932              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   933                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   934                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   935                   | T => T | F => pi | NOT x => Or (pi, r)
   936                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   937                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   938                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   939              end
   940          | T => T | F => explode_disj (is, p)
   941          | NOT x =>
   942              let val r = explode_disj (is, p)
   943              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   944                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   945                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   946                   | T => T | F => pi | NOT x => Or (pi, r)
   947                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   948                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   949                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   950              end
   951          | And (x, xa) =>
   952              let val r = explode_disj (is, p)
   953              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   954                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   955                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   956                   | T => T | F => pi | NOT x => Or (pi, r)
   957                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   958                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   959                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   960              end
   961          | Or (x, xa) =>
   962              let val r = explode_disj (is, p)
   963              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   964                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   965                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   966                   | T => T | F => pi | NOT x => Or (pi, r)
   967                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   968                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   969                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   970              end
   971          | Imp (x, xa) =>
   972              let val r = explode_disj (is, p)
   973              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   974                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   975                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   976                   | T => T | F => pi | NOT x => Or (pi, r)
   977                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   978                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   979                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   980              end
   981          | Equ (x, xa) =>
   982              let val r = explode_disj (is, p)
   983              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   984                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   985                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   986                   | T => T | F => pi | NOT x => Or (pi, r)
   987                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   988                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   989                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   990              end
   991          | QAll x =>
   992              let val r = explode_disj (is, p)
   993              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   994                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   995                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   996                   | T => T | F => pi | NOT x => Or (pi, r)
   997                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   998                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   999                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
  1000              end
  1001          | QEx x =>
  1002              let val r = explode_disj (is, p)
  1003              in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
  1004                   | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
  1005                   | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
  1006                   | T => T | F => pi | NOT x => Or (pi, r)
  1007                   | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
  1008                   | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
  1009                   | QAll x => Or (pi, r) | QEx x => Or (pi, r))
  1010              end)
  1011     end;
  1012 
  1013 fun minusinf (And (p, q)) = And (minusinf p, minusinf q)
  1014   | minusinf (Or (p, q)) = Or (minusinf p, minusinf q)
  1015   | minusinf (Lt (u, v)) = Lt (u, v)
  1016   | minusinf (Gt (w, x)) = Gt (w, x)
  1017   | minusinf (Le (Cst bo, z)) = Le (Cst bo, z)
  1018   | minusinf (Le (Var bp, z)) = Le (Var bp, z)
  1019   | minusinf (Le (Neg bq, z)) = Le (Neg bq, z)
  1020   | minusinf (Le (Add (Cst cg, bs), z)) = Le (Add (Cst cg, bs), z)
  1021   | minusinf (Le (Add (Var ch, bs), z)) = Le (Add (Var ch, bs), z)
  1022   | minusinf (Le (Add (Neg ci, bs), z)) = Le (Add (Neg ci, bs), z)
  1023   | minusinf (Le (Add (Add (cj, ck), bs), z)) = Le (Add (Add (cj, ck), bs), z)
  1024   | minusinf (Le (Add (Sub (cl, cm), bs), z)) = Le (Add (Sub (cl, cm), bs), z)
  1025   | minusinf (Le (Add (Mult (Cst cy, Cst dq), bs), z)) =
  1026     Le (Add (Mult (Cst cy, Cst dq), bs), z)
  1027   | minusinf (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
  1028     (if (ei = 0) then (if (cy < 0) then F else T)
  1029       else Le (Add (Mult (Cst cy, Var (op_45_def0 ei id_1_def0 + 1)), bs), z))
  1030   | minusinf (Le (Add (Mult (Cst cy, Neg ds), bs), z)) =
  1031     Le (Add (Mult (Cst cy, Neg ds), bs), z)
  1032   | minusinf (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) =
  1033     Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)
  1034   | minusinf (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) =
  1035     Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)
  1036   | minusinf (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) =
  1037     Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)
  1038   | minusinf (Le (Add (Mult (Var cz, co), bs), z)) =
  1039     Le (Add (Mult (Var cz, co), bs), z)
  1040   | minusinf (Le (Add (Mult (Neg da, co), bs), z)) =
  1041     Le (Add (Mult (Neg da, co), bs), z)
  1042   | minusinf (Le (Add (Mult (Add (db, dc), co), bs), z)) =
  1043     Le (Add (Mult (Add (db, dc), co), bs), z)
  1044   | minusinf (Le (Add (Mult (Sub (dd, de), co), bs), z)) =
  1045     Le (Add (Mult (Sub (dd, de), co), bs), z)
  1046   | minusinf (Le (Add (Mult (Mult (df, dg), co), bs), z)) =
  1047     Le (Add (Mult (Mult (df, dg), co), bs), z)
  1048   | minusinf (Le (Sub (bt, bu), z)) = Le (Sub (bt, bu), z)
  1049   | minusinf (Le (Mult (bv, bw), z)) = Le (Mult (bv, bw), z)
  1050   | minusinf (Ge (aa, ab)) = Ge (aa, ab)
  1051   | minusinf (Eq (Cst ek, ad)) = Eq (Cst ek, ad)
  1052   | minusinf (Eq (Var el, ad)) = Eq (Var el, ad)
  1053   | minusinf (Eq (Neg em, ad)) = Eq (Neg em, ad)
  1054   | minusinf (Eq (Add (Cst fc, eo), ad)) = Eq (Add (Cst fc, eo), ad)
  1055   | minusinf (Eq (Add (Var fd, eo), ad)) = Eq (Add (Var fd, eo), ad)
  1056   | minusinf (Eq (Add (Neg fe, eo), ad)) = Eq (Add (Neg fe, eo), ad)
  1057   | minusinf (Eq (Add (Add (ff, fg), eo), ad)) = Eq (Add (Add (ff, fg), eo), ad)
  1058   | minusinf (Eq (Add (Sub (fh, fi), eo), ad)) = Eq (Add (Sub (fh, fi), eo), ad)
  1059   | minusinf (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) =
  1060     Eq (Add (Mult (Cst fu, Cst gm), eo), ad)
  1061   | minusinf (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
  1062     (if (he = 0) then F
  1063       else Eq (Add (Mult (Cst fu, Var (op_45_def0 he id_1_def0 + 1)), eo), ad))
  1064   | minusinf (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) =
  1065     Eq (Add (Mult (Cst fu, Neg go), eo), ad)
  1066   | minusinf (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) =
  1067     Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)
  1068   | minusinf (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) =
  1069     Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)
  1070   | minusinf (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) =
  1071     Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)
  1072   | minusinf (Eq (Add (Mult (Var fv, fk), eo), ad)) =
  1073     Eq (Add (Mult (Var fv, fk), eo), ad)
  1074   | minusinf (Eq (Add (Mult (Neg fw, fk), eo), ad)) =
  1075     Eq (Add (Mult (Neg fw, fk), eo), ad)
  1076   | minusinf (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) =
  1077     Eq (Add (Mult (Add (fx, fy), fk), eo), ad)
  1078   | minusinf (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) =
  1079     Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)
  1080   | minusinf (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) =
  1081     Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)
  1082   | minusinf (Eq (Sub (ep, eq), ad)) = Eq (Sub (ep, eq), ad)
  1083   | minusinf (Eq (Mult (er, es), ad)) = Eq (Mult (er, es), ad)
  1084   | minusinf (Divides (ae, af)) = Divides (ae, af)
  1085   | minusinf T = T
  1086   | minusinf F = F
  1087   | minusinf (NOT (Lt (hg, hh))) = NOT (Lt (hg, hh))
  1088   | minusinf (NOT (Gt (hi, hj))) = NOT (Gt (hi, hj))
  1089   | minusinf (NOT (Le (hk, hl))) = NOT (Le (hk, hl))
  1090   | minusinf (NOT (Ge (hm, hn))) = NOT (Ge (hm, hn))
  1091   | minusinf (NOT (Eq (Cst ja, hp))) = NOT (Eq (Cst ja, hp))
  1092   | minusinf (NOT (Eq (Var jb, hp))) = NOT (Eq (Var jb, hp))
  1093   | minusinf (NOT (Eq (Neg jc, hp))) = NOT (Eq (Neg jc, hp))
  1094   | minusinf (NOT (Eq (Add (Cst js, je), hp))) = NOT (Eq (Add (Cst js, je), hp))
  1095   | minusinf (NOT (Eq (Add (Var jt, je), hp))) = NOT (Eq (Add (Var jt, je), hp))
  1096   | minusinf (NOT (Eq (Add (Neg ju, je), hp))) = NOT (Eq (Add (Neg ju, je), hp))
  1097   | minusinf (NOT (Eq (Add (Add (jv, jw), je), hp))) =
  1098     NOT (Eq (Add (Add (jv, jw), je), hp))
  1099   | minusinf (NOT (Eq (Add (Sub (jx, jy), je), hp))) =
  1100     NOT (Eq (Add (Sub (jx, jy), je), hp))
  1101   | minusinf (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) =
  1102     NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))
  1103   | minusinf (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
  1104     (if (lu = 0) then T
  1105       else NOT (Eq (Add (Mult (Cst kk, Var (op_45_def0 lu id_1_def0 + 1)), je),
  1106                      hp)))
  1107   | minusinf (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) =
  1108     NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))
  1109   | minusinf (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) =
  1110     NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))
  1111   | minusinf (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) =
  1112     NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))
  1113   | minusinf (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) =
  1114     NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))
  1115   | minusinf (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) =
  1116     NOT (Eq (Add (Mult (Var kl, ka), je), hp))
  1117   | minusinf (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) =
  1118     NOT (Eq (Add (Mult (Neg km, ka), je), hp))
  1119   | minusinf (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) =
  1120     NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))
  1121   | minusinf (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) =
  1122     NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))
  1123   | minusinf (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) =
  1124     NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))
  1125   | minusinf (NOT (Eq (Sub (jf, jg), hp))) = NOT (Eq (Sub (jf, jg), hp))
  1126   | minusinf (NOT (Eq (Mult (jh, ji), hp))) = NOT (Eq (Mult (jh, ji), hp))
  1127   | minusinf (NOT (Divides (hq, hr))) = NOT (Divides (hq, hr))
  1128   | minusinf (NOT T) = NOT T
  1129   | minusinf (NOT F) = NOT F
  1130   | minusinf (NOT (NOT hs)) = NOT (NOT hs)
  1131   | minusinf (NOT (And (ht, hu))) = NOT (And (ht, hu))
  1132   | minusinf (NOT (Or (hv, hw))) = NOT (Or (hv, hw))
  1133   | minusinf (NOT (Imp (hx, hy))) = NOT (Imp (hx, hy))
  1134   | minusinf (NOT (Equ (hz, ia))) = NOT (Equ (hz, ia))
  1135   | minusinf (NOT (QAll ib)) = NOT (QAll ib)
  1136   | minusinf (NOT (QEx ic)) = NOT (QEx ic)
  1137   | minusinf (Imp (al, am)) = Imp (al, am)
  1138   | minusinf (Equ (an, ao)) = Equ (an, ao)
  1139   | minusinf (QAll ap) = QAll ap
  1140   | minusinf (QEx aq) = QEx aq;
  1141 
  1142 fun abs i = (if (i < 0) then ~ i else i);
  1143 
  1144 fun op_div_def1 a b = fst (divAlg (a, b));
  1145 
  1146 fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
  1147 
  1148 fun ngcd (m, n) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
  1149 
  1150 fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
  1151 
  1152 fun ilcm a b = op_div_def1 (a * b) (igcd (a, b));
  1153 
  1154 fun divlcm (NOT p) = divlcm p
  1155   | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
  1156   | divlcm (Or (p, q)) = ilcm (divlcm p) (divlcm q)
  1157   | divlcm (Lt (u, v)) = 1
  1158   | divlcm (Gt (w, x)) = 1
  1159   | divlcm (Le (y, z)) = 1
  1160   | divlcm (Ge (aa, ab)) = 1
  1161   | divlcm (Eq (ac, ad)) = 1
  1162   | divlcm (Divides (Cst bo, Cst cg)) = 1
  1163   | divlcm (Divides (Cst bo, Var ch)) = 1
  1164   | divlcm (Divides (Cst bo, Neg ci)) = 1
  1165   | divlcm (Divides (Cst bo, Add (Cst cy, ck))) = 1
  1166   | divlcm (Divides (Cst bo, Add (Var cz, ck))) = 1
  1167   | divlcm (Divides (Cst bo, Add (Neg da, ck))) = 1
  1168   | divlcm (Divides (Cst bo, Add (Add (db, dc), ck))) = 1
  1169   | divlcm (Divides (Cst bo, Add (Sub (dd, de), ck))) = 1
  1170   | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Cst ei), ck))) = 1
  1171   | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Var fa), ck))) =
  1172     (if (fa = 0) then abs bo else 1)
  1173   | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Neg ek), ck))) = 1
  1174   | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Add (el, em)), ck))) = 1
  1175   | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Sub (en, eo)), ck))) = 1
  1176   | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Mult (ep, eq)), ck))) = 1
  1177   | divlcm (Divides (Cst bo, Add (Mult (Var dr, dg), ck))) = 1
  1178   | divlcm (Divides (Cst bo, Add (Mult (Neg ds, dg), ck))) = 1
  1179   | divlcm (Divides (Cst bo, Add (Mult (Add (dt, du), dg), ck))) = 1
  1180   | divlcm (Divides (Cst bo, Add (Mult (Sub (dv, dw), dg), ck))) = 1
  1181   | divlcm (Divides (Cst bo, Add (Mult (Mult (dx, dy), dg), ck))) = 1
  1182   | divlcm (Divides (Cst bo, Sub (cl, cm))) = 1
  1183   | divlcm (Divides (Cst bo, Mult (cn, co))) = 1
  1184   | divlcm (Divides (Var bp, af)) = 1
  1185   | divlcm (Divides (Neg bq, af)) = 1
  1186   | divlcm (Divides (Add (br, bs), af)) = 1
  1187   | divlcm (Divides (Sub (bt, bu), af)) = 1
  1188   | divlcm (Divides (Mult (bv, bw), af)) = 1
  1189   | divlcm T = 1
  1190   | divlcm F = 1
  1191   | divlcm (Imp (al, am)) = 1
  1192   | divlcm (Equ (an, ao)) = 1
  1193   | divlcm (QAll ap) = 1
  1194   | divlcm (QEx aq) = 1;
  1195 
  1196 fun explode_minf (q, B) =
  1197     let val d = divlcm q; val pm = minusinf q;
  1198         val dj1 = explode_disj (map (fn x => Cst x) (iupto (1, d)), pm)
  1199     in (case dj1 of
  1200          Lt (x, xa) =>
  1201            let val dj2 = explode_disj (all_sums (d, B), q)
  1202            in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1203                 | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1204                 | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1205                 | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1206                 | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1207                 | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1208                 | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1209                 | QEx x => Or (dj1, dj2))
  1210            end
  1211          | Gt (x, xa) =>
  1212              let val dj2 = explode_disj (all_sums (d, B), q)
  1213              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1214                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1215                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1216                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1217                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1218                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1219                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1220                   | QEx x => Or (dj1, dj2))
  1221              end
  1222          | Le (x, xa) =>
  1223              let val dj2 = explode_disj (all_sums (d, B), q)
  1224              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1225                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1226                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1227                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1228                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1229                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1230                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1231                   | QEx x => Or (dj1, dj2))
  1232              end
  1233          | Ge (x, xa) =>
  1234              let val dj2 = explode_disj (all_sums (d, B), q)
  1235              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1236                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1237                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1238                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1239                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1240                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1241                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1242                   | QEx x => Or (dj1, dj2))
  1243              end
  1244          | Eq (x, xa) =>
  1245              let val dj2 = explode_disj (all_sums (d, B), q)
  1246              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1247                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1248                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1249                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1250                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1251                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1252                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1253                   | QEx x => Or (dj1, dj2))
  1254              end
  1255          | Divides (x, xa) =>
  1256              let val dj2 = explode_disj (all_sums (d, B), q)
  1257              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1258                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1259                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1260                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1261                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1262                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1263                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1264                   | QEx x => Or (dj1, dj2))
  1265              end
  1266          | T => T | F => explode_disj (all_sums (d, B), q)
  1267          | NOT x =>
  1268              let val dj2 = explode_disj (all_sums (d, B), q)
  1269              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1270                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1271                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1272                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1273                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1274                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1275                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1276                   | QEx x => Or (dj1, dj2))
  1277              end
  1278          | And (x, xa) =>
  1279              let val dj2 = explode_disj (all_sums (d, B), q)
  1280              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1281                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1282                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1283                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1284                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1285                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1286                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1287                   | QEx x => Or (dj1, dj2))
  1288              end
  1289          | Or (x, xa) =>
  1290              let val dj2 = explode_disj (all_sums (d, B), q)
  1291              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1292                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1293                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1294                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1295                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1296                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1297                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1298                   | QEx x => Or (dj1, dj2))
  1299              end
  1300          | Imp (x, xa) =>
  1301              let val dj2 = explode_disj (all_sums (d, B), q)
  1302              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1303                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1304                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1305                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1306                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1307                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1308                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1309                   | QEx x => Or (dj1, dj2))
  1310              end
  1311          | Equ (x, xa) =>
  1312              let val dj2 = explode_disj (all_sums (d, B), q)
  1313              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1314                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1315                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1316                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1317                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1318                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1319                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1320                   | QEx x => Or (dj1, dj2))
  1321              end
  1322          | QAll x =>
  1323              let val dj2 = explode_disj (all_sums (d, B), q)
  1324              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1325                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1326                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1327                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1328                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1329                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1330                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1331                   | QEx x => Or (dj1, dj2))
  1332              end
  1333          | QEx x =>
  1334              let val dj2 = explode_disj (all_sums (d, B), q)
  1335              in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1336                   | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1337                   | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1338                   | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1339                   | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1340                   | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1341                   | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1342                   | QEx x => Or (dj1, dj2))
  1343              end)
  1344     end;
  1345 
  1346 fun mirror (And (p, q)) = And (mirror p, mirror q)
  1347   | mirror (Or (p, q)) = Or (mirror p, mirror q)
  1348   | mirror (Lt (u, v)) = Lt (u, v)
  1349   | mirror (Gt (w, x)) = Gt (w, x)
  1350   | mirror (Le (Cst bp, aa)) = Le (Cst bp, aa)
  1351   | mirror (Le (Var bq, aa)) = Le (Var bq, aa)
  1352   | mirror (Le (Neg br, aa)) = Le (Neg br, aa)
  1353   | mirror (Le (Add (Cst ch, bt), aa)) = Le (Add (Cst ch, bt), aa)
  1354   | mirror (Le (Add (Var ci, bt), aa)) = Le (Add (Var ci, bt), aa)
  1355   | mirror (Le (Add (Neg cj, bt), aa)) = Le (Add (Neg cj, bt), aa)
  1356   | mirror (Le (Add (Add (ck, cl), bt), aa)) = Le (Add (Add (ck, cl), bt), aa)
  1357   | mirror (Le (Add (Sub (cm, cn), bt), aa)) = Le (Add (Sub (cm, cn), bt), aa)
  1358   | mirror (Le (Add (Mult (Cst cz, Cst dr), bt), aa)) =
  1359     Le (Add (Mult (Cst cz, Cst dr), bt), aa)
  1360   | mirror (Le (Add (Mult (Cst cz, Var ej), bt), aa)) =
  1361     (if (ej = 0) then Le (Add (Mult (Cst (~ cz), Var 0), bt), aa)
  1362       else Le (Add (Mult (Cst cz, Var (op_45_def0 ej id_1_def0 + 1)), bt), aa))
  1363   | mirror (Le (Add (Mult (Cst cz, Neg dt), bt), aa)) =
  1364     Le (Add (Mult (Cst cz, Neg dt), bt), aa)
  1365   | mirror (Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)) =
  1366     Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)
  1367   | mirror (Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)) =
  1368     Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)
  1369   | mirror (Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)) =
  1370     Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)
  1371   | mirror (Le (Add (Mult (Var da, cp), bt), aa)) =
  1372     Le (Add (Mult (Var da, cp), bt), aa)
  1373   | mirror (Le (Add (Mult (Neg db, cp), bt), aa)) =
  1374     Le (Add (Mult (Neg db, cp), bt), aa)
  1375   | mirror (Le (Add (Mult (Add (dc, dd), cp), bt), aa)) =
  1376     Le (Add (Mult (Add (dc, dd), cp), bt), aa)
  1377   | mirror (Le (Add (Mult (Sub (de, df), cp), bt), aa)) =
  1378     Le (Add (Mult (Sub (de, df), cp), bt), aa)
  1379   | mirror (Le (Add (Mult (Mult (dg, dh), cp), bt), aa)) =
  1380     Le (Add (Mult (Mult (dg, dh), cp), bt), aa)
  1381   | mirror (Le (Sub (bu, bv), aa)) = Le (Sub (bu, bv), aa)
  1382   | mirror (Le (Mult (bw, bx), aa)) = Le (Mult (bw, bx), aa)
  1383   | mirror (Ge (ab, ac)) = Ge (ab, ac)
  1384   | mirror (Eq (Cst el, ae)) = Eq (Cst el, ae)
  1385   | mirror (Eq (Var em, ae)) = Eq (Var em, ae)
  1386   | mirror (Eq (Neg en, ae)) = Eq (Neg en, ae)
  1387   | mirror (Eq (Add (Cst fd, ep), ae)) = Eq (Add (Cst fd, ep), ae)
  1388   | mirror (Eq (Add (Var fe, ep), ae)) = Eq (Add (Var fe, ep), ae)
  1389   | mirror (Eq (Add (Neg ff, ep), ae)) = Eq (Add (Neg ff, ep), ae)
  1390   | mirror (Eq (Add (Add (fg, fh), ep), ae)) = Eq (Add (Add (fg, fh), ep), ae)
  1391   | mirror (Eq (Add (Sub (fi, fj), ep), ae)) = Eq (Add (Sub (fi, fj), ep), ae)
  1392   | mirror (Eq (Add (Mult (Cst fv, Cst gn), ep), ae)) =
  1393     Eq (Add (Mult (Cst fv, Cst gn), ep), ae)
  1394   | mirror (Eq (Add (Mult (Cst fv, Var hf), ep), ae)) =
  1395     (if (hf = 0) then Eq (Add (Mult (Cst (~ fv), Var 0), ep), ae)
  1396       else Eq (Add (Mult (Cst fv, Var (op_45_def0 hf id_1_def0 + 1)), ep), ae))
  1397   | mirror (Eq (Add (Mult (Cst fv, Neg gp), ep), ae)) =
  1398     Eq (Add (Mult (Cst fv, Neg gp), ep), ae)
  1399   | mirror (Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)) =
  1400     Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)
  1401   | mirror (Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)) =
  1402     Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)
  1403   | mirror (Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)) =
  1404     Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)
  1405   | mirror (Eq (Add (Mult (Var fw, fl), ep), ae)) =
  1406     Eq (Add (Mult (Var fw, fl), ep), ae)
  1407   | mirror (Eq (Add (Mult (Neg fx, fl), ep), ae)) =
  1408     Eq (Add (Mult (Neg fx, fl), ep), ae)
  1409   | mirror (Eq (Add (Mult (Add (fy, fz), fl), ep), ae)) =
  1410     Eq (Add (Mult (Add (fy, fz), fl), ep), ae)
  1411   | mirror (Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)) =
  1412     Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)
  1413   | mirror (Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)) =
  1414     Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)
  1415   | mirror (Eq (Sub (eq, er), ae)) = Eq (Sub (eq, er), ae)
  1416   | mirror (Eq (Mult (es, et), ae)) = Eq (Mult (es, et), ae)
  1417   | mirror (Divides (Cst hh, Cst hz)) = Divides (Cst hh, Cst hz)
  1418   | mirror (Divides (Cst hh, Var ia)) = Divides (Cst hh, Var ia)
  1419   | mirror (Divides (Cst hh, Neg ib)) = Divides (Cst hh, Neg ib)
  1420   | mirror (Divides (Cst hh, Add (Cst ir, id))) =
  1421     Divides (Cst hh, Add (Cst ir, id))
  1422   | mirror (Divides (Cst hh, Add (Var is, id))) =
  1423     Divides (Cst hh, Add (Var is, id))
  1424   | mirror (Divides (Cst hh, Add (Neg it, id))) =
  1425     Divides (Cst hh, Add (Neg it, id))
  1426   | mirror (Divides (Cst hh, Add (Add (iu, iv), id))) =
  1427     Divides (Cst hh, Add (Add (iu, iv), id))
  1428   | mirror (Divides (Cst hh, Add (Sub (iw, ix), id))) =
  1429     Divides (Cst hh, Add (Sub (iw, ix), id))
  1430   | mirror (Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))) =
  1431     Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))
  1432   | mirror (Divides (Cst hh, Add (Mult (Cst jj, Var kt), id))) =
  1433     (if (kt = 0) then Divides (Cst hh, Add (Mult (Cst (~ jj), Var 0), id))
  1434       else Divides
  1435              (Cst hh,
  1436                Add (Mult (Cst jj, Var (op_45_def0 kt id_1_def0 + 1)), id)))
  1437   | mirror (Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))) =
  1438     Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))
  1439   | mirror (Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))) =
  1440     Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))
  1441   | mirror (Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))) =
  1442     Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))
  1443   | mirror (Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))) =
  1444     Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))
  1445   | mirror (Divides (Cst hh, Add (Mult (Var jk, iz), id))) =
  1446     Divides (Cst hh, Add (Mult (Var jk, iz), id))
  1447   | mirror (Divides (Cst hh, Add (Mult (Neg jl, iz), id))) =
  1448     Divides (Cst hh, Add (Mult (Neg jl, iz), id))
  1449   | mirror (Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))) =
  1450     Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))
  1451   | mirror (Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))) =
  1452     Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))
  1453   | mirror (Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))) =
  1454     Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))
  1455   | mirror (Divides (Cst hh, Sub (ie, if'))) = Divides (Cst hh, Sub (ie, if'))
  1456   | mirror (Divides (Cst hh, Mult (ig, ih))) = Divides (Cst hh, Mult (ig, ih))
  1457   | mirror (Divides (Var hi, ag)) = Divides (Var hi, ag)
  1458   | mirror (Divides (Neg hj, ag)) = Divides (Neg hj, ag)
  1459   | mirror (Divides (Add (hk, hl), ag)) = Divides (Add (hk, hl), ag)
  1460   | mirror (Divides (Sub (hm, hn), ag)) = Divides (Sub (hm, hn), ag)
  1461   | mirror (Divides (Mult (ho, hp), ag)) = Divides (Mult (ho, hp), ag)
  1462   | mirror T = T
  1463   | mirror F = F
  1464   | mirror (NOT (Lt (kv, kw))) = NOT (Lt (kv, kw))
  1465   | mirror (NOT (Gt (kx, ky))) = NOT (Gt (kx, ky))
  1466   | mirror (NOT (Le (kz, la))) = NOT (Le (kz, la))
  1467   | mirror (NOT (Ge (lb, lc))) = NOT (Ge (lb, lc))
  1468   | mirror (NOT (Eq (Cst mp, le))) = NOT (Eq (Cst mp, le))
  1469   | mirror (NOT (Eq (Var mq, le))) = NOT (Eq (Var mq, le))
  1470   | mirror (NOT (Eq (Neg mr, le))) = NOT (Eq (Neg mr, le))
  1471   | mirror (NOT (Eq (Add (Cst nh, mt), le))) = NOT (Eq (Add (Cst nh, mt), le))
  1472   | mirror (NOT (Eq (Add (Var ni, mt), le))) = NOT (Eq (Add (Var ni, mt), le))
  1473   | mirror (NOT (Eq (Add (Neg nj, mt), le))) = NOT (Eq (Add (Neg nj, mt), le))
  1474   | mirror (NOT (Eq (Add (Add (nk, nl), mt), le))) =
  1475     NOT (Eq (Add (Add (nk, nl), mt), le))
  1476   | mirror (NOT (Eq (Add (Sub (nm, nn), mt), le))) =
  1477     NOT (Eq (Add (Sub (nm, nn), mt), le))
  1478   | mirror (NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))) =
  1479     NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))
  1480   | mirror (NOT (Eq (Add (Mult (Cst nz, Var pj), mt), le))) =
  1481     (if (pj = 0) then NOT (Eq (Add (Mult (Cst (~ nz), Var 0), mt), le))
  1482       else NOT (Eq (Add (Mult (Cst nz, Var (op_45_def0 pj id_1_def0 + 1)), mt),
  1483                      le)))
  1484   | mirror (NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))) =
  1485     NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))
  1486   | mirror (NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))) =
  1487     NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))
  1488   | mirror (NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))) =
  1489     NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))
  1490   | mirror (NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))) =
  1491     NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))
  1492   | mirror (NOT (Eq (Add (Mult (Var oa, np), mt), le))) =
  1493     NOT (Eq (Add (Mult (Var oa, np), mt), le))
  1494   | mirror (NOT (Eq (Add (Mult (Neg ob, np), mt), le))) =
  1495     NOT (Eq (Add (Mult (Neg ob, np), mt), le))
  1496   | mirror (NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))) =
  1497     NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))
  1498   | mirror (NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))) =
  1499     NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))
  1500   | mirror (NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))) =
  1501     NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))
  1502   | mirror (NOT (Eq (Sub (mu, mv), le))) = NOT (Eq (Sub (mu, mv), le))
  1503   | mirror (NOT (Eq (Mult (mw, mx), le))) = NOT (Eq (Mult (mw, mx), le))
  1504   | mirror (NOT (Divides (Cst pl, Cst qd))) = NOT (Divides (Cst pl, Cst qd))
  1505   | mirror (NOT (Divides (Cst pl, Var qe))) = NOT (Divides (Cst pl, Var qe))
  1506   | mirror (NOT (Divides (Cst pl, Neg qf))) = NOT (Divides (Cst pl, Neg qf))
  1507   | mirror (NOT (Divides (Cst pl, Add (Cst qv, qh)))) =
  1508     NOT (Divides (Cst pl, Add (Cst qv, qh)))
  1509   | mirror (NOT (Divides (Cst pl, Add (Var qw, qh)))) =
  1510     NOT (Divides (Cst pl, Add (Var qw, qh)))
  1511   | mirror (NOT (Divides (Cst pl, Add (Neg qx, qh)))) =
  1512     NOT (Divides (Cst pl, Add (Neg qx, qh)))
  1513   | mirror (NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))) =
  1514     NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))
  1515   | mirror (NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))) =
  1516     NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))
  1517   | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))) =
  1518     NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))
  1519   | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Var sx), qh)))) =
  1520     (if (sx = 0)
  1521       then NOT (Divides (Cst pl, Add (Mult (Cst (~ rn), Var 0), qh)))
  1522       else NOT (Divides
  1523                   (Cst pl,
  1524                     Add (Mult (Cst rn, Var (op_45_def0 sx id_1_def0 + 1)),
  1525                           qh))))
  1526   | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))) =
  1527     NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))
  1528   | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))) =
  1529     NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))
  1530   | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))) =
  1531     NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))
  1532   | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))) =
  1533     NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))
  1534   | mirror (NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))) =
  1535     NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))
  1536   | mirror (NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))) =
  1537     NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))
  1538   | mirror (NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))) =
  1539     NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))
  1540   | mirror (NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))) =
  1541     NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))
  1542   | mirror (NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))) =
  1543     NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))
  1544   | mirror (NOT (Divides (Cst pl, Sub (qi, qj)))) =
  1545     NOT (Divides (Cst pl, Sub (qi, qj)))
  1546   | mirror (NOT (Divides (Cst pl, Mult (qk, ql)))) =
  1547     NOT (Divides (Cst pl, Mult (qk, ql)))
  1548   | mirror (NOT (Divides (Var pm, lg))) = NOT (Divides (Var pm, lg))
  1549   | mirror (NOT (Divides (Neg pn, lg))) = NOT (Divides (Neg pn, lg))
  1550   | mirror (NOT (Divides (Add (po, pp), lg))) = NOT (Divides (Add (po, pp), lg))
  1551   | mirror (NOT (Divides (Sub (pq, pr), lg))) = NOT (Divides (Sub (pq, pr), lg))
  1552   | mirror (NOT (Divides (Mult (ps, pt), lg))) =
  1553     NOT (Divides (Mult (ps, pt), lg))
  1554   | mirror (NOT T) = NOT T
  1555   | mirror (NOT F) = NOT F
  1556   | mirror (NOT (NOT lh)) = NOT (NOT lh)
  1557   | mirror (NOT (And (li, lj))) = NOT (And (li, lj))
  1558   | mirror (NOT (Or (lk, ll))) = NOT (Or (lk, ll))
  1559   | mirror (NOT (Imp (lm, ln))) = NOT (Imp (lm, ln))
  1560   | mirror (NOT (Equ (lo, lp))) = NOT (Equ (lo, lp))
  1561   | mirror (NOT (QAll lq)) = NOT (QAll lq)
  1562   | mirror (NOT (QEx lr)) = NOT (QEx lr)
  1563   | mirror (Imp (am, an)) = Imp (am, an)
  1564   | mirror (Equ (ao, ap)) = Equ (ao, ap)
  1565   | mirror (QAll aq) = QAll aq
  1566   | mirror (QEx ar) = QEx ar;
  1567 
  1568 fun op_43_def0 m n = nat ((m) + (n));
  1569 
  1570 fun size_def1 [] = 0
  1571   | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
  1572 
  1573 fun aset (And (p, q)) = op_64 (aset p) (aset q)
  1574   | aset (Or (p, q)) = op_64 (aset p) (aset q)
  1575   | aset (Lt (u, v)) = []
  1576   | aset (Gt (w, x)) = []
  1577   | aset (Le (Cst bo, z)) = []
  1578   | aset (Le (Var bp, z)) = []
  1579   | aset (Le (Neg bq, z)) = []
  1580   | aset (Le (Add (Cst cg, bs), z)) = []
  1581   | aset (Le (Add (Var ch, bs), z)) = []
  1582   | aset (Le (Add (Neg ci, bs), z)) = []
  1583   | aset (Le (Add (Add (cj, ck), bs), z)) = []
  1584   | aset (Le (Add (Sub (cl, cm), bs), z)) = []
  1585   | aset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
  1586   | aset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
  1587     (if (ei = 0)
  1588       then (if (cy < 0) then [lin_add (bs, Cst 1)]
  1589              else [lin_neg bs, lin_add (lin_neg bs, Cst 1)])
  1590       else [])
  1591   | aset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = []
  1592   | aset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = []
  1593   | aset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = []
  1594   | aset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = []
  1595   | aset (Le (Add (Mult (Var cz, co), bs), z)) = []
  1596   | aset (Le (Add (Mult (Neg da, co), bs), z)) = []
  1597   | aset (Le (Add (Mult (Add (db, dc), co), bs), z)) = []
  1598   | aset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = []
  1599   | aset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = []
  1600   | aset (Le (Sub (bt, bu), z)) = []
  1601   | aset (Le (Mult (bv, bw), z)) = []
  1602   | aset (Ge (aa, ab)) = []
  1603   | aset (Eq (Cst ek, ad)) = []
  1604   | aset (Eq (Var el, ad)) = []
  1605   | aset (Eq (Neg em, ad)) = []
  1606   | aset (Eq (Add (Cst fc, eo), ad)) = []
  1607   | aset (Eq (Add (Var fd, eo), ad)) = []
  1608   | aset (Eq (Add (Neg fe, eo), ad)) = []
  1609   | aset (Eq (Add (Add (ff, fg), eo), ad)) = []
  1610   | aset (Eq (Add (Sub (fh, fi), eo), ad)) = []
  1611   | aset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = []
  1612   | aset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
  1613     (if (he = 0)
  1614       then (if (fu < 0) then [lin_add (eo, Cst 1)]
  1615              else [lin_add (lin_neg eo, Cst 1)])
  1616       else [])
  1617   | aset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = []
  1618   | aset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = []
  1619   | aset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = []
  1620   | aset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = []
  1621   | aset (Eq (Add (Mult (Var fv, fk), eo), ad)) = []
  1622   | aset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = []
  1623   | aset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = []
  1624   | aset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = []
  1625   | aset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = []
  1626   | aset (Eq (Sub (ep, eq), ad)) = []
  1627   | aset (Eq (Mult (er, es), ad)) = []
  1628   | aset (Divides (ae, af)) = []
  1629   | aset T = []
  1630   | aset F = []
  1631   | aset (NOT (Lt (hg, hh))) = []
  1632   | aset (NOT (Gt (hi, hj))) = []
  1633   | aset (NOT (Le (hk, hl))) = []
  1634   | aset (NOT (Ge (hm, hn))) = []
  1635   | aset (NOT (Eq (Cst ja, hp))) = []
  1636   | aset (NOT (Eq (Var jb, hp))) = []
  1637   | aset (NOT (Eq (Neg jc, hp))) = []
  1638   | aset (NOT (Eq (Add (Cst js, je), hp))) = []
  1639   | aset (NOT (Eq (Add (Var jt, je), hp))) = []
  1640   | aset (NOT (Eq (Add (Neg ju, je), hp))) = []
  1641   | aset (NOT (Eq (Add (Add (jv, jw), je), hp))) = []
  1642   | aset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = []
  1643   | aset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = []
  1644   | aset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
  1645     (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else [])
  1646   | aset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = []
  1647   | aset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = []
  1648   | aset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = []
  1649   | aset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = []
  1650   | aset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = []
  1651   | aset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = []
  1652   | aset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = []
  1653   | aset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = []
  1654   | aset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = []
  1655   | aset (NOT (Eq (Sub (jf, jg), hp))) = []
  1656   | aset (NOT (Eq (Mult (jh, ji), hp))) = []
  1657   | aset (NOT (Divides (hq, hr))) = []
  1658   | aset (NOT T) = []
  1659   | aset (NOT F) = []
  1660   | aset (NOT (NOT hs)) = []
  1661   | aset (NOT (And (ht, hu))) = []
  1662   | aset (NOT (Or (hv, hw))) = []
  1663   | aset (NOT (Imp (hx, hy))) = []
  1664   | aset (NOT (Equ (hz, ia))) = []
  1665   | aset (NOT (QAll ib)) = []
  1666   | aset (NOT (QEx ic)) = []
  1667   | aset (Imp (al, am)) = []
  1668   | aset (Equ (an, ao)) = []
  1669   | aset (QAll ap) = []
  1670   | aset (QEx aq) = [];
  1671 
  1672 fun op_mem x [] = false
  1673   | op_mem x (y :: ys) = (if (y = x) then true else op_mem x ys);
  1674 
  1675 fun list_insert x xs = (if op_mem x xs then xs else (x :: xs));
  1676 
  1677 fun list_set [] = []
  1678   | list_set (x :: xs) = list_insert x (list_set xs);
  1679 
  1680 fun bset (And (p, q)) = op_64 (bset p) (bset q)
  1681   | bset (Or (p, q)) = op_64 (bset p) (bset q)
  1682   | bset (Lt (u, v)) = []
  1683   | bset (Gt (w, x)) = []
  1684   | bset (Le (Cst bo, z)) = []
  1685   | bset (Le (Var bp, z)) = []
  1686   | bset (Le (Neg bq, z)) = []
  1687   | bset (Le (Add (Cst cg, bs), z)) = []
  1688   | bset (Le (Add (Var ch, bs), z)) = []
  1689   | bset (Le (Add (Neg ci, bs), z)) = []
  1690   | bset (Le (Add (Add (cj, ck), bs), z)) = []
  1691   | bset (Le (Add (Sub (cl, cm), bs), z)) = []
  1692   | bset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
  1693   | bset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
  1694     (if (ei = 0)
  1695       then (if (cy < 0) then [lin_add (bs, Cst ~1), bs]
  1696              else [lin_add (lin_neg bs, Cst ~1)])
  1697       else [])
  1698   | bset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = []
  1699   | bset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = []
  1700   | bset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = []
  1701   | bset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = []
  1702   | bset (Le (Add (Mult (Var cz, co), bs), z)) = []
  1703   | bset (Le (Add (Mult (Neg da, co), bs), z)) = []
  1704   | bset (Le (Add (Mult (Add (db, dc), co), bs), z)) = []
  1705   | bset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = []
  1706   | bset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = []
  1707   | bset (Le (Sub (bt, bu), z)) = []
  1708   | bset (Le (Mult (bv, bw), z)) = []
  1709   | bset (Ge (aa, ab)) = []
  1710   | bset (Eq (Cst ek, ad)) = []
  1711   | bset (Eq (Var el, ad)) = []
  1712   | bset (Eq (Neg em, ad)) = []
  1713   | bset (Eq (Add (Cst fc, eo), ad)) = []
  1714   | bset (Eq (Add (Var fd, eo), ad)) = []
  1715   | bset (Eq (Add (Neg fe, eo), ad)) = []
  1716   | bset (Eq (Add (Add (ff, fg), eo), ad)) = []
  1717   | bset (Eq (Add (Sub (fh, fi), eo), ad)) = []
  1718   | bset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = []
  1719   | bset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
  1720     (if (he = 0)
  1721       then (if (fu < 0) then [lin_add (eo, Cst ~1)]
  1722              else [lin_add (lin_neg eo, Cst ~1)])
  1723       else [])
  1724   | bset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = []
  1725   | bset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = []
  1726   | bset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = []
  1727   | bset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = []
  1728   | bset (Eq (Add (Mult (Var fv, fk), eo), ad)) = []
  1729   | bset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = []
  1730   | bset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = []
  1731   | bset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = []
  1732   | bset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = []
  1733   | bset (Eq (Sub (ep, eq), ad)) = []
  1734   | bset (Eq (Mult (er, es), ad)) = []
  1735   | bset (Divides (ae, af)) = []
  1736   | bset T = []
  1737   | bset F = []
  1738   | bset (NOT (Lt (hg, hh))) = []
  1739   | bset (NOT (Gt (hi, hj))) = []
  1740   | bset (NOT (Le (hk, hl))) = []
  1741   | bset (NOT (Ge (hm, hn))) = []
  1742   | bset (NOT (Eq (Cst ja, hp))) = []
  1743   | bset (NOT (Eq (Var jb, hp))) = []
  1744   | bset (NOT (Eq (Neg jc, hp))) = []
  1745   | bset (NOT (Eq (Add (Cst js, je), hp))) = []
  1746   | bset (NOT (Eq (Add (Var jt, je), hp))) = []
  1747   | bset (NOT (Eq (Add (Neg ju, je), hp))) = []
  1748   | bset (NOT (Eq (Add (Add (jv, jw), je), hp))) = []
  1749   | bset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = []
  1750   | bset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = []
  1751   | bset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
  1752     (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else [])
  1753   | bset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = []
  1754   | bset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = []
  1755   | bset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = []
  1756   | bset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = []
  1757   | bset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = []
  1758   | bset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = []
  1759   | bset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = []
  1760   | bset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = []
  1761   | bset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = []
  1762   | bset (NOT (Eq (Sub (jf, jg), hp))) = []
  1763   | bset (NOT (Eq (Mult (jh, ji), hp))) = []
  1764   | bset (NOT (Divides (hq, hr))) = []
  1765   | bset (NOT T) = []
  1766   | bset (NOT F) = []
  1767   | bset (NOT (NOT hs)) = []
  1768   | bset (NOT (And (ht, hu))) = []
  1769   | bset (NOT (Or (hv, hw))) = []
  1770   | bset (NOT (Imp (hx, hy))) = []
  1771   | bset (NOT (Equ (hz, ia))) = []
  1772   | bset (NOT (QAll ib)) = []
  1773   | bset (NOT (QEx ic)) = []
  1774   | bset (Imp (al, am)) = []
  1775   | bset (Equ (an, ao)) = []
  1776   | bset (QAll ap) = []
  1777   | bset (QEx aq) = [];
  1778 
  1779 fun adjustcoeff (l, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
  1780     (if (c <= 0)
  1781       then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)),
  1782                 Cst 0)
  1783       else Le (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0))
  1784   | adjustcoeff (l, Eq (Add (Mult (Cst c, Var 0), r), Cst i)) =
  1785     Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0)
  1786   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst c, Var 0), r), Cst i))) =
  1787     NOT (Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0))
  1788   | adjustcoeff (l, And (p, q)) = And (adjustcoeff (l, p), adjustcoeff (l, q))
  1789   | adjustcoeff (l, Or (p, q)) = Or (adjustcoeff (l, p), adjustcoeff (l, q))
  1790   | adjustcoeff (l, Lt (w, x)) = Lt (w, x)
  1791   | adjustcoeff (l, Gt (y, z)) = Gt (y, z)
  1792   | adjustcoeff (l, Le (Cst bq, ab)) = Le (Cst bq, ab)
  1793   | adjustcoeff (l, Le (Var br, ab)) = Le (Var br, ab)
  1794   | adjustcoeff (l, Le (Neg bs, ab)) = Le (Neg bs, ab)
  1795   | adjustcoeff (l, Le (Add (Cst ci, bu), ab)) = Le (Add (Cst ci, bu), ab)
  1796   | adjustcoeff (l, Le (Add (Var cj, bu), ab)) = Le (Add (Var cj, bu), ab)
  1797   | adjustcoeff (l, Le (Add (Neg ck, bu), ab)) = Le (Add (Neg ck, bu), ab)
  1798   | adjustcoeff (l, Le (Add (Add (cl, cm), bu), ab)) =
  1799     Le (Add (Add (cl, cm), bu), ab)
  1800   | adjustcoeff (l, Le (Add (Sub (cn, co), bu), ab)) =
  1801     Le (Add (Sub (cn, co), bu), ab)
  1802   | adjustcoeff (l, Le (Add (Mult (Cst da, Cst ds), bu), ab)) =
  1803     Le (Add (Mult (Cst da, Cst ds), bu), ab)
  1804   | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Var en)) =
  1805     Le (Add (Mult (Cst da, Var 0), bu), Var en)
  1806   | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Neg eo)) =
  1807     Le (Add (Mult (Cst da, Var 0), bu), Neg eo)
  1808   | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq))) =
  1809     Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq))
  1810   | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es))) =
  1811     Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es))
  1812   | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu))) =
  1813     Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu))
  1814   | adjustcoeff (l, Le (Add (Mult (Cst da, Var ek), bu), ab)) =
  1815     Le (Add (Mult (Cst da, Var ek), bu), ab)
  1816   | adjustcoeff (l, Le (Add (Mult (Cst da, Neg du), bu), ab)) =
  1817     Le (Add (Mult (Cst da, Neg du), bu), ab)
  1818   | adjustcoeff (l, Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab)) =
  1819     Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab)
  1820   | adjustcoeff (l, Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab)) =
  1821     Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab)
  1822   | adjustcoeff (l, Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab)) =
  1823     Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab)
  1824   | adjustcoeff (l, Le (Add (Mult (Var db, cq), bu), ab)) =
  1825     Le (Add (Mult (Var db, cq), bu), ab)
  1826   | adjustcoeff (l, Le (Add (Mult (Neg dc, cq), bu), ab)) =
  1827     Le (Add (Mult (Neg dc, cq), bu), ab)
  1828   | adjustcoeff (l, Le (Add (Mult (Add (dd, de), cq), bu), ab)) =
  1829     Le (Add (Mult (Add (dd, de), cq), bu), ab)
  1830   | adjustcoeff (l, Le (Add (Mult (Sub (df, dg), cq), bu), ab)) =
  1831     Le (Add (Mult (Sub (df, dg), cq), bu), ab)
  1832   | adjustcoeff (l, Le (Add (Mult (Mult (dh, di), cq), bu), ab)) =
  1833     Le (Add (Mult (Mult (dh, di), cq), bu), ab)
  1834   | adjustcoeff (l, Le (Sub (bv, bw), ab)) = Le (Sub (bv, bw), ab)
  1835   | adjustcoeff (l, Le (Mult (bx, by), ab)) = Le (Mult (bx, by), ab)
  1836   | adjustcoeff (l, Ge (ac, ad)) = Ge (ac, ad)
  1837   | adjustcoeff (l, Eq (Cst fe, af)) = Eq (Cst fe, af)
  1838   | adjustcoeff (l, Eq (Var ff, af)) = Eq (Var ff, af)
  1839   | adjustcoeff (l, Eq (Neg fg, af)) = Eq (Neg fg, af)
  1840   | adjustcoeff (l, Eq (Add (Cst fw, fi), af)) = Eq (Add (Cst fw, fi), af)
  1841   | adjustcoeff (l, Eq (Add (Var fx, fi), af)) = Eq (Add (Var fx, fi), af)
  1842   | adjustcoeff (l, Eq (Add (Neg fy, fi), af)) = Eq (Add (Neg fy, fi), af)
  1843   | adjustcoeff (l, Eq (Add (Add (fz, ga), fi), af)) =
  1844     Eq (Add (Add (fz, ga), fi), af)
  1845   | adjustcoeff (l, Eq (Add (Sub (gb, gc), fi), af)) =
  1846     Eq (Add (Sub (gb, gc), fi), af)
  1847   | adjustcoeff (l, Eq (Add (Mult (Cst go, Cst hg), fi), af)) =
  1848     Eq (Add (Mult (Cst go, Cst hg), fi), af)
  1849   | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Var ib)) =
  1850     Eq (Add (Mult (Cst go, Var 0), fi), Var ib)
  1851   | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Neg ic)) =
  1852     Eq (Add (Mult (Cst go, Var 0), fi), Neg ic)
  1853   | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie))) =
  1854     Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie))
  1855   | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig))) =
  1856     Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig))
  1857   | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii))) =
  1858     Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii))
  1859   | adjustcoeff (l, Eq (Add (Mult (Cst go, Var hy), fi), af)) =
  1860     Eq (Add (Mult (Cst go, Var hy), fi), af)
  1861   | adjustcoeff (l, Eq (Add (Mult (Cst go, Neg hi), fi), af)) =
  1862     Eq (Add (Mult (Cst go, Neg hi), fi), af)
  1863   | adjustcoeff (l, Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af)) =
  1864     Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af)
  1865   | adjustcoeff (l, Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af)) =
  1866     Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af)
  1867   | adjustcoeff (l, Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af)) =
  1868     Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af)
  1869   | adjustcoeff (l, Eq (Add (Mult (Var gp, ge), fi), af)) =
  1870     Eq (Add (Mult (Var gp, ge), fi), af)
  1871   | adjustcoeff (l, Eq (Add (Mult (Neg gq, ge), fi), af)) =
  1872     Eq (Add (Mult (Neg gq, ge), fi), af)
  1873   | adjustcoeff (l, Eq (Add (Mult (Add (gr, gs), ge), fi), af)) =
  1874     Eq (Add (Mult (Add (gr, gs), ge), fi), af)
  1875   | adjustcoeff (l, Eq (Add (Mult (Sub (gt, gu), ge), fi), af)) =
  1876     Eq (Add (Mult (Sub (gt, gu), ge), fi), af)
  1877   | adjustcoeff (l, Eq (Add (Mult (Mult (gv, gw), ge), fi), af)) =
  1878     Eq (Add (Mult (Mult (gv, gw), ge), fi), af)
  1879   | adjustcoeff (l, Eq (Sub (fj, fk), af)) = Eq (Sub (fj, fk), af)
  1880   | adjustcoeff (l, Eq (Mult (fl, fm), af)) = Eq (Mult (fl, fm), af)
  1881   | adjustcoeff (l, Divides (Cst is, Cst jk)) = Divides (Cst is, Cst jk)
  1882   | adjustcoeff (l, Divides (Cst is, Var jl)) = Divides (Cst is, Var jl)
  1883   | adjustcoeff (l, Divides (Cst is, Neg jm)) = Divides (Cst is, Neg jm)
  1884   | adjustcoeff (l, Divides (Cst is, Add (Cst kc, jo))) =
  1885     Divides (Cst is, Add (Cst kc, jo))
  1886   | adjustcoeff (l, Divides (Cst is, Add (Var kd, jo))) =
  1887     Divides (Cst is, Add (Var kd, jo))
  1888   | adjustcoeff (l, Divides (Cst is, Add (Neg ke, jo))) =
  1889     Divides (Cst is, Add (Neg ke, jo))
  1890   | adjustcoeff (l, Divides (Cst is, Add (Add (kf, kg), jo))) =
  1891     Divides (Cst is, Add (Add (kf, kg), jo))
  1892   | adjustcoeff (l, Divides (Cst is, Add (Sub (kh, ki), jo))) =
  1893     Divides (Cst is, Add (Sub (kh, ki), jo))
  1894   | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo))) =
  1895     Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo))
  1896   | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Var me), jo))) =
  1897     (if (me = 0)
  1898       then Divides
  1899              (Cst (op_div_def1 l ku * is),
  1900                Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l ku, jo)))
  1901       else Divides
  1902              (Cst is,
  1903                Add (Mult (Cst ku, Var (op_45_def0 me id_1_def0 + 1)), jo)))
  1904   | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo))) =
  1905     Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo))
  1906   | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo))) =
  1907     Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo))
  1908   | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo))) =
  1909     Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo))
  1910   | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo))) =
  1911     Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo))
  1912   | adjustcoeff (l, Divides (Cst is, Add (Mult (Var kv, kk), jo))) =
  1913     Divides (Cst is, Add (Mult (Var kv, kk), jo))
  1914   | adjustcoeff (l, Divides (Cst is, Add (Mult (Neg kw, kk), jo))) =
  1915     Divides (Cst is, Add (Mult (Neg kw, kk), jo))
  1916   | adjustcoeff (l, Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo))) =
  1917     Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo))
  1918   | adjustcoeff (l, Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo))) =
  1919     Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo))
  1920   | adjustcoeff (l, Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo))) =
  1921     Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo))
  1922   | adjustcoeff (l, Divides (Cst is, Sub (jp, jq))) =
  1923     Divides (Cst is, Sub (jp, jq))
  1924   | adjustcoeff (l, Divides (Cst is, Mult (jr, js))) =
  1925     Divides (Cst is, Mult (jr, js))
  1926   | adjustcoeff (l, Divides (Var it, ah)) = Divides (Var it, ah)
  1927   | adjustcoeff (l, Divides (Neg iu, ah)) = Divides (Neg iu, ah)
  1928   | adjustcoeff (l, Divides (Add (iv, iw), ah)) = Divides (Add (iv, iw), ah)
  1929   | adjustcoeff (l, Divides (Sub (ix, iy), ah)) = Divides (Sub (ix, iy), ah)
  1930   | adjustcoeff (l, Divides (Mult (iz, ja), ah)) = Divides (Mult (iz, ja), ah)
  1931   | adjustcoeff (l, T) = T
  1932   | adjustcoeff (l, F) = F
  1933   | adjustcoeff (l, NOT (Lt (mg, mh))) = NOT (Lt (mg, mh))
  1934   | adjustcoeff (l, NOT (Gt (mi, mj))) = NOT (Gt (mi, mj))
  1935   | adjustcoeff (l, NOT (Le (mk, ml))) = NOT (Le (mk, ml))
  1936   | adjustcoeff (l, NOT (Ge (mm, mn))) = NOT (Ge (mm, mn))
  1937   | adjustcoeff (l, NOT (Eq (Cst oa, mp))) = NOT (Eq (Cst oa, mp))
  1938   | adjustcoeff (l, NOT (Eq (Var ob, mp))) = NOT (Eq (Var ob, mp))
  1939   | adjustcoeff (l, NOT (Eq (Neg oc, mp))) = NOT (Eq (Neg oc, mp))
  1940   | adjustcoeff (l, NOT (Eq (Add (Cst os, oe), mp))) =
  1941     NOT (Eq (Add (Cst os, oe), mp))
  1942   | adjustcoeff (l, NOT (Eq (Add (Var ot, oe), mp))) =
  1943     NOT (Eq (Add (Var ot, oe), mp))
  1944   | adjustcoeff (l, NOT (Eq (Add (Neg ou, oe), mp))) =
  1945     NOT (Eq (Add (Neg ou, oe), mp))
  1946   | adjustcoeff (l, NOT (Eq (Add (Add (ov, ow), oe), mp))) =
  1947     NOT (Eq (Add (Add (ov, ow), oe), mp))
  1948   | adjustcoeff (l, NOT (Eq (Add (Sub (ox, oy), oe), mp))) =
  1949     NOT (Eq (Add (Sub (ox, oy), oe), mp))
  1950   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp))) =
  1951     NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp))
  1952   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx))) =
  1953     NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx))
  1954   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy))) =
  1955     NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy))
  1956   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra)))) =
  1957     NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra)))
  1958   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc)))) =
  1959     NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc)))
  1960   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re)))) =
  1961     NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re)))
  1962   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp))) =
  1963     NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp))
  1964   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp))) =
  1965     NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp))
  1966   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp))) =
  1967     NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp))
  1968   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp))) =
  1969     NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp))
  1970   | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp))) =
  1971     NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp))
  1972   | adjustcoeff (l, NOT (Eq (Add (Mult (Var pl, pa), oe), mp))) =
  1973     NOT (Eq (Add (Mult (Var pl, pa), oe), mp))
  1974   | adjustcoeff (l, NOT (Eq (Add (Mult (Neg pm, pa), oe), mp))) =
  1975     NOT (Eq (Add (Mult (Neg pm, pa), oe), mp))
  1976   | adjustcoeff (l, NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp))) =
  1977     NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp))
  1978   | adjustcoeff (l, NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp))) =
  1979     NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp))
  1980   | adjustcoeff (l, NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp))) =
  1981     NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp))
  1982   | adjustcoeff (l, NOT (Eq (Sub (of', og), mp))) = NOT (Eq (Sub (of', og), mp))
  1983   | adjustcoeff (l, NOT (Eq (Mult (oh, oi), mp))) = NOT (Eq (Mult (oh, oi), mp))
  1984   | adjustcoeff (l, NOT (Divides (Cst ro, Cst sg))) =
  1985     NOT (Divides (Cst ro, Cst sg))
  1986   | adjustcoeff (l, NOT (Divides (Cst ro, Var sh))) =
  1987     NOT (Divides (Cst ro, Var sh))
  1988   | adjustcoeff (l, NOT (Divides (Cst ro, Neg si))) =
  1989     NOT (Divides (Cst ro, Neg si))
  1990   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Cst sy, sk)))) =
  1991     NOT (Divides (Cst ro, Add (Cst sy, sk)))
  1992   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Var sz, sk)))) =
  1993     NOT (Divides (Cst ro, Add (Var sz, sk)))
  1994   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Neg ta, sk)))) =
  1995     NOT (Divides (Cst ro, Add (Neg ta, sk)))
  1996   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Add (tb, tc), sk)))) =
  1997     NOT (Divides (Cst ro, Add (Add (tb, tc), sk)))
  1998   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Sub (td, te), sk)))) =
  1999     NOT (Divides (Cst ro, Add (Sub (td, te), sk)))
  2000   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk)))) =
  2001     NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk)))
  2002   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Var va), sk)))) =
  2003     (if (va = 0)
  2004       then NOT (Divides
  2005                   (Cst (op_div_def1 l tq * ro),
  2006                     Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l tq, sk))))
  2007       else NOT (Divides
  2008                   (Cst ro,
  2009                     Add (Mult (Cst tq, Var (op_45_def0 va id_1_def0 + 1)),
  2010                           sk))))
  2011   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk)))) =
  2012     NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk)))
  2013   | adjustcoeff
  2014       (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk)))) =
  2015     NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk)))
  2016   | adjustcoeff
  2017       (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk)))) =
  2018     NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk)))
  2019   | adjustcoeff
  2020       (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk)))) =
  2021     NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk)))
  2022   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk)))) =
  2023     NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk)))
  2024   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk)))) =
  2025     NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk)))
  2026   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk)))) =
  2027     NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk)))
  2028   | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk)))) =
  2029     NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk)))
  2030   | adjustcoeff
  2031       (l, NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk)))) =
  2032     NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk)))
  2033   | adjustcoeff (l, NOT (Divides (Cst ro, Sub (sl, sm)))) =
  2034     NOT (Divides (Cst ro, Sub (sl, sm)))
  2035   | adjustcoeff (l, NOT (Divides (Cst ro, Mult (sn, so)))) =
  2036     NOT (Divides (Cst ro, Mult (sn, so)))
  2037   | adjustcoeff (l, NOT (Divides (Var rp, mr))) = NOT (Divides (Var rp, mr))
  2038   | adjustcoeff (l, NOT (Divides (Neg rq, mr))) = NOT (Divides (Neg rq, mr))
  2039   | adjustcoeff (l, NOT (Divides (Add (rr, rs), mr))) =
  2040     NOT (Divides (Add (rr, rs), mr))
  2041   | adjustcoeff (l, NOT (Divides (Sub (rt, ru), mr))) =
  2042     NOT (Divides (Sub (rt, ru), mr))
  2043   | adjustcoeff (l, NOT (Divides (Mult (rv, rw), mr))) =
  2044     NOT (Divides (Mult (rv, rw), mr))
  2045   | adjustcoeff (l, NOT T) = NOT T
  2046   | adjustcoeff (l, NOT F) = NOT F
  2047   | adjustcoeff (l, NOT (NOT ms)) = NOT (NOT ms)
  2048   | adjustcoeff (l, NOT (And (mt, mu))) = NOT (And (mt, mu))
  2049   | adjustcoeff (l, NOT (Or (mv, mw))) = NOT (Or (mv, mw))
  2050   | adjustcoeff (l, NOT (Imp (mx, my))) = NOT (Imp (mx, my))
  2051   | adjustcoeff (l, NOT (Equ (mz, na))) = NOT (Equ (mz, na))
  2052   | adjustcoeff (l, NOT (QAll nb)) = NOT (QAll nb)
  2053   | adjustcoeff (l, NOT (QEx nc)) = NOT (QEx nc)
  2054   | adjustcoeff (l, Imp (an, ao)) = Imp (an, ao)
  2055   | adjustcoeff (l, Equ (ap, aq)) = Equ (ap, aq)
  2056   | adjustcoeff (l, QAll ar) = QAll ar
  2057   | adjustcoeff (l, QEx as') = QEx as';
  2058 
  2059 fun formlcm (Le (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c
  2060   | formlcm (Eq (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c
  2061   | formlcm (NOT p) = formlcm p
  2062   | formlcm (And (p, q)) = ilcm (formlcm p) (formlcm q)
  2063   | formlcm (Or (p, q)) = ilcm (formlcm p) (formlcm q)
  2064   | formlcm (Lt (u, v)) = 1
  2065   | formlcm (Gt (w, x)) = 1
  2066   | formlcm (Le (Cst bo, z)) = 1
  2067   | formlcm (Le (Var bp, z)) = 1
  2068   | formlcm (Le (Neg bq, z)) = 1
  2069   | formlcm (Le (Add (Cst cg, bs), z)) = 1
  2070   | formlcm (Le (Add (Var ch, bs), z)) = 1
  2071   | formlcm (Le (Add (Neg ci, bs), z)) = 1
  2072   | formlcm (Le (Add (Add (cj, ck), bs), z)) = 1
  2073   | formlcm (Le (Add (Sub (cl, cm), bs), z)) = 1
  2074   | formlcm (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = 1
  2075   | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Var el)) = 1
  2076   | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Neg em)) = 1
  2077   | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Add (en, eo))) = 1
  2078   | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Sub (ep, eq))) = 1
  2079   | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Mult (er, es))) = 1
  2080   | formlcm (Le (Add (Mult (Cst cy, Var ei ), bs), z)) = 1
  2081   | formlcm (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = 1
  2082   | formlcm (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = 1
  2083   | formlcm (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = 1
  2084   | formlcm (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = 1
  2085   | formlcm (Le (Add (Mult (Var cz, co), bs), z)) = 1
  2086   | formlcm (Le (Add (Mult (Neg da, co), bs), z)) = 1
  2087   | formlcm (Le (Add (Mult (Add (db, dc), co), bs), z)) = 1
  2088   | formlcm (Le (Add (Mult (Sub (dd, de), co), bs), z)) = 1
  2089   | formlcm (Le (Add (Mult (Mult (df, dg), co), bs), z)) = 1
  2090   | formlcm (Le (Sub (bt, bu), z)) = 1
  2091   | formlcm (Le (Mult (bv, bw), z)) = 1
  2092   | formlcm (Ge (aa, ab)) = 1
  2093   | formlcm (Eq (Cst fc, ad)) = 1
  2094   | formlcm (Eq (Var fd, ad)) = 1
  2095   | formlcm (Eq (Neg fe, ad)) = 1
  2096   | formlcm (Eq (Add (Cst fu, fg), ad)) = 1
  2097   | formlcm (Eq (Add (Var fv, fg), ad)) = 1
  2098   | formlcm (Eq (Add (Neg fw, fg), ad)) = 1
  2099   | formlcm (Eq (Add (Add (fx, fy), fg), ad)) = 1
  2100   | formlcm (Eq (Add (Sub (fz, ga), fg), ad)) = 1
  2101   | formlcm (Eq (Add (Mult (Cst gm, Cst he), fg), ad)) = 1
  2102   | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Var hz)) = 1
  2103   | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Neg ia)) = 1
  2104   | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Add (ib, ic))) = 1
  2105   | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Sub (id, ie))) = 1
  2106   | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Mult (if', ig))) = 1
  2107   | formlcm (Eq (Add (Mult (Cst gm, Var hw), fg), ad)) = 1
  2108   | formlcm (Eq (Add (Mult (Cst gm, Neg hg), fg), ad)) = 1
  2109   | formlcm (Eq (Add (Mult (Cst gm, Add (hh, hi)), fg), ad)) = 1
  2110   | formlcm (Eq (Add (Mult (Cst gm, Sub (hj, hk)), fg), ad)) = 1
  2111   | formlcm (Eq (Add (Mult (Cst gm, Mult (hl, hm)), fg), ad)) = 1
  2112   | formlcm (Eq (Add (Mult (Var gn, gc), fg), ad)) = 1
  2113   | formlcm (Eq (Add (Mult (Neg go, gc), fg), ad)) = 1
  2114   | formlcm (Eq (Add (Mult (Add (gp, gq), gc), fg), ad)) = 1
  2115   | formlcm (Eq (Add (Mult (Sub (gr, gs), gc), fg), ad)) = 1
  2116   | formlcm (Eq (Add (Mult (Mult (gt, gu), gc), fg), ad)) = 1
  2117   | formlcm (Eq (Sub (fh, fi), ad)) = 1
  2118   | formlcm (Eq (Mult (fj, fk), ad)) = 1
  2119   | formlcm (Divides (Cst iq, Cst ji)) = 1
  2120   | formlcm (Divides (Cst iq, Var jj)) = 1
  2121   | formlcm (Divides (Cst iq, Neg jk)) = 1
  2122   | formlcm (Divides (Cst iq, Add (Cst ka, jm))) = 1
  2123   | formlcm (Divides (Cst iq, Add (Var kb, jm))) = 1
  2124   | formlcm (Divides (Cst iq, Add (Neg kc, jm))) = 1
  2125   | formlcm (Divides (Cst iq, Add (Add (kd, ke), jm))) = 1
  2126   | formlcm (Divides (Cst iq, Add (Sub (kf, kg), jm))) = 1
  2127   | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Cst lk), jm))) = 1
  2128   | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Var mc), jm))) =
  2129     (if (mc = 0) then abs ks else 1)
  2130   | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Neg lm), jm))) = 1
  2131   | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Add (ln, lo)), jm))) = 1
  2132   | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Sub (lp, lq)), jm))) = 1
  2133   | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Mult (lr, ls)), jm))) = 1
  2134   | formlcm (Divides (Cst iq, Add (Mult (Var kt, ki), jm))) = 1
  2135   | formlcm (Divides (Cst iq, Add (Mult (Neg ku, ki), jm))) = 1
  2136   | formlcm (Divides (Cst iq, Add (Mult (Add (kv, kw), ki), jm))) = 1
  2137   | formlcm (Divides (Cst iq, Add (Mult (Sub (kx, ky), ki), jm))) = 1
  2138   | formlcm (Divides (Cst iq, Add (Mult (Mult (kz, la), ki), jm))) = 1
  2139   | formlcm (Divides (Cst iq, Sub (jn, jo))) = 1
  2140   | formlcm (Divides (Cst iq, Mult (jp, jq))) = 1
  2141   | formlcm (Divides (Var ir, af)) = 1
  2142   | formlcm (Divides (Neg is, af)) = 1
  2143   | formlcm (Divides (Add (it, iu), af)) = 1
  2144   | formlcm (Divides (Sub (iv, iw), af)) = 1
  2145   | formlcm (Divides (Mult (ix, iy), af)) = 1
  2146   | formlcm T = 1
  2147   | formlcm F = 1
  2148   | formlcm (Imp (al, am)) = 1
  2149   | formlcm (Equ (an, ao)) = 1
  2150   | formlcm (QAll ap) = 1
  2151   | formlcm (QEx aq) = 1;
  2152 
  2153 fun unitycoeff p =
  2154   let val l = formlcm p; val p' = adjustcoeff (l, p)
  2155   in (if (l = 1) then p'
  2156        else And (Divides (Cst l, Add (Mult (Cst 1, Var 0), Cst 0)), p'))
  2157   end;
  2158 
  2159 fun unify p =
  2160   let val q = unitycoeff p; val B = list_set (bset q); val A = list_set (aset q)
  2161   in (if op_60_61_def0 (size_def1 B) (size_def1 A) then (q, B)
  2162        else (mirror q, map lin_neg A))
  2163   end;
  2164 
  2165 fun cooper p =
  2166   lift_un (fn q => decrvars (explode_minf (unify q))) (linform (nnf p));
  2167 
  2168 fun pa p = lift_un psimpl (qelim (cooper, p));
  2169 
  2170 val test = pa;
  2171 
  2172 end;