src/HOL/Integ/reflected_presburger.ML
changeset 17378 105519771c67
child 17390 df2b53a66937
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/reflected_presburger.ML	Wed Sep 14 17:25:52 2005 +0200
     1.3 @@ -0,0 +1,2172 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6 +    (* Caution: This file should not be modified. *)
     1.7 +    (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
     1.8 +fun nat i = if i < 0 then 0 else i;
     1.9 +structure Generated =
    1.10 +struct
    1.11 +
    1.12 +datatype intterm = Cst of int | Var of int | Neg of intterm
    1.13 +  | Add of intterm * intterm | Sub of intterm * intterm
    1.14 +  | Mult of intterm * intterm;
    1.15 +
    1.16 +datatype QF = Lt of intterm * intterm | Gt of intterm * intterm
    1.17 +  | Le of intterm * intterm | Ge of intterm * intterm | Eq of intterm * intterm
    1.18 +  | Divides of intterm * intterm | T | F | NOT of QF | And of QF * QF
    1.19 +  | Or of QF * QF | Imp of QF * QF | Equ of QF * QF | QAll of QF | QEx of QF;
    1.20 +
    1.21 +datatype 'a option = None | Some of 'a;
    1.22 +
    1.23 +fun lift_un c None = None
    1.24 +  | lift_un c (Some p) = Some (c p);
    1.25 +
    1.26 +fun lift_bin (c, (Some a, Some b)) = Some (c a b)
    1.27 +  | lift_bin (c, (None, y)) = None
    1.28 +  | lift_bin (c, (Some y, None)) = None;
    1.29 +
    1.30 +fun lift_qe qe None = None
    1.31 +  | lift_qe qe (Some p) = qe p;
    1.32 +
    1.33 +fun qelim (qe, QAll p) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe, p))))
    1.34 +  | qelim (qe, QEx p) = lift_qe qe (qelim (qe, p))
    1.35 +  | qelim (qe, And (p, q)) =
    1.36 +    lift_bin ((fn x => fn xa => And (x, xa)), (qelim (qe, p), qelim (qe, q)))
    1.37 +  | qelim (qe, Or (p, q)) =
    1.38 +    lift_bin ((fn x => fn xa => Or (x, xa)), (qelim (qe, p), qelim (qe, q)))
    1.39 +  | qelim (qe, Imp (p, q)) =
    1.40 +    lift_bin ((fn x => fn xa => Imp (x, xa)), (qelim (qe, p), qelim (qe, q)))
    1.41 +  | qelim (qe, Equ (p, q)) =
    1.42 +    lift_bin ((fn x => fn xa => Equ (x, xa)), (qelim (qe, p), qelim (qe, q)))
    1.43 +  | qelim (qe, NOT p) = lift_un NOT (qelim (qe, p))
    1.44 +  | qelim (qe, Lt (w, x)) = Some (Lt (w, x))
    1.45 +  | qelim (qe, Gt (y, z)) = Some (Gt (y, z))
    1.46 +  | qelim (qe, Le (aa, ab)) = Some (Le (aa, ab))
    1.47 +  | qelim (qe, Ge (ac, ad)) = Some (Ge (ac, ad))
    1.48 +  | qelim (qe, Eq (ae, af)) = Some (Eq (ae, af))
    1.49 +  | qelim (qe, Divides (ag, ah)) = Some (Divides (ag, ah))
    1.50 +  | qelim (qe, T) = Some T
    1.51 +  | qelim (qe, F) = Some F;
    1.52 +
    1.53 +fun lin_mul (c, Cst i) = Cst (c * i)
    1.54 +  | lin_mul (c, Add (Mult (Cst c', Var n), r)) =
    1.55 +    (if (c = 0) then Cst 0
    1.56 +      else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
    1.57 +
    1.58 +fun op_60_def0 m n = ((m) < (n));
    1.59 +
    1.60 +fun op_60_61_def0 m n = not (op_60_def0 n m);
    1.61 +
    1.62 +fun lin_add (Add (Mult (Cst c1, Var n1), r1), Add (Mult (Cst c2, Var n2), r2)) =
    1.63 +    (if (n1 = n2)
    1.64 +      then let val c = Cst (c1 + c2)
    1.65 +           in (if ((c1 + c2) = 0) then lin_add (r1, r2)
    1.66 +                else Add (Mult (c, Var n1), lin_add (r1, r2)))
    1.67 +           end
    1.68 +      else (if op_60_61_def0 n1 n2
    1.69 +             then Add (Mult (Cst c1, Var n1),
    1.70 +                        lin_add (r1, Add (Mult (Cst c2, Var n2), r2)))
    1.71 +             else Add (Mult (Cst c2, Var n2),
    1.72 +                        lin_add (Add (Mult (Cst c1, Var n1), r1), r2))))
    1.73 +  | lin_add (Add (Mult (Cst c1, Var n1), r1), Cst b) =
    1.74 +    Add (Mult (Cst c1, Var n1), lin_add (r1, Cst b))
    1.75 +  | lin_add (Cst x, Add (Mult (Cst c2, Var n2), r2)) =
    1.76 +    Add (Mult (Cst c2, Var n2), lin_add (Cst x, r2))
    1.77 +  | lin_add (Cst b1, Cst b2) = Cst (b1 + b2);
    1.78 +
    1.79 +fun lin_neg i = lin_mul (~1, i);
    1.80 +
    1.81 +fun linearize (Cst b) = Some (Cst b)
    1.82 +  | linearize (Var n) = Some (Add (Mult (Cst 1, Var n), Cst 0))
    1.83 +  | linearize (Neg i) = lift_un lin_neg (linearize i)
    1.84 +  | linearize (Add (i, j)) =
    1.85 +    lift_bin ((fn x => fn y => lin_add (x, y)), (linearize i, linearize j))
    1.86 +  | linearize (Sub (i, j)) =
    1.87 +    lift_bin
    1.88 +      ((fn x => fn y => lin_add (x, lin_neg y)), (linearize i, linearize j))
    1.89 +  | linearize (Mult (i, j)) =
    1.90 +    (case linearize i of None => None
    1.91 +      | Some x =>
    1.92 +          (case x of
    1.93 +            Cst xa =>
    1.94 +              (case linearize j of None => None
    1.95 +                | Some x => Some (lin_mul (xa, x)))
    1.96 +            | Var xa =>
    1.97 +                (case linearize j of None => None
    1.98 +                  | Some xa =>
    1.99 +                      (case xa of Cst xa => Some (lin_mul (xa, x))
   1.100 +                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
   1.101 +                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
   1.102 +            | Neg xa =>
   1.103 +                (case linearize j of None => None
   1.104 +                  | Some xa =>
   1.105 +                      (case xa of Cst xa => Some (lin_mul (xa, x))
   1.106 +                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
   1.107 +                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
   1.108 +            | Add (xa, xb) =>
   1.109 +                (case linearize j of None => None
   1.110 +                  | Some xa =>
   1.111 +                      (case xa of Cst xa => Some (lin_mul (xa, x))
   1.112 +                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
   1.113 +                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
   1.114 +            | Sub (xa, xb) =>
   1.115 +                (case linearize j of None => None
   1.116 +                  | Some xa =>
   1.117 +                      (case xa of Cst xa => Some (lin_mul (xa, x))
   1.118 +                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
   1.119 +                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
   1.120 +            | Mult (xa, xb) =>
   1.121 +                (case linearize j of None => None
   1.122 +                  | Some xa =>
   1.123 +                      (case xa of Cst xa => Some (lin_mul (xa, x))
   1.124 +                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
   1.125 +                        | Sub (xa, xb) => None | Mult (xa, xb) => None))));
   1.126 +
   1.127 +fun linform (Le (it1, it2)) =
   1.128 +    lift_bin
   1.129 +      ((fn x => fn y => Le (lin_add (x, lin_neg y), Cst 0)),
   1.130 +        (linearize it1, linearize it2))
   1.131 +  | linform (Eq (it1, it2)) =
   1.132 +    lift_bin
   1.133 +      ((fn x => fn y => Eq (lin_add (x, lin_neg y), Cst 0)),
   1.134 +        (linearize it1, linearize it2))
   1.135 +  | linform (Divides (d, t)) =
   1.136 +    (case linearize d of None => None
   1.137 +      | Some x =>
   1.138 +          (case x of
   1.139 +            Cst xa =>
   1.140 +              (if (xa = 0) then None
   1.141 +                else (case linearize t of None => None
   1.142 +                       | Some xa => Some (Divides (x, xa))))
   1.143 +            | Var xa => None | Neg xa => None | Add (xa, xb) => None
   1.144 +            | Sub (xa, xb) => None | Mult (xa, xb) => None))
   1.145 +  | linform T = Some T
   1.146 +  | linform F = Some F
   1.147 +  | linform (NOT p) = lift_un NOT (linform p)
   1.148 +  | linform (And (p, q)) =
   1.149 +    lift_bin ((fn f => fn g => And (f, g)), (linform p, linform q))
   1.150 +  | linform (Or (p, q)) =
   1.151 +    lift_bin ((fn f => fn g => Or (f, g)), (linform p, linform q));
   1.152 +
   1.153 +fun nnf (Lt (it1, it2)) = Le (Sub (it1, it2), Cst (~ 1))
   1.154 +  | nnf (Gt (it1, it2)) = Le (Sub (it2, it1), Cst (~ 1))
   1.155 +  | nnf (Le (it1, it2)) = Le (it1, it2)
   1.156 +  | nnf (Ge (it1, it2)) = Le (it2, it1)
   1.157 +  | nnf (Eq (it1, it2)) = Eq (it2, it1)
   1.158 +  | nnf (Divides (d, t)) = Divides (d, t)
   1.159 +  | nnf T = T
   1.160 +  | nnf F = F
   1.161 +  | nnf (And (p, q)) = And (nnf p, nnf q)
   1.162 +  | nnf (Or (p, q)) = Or (nnf p, nnf q)
   1.163 +  | nnf (Imp (p, q)) = Or (nnf (NOT p), nnf q)
   1.164 +  | nnf (Equ (p, q)) = Or (And (nnf p, nnf q), And (nnf (NOT p), nnf (NOT q)))
   1.165 +  | nnf (NOT (Lt (it1, it2))) = Le (it2, it1)
   1.166 +  | nnf (NOT (Gt (it1, it2))) = Le (it1, it2)
   1.167 +  | nnf (NOT (Le (it1, it2))) = Le (Sub (it2, it1), Cst (~ 1))
   1.168 +  | nnf (NOT (Ge (it1, it2))) = Le (Sub (it1, it2), Cst (~ 1))
   1.169 +  | nnf (NOT (Eq (it1, it2))) = NOT (Eq (it1, it2))
   1.170 +  | nnf (NOT (Divides (d, t))) = NOT (Divides (d, t))
   1.171 +  | nnf (NOT T) = F
   1.172 +  | nnf (NOT F) = T
   1.173 +  | nnf (NOT (NOT p)) = nnf p
   1.174 +  | nnf (NOT (And (p, q))) = Or (nnf (NOT p), nnf (NOT q))
   1.175 +  | nnf (NOT (Or (p, q))) = And (nnf (NOT p), nnf (NOT q))
   1.176 +  | nnf (NOT (Imp (p, q))) = And (nnf p, nnf (NOT q))
   1.177 +  | nnf (NOT (Equ (p, q))) =
   1.178 +    Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
   1.179 +
   1.180 +fun op_45_def2 z w = (z + ~ w);
   1.181 +
   1.182 +fun op_45_def0 m n = nat (op_45_def2 (m) (n));
   1.183 +
   1.184 +val id_1_def0 : int = (0 + 1);
   1.185 +
   1.186 +fun decrvarsI (Cst i) = Cst i
   1.187 +  | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
   1.188 +  | decrvarsI (Neg a) = Neg (decrvarsI a)
   1.189 +  | decrvarsI (Add (a, b)) = Add (decrvarsI a, decrvarsI b)
   1.190 +  | decrvarsI (Sub (a, b)) = Sub (decrvarsI a, decrvarsI b)
   1.191 +  | decrvarsI (Mult (a, b)) = Mult (decrvarsI a, decrvarsI b);
   1.192 +
   1.193 +fun decrvars (Lt (a, b)) = Lt (decrvarsI a, decrvarsI b)
   1.194 +  | decrvars (Gt (a, b)) = Gt (decrvarsI a, decrvarsI b)
   1.195 +  | decrvars (Le (a, b)) = Le (decrvarsI a, decrvarsI b)
   1.196 +  | decrvars (Ge (a, b)) = Ge (decrvarsI a, decrvarsI b)
   1.197 +  | decrvars (Eq (a, b)) = Eq (decrvarsI a, decrvarsI b)
   1.198 +  | decrvars (Divides (a, b)) = Divides (decrvarsI a, decrvarsI b)
   1.199 +  | decrvars T = T
   1.200 +  | decrvars F = F
   1.201 +  | decrvars (NOT p) = NOT (decrvars p)
   1.202 +  | decrvars (And (p, q)) = And (decrvars p, decrvars q)
   1.203 +  | decrvars (Or (p, q)) = Or (decrvars p, decrvars q)
   1.204 +  | decrvars (Imp (p, q)) = Imp (decrvars p, decrvars q)
   1.205 +  | decrvars (Equ (p, q)) = Equ (decrvars p, decrvars q);
   1.206 +
   1.207 +fun op_64 [] ys = ys
   1.208 +  | op_64 (x :: xs) ys = (x :: op_64 xs ys);
   1.209 +
   1.210 +fun map f [] = []
   1.211 +  | map f (x :: xs) = (f x :: map f xs);
   1.212 +
   1.213 +fun iupto (i, j) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
   1.214 +
   1.215 +fun all_sums (j, []) = []
   1.216 +  | all_sums (j, (i :: is)) =
   1.217 +    op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
   1.218 +
   1.219 +fun split x = (fn p => x (fst p) (snd p));
   1.220 +
   1.221 +fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
   1.222 +
   1.223 +fun adjust b =
   1.224 +  (fn (q, r) =>
   1.225 +    (if (0 <= op_45_def2 r b) then (((2 * q) + 1), op_45_def2 r b)
   1.226 +      else ((2 * q), r)));
   1.227 +
   1.228 +fun negDivAlg (a, b) =
   1.229 +    (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
   1.230 +      else adjust b (negDivAlg (a, (2 * b))));
   1.231 +
   1.232 +fun posDivAlg (a, b) =
   1.233 +    (if ((a < b) orelse (b <= 0)) then (0, a)
   1.234 +      else adjust b (posDivAlg (a, (2 * b))));
   1.235 +
   1.236 +fun divAlg x =
   1.237 +  split (fn a => fn b =>
   1.238 +          (if (0 <= a)
   1.239 +            then (if (0 <= b) then posDivAlg (a, b)
   1.240 +                   else (if (a = 0) then (0, 0)
   1.241 +                          else negateSnd (negDivAlg (~ a, ~ b))))
   1.242 +            else (if (0 < b) then negDivAlg (a, b)
   1.243 +                   else negateSnd (posDivAlg (~ a, ~ b)))))
   1.244 +    x;
   1.245 +
   1.246 +fun op_mod_def1 a b = snd (divAlg (a, b));
   1.247 +
   1.248 +fun op_dvd m n = (op_mod_def1 n m = 0);
   1.249 +
   1.250 +fun psimpl (Le (l, r)) =
   1.251 +    (case lift_bin
   1.252 +            ((fn x => fn y => lin_add (x, lin_neg y)),
   1.253 +              (linearize l, linearize r)) of
   1.254 +      None => Le (l, r)
   1.255 +      | Some x =>
   1.256 +          (case x of Cst xa => (if (xa <= 0) then T else F)
   1.257 +            | Var xa => Le (x, Cst 0) | Neg xa => Le (x, Cst 0)
   1.258 +            | Add (xa, xb) => Le (x, Cst 0) | Sub (xa, xb) => Le (x, Cst 0)
   1.259 +            | Mult (xa, xb) => Le (x, Cst 0)))
   1.260 +  | psimpl (Eq (l, r)) =
   1.261 +    (case lift_bin
   1.262 +            ((fn x => fn y => lin_add (x, lin_neg y)),
   1.263 +              (linearize l, linearize r)) of
   1.264 +      None => Eq (l, r)
   1.265 +      | Some x =>
   1.266 +          (case x of Cst xa => (if (xa = 0) then T else F)
   1.267 +            | Var xa => Eq (x, Cst 0) | Neg xa => Eq (x, Cst 0)
   1.268 +            | Add (xa, xb) => Eq (x, Cst 0) | Sub (xa, xb) => Eq (x, Cst 0)
   1.269 +            | Mult (xa, xb) => Eq (x, Cst 0)))
   1.270 +  | psimpl (Divides (Cst d, t)) =
   1.271 +    (case linearize t of None => Divides (Cst d, t)
   1.272 +      | Some x =>
   1.273 +          (case x of Cst xa => (if op_dvd d xa then T else F)
   1.274 +            | Var xa => Divides (Cst d, x) | Neg xa => Divides (Cst d, x)
   1.275 +            | Add (xa, xb) => Divides (Cst d, x)
   1.276 +            | Sub (xa, xb) => Divides (Cst d, x)
   1.277 +            | Mult (xa, xb) => Divides (Cst d, x)))
   1.278 +  | psimpl (Equ (p, q)) =
   1.279 +    let val p' = psimpl p; val q' = psimpl q
   1.280 +    in (case p' of
   1.281 +         Lt (x, xa) =>
   1.282 +           (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.283 +             | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.284 +             | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.285 +             | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.286 +             | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.287 +             | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.288 +             | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.289 +         | Gt (x, xa) =>
   1.290 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.291 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.292 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.293 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.294 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.295 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.296 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.297 +         | Le (x, xa) =>
   1.298 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.299 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.300 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.301 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.302 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.303 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.304 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.305 +         | Ge (x, xa) =>
   1.306 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.307 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.308 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.309 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.310 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.311 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.312 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.313 +         | Eq (x, xa) =>
   1.314 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.315 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.316 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.317 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.318 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.319 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.320 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.321 +         | Divides (x, xa) =>
   1.322 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.323 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.324 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.325 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.326 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.327 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.328 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.329 +         | T => q'
   1.330 +         | F => (case q' of Lt (x, xa) => NOT q' | Gt (x, xa) => NOT q'
   1.331 +                  | Le (x, xa) => NOT q' | Ge (x, xa) => NOT q'
   1.332 +                  | Eq (x, xa) => NOT q' | Divides (x, xa) => NOT q' | T => F
   1.333 +                  | F => T | NOT x => x | And (x, xa) => NOT q'
   1.334 +                  | Or (x, xa) => NOT q' | Imp (x, xa) => NOT q'
   1.335 +                  | Equ (x, xa) => NOT q' | QAll x => NOT q' | QEx x => NOT q')
   1.336 +         | NOT x =>
   1.337 +             (case q' of Lt (xa, xb) => Equ (p', q')
   1.338 +               | Gt (xa, xb) => Equ (p', q') | Le (xa, xb) => Equ (p', q')
   1.339 +               | Ge (xa, xb) => Equ (p', q') | Eq (xa, xb) => Equ (p', q')
   1.340 +               | Divides (xa, xb) => Equ (p', q') | T => p' | F => x
   1.341 +               | NOT xa => Equ (x, xa) | And (xa, xb) => Equ (p', q')
   1.342 +               | Or (xa, xb) => Equ (p', q') | Imp (xa, xb) => Equ (p', q')
   1.343 +               | Equ (xa, xb) => Equ (p', q') | QAll xa => Equ (p', q')
   1.344 +               | QEx xa => Equ (p', q'))
   1.345 +         | And (x, xa) =>
   1.346 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.347 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.348 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.349 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.350 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.351 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.352 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.353 +         | Or (x, xa) =>
   1.354 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.355 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.356 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.357 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.358 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.359 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.360 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.361 +         | Imp (x, xa) =>
   1.362 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.363 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.364 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.365 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.366 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.367 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.368 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.369 +         | Equ (x, xa) =>
   1.370 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.371 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.372 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.373 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.374 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.375 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.376 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.377 +         | QAll x =>
   1.378 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.379 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.380 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.381 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.382 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.383 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.384 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
   1.385 +         | QEx x =>
   1.386 +             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
   1.387 +               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
   1.388 +               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
   1.389 +               | T => p' | F => NOT p' | NOT x => Equ (p', q')
   1.390 +               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
   1.391 +               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
   1.392 +               | QAll x => Equ (p', q') | QEx x => Equ (p', q')))
   1.393 +    end
   1.394 +  | psimpl (NOT p) =
   1.395 +    let val p' = psimpl p
   1.396 +    in (case p' of Lt (x, xa) => NOT p' | Gt (x, xa) => NOT p'
   1.397 +         | Le (x, xa) => NOT p' | Ge (x, xa) => NOT p' | Eq (x, xa) => NOT p'
   1.398 +         | Divides (x, xa) => NOT p' | T => F | F => T | NOT x => x
   1.399 +         | And (x, xa) => NOT p' | Or (x, xa) => NOT p' | Imp (x, xa) => NOT p'
   1.400 +         | Equ (x, xa) => NOT p' | QAll x => NOT p' | QEx x => NOT p')
   1.401 +    end
   1.402 +  | psimpl (Lt (u, v)) = Lt (u, v)
   1.403 +  | psimpl (Gt (w, x)) = Gt (w, x)
   1.404 +  | psimpl (Ge (aa, ab)) = Ge (aa, ab)
   1.405 +  | psimpl (Divides (Var bp, af)) = Divides (Var bp, af)
   1.406 +  | psimpl (Divides (Neg bq, af)) = Divides (Neg bq, af)
   1.407 +  | psimpl (Divides (Add (br, bs), af)) = Divides (Add (br, bs), af)
   1.408 +  | psimpl (Divides (Sub (bt, bu), af)) = Divides (Sub (bt, bu), af)
   1.409 +  | psimpl (Divides (Mult (bv, bw), af)) = Divides (Mult (bv, bw), af)
   1.410 +  | psimpl T = T
   1.411 +  | psimpl F = F
   1.412 +  | psimpl (QAll ap) = QAll ap
   1.413 +  | psimpl (QEx aq) = QEx aq
   1.414 +  | psimpl (And (p, q)) =
   1.415 +    let val p' = psimpl p
   1.416 +    in (case p' of
   1.417 +         Lt (x, xa) =>
   1.418 +           let val q' = psimpl q
   1.419 +           in (case q' of Lt (x, xa) => And (p', q')
   1.420 +                | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.421 +                | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.422 +                | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.423 +                | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.424 +                | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.425 +                | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.426 +                | QEx x => And (p', q'))
   1.427 +           end
   1.428 +         | Gt (x, xa) =>
   1.429 +             let val q' = psimpl q
   1.430 +             in (case q' of Lt (x, xa) => And (p', q')
   1.431 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.432 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.433 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.434 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.435 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.436 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.437 +                  | QEx x => And (p', q'))
   1.438 +             end
   1.439 +         | Le (x, xa) =>
   1.440 +             let val q' = psimpl q
   1.441 +             in (case q' of Lt (x, xa) => And (p', q')
   1.442 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.443 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.444 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.445 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.446 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.447 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.448 +                  | QEx x => And (p', q'))
   1.449 +             end
   1.450 +         | Ge (x, xa) =>
   1.451 +             let val q' = psimpl q
   1.452 +             in (case q' of Lt (x, xa) => And (p', q')
   1.453 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.454 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.455 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.456 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.457 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.458 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.459 +                  | QEx x => And (p', q'))
   1.460 +             end
   1.461 +         | Eq (x, xa) =>
   1.462 +             let val q' = psimpl q
   1.463 +             in (case q' of Lt (x, xa) => And (p', q')
   1.464 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.465 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.466 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.467 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.468 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.469 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.470 +                  | QEx x => And (p', q'))
   1.471 +             end
   1.472 +         | Divides (x, xa) =>
   1.473 +             let val q' = psimpl q
   1.474 +             in (case q' of Lt (x, xa) => And (p', q')
   1.475 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.476 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.477 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.478 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.479 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.480 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.481 +                  | QEx x => And (p', q'))
   1.482 +             end
   1.483 +         | T => psimpl q | F => F
   1.484 +         | NOT x =>
   1.485 +             let val q' = psimpl q
   1.486 +             in (case q' of Lt (x, xa) => And (p', q')
   1.487 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.488 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.489 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.490 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.491 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.492 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.493 +                  | QEx x => And (p', q'))
   1.494 +             end
   1.495 +         | And (x, xa) =>
   1.496 +             let val q' = psimpl q
   1.497 +             in (case q' of Lt (x, xa) => And (p', q')
   1.498 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.499 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.500 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.501 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.502 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.503 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.504 +                  | QEx x => And (p', q'))
   1.505 +             end
   1.506 +         | Or (x, xa) =>
   1.507 +             let val q' = psimpl q
   1.508 +             in (case q' of Lt (x, xa) => And (p', q')
   1.509 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.510 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.511 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.512 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.513 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.514 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.515 +                  | QEx x => And (p', q'))
   1.516 +             end
   1.517 +         | Imp (x, xa) =>
   1.518 +             let val q' = psimpl q
   1.519 +             in (case q' of Lt (x, xa) => And (p', q')
   1.520 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.521 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.522 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.523 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.524 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.525 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.526 +                  | QEx x => And (p', q'))
   1.527 +             end
   1.528 +         | Equ (x, xa) =>
   1.529 +             let val q' = psimpl q
   1.530 +             in (case q' of Lt (x, xa) => And (p', q')
   1.531 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.532 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.533 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.534 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.535 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.536 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.537 +                  | QEx x => And (p', q'))
   1.538 +             end
   1.539 +         | QAll x =>
   1.540 +             let val q' = psimpl q
   1.541 +             in (case q' of Lt (x, xa) => And (p', q')
   1.542 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.543 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.544 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.545 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.546 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.547 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.548 +                  | QEx x => And (p', q'))
   1.549 +             end
   1.550 +         | QEx x =>
   1.551 +             let val q' = psimpl q
   1.552 +             in (case q' of Lt (x, xa) => And (p', q')
   1.553 +                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
   1.554 +                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
   1.555 +                  | Divides (x, xa) => And (p', q') | T => p' | F => F
   1.556 +                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
   1.557 +                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
   1.558 +                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
   1.559 +                  | QEx x => And (p', q'))
   1.560 +             end)
   1.561 +    end
   1.562 +  | psimpl (Or (p, q)) =
   1.563 +    let val p' = psimpl p
   1.564 +    in (case p' of
   1.565 +         Lt (x, xa) =>
   1.566 +           let val q' = psimpl q
   1.567 +           in (case q' of Lt (x, xa) => Or (p', q') | Gt (x, xa) => Or (p', q')
   1.568 +                | Le (x, xa) => Or (p', q') | Ge (x, xa) => Or (p', q')
   1.569 +                | Eq (x, xa) => Or (p', q') | Divides (x, xa) => Or (p', q')
   1.570 +                | T => T | F => p' | NOT x => Or (p', q')
   1.571 +                | And (x, xa) => Or (p', q') | Or (x, xa) => Or (p', q')
   1.572 +                | Imp (x, xa) => Or (p', q') | Equ (x, xa) => Or (p', q')
   1.573 +                | QAll x => Or (p', q') | QEx x => Or (p', q'))
   1.574 +           end
   1.575 +         | Gt (x, xa) =>
   1.576 +             let val q' = psimpl q
   1.577 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.578 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.579 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.580 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.581 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.582 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.583 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.584 +                  | QEx x => Or (p', q'))
   1.585 +             end
   1.586 +         | Le (x, xa) =>
   1.587 +             let val q' = psimpl q
   1.588 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.589 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.590 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.591 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.592 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.593 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.594 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.595 +                  | QEx x => Or (p', q'))
   1.596 +             end
   1.597 +         | Ge (x, xa) =>
   1.598 +             let val q' = psimpl q
   1.599 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.600 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.601 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.602 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.603 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.604 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.605 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.606 +                  | QEx x => Or (p', q'))
   1.607 +             end
   1.608 +         | Eq (x, xa) =>
   1.609 +             let val q' = psimpl q
   1.610 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.611 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.612 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.613 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.614 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.615 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.616 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.617 +                  | QEx x => Or (p', q'))
   1.618 +             end
   1.619 +         | Divides (x, xa) =>
   1.620 +             let val q' = psimpl q
   1.621 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.622 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.623 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.624 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.625 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.626 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.627 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.628 +                  | QEx x => Or (p', q'))
   1.629 +             end
   1.630 +         | T => T | F => psimpl q
   1.631 +         | NOT x =>
   1.632 +             let val q' = psimpl q
   1.633 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.634 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.635 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.636 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.637 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.638 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.639 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.640 +                  | QEx x => Or (p', q'))
   1.641 +             end
   1.642 +         | And (x, xa) =>
   1.643 +             let val q' = psimpl q
   1.644 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.645 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.646 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.647 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.648 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.649 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.650 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.651 +                  | QEx x => Or (p', q'))
   1.652 +             end
   1.653 +         | Or (x, xa) =>
   1.654 +             let val q' = psimpl q
   1.655 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.656 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.657 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.658 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.659 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.660 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.661 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.662 +                  | QEx x => Or (p', q'))
   1.663 +             end
   1.664 +         | Imp (x, xa) =>
   1.665 +             let val q' = psimpl q
   1.666 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.667 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.668 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.669 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.670 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.671 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.672 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.673 +                  | QEx x => Or (p', q'))
   1.674 +             end
   1.675 +         | Equ (x, xa) =>
   1.676 +             let val q' = psimpl q
   1.677 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.678 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.679 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.680 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.681 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.682 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.683 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.684 +                  | QEx x => Or (p', q'))
   1.685 +             end
   1.686 +         | QAll x =>
   1.687 +             let val q' = psimpl q
   1.688 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.689 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.690 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.691 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.692 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.693 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.694 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.695 +                  | QEx x => Or (p', q'))
   1.696 +             end
   1.697 +         | QEx x =>
   1.698 +             let val q' = psimpl q
   1.699 +             in (case q' of Lt (x, xa) => Or (p', q')
   1.700 +                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
   1.701 +                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
   1.702 +                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
   1.703 +                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
   1.704 +                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
   1.705 +                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
   1.706 +                  | QEx x => Or (p', q'))
   1.707 +             end)
   1.708 +    end
   1.709 +  | psimpl (Imp (p, q)) =
   1.710 +    let val p' = psimpl p
   1.711 +    in (case p' of
   1.712 +         Lt (x, xa) =>
   1.713 +           let val q' = psimpl q
   1.714 +           in (case q' of Lt (x, xa) => Imp (p', q')
   1.715 +                | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.716 +                | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.717 +                | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.718 +                | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.719 +                | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.720 +                | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.721 +                | QEx x => Imp (p', q'))
   1.722 +           end
   1.723 +         | Gt (x, xa) =>
   1.724 +             let val q' = psimpl q
   1.725 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.726 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.727 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.728 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.729 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.730 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.731 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.732 +                  | QEx x => Imp (p', q'))
   1.733 +             end
   1.734 +         | Le (x, xa) =>
   1.735 +             let val q' = psimpl q
   1.736 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.737 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.738 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.739 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.740 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.741 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.742 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.743 +                  | QEx x => Imp (p', q'))
   1.744 +             end
   1.745 +         | Ge (x, xa) =>
   1.746 +             let val q' = psimpl q
   1.747 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.748 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.749 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.750 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.751 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.752 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.753 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.754 +                  | QEx x => Imp (p', q'))
   1.755 +             end
   1.756 +         | Eq (x, xa) =>
   1.757 +             let val q' = psimpl q
   1.758 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.759 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.760 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.761 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.762 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.763 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.764 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.765 +                  | QEx x => Imp (p', q'))
   1.766 +             end
   1.767 +         | Divides (x, xa) =>
   1.768 +             let val q' = psimpl q
   1.769 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.770 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.771 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.772 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.773 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.774 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.775 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.776 +                  | QEx x => Imp (p', q'))
   1.777 +             end
   1.778 +         | T => psimpl q | F => T
   1.779 +         | NOT x =>
   1.780 +             let val q' = psimpl q
   1.781 +             in (case q' of Lt (xa, xb) => Or (x, q')
   1.782 +                  | Gt (xa, xb) => Or (x, q') | Le (xa, xb) => Or (x, q')
   1.783 +                  | Ge (xa, xb) => Or (x, q') | Eq (xa, xb) => Or (x, q')
   1.784 +                  | Divides (xa, xb) => Or (x, q') | T => T | F => x
   1.785 +                  | NOT xa => Or (x, q') | And (xa, xb) => Or (x, q')
   1.786 +                  | Or (xa, xb) => Or (x, q') | Imp (xa, xb) => Or (x, q')
   1.787 +                  | Equ (xa, xb) => Or (x, q') | QAll xa => Or (x, q')
   1.788 +                  | QEx xa => Or (x, q'))
   1.789 +             end
   1.790 +         | And (x, xa) =>
   1.791 +             let val q' = psimpl q
   1.792 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.793 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.794 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.795 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.796 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.797 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.798 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.799 +                  | QEx x => Imp (p', q'))
   1.800 +             end
   1.801 +         | Or (x, xa) =>
   1.802 +             let val q' = psimpl q
   1.803 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.804 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.805 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.806 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.807 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.808 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.809 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.810 +                  | QEx x => Imp (p', q'))
   1.811 +             end
   1.812 +         | Imp (x, xa) =>
   1.813 +             let val q' = psimpl q
   1.814 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.815 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.816 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.817 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.818 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.819 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.820 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.821 +                  | QEx x => Imp (p', q'))
   1.822 +             end
   1.823 +         | Equ (x, xa) =>
   1.824 +             let val q' = psimpl q
   1.825 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.826 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.827 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.828 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.829 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.830 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.831 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.832 +                  | QEx x => Imp (p', q'))
   1.833 +             end
   1.834 +         | QAll x =>
   1.835 +             let val q' = psimpl q
   1.836 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.837 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.838 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.839 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.840 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.841 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.842 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.843 +                  | QEx x => Imp (p', q'))
   1.844 +             end
   1.845 +         | QEx x =>
   1.846 +             let val q' = psimpl q
   1.847 +             in (case q' of Lt (x, xa) => Imp (p', q')
   1.848 +                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
   1.849 +                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
   1.850 +                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
   1.851 +                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
   1.852 +                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
   1.853 +                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
   1.854 +                  | QEx x => Imp (p', q'))
   1.855 +             end)
   1.856 +    end;
   1.857 +
   1.858 +fun subst_it i (Cst b) = Cst b
   1.859 +  | subst_it i (Var n) = (if (n = 0) then i else Var n)
   1.860 +  | subst_it i (Neg it) = Neg (subst_it i it)
   1.861 +  | subst_it i (Add (it1, it2)) = Add (subst_it i it1, subst_it i it2)
   1.862 +  | subst_it i (Sub (it1, it2)) = Sub (subst_it i it1, subst_it i it2)
   1.863 +  | subst_it i (Mult (it1, it2)) = Mult (subst_it i it1, subst_it i it2);
   1.864 +
   1.865 +fun subst_p i (Le (it1, it2)) = Le (subst_it i it1, subst_it i it2)
   1.866 +  | subst_p i (Lt (it1, it2)) = Lt (subst_it i it1, subst_it i it2)
   1.867 +  | subst_p i (Ge (it1, it2)) = Ge (subst_it i it1, subst_it i it2)
   1.868 +  | subst_p i (Gt (it1, it2)) = Gt (subst_it i it1, subst_it i it2)
   1.869 +  | subst_p i (Eq (it1, it2)) = Eq (subst_it i it1, subst_it i it2)
   1.870 +  | subst_p i (Divides (d, t)) = Divides (subst_it i d, subst_it i t)
   1.871 +  | subst_p i T = T
   1.872 +  | subst_p i F = F
   1.873 +  | subst_p i (And (p, q)) = And (subst_p i p, subst_p i q)
   1.874 +  | subst_p i (Or (p, q)) = Or (subst_p i p, subst_p i q)
   1.875 +  | subst_p i (Imp (p, q)) = Imp (subst_p i p, subst_p i q)
   1.876 +  | subst_p i (Equ (p, q)) = Equ (subst_p i p, subst_p i q)
   1.877 +  | subst_p i (NOT p) = NOT (subst_p i p);
   1.878 +
   1.879 +fun explode_disj ([], p) = F
   1.880 +  | explode_disj ((i :: is), p) =
   1.881 +    let val pi = psimpl (subst_p i p)
   1.882 +    in (case pi of
   1.883 +         Lt (x, xa) =>
   1.884 +           let val r = explode_disj (is, p)
   1.885 +           in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.886 +                | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.887 +                | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.888 +                | T => T | F => pi | NOT x => Or (pi, r)
   1.889 +                | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.890 +                | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.891 +                | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.892 +           end
   1.893 +         | Gt (x, xa) =>
   1.894 +             let val r = explode_disj (is, p)
   1.895 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.896 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.897 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.898 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.899 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.900 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.901 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.902 +             end
   1.903 +         | Le (x, xa) =>
   1.904 +             let val r = explode_disj (is, p)
   1.905 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.906 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.907 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.908 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.909 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.910 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.911 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.912 +             end
   1.913 +         | Ge (x, xa) =>
   1.914 +             let val r = explode_disj (is, p)
   1.915 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.916 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.917 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.918 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.919 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.920 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.921 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.922 +             end
   1.923 +         | Eq (x, xa) =>
   1.924 +             let val r = explode_disj (is, p)
   1.925 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.926 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.927 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.928 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.929 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.930 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.931 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.932 +             end
   1.933 +         | Divides (x, xa) =>
   1.934 +             let val r = explode_disj (is, p)
   1.935 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.936 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.937 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.938 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.939 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.940 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.941 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.942 +             end
   1.943 +         | T => T | F => explode_disj (is, p)
   1.944 +         | NOT x =>
   1.945 +             let val r = explode_disj (is, p)
   1.946 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.947 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.948 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.949 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.950 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.951 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.952 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.953 +             end
   1.954 +         | And (x, xa) =>
   1.955 +             let val r = explode_disj (is, p)
   1.956 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.957 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.958 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.959 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.960 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.961 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.962 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.963 +             end
   1.964 +         | Or (x, xa) =>
   1.965 +             let val r = explode_disj (is, p)
   1.966 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.967 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.968 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.969 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.970 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.971 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.972 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.973 +             end
   1.974 +         | Imp (x, xa) =>
   1.975 +             let val r = explode_disj (is, p)
   1.976 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.977 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.978 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.979 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.980 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.981 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.982 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.983 +             end
   1.984 +         | Equ (x, xa) =>
   1.985 +             let val r = explode_disj (is, p)
   1.986 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.987 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.988 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.989 +                  | T => T | F => pi | NOT x => Or (pi, r)
   1.990 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
   1.991 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
   1.992 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
   1.993 +             end
   1.994 +         | QAll x =>
   1.995 +             let val r = explode_disj (is, p)
   1.996 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
   1.997 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
   1.998 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
   1.999 +                  | T => T | F => pi | NOT x => Or (pi, r)
  1.1000 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
  1.1001 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
  1.1002 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
  1.1003 +             end
  1.1004 +         | QEx x =>
  1.1005 +             let val r = explode_disj (is, p)
  1.1006 +             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
  1.1007 +                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
  1.1008 +                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
  1.1009 +                  | T => T | F => pi | NOT x => Or (pi, r)
  1.1010 +                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
  1.1011 +                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
  1.1012 +                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
  1.1013 +             end)
  1.1014 +    end;
  1.1015 +
  1.1016 +fun minusinf (And (p, q)) = And (minusinf p, minusinf q)
  1.1017 +  | minusinf (Or (p, q)) = Or (minusinf p, minusinf q)
  1.1018 +  | minusinf (Lt (u, v)) = Lt (u, v)
  1.1019 +  | minusinf (Gt (w, x)) = Gt (w, x)
  1.1020 +  | minusinf (Le (Cst bo, z)) = Le (Cst bo, z)
  1.1021 +  | minusinf (Le (Var bp, z)) = Le (Var bp, z)
  1.1022 +  | minusinf (Le (Neg bq, z)) = Le (Neg bq, z)
  1.1023 +  | minusinf (Le (Add (Cst cg, bs), z)) = Le (Add (Cst cg, bs), z)
  1.1024 +  | minusinf (Le (Add (Var ch, bs), z)) = Le (Add (Var ch, bs), z)
  1.1025 +  | minusinf (Le (Add (Neg ci, bs), z)) = Le (Add (Neg ci, bs), z)
  1.1026 +  | minusinf (Le (Add (Add (cj, ck), bs), z)) = Le (Add (Add (cj, ck), bs), z)
  1.1027 +  | minusinf (Le (Add (Sub (cl, cm), bs), z)) = Le (Add (Sub (cl, cm), bs), z)
  1.1028 +  | minusinf (Le (Add (Mult (Cst cy, Cst dq), bs), z)) =
  1.1029 +    Le (Add (Mult (Cst cy, Cst dq), bs), z)
  1.1030 +  | minusinf (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
  1.1031 +    (if (ei = 0) then (if (cy < 0) then F else T)
  1.1032 +      else Le (Add (Mult (Cst cy, Var (op_45_def0 ei id_1_def0 + 1)), bs), z))
  1.1033 +  | minusinf (Le (Add (Mult (Cst cy, Neg ds), bs), z)) =
  1.1034 +    Le (Add (Mult (Cst cy, Neg ds), bs), z)
  1.1035 +  | minusinf (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) =
  1.1036 +    Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)
  1.1037 +  | minusinf (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) =
  1.1038 +    Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)
  1.1039 +  | minusinf (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) =
  1.1040 +    Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)
  1.1041 +  | minusinf (Le (Add (Mult (Var cz, co), bs), z)) =
  1.1042 +    Le (Add (Mult (Var cz, co), bs), z)
  1.1043 +  | minusinf (Le (Add (Mult (Neg da, co), bs), z)) =
  1.1044 +    Le (Add (Mult (Neg da, co), bs), z)
  1.1045 +  | minusinf (Le (Add (Mult (Add (db, dc), co), bs), z)) =
  1.1046 +    Le (Add (Mult (Add (db, dc), co), bs), z)
  1.1047 +  | minusinf (Le (Add (Mult (Sub (dd, de), co), bs), z)) =
  1.1048 +    Le (Add (Mult (Sub (dd, de), co), bs), z)
  1.1049 +  | minusinf (Le (Add (Mult (Mult (df, dg), co), bs), z)) =
  1.1050 +    Le (Add (Mult (Mult (df, dg), co), bs), z)
  1.1051 +  | minusinf (Le (Sub (bt, bu), z)) = Le (Sub (bt, bu), z)
  1.1052 +  | minusinf (Le (Mult (bv, bw), z)) = Le (Mult (bv, bw), z)
  1.1053 +  | minusinf (Ge (aa, ab)) = Ge (aa, ab)
  1.1054 +  | minusinf (Eq (Cst ek, ad)) = Eq (Cst ek, ad)
  1.1055 +  | minusinf (Eq (Var el, ad)) = Eq (Var el, ad)
  1.1056 +  | minusinf (Eq (Neg em, ad)) = Eq (Neg em, ad)
  1.1057 +  | minusinf (Eq (Add (Cst fc, eo), ad)) = Eq (Add (Cst fc, eo), ad)
  1.1058 +  | minusinf (Eq (Add (Var fd, eo), ad)) = Eq (Add (Var fd, eo), ad)
  1.1059 +  | minusinf (Eq (Add (Neg fe, eo), ad)) = Eq (Add (Neg fe, eo), ad)
  1.1060 +  | minusinf (Eq (Add (Add (ff, fg), eo), ad)) = Eq (Add (Add (ff, fg), eo), ad)
  1.1061 +  | minusinf (Eq (Add (Sub (fh, fi), eo), ad)) = Eq (Add (Sub (fh, fi), eo), ad)
  1.1062 +  | minusinf (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) =
  1.1063 +    Eq (Add (Mult (Cst fu, Cst gm), eo), ad)
  1.1064 +  | minusinf (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
  1.1065 +    (if (he = 0) then F
  1.1066 +      else Eq (Add (Mult (Cst fu, Var (op_45_def0 he id_1_def0 + 1)), eo), ad))
  1.1067 +  | minusinf (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) =
  1.1068 +    Eq (Add (Mult (Cst fu, Neg go), eo), ad)
  1.1069 +  | minusinf (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) =
  1.1070 +    Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)
  1.1071 +  | minusinf (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) =
  1.1072 +    Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)
  1.1073 +  | minusinf (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) =
  1.1074 +    Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)
  1.1075 +  | minusinf (Eq (Add (Mult (Var fv, fk), eo), ad)) =
  1.1076 +    Eq (Add (Mult (Var fv, fk), eo), ad)
  1.1077 +  | minusinf (Eq (Add (Mult (Neg fw, fk), eo), ad)) =
  1.1078 +    Eq (Add (Mult (Neg fw, fk), eo), ad)
  1.1079 +  | minusinf (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) =
  1.1080 +    Eq (Add (Mult (Add (fx, fy), fk), eo), ad)
  1.1081 +  | minusinf (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) =
  1.1082 +    Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)
  1.1083 +  | minusinf (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) =
  1.1084 +    Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)
  1.1085 +  | minusinf (Eq (Sub (ep, eq), ad)) = Eq (Sub (ep, eq), ad)
  1.1086 +  | minusinf (Eq (Mult (er, es), ad)) = Eq (Mult (er, es), ad)
  1.1087 +  | minusinf (Divides (ae, af)) = Divides (ae, af)
  1.1088 +  | minusinf T = T
  1.1089 +  | minusinf F = F
  1.1090 +  | minusinf (NOT (Lt (hg, hh))) = NOT (Lt (hg, hh))
  1.1091 +  | minusinf (NOT (Gt (hi, hj))) = NOT (Gt (hi, hj))
  1.1092 +  | minusinf (NOT (Le (hk, hl))) = NOT (Le (hk, hl))
  1.1093 +  | minusinf (NOT (Ge (hm, hn))) = NOT (Ge (hm, hn))
  1.1094 +  | minusinf (NOT (Eq (Cst ja, hp))) = NOT (Eq (Cst ja, hp))
  1.1095 +  | minusinf (NOT (Eq (Var jb, hp))) = NOT (Eq (Var jb, hp))
  1.1096 +  | minusinf (NOT (Eq (Neg jc, hp))) = NOT (Eq (Neg jc, hp))
  1.1097 +  | minusinf (NOT (Eq (Add (Cst js, je), hp))) = NOT (Eq (Add (Cst js, je), hp))
  1.1098 +  | minusinf (NOT (Eq (Add (Var jt, je), hp))) = NOT (Eq (Add (Var jt, je), hp))
  1.1099 +  | minusinf (NOT (Eq (Add (Neg ju, je), hp))) = NOT (Eq (Add (Neg ju, je), hp))
  1.1100 +  | minusinf (NOT (Eq (Add (Add (jv, jw), je), hp))) =
  1.1101 +    NOT (Eq (Add (Add (jv, jw), je), hp))
  1.1102 +  | minusinf (NOT (Eq (Add (Sub (jx, jy), je), hp))) =
  1.1103 +    NOT (Eq (Add (Sub (jx, jy), je), hp))
  1.1104 +  | minusinf (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) =
  1.1105 +    NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))
  1.1106 +  | minusinf (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
  1.1107 +    (if (lu = 0) then T
  1.1108 +      else NOT (Eq (Add (Mult (Cst kk, Var (op_45_def0 lu id_1_def0 + 1)), je),
  1.1109 +                     hp)))
  1.1110 +  | minusinf (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) =
  1.1111 +    NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))
  1.1112 +  | minusinf (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) =
  1.1113 +    NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))
  1.1114 +  | minusinf (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) =
  1.1115 +    NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))
  1.1116 +  | minusinf (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) =
  1.1117 +    NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))
  1.1118 +  | minusinf (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) =
  1.1119 +    NOT (Eq (Add (Mult (Var kl, ka), je), hp))
  1.1120 +  | minusinf (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) =
  1.1121 +    NOT (Eq (Add (Mult (Neg km, ka), je), hp))
  1.1122 +  | minusinf (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) =
  1.1123 +    NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))
  1.1124 +  | minusinf (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) =
  1.1125 +    NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))
  1.1126 +  | minusinf (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) =
  1.1127 +    NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))
  1.1128 +  | minusinf (NOT (Eq (Sub (jf, jg), hp))) = NOT (Eq (Sub (jf, jg), hp))
  1.1129 +  | minusinf (NOT (Eq (Mult (jh, ji), hp))) = NOT (Eq (Mult (jh, ji), hp))
  1.1130 +  | minusinf (NOT (Divides (hq, hr))) = NOT (Divides (hq, hr))
  1.1131 +  | minusinf (NOT T) = NOT T
  1.1132 +  | minusinf (NOT F) = NOT F
  1.1133 +  | minusinf (NOT (NOT hs)) = NOT (NOT hs)
  1.1134 +  | minusinf (NOT (And (ht, hu))) = NOT (And (ht, hu))
  1.1135 +  | minusinf (NOT (Or (hv, hw))) = NOT (Or (hv, hw))
  1.1136 +  | minusinf (NOT (Imp (hx, hy))) = NOT (Imp (hx, hy))
  1.1137 +  | minusinf (NOT (Equ (hz, ia))) = NOT (Equ (hz, ia))
  1.1138 +  | minusinf (NOT (QAll ib)) = NOT (QAll ib)
  1.1139 +  | minusinf (NOT (QEx ic)) = NOT (QEx ic)
  1.1140 +  | minusinf (Imp (al, am)) = Imp (al, am)
  1.1141 +  | minusinf (Equ (an, ao)) = Equ (an, ao)
  1.1142 +  | minusinf (QAll ap) = QAll ap
  1.1143 +  | minusinf (QEx aq) = QEx aq;
  1.1144 +
  1.1145 +fun abs i = (if (i < 0) then ~ i else i);
  1.1146 +
  1.1147 +fun op_div_def1 a b = fst (divAlg (a, b));
  1.1148 +
  1.1149 +fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
  1.1150 +
  1.1151 +fun ngcd (m, n) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
  1.1152 +
  1.1153 +fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
  1.1154 +
  1.1155 +fun ilcm a b = op_div_def1 (a * b) (igcd (a, b));
  1.1156 +
  1.1157 +fun divlcm (NOT p) = divlcm p
  1.1158 +  | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
  1.1159 +  | divlcm (Or (p, q)) = ilcm (divlcm p) (divlcm q)
  1.1160 +  | divlcm (Lt (u, v)) = 1
  1.1161 +  | divlcm (Gt (w, x)) = 1
  1.1162 +  | divlcm (Le (y, z)) = 1
  1.1163 +  | divlcm (Ge (aa, ab)) = 1
  1.1164 +  | divlcm (Eq (ac, ad)) = 1
  1.1165 +  | divlcm (Divides (Cst bo, Cst cg)) = 1
  1.1166 +  | divlcm (Divides (Cst bo, Var ch)) = 1
  1.1167 +  | divlcm (Divides (Cst bo, Neg ci)) = 1
  1.1168 +  | divlcm (Divides (Cst bo, Add (Cst cy, ck))) = 1
  1.1169 +  | divlcm (Divides (Cst bo, Add (Var cz, ck))) = 1
  1.1170 +  | divlcm (Divides (Cst bo, Add (Neg da, ck))) = 1
  1.1171 +  | divlcm (Divides (Cst bo, Add (Add (db, dc), ck))) = 1
  1.1172 +  | divlcm (Divides (Cst bo, Add (Sub (dd, de), ck))) = 1
  1.1173 +  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Cst ei), ck))) = 1
  1.1174 +  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Var fa), ck))) =
  1.1175 +    (if (fa = 0) then abs bo else 1)
  1.1176 +  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Neg ek), ck))) = 1
  1.1177 +  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Add (el, em)), ck))) = 1
  1.1178 +  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Sub (en, eo)), ck))) = 1
  1.1179 +  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Mult (ep, eq)), ck))) = 1
  1.1180 +  | divlcm (Divides (Cst bo, Add (Mult (Var dr, dg), ck))) = 1
  1.1181 +  | divlcm (Divides (Cst bo, Add (Mult (Neg ds, dg), ck))) = 1
  1.1182 +  | divlcm (Divides (Cst bo, Add (Mult (Add (dt, du), dg), ck))) = 1
  1.1183 +  | divlcm (Divides (Cst bo, Add (Mult (Sub (dv, dw), dg), ck))) = 1
  1.1184 +  | divlcm (Divides (Cst bo, Add (Mult (Mult (dx, dy), dg), ck))) = 1
  1.1185 +  | divlcm (Divides (Cst bo, Sub (cl, cm))) = 1
  1.1186 +  | divlcm (Divides (Cst bo, Mult (cn, co))) = 1
  1.1187 +  | divlcm (Divides (Var bp, af)) = 1
  1.1188 +  | divlcm (Divides (Neg bq, af)) = 1
  1.1189 +  | divlcm (Divides (Add (br, bs), af)) = 1
  1.1190 +  | divlcm (Divides (Sub (bt, bu), af)) = 1
  1.1191 +  | divlcm (Divides (Mult (bv, bw), af)) = 1
  1.1192 +  | divlcm T = 1
  1.1193 +  | divlcm F = 1
  1.1194 +  | divlcm (Imp (al, am)) = 1
  1.1195 +  | divlcm (Equ (an, ao)) = 1
  1.1196 +  | divlcm (QAll ap) = 1
  1.1197 +  | divlcm (QEx aq) = 1;
  1.1198 +
  1.1199 +fun explode_minf (q, B) =
  1.1200 +    let val d = divlcm q; val pm = minusinf q;
  1.1201 +        val dj1 = explode_disj (map (fn x => Cst x) (iupto (1, d)), pm)
  1.1202 +    in (case dj1 of
  1.1203 +         Lt (x, xa) =>
  1.1204 +           let val dj2 = explode_disj (all_sums (d, B), q)
  1.1205 +           in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1206 +                | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1207 +                | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1208 +                | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1209 +                | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1210 +                | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1211 +                | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1212 +                | QEx x => Or (dj1, dj2))
  1.1213 +           end
  1.1214 +         | Gt (x, xa) =>
  1.1215 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1216 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1217 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1218 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1219 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1220 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1221 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1222 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1223 +                  | QEx x => Or (dj1, dj2))
  1.1224 +             end
  1.1225 +         | Le (x, xa) =>
  1.1226 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1227 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1228 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1229 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1230 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1231 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1232 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1233 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1234 +                  | QEx x => Or (dj1, dj2))
  1.1235 +             end
  1.1236 +         | Ge (x, xa) =>
  1.1237 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1238 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1239 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1240 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1241 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1242 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1243 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1244 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1245 +                  | QEx x => Or (dj1, dj2))
  1.1246 +             end
  1.1247 +         | Eq (x, xa) =>
  1.1248 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1249 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1250 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1251 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1252 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1253 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1254 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1255 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1256 +                  | QEx x => Or (dj1, dj2))
  1.1257 +             end
  1.1258 +         | Divides (x, xa) =>
  1.1259 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1260 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1261 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1262 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1263 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1264 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1265 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1266 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1267 +                  | QEx x => Or (dj1, dj2))
  1.1268 +             end
  1.1269 +         | T => T | F => explode_disj (all_sums (d, B), q)
  1.1270 +         | NOT x =>
  1.1271 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1272 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1273 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1274 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1275 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1276 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1277 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1278 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1279 +                  | QEx x => Or (dj1, dj2))
  1.1280 +             end
  1.1281 +         | And (x, xa) =>
  1.1282 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1283 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1284 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1285 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1286 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1287 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1288 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1289 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1290 +                  | QEx x => Or (dj1, dj2))
  1.1291 +             end
  1.1292 +         | Or (x, xa) =>
  1.1293 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1294 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1295 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1296 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1297 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1298 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1299 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1300 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1301 +                  | QEx x => Or (dj1, dj2))
  1.1302 +             end
  1.1303 +         | Imp (x, xa) =>
  1.1304 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1305 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1306 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1307 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1308 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1309 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1310 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1311 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1312 +                  | QEx x => Or (dj1, dj2))
  1.1313 +             end
  1.1314 +         | Equ (x, xa) =>
  1.1315 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1316 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1317 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1318 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1319 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1320 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1321 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1322 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1323 +                  | QEx x => Or (dj1, dj2))
  1.1324 +             end
  1.1325 +         | QAll x =>
  1.1326 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1327 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1328 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1329 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1330 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1331 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1332 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1333 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1334 +                  | QEx x => Or (dj1, dj2))
  1.1335 +             end
  1.1336 +         | QEx x =>
  1.1337 +             let val dj2 = explode_disj (all_sums (d, B), q)
  1.1338 +             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
  1.1339 +                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
  1.1340 +                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
  1.1341 +                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
  1.1342 +                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
  1.1343 +                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
  1.1344 +                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
  1.1345 +                  | QEx x => Or (dj1, dj2))
  1.1346 +             end)
  1.1347 +    end;
  1.1348 +
  1.1349 +fun mirror (And (p, q)) = And (mirror p, mirror q)
  1.1350 +  | mirror (Or (p, q)) = Or (mirror p, mirror q)
  1.1351 +  | mirror (Lt (u, v)) = Lt (u, v)
  1.1352 +  | mirror (Gt (w, x)) = Gt (w, x)
  1.1353 +  | mirror (Le (Cst bp, aa)) = Le (Cst bp, aa)
  1.1354 +  | mirror (Le (Var bq, aa)) = Le (Var bq, aa)
  1.1355 +  | mirror (Le (Neg br, aa)) = Le (Neg br, aa)
  1.1356 +  | mirror (Le (Add (Cst ch, bt), aa)) = Le (Add (Cst ch, bt), aa)
  1.1357 +  | mirror (Le (Add (Var ci, bt), aa)) = Le (Add (Var ci, bt), aa)
  1.1358 +  | mirror (Le (Add (Neg cj, bt), aa)) = Le (Add (Neg cj, bt), aa)
  1.1359 +  | mirror (Le (Add (Add (ck, cl), bt), aa)) = Le (Add (Add (ck, cl), bt), aa)
  1.1360 +  | mirror (Le (Add (Sub (cm, cn), bt), aa)) = Le (Add (Sub (cm, cn), bt), aa)
  1.1361 +  | mirror (Le (Add (Mult (Cst cz, Cst dr), bt), aa)) =
  1.1362 +    Le (Add (Mult (Cst cz, Cst dr), bt), aa)
  1.1363 +  | mirror (Le (Add (Mult (Cst cz, Var ej), bt), aa)) =
  1.1364 +    (if (ej = 0) then Le (Add (Mult (Cst (~ cz), Var 0), bt), aa)
  1.1365 +      else Le (Add (Mult (Cst cz, Var (op_45_def0 ej id_1_def0 + 1)), bt), aa))
  1.1366 +  | mirror (Le (Add (Mult (Cst cz, Neg dt), bt), aa)) =
  1.1367 +    Le (Add (Mult (Cst cz, Neg dt), bt), aa)
  1.1368 +  | mirror (Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)) =
  1.1369 +    Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)
  1.1370 +  | mirror (Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)) =
  1.1371 +    Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)
  1.1372 +  | mirror (Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)) =
  1.1373 +    Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)
  1.1374 +  | mirror (Le (Add (Mult (Var da, cp), bt), aa)) =
  1.1375 +    Le (Add (Mult (Var da, cp), bt), aa)
  1.1376 +  | mirror (Le (Add (Mult (Neg db, cp), bt), aa)) =
  1.1377 +    Le (Add (Mult (Neg db, cp), bt), aa)
  1.1378 +  | mirror (Le (Add (Mult (Add (dc, dd), cp), bt), aa)) =
  1.1379 +    Le (Add (Mult (Add (dc, dd), cp), bt), aa)
  1.1380 +  | mirror (Le (Add (Mult (Sub (de, df), cp), bt), aa)) =
  1.1381 +    Le (Add (Mult (Sub (de, df), cp), bt), aa)
  1.1382 +  | mirror (Le (Add (Mult (Mult (dg, dh), cp), bt), aa)) =
  1.1383 +    Le (Add (Mult (Mult (dg, dh), cp), bt), aa)
  1.1384 +  | mirror (Le (Sub (bu, bv), aa)) = Le (Sub (bu, bv), aa)
  1.1385 +  | mirror (Le (Mult (bw, bx), aa)) = Le (Mult (bw, bx), aa)
  1.1386 +  | mirror (Ge (ab, ac)) = Ge (ab, ac)
  1.1387 +  | mirror (Eq (Cst el, ae)) = Eq (Cst el, ae)
  1.1388 +  | mirror (Eq (Var em, ae)) = Eq (Var em, ae)
  1.1389 +  | mirror (Eq (Neg en, ae)) = Eq (Neg en, ae)
  1.1390 +  | mirror (Eq (Add (Cst fd, ep), ae)) = Eq (Add (Cst fd, ep), ae)
  1.1391 +  | mirror (Eq (Add (Var fe, ep), ae)) = Eq (Add (Var fe, ep), ae)
  1.1392 +  | mirror (Eq (Add (Neg ff, ep), ae)) = Eq (Add (Neg ff, ep), ae)
  1.1393 +  | mirror (Eq (Add (Add (fg, fh), ep), ae)) = Eq (Add (Add (fg, fh), ep), ae)
  1.1394 +  | mirror (Eq (Add (Sub (fi, fj), ep), ae)) = Eq (Add (Sub (fi, fj), ep), ae)
  1.1395 +  | mirror (Eq (Add (Mult (Cst fv, Cst gn), ep), ae)) =
  1.1396 +    Eq (Add (Mult (Cst fv, Cst gn), ep), ae)
  1.1397 +  | mirror (Eq (Add (Mult (Cst fv, Var hf), ep), ae)) =
  1.1398 +    (if (hf = 0) then Eq (Add (Mult (Cst (~ fv), Var 0), ep), ae)
  1.1399 +      else Eq (Add (Mult (Cst fv, Var (op_45_def0 hf id_1_def0 + 1)), ep), ae))
  1.1400 +  | mirror (Eq (Add (Mult (Cst fv, Neg gp), ep), ae)) =
  1.1401 +    Eq (Add (Mult (Cst fv, Neg gp), ep), ae)
  1.1402 +  | mirror (Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)) =
  1.1403 +    Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)
  1.1404 +  | mirror (Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)) =
  1.1405 +    Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)
  1.1406 +  | mirror (Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)) =
  1.1407 +    Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)
  1.1408 +  | mirror (Eq (Add (Mult (Var fw, fl), ep), ae)) =
  1.1409 +    Eq (Add (Mult (Var fw, fl), ep), ae)
  1.1410 +  | mirror (Eq (Add (Mult (Neg fx, fl), ep), ae)) =
  1.1411 +    Eq (Add (Mult (Neg fx, fl), ep), ae)
  1.1412 +  | mirror (Eq (Add (Mult (Add (fy, fz), fl), ep), ae)) =
  1.1413 +    Eq (Add (Mult (Add (fy, fz), fl), ep), ae)
  1.1414 +  | mirror (Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)) =
  1.1415 +    Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)
  1.1416 +  | mirror (Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)) =
  1.1417 +    Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)
  1.1418 +  | mirror (Eq (Sub (eq, er), ae)) = Eq (Sub (eq, er), ae)
  1.1419 +  | mirror (Eq (Mult (es, et), ae)) = Eq (Mult (es, et), ae)
  1.1420 +  | mirror (Divides (Cst hh, Cst hz)) = Divides (Cst hh, Cst hz)
  1.1421 +  | mirror (Divides (Cst hh, Var ia)) = Divides (Cst hh, Var ia)
  1.1422 +  | mirror (Divides (Cst hh, Neg ib)) = Divides (Cst hh, Neg ib)
  1.1423 +  | mirror (Divides (Cst hh, Add (Cst ir, id))) =
  1.1424 +    Divides (Cst hh, Add (Cst ir, id))
  1.1425 +  | mirror (Divides (Cst hh, Add (Var is, id))) =
  1.1426 +    Divides (Cst hh, Add (Var is, id))
  1.1427 +  | mirror (Divides (Cst hh, Add (Neg it, id))) =
  1.1428 +    Divides (Cst hh, Add (Neg it, id))
  1.1429 +  | mirror (Divides (Cst hh, Add (Add (iu, iv), id))) =
  1.1430 +    Divides (Cst hh, Add (Add (iu, iv), id))
  1.1431 +  | mirror (Divides (Cst hh, Add (Sub (iw, ix), id))) =
  1.1432 +    Divides (Cst hh, Add (Sub (iw, ix), id))
  1.1433 +  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))) =
  1.1434 +    Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))
  1.1435 +  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Var kt), id))) =
  1.1436 +    (if (kt = 0) then Divides (Cst hh, Add (Mult (Cst (~ jj), Var 0), id))
  1.1437 +      else Divides
  1.1438 +             (Cst hh,
  1.1439 +               Add (Mult (Cst jj, Var (op_45_def0 kt id_1_def0 + 1)), id)))
  1.1440 +  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))) =
  1.1441 +    Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))
  1.1442 +  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))) =
  1.1443 +    Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))
  1.1444 +  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))) =
  1.1445 +    Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))
  1.1446 +  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))) =
  1.1447 +    Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))
  1.1448 +  | mirror (Divides (Cst hh, Add (Mult (Var jk, iz), id))) =
  1.1449 +    Divides (Cst hh, Add (Mult (Var jk, iz), id))
  1.1450 +  | mirror (Divides (Cst hh, Add (Mult (Neg jl, iz), id))) =
  1.1451 +    Divides (Cst hh, Add (Mult (Neg jl, iz), id))
  1.1452 +  | mirror (Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))) =
  1.1453 +    Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))
  1.1454 +  | mirror (Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))) =
  1.1455 +    Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))
  1.1456 +  | mirror (Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))) =
  1.1457 +    Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))
  1.1458 +  | mirror (Divides (Cst hh, Sub (ie, if'))) = Divides (Cst hh, Sub (ie, if'))
  1.1459 +  | mirror (Divides (Cst hh, Mult (ig, ih))) = Divides (Cst hh, Mult (ig, ih))
  1.1460 +  | mirror (Divides (Var hi, ag)) = Divides (Var hi, ag)
  1.1461 +  | mirror (Divides (Neg hj, ag)) = Divides (Neg hj, ag)
  1.1462 +  | mirror (Divides (Add (hk, hl), ag)) = Divides (Add (hk, hl), ag)
  1.1463 +  | mirror (Divides (Sub (hm, hn), ag)) = Divides (Sub (hm, hn), ag)
  1.1464 +  | mirror (Divides (Mult (ho, hp), ag)) = Divides (Mult (ho, hp), ag)
  1.1465 +  | mirror T = T
  1.1466 +  | mirror F = F
  1.1467 +  | mirror (NOT (Lt (kv, kw))) = NOT (Lt (kv, kw))
  1.1468 +  | mirror (NOT (Gt (kx, ky))) = NOT (Gt (kx, ky))
  1.1469 +  | mirror (NOT (Le (kz, la))) = NOT (Le (kz, la))
  1.1470 +  | mirror (NOT (Ge (lb, lc))) = NOT (Ge (lb, lc))
  1.1471 +  | mirror (NOT (Eq (Cst mp, le))) = NOT (Eq (Cst mp, le))
  1.1472 +  | mirror (NOT (Eq (Var mq, le))) = NOT (Eq (Var mq, le))
  1.1473 +  | mirror (NOT (Eq (Neg mr, le))) = NOT (Eq (Neg mr, le))
  1.1474 +  | mirror (NOT (Eq (Add (Cst nh, mt), le))) = NOT (Eq (Add (Cst nh, mt), le))
  1.1475 +  | mirror (NOT (Eq (Add (Var ni, mt), le))) = NOT (Eq (Add (Var ni, mt), le))
  1.1476 +  | mirror (NOT (Eq (Add (Neg nj, mt), le))) = NOT (Eq (Add (Neg nj, mt), le))
  1.1477 +  | mirror (NOT (Eq (Add (Add (nk, nl), mt), le))) =
  1.1478 +    NOT (Eq (Add (Add (nk, nl), mt), le))
  1.1479 +  | mirror (NOT (Eq (Add (Sub (nm, nn), mt), le))) =
  1.1480 +    NOT (Eq (Add (Sub (nm, nn), mt), le))
  1.1481 +  | mirror (NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))) =
  1.1482 +    NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))
  1.1483 +  | mirror (NOT (Eq (Add (Mult (Cst nz, Var pj), mt), le))) =
  1.1484 +    (if (pj = 0) then NOT (Eq (Add (Mult (Cst (~ nz), Var 0), mt), le))
  1.1485 +      else NOT (Eq (Add (Mult (Cst nz, Var (op_45_def0 pj id_1_def0 + 1)), mt),
  1.1486 +                     le)))
  1.1487 +  | mirror (NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))) =
  1.1488 +    NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))
  1.1489 +  | mirror (NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))) =
  1.1490 +    NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))
  1.1491 +  | mirror (NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))) =
  1.1492 +    NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))
  1.1493 +  | mirror (NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))) =
  1.1494 +    NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))
  1.1495 +  | mirror (NOT (Eq (Add (Mult (Var oa, np), mt), le))) =
  1.1496 +    NOT (Eq (Add (Mult (Var oa, np), mt), le))
  1.1497 +  | mirror (NOT (Eq (Add (Mult (Neg ob, np), mt), le))) =
  1.1498 +    NOT (Eq (Add (Mult (Neg ob, np), mt), le))
  1.1499 +  | mirror (NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))) =
  1.1500 +    NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))
  1.1501 +  | mirror (NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))) =
  1.1502 +    NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))
  1.1503 +  | mirror (NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))) =
  1.1504 +    NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))
  1.1505 +  | mirror (NOT (Eq (Sub (mu, mv), le))) = NOT (Eq (Sub (mu, mv), le))
  1.1506 +  | mirror (NOT (Eq (Mult (mw, mx), le))) = NOT (Eq (Mult (mw, mx), le))
  1.1507 +  | mirror (NOT (Divides (Cst pl, Cst qd))) = NOT (Divides (Cst pl, Cst qd))
  1.1508 +  | mirror (NOT (Divides (Cst pl, Var qe))) = NOT (Divides (Cst pl, Var qe))
  1.1509 +  | mirror (NOT (Divides (Cst pl, Neg qf))) = NOT (Divides (Cst pl, Neg qf))
  1.1510 +  | mirror (NOT (Divides (Cst pl, Add (Cst qv, qh)))) =
  1.1511 +    NOT (Divides (Cst pl, Add (Cst qv, qh)))
  1.1512 +  | mirror (NOT (Divides (Cst pl, Add (Var qw, qh)))) =
  1.1513 +    NOT (Divides (Cst pl, Add (Var qw, qh)))
  1.1514 +  | mirror (NOT (Divides (Cst pl, Add (Neg qx, qh)))) =
  1.1515 +    NOT (Divides (Cst pl, Add (Neg qx, qh)))
  1.1516 +  | mirror (NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))) =
  1.1517 +    NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))
  1.1518 +  | mirror (NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))) =
  1.1519 +    NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))
  1.1520 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))) =
  1.1521 +    NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))
  1.1522 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Var sx), qh)))) =
  1.1523 +    (if (sx = 0)
  1.1524 +      then NOT (Divides (Cst pl, Add (Mult (Cst (~ rn), Var 0), qh)))
  1.1525 +      else NOT (Divides
  1.1526 +                  (Cst pl,
  1.1527 +                    Add (Mult (Cst rn, Var (op_45_def0 sx id_1_def0 + 1)),
  1.1528 +                          qh))))
  1.1529 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))) =
  1.1530 +    NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))
  1.1531 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))) =
  1.1532 +    NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))
  1.1533 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))) =
  1.1534 +    NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))
  1.1535 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))) =
  1.1536 +    NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))
  1.1537 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))) =
  1.1538 +    NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))
  1.1539 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))) =
  1.1540 +    NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))
  1.1541 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))) =
  1.1542 +    NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))
  1.1543 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))) =
  1.1544 +    NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))
  1.1545 +  | mirror (NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))) =
  1.1546 +    NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))
  1.1547 +  | mirror (NOT (Divides (Cst pl, Sub (qi, qj)))) =
  1.1548 +    NOT (Divides (Cst pl, Sub (qi, qj)))
  1.1549 +  | mirror (NOT (Divides (Cst pl, Mult (qk, ql)))) =
  1.1550 +    NOT (Divides (Cst pl, Mult (qk, ql)))
  1.1551 +  | mirror (NOT (Divides (Var pm, lg))) = NOT (Divides (Var pm, lg))
  1.1552 +  | mirror (NOT (Divides (Neg pn, lg))) = NOT (Divides (Neg pn, lg))
  1.1553 +  | mirror (NOT (Divides (Add (po, pp), lg))) = NOT (Divides (Add (po, pp), lg))
  1.1554 +  | mirror (NOT (Divides (Sub (pq, pr), lg))) = NOT (Divides (Sub (pq, pr), lg))
  1.1555 +  | mirror (NOT (Divides (Mult (ps, pt), lg))) =
  1.1556 +    NOT (Divides (Mult (ps, pt), lg))
  1.1557 +  | mirror (NOT T) = NOT T
  1.1558 +  | mirror (NOT F) = NOT F
  1.1559 +  | mirror (NOT (NOT lh)) = NOT (NOT lh)
  1.1560 +  | mirror (NOT (And (li, lj))) = NOT (And (li, lj))
  1.1561 +  | mirror (NOT (Or (lk, ll))) = NOT (Or (lk, ll))
  1.1562 +  | mirror (NOT (Imp (lm, ln))) = NOT (Imp (lm, ln))
  1.1563 +  | mirror (NOT (Equ (lo, lp))) = NOT (Equ (lo, lp))
  1.1564 +  | mirror (NOT (QAll lq)) = NOT (QAll lq)
  1.1565 +  | mirror (NOT (QEx lr)) = NOT (QEx lr)
  1.1566 +  | mirror (Imp (am, an)) = Imp (am, an)
  1.1567 +  | mirror (Equ (ao, ap)) = Equ (ao, ap)
  1.1568 +  | mirror (QAll aq) = QAll aq
  1.1569 +  | mirror (QEx ar) = QEx ar;
  1.1570 +
  1.1571 +fun op_43_def0 m n = nat ((m) + (n));
  1.1572 +
  1.1573 +fun size_def1 [] = 0
  1.1574 +  | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
  1.1575 +
  1.1576 +fun aset (And (p, q)) = op_64 (aset p) (aset q)
  1.1577 +  | aset (Or (p, q)) = op_64 (aset p) (aset q)
  1.1578 +  | aset (Lt (u, v)) = []
  1.1579 +  | aset (Gt (w, x)) = []
  1.1580 +  | aset (Le (Cst bo, z)) = []
  1.1581 +  | aset (Le (Var bp, z)) = []
  1.1582 +  | aset (Le (Neg bq, z)) = []
  1.1583 +  | aset (Le (Add (Cst cg, bs), z)) = []
  1.1584 +  | aset (Le (Add (Var ch, bs), z)) = []
  1.1585 +  | aset (Le (Add (Neg ci, bs), z)) = []
  1.1586 +  | aset (Le (Add (Add (cj, ck), bs), z)) = []
  1.1587 +  | aset (Le (Add (Sub (cl, cm), bs), z)) = []
  1.1588 +  | aset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
  1.1589 +  | aset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
  1.1590 +    (if (ei = 0)
  1.1591 +      then (if (cy < 0) then [lin_add (bs, Cst 1)]
  1.1592 +             else [lin_neg bs, lin_add (lin_neg bs, Cst 1)])
  1.1593 +      else [])
  1.1594 +  | aset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = []
  1.1595 +  | aset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = []
  1.1596 +  | aset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = []
  1.1597 +  | aset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = []
  1.1598 +  | aset (Le (Add (Mult (Var cz, co), bs), z)) = []
  1.1599 +  | aset (Le (Add (Mult (Neg da, co), bs), z)) = []
  1.1600 +  | aset (Le (Add (Mult (Add (db, dc), co), bs), z)) = []
  1.1601 +  | aset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = []
  1.1602 +  | aset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = []
  1.1603 +  | aset (Le (Sub (bt, bu), z)) = []
  1.1604 +  | aset (Le (Mult (bv, bw), z)) = []
  1.1605 +  | aset (Ge (aa, ab)) = []
  1.1606 +  | aset (Eq (Cst ek, ad)) = []
  1.1607 +  | aset (Eq (Var el, ad)) = []
  1.1608 +  | aset (Eq (Neg em, ad)) = []
  1.1609 +  | aset (Eq (Add (Cst fc, eo), ad)) = []
  1.1610 +  | aset (Eq (Add (Var fd, eo), ad)) = []
  1.1611 +  | aset (Eq (Add (Neg fe, eo), ad)) = []
  1.1612 +  | aset (Eq (Add (Add (ff, fg), eo), ad)) = []
  1.1613 +  | aset (Eq (Add (Sub (fh, fi), eo), ad)) = []
  1.1614 +  | aset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = []
  1.1615 +  | aset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
  1.1616 +    (if (he = 0)
  1.1617 +      then (if (fu < 0) then [lin_add (eo, Cst 1)]
  1.1618 +             else [lin_add (lin_neg eo, Cst 1)])
  1.1619 +      else [])
  1.1620 +  | aset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = []
  1.1621 +  | aset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = []
  1.1622 +  | aset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = []
  1.1623 +  | aset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = []
  1.1624 +  | aset (Eq (Add (Mult (Var fv, fk), eo), ad)) = []
  1.1625 +  | aset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = []
  1.1626 +  | aset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = []
  1.1627 +  | aset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = []
  1.1628 +  | aset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = []
  1.1629 +  | aset (Eq (Sub (ep, eq), ad)) = []
  1.1630 +  | aset (Eq (Mult (er, es), ad)) = []
  1.1631 +  | aset (Divides (ae, af)) = []
  1.1632 +  | aset T = []
  1.1633 +  | aset F = []
  1.1634 +  | aset (NOT (Lt (hg, hh))) = []
  1.1635 +  | aset (NOT (Gt (hi, hj))) = []
  1.1636 +  | aset (NOT (Le (hk, hl))) = []
  1.1637 +  | aset (NOT (Ge (hm, hn))) = []
  1.1638 +  | aset (NOT (Eq (Cst ja, hp))) = []
  1.1639 +  | aset (NOT (Eq (Var jb, hp))) = []
  1.1640 +  | aset (NOT (Eq (Neg jc, hp))) = []
  1.1641 +  | aset (NOT (Eq (Add (Cst js, je), hp))) = []
  1.1642 +  | aset (NOT (Eq (Add (Var jt, je), hp))) = []
  1.1643 +  | aset (NOT (Eq (Add (Neg ju, je), hp))) = []
  1.1644 +  | aset (NOT (Eq (Add (Add (jv, jw), je), hp))) = []
  1.1645 +  | aset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = []
  1.1646 +  | aset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = []
  1.1647 +  | aset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
  1.1648 +    (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else [])
  1.1649 +  | aset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = []
  1.1650 +  | aset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = []
  1.1651 +  | aset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = []
  1.1652 +  | aset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = []
  1.1653 +  | aset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = []
  1.1654 +  | aset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = []
  1.1655 +  | aset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = []
  1.1656 +  | aset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = []
  1.1657 +  | aset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = []
  1.1658 +  | aset (NOT (Eq (Sub (jf, jg), hp))) = []
  1.1659 +  | aset (NOT (Eq (Mult (jh, ji), hp))) = []
  1.1660 +  | aset (NOT (Divides (hq, hr))) = []
  1.1661 +  | aset (NOT T) = []
  1.1662 +  | aset (NOT F) = []
  1.1663 +  | aset (NOT (NOT hs)) = []
  1.1664 +  | aset (NOT (And (ht, hu))) = []
  1.1665 +  | aset (NOT (Or (hv, hw))) = []
  1.1666 +  | aset (NOT (Imp (hx, hy))) = []
  1.1667 +  | aset (NOT (Equ (hz, ia))) = []
  1.1668 +  | aset (NOT (QAll ib)) = []
  1.1669 +  | aset (NOT (QEx ic)) = []
  1.1670 +  | aset (Imp (al, am)) = []
  1.1671 +  | aset (Equ (an, ao)) = []
  1.1672 +  | aset (QAll ap) = []
  1.1673 +  | aset (QEx aq) = [];
  1.1674 +
  1.1675 +fun op_mem x [] = false
  1.1676 +  | op_mem x (y :: ys) = (if (y = x) then true else op_mem x ys);
  1.1677 +
  1.1678 +fun list_insert x xs = (if op_mem x xs then xs else (x :: xs));
  1.1679 +
  1.1680 +fun list_set [] = []
  1.1681 +  | list_set (x :: xs) = list_insert x (list_set xs);
  1.1682 +
  1.1683 +fun bset (And (p, q)) = op_64 (bset p) (bset q)
  1.1684 +  | bset (Or (p, q)) = op_64 (bset p) (bset q)
  1.1685 +  | bset (Lt (u, v)) = []
  1.1686 +  | bset (Gt (w, x)) = []
  1.1687 +  | bset (Le (Cst bo, z)) = []
  1.1688 +  | bset (Le (Var bp, z)) = []
  1.1689 +  | bset (Le (Neg bq, z)) = []
  1.1690 +  | bset (Le (Add (Cst cg, bs), z)) = []
  1.1691 +  | bset (Le (Add (Var ch, bs), z)) = []
  1.1692 +  | bset (Le (Add (Neg ci, bs), z)) = []
  1.1693 +  | bset (Le (Add (Add (cj, ck), bs), z)) = []
  1.1694 +  | bset (Le (Add (Sub (cl, cm), bs), z)) = []
  1.1695 +  | bset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
  1.1696 +  | bset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
  1.1697 +    (if (ei = 0)
  1.1698 +      then (if (cy < 0) then [lin_add (bs, Cst ~1), bs]
  1.1699 +             else [lin_add (lin_neg bs, Cst ~1)])
  1.1700 +      else [])
  1.1701 +  | bset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = []
  1.1702 +  | bset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = []
  1.1703 +  | bset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = []
  1.1704 +  | bset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = []
  1.1705 +  | bset (Le (Add (Mult (Var cz, co), bs), z)) = []
  1.1706 +  | bset (Le (Add (Mult (Neg da, co), bs), z)) = []
  1.1707 +  | bset (Le (Add (Mult (Add (db, dc), co), bs), z)) = []
  1.1708 +  | bset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = []
  1.1709 +  | bset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = []
  1.1710 +  | bset (Le (Sub (bt, bu), z)) = []
  1.1711 +  | bset (Le (Mult (bv, bw), z)) = []
  1.1712 +  | bset (Ge (aa, ab)) = []
  1.1713 +  | bset (Eq (Cst ek, ad)) = []
  1.1714 +  | bset (Eq (Var el, ad)) = []
  1.1715 +  | bset (Eq (Neg em, ad)) = []
  1.1716 +  | bset (Eq (Add (Cst fc, eo), ad)) = []
  1.1717 +  | bset (Eq (Add (Var fd, eo), ad)) = []
  1.1718 +  | bset (Eq (Add (Neg fe, eo), ad)) = []
  1.1719 +  | bset (Eq (Add (Add (ff, fg), eo), ad)) = []
  1.1720 +  | bset (Eq (Add (Sub (fh, fi), eo), ad)) = []
  1.1721 +  | bset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = []
  1.1722 +  | bset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
  1.1723 +    (if (he = 0)
  1.1724 +      then (if (fu < 0) then [lin_add (eo, Cst ~1)]
  1.1725 +             else [lin_add (lin_neg eo, Cst ~1)])
  1.1726 +      else [])
  1.1727 +  | bset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = []
  1.1728 +  | bset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = []
  1.1729 +  | bset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = []
  1.1730 +  | bset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = []
  1.1731 +  | bset (Eq (Add (Mult (Var fv, fk), eo), ad)) = []
  1.1732 +  | bset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = []
  1.1733 +  | bset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = []
  1.1734 +  | bset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = []
  1.1735 +  | bset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = []
  1.1736 +  | bset (Eq (Sub (ep, eq), ad)) = []
  1.1737 +  | bset (Eq (Mult (er, es), ad)) = []
  1.1738 +  | bset (Divides (ae, af)) = []
  1.1739 +  | bset T = []
  1.1740 +  | bset F = []
  1.1741 +  | bset (NOT (Lt (hg, hh))) = []
  1.1742 +  | bset (NOT (Gt (hi, hj))) = []
  1.1743 +  | bset (NOT (Le (hk, hl))) = []
  1.1744 +  | bset (NOT (Ge (hm, hn))) = []
  1.1745 +  | bset (NOT (Eq (Cst ja, hp))) = []
  1.1746 +  | bset (NOT (Eq (Var jb, hp))) = []
  1.1747 +  | bset (NOT (Eq (Neg jc, hp))) = []
  1.1748 +  | bset (NOT (Eq (Add (Cst js, je), hp))) = []
  1.1749 +  | bset (NOT (Eq (Add (Var jt, je), hp))) = []
  1.1750 +  | bset (NOT (Eq (Add (Neg ju, je), hp))) = []
  1.1751 +  | bset (NOT (Eq (Add (Add (jv, jw), je), hp))) = []
  1.1752 +  | bset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = []
  1.1753 +  | bset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = []
  1.1754 +  | bset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
  1.1755 +    (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else [])
  1.1756 +  | bset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = []
  1.1757 +  | bset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = []
  1.1758 +  | bset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = []
  1.1759 +  | bset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = []
  1.1760 +  | bset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = []
  1.1761 +  | bset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = []
  1.1762 +  | bset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = []
  1.1763 +  | bset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = []
  1.1764 +  | bset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = []
  1.1765 +  | bset (NOT (Eq (Sub (jf, jg), hp))) = []
  1.1766 +  | bset (NOT (Eq (Mult (jh, ji), hp))) = []
  1.1767 +  | bset (NOT (Divides (hq, hr))) = []
  1.1768 +  | bset (NOT T) = []
  1.1769 +  | bset (NOT F) = []
  1.1770 +  | bset (NOT (NOT hs)) = []
  1.1771 +  | bset (NOT (And (ht, hu))) = []
  1.1772 +  | bset (NOT (Or (hv, hw))) = []
  1.1773 +  | bset (NOT (Imp (hx, hy))) = []
  1.1774 +  | bset (NOT (Equ (hz, ia))) = []
  1.1775 +  | bset (NOT (QAll ib)) = []
  1.1776 +  | bset (NOT (QEx ic)) = []
  1.1777 +  | bset (Imp (al, am)) = []
  1.1778 +  | bset (Equ (an, ao)) = []
  1.1779 +  | bset (QAll ap) = []
  1.1780 +  | bset (QEx aq) = [];
  1.1781 +
  1.1782 +fun adjustcoeff (l, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
  1.1783 +    (if (c <= 0)
  1.1784 +      then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)),
  1.1785 +                Cst 0)
  1.1786 +      else Le (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0))
  1.1787 +  | adjustcoeff (l, Eq (Add (Mult (Cst c, Var 0), r), Cst i)) =
  1.1788 +    Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0)
  1.1789 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst c, Var 0), r), Cst i))) =
  1.1790 +    NOT (Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0))
  1.1791 +  | adjustcoeff (l, And (p, q)) = And (adjustcoeff (l, p), adjustcoeff (l, q))
  1.1792 +  | adjustcoeff (l, Or (p, q)) = Or (adjustcoeff (l, p), adjustcoeff (l, q))
  1.1793 +  | adjustcoeff (l, Lt (w, x)) = Lt (w, x)
  1.1794 +  | adjustcoeff (l, Gt (y, z)) = Gt (y, z)
  1.1795 +  | adjustcoeff (l, Le (Cst bq, ab)) = Le (Cst bq, ab)
  1.1796 +  | adjustcoeff (l, Le (Var br, ab)) = Le (Var br, ab)
  1.1797 +  | adjustcoeff (l, Le (Neg bs, ab)) = Le (Neg bs, ab)
  1.1798 +  | adjustcoeff (l, Le (Add (Cst ci, bu), ab)) = Le (Add (Cst ci, bu), ab)
  1.1799 +  | adjustcoeff (l, Le (Add (Var cj, bu), ab)) = Le (Add (Var cj, bu), ab)
  1.1800 +  | adjustcoeff (l, Le (Add (Neg ck, bu), ab)) = Le (Add (Neg ck, bu), ab)
  1.1801 +  | adjustcoeff (l, Le (Add (Add (cl, cm), bu), ab)) =
  1.1802 +    Le (Add (Add (cl, cm), bu), ab)
  1.1803 +  | adjustcoeff (l, Le (Add (Sub (cn, co), bu), ab)) =
  1.1804 +    Le (Add (Sub (cn, co), bu), ab)
  1.1805 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Cst ds), bu), ab)) =
  1.1806 +    Le (Add (Mult (Cst da, Cst ds), bu), ab)
  1.1807 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Var en)) =
  1.1808 +    Le (Add (Mult (Cst da, Var 0), bu), Var en)
  1.1809 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Neg eo)) =
  1.1810 +    Le (Add (Mult (Cst da, Var 0), bu), Neg eo)
  1.1811 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq))) =
  1.1812 +    Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq))
  1.1813 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es))) =
  1.1814 +    Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es))
  1.1815 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu))) =
  1.1816 +    Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu))
  1.1817 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Var ek), bu), ab)) =
  1.1818 +    Le (Add (Mult (Cst da, Var ek), bu), ab)
  1.1819 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Neg du), bu), ab)) =
  1.1820 +    Le (Add (Mult (Cst da, Neg du), bu), ab)
  1.1821 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab)) =
  1.1822 +    Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab)
  1.1823 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab)) =
  1.1824 +    Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab)
  1.1825 +  | adjustcoeff (l, Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab)) =
  1.1826 +    Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab)
  1.1827 +  | adjustcoeff (l, Le (Add (Mult (Var db, cq), bu), ab)) =
  1.1828 +    Le (Add (Mult (Var db, cq), bu), ab)
  1.1829 +  | adjustcoeff (l, Le (Add (Mult (Neg dc, cq), bu), ab)) =
  1.1830 +    Le (Add (Mult (Neg dc, cq), bu), ab)
  1.1831 +  | adjustcoeff (l, Le (Add (Mult (Add (dd, de), cq), bu), ab)) =
  1.1832 +    Le (Add (Mult (Add (dd, de), cq), bu), ab)
  1.1833 +  | adjustcoeff (l, Le (Add (Mult (Sub (df, dg), cq), bu), ab)) =
  1.1834 +    Le (Add (Mult (Sub (df, dg), cq), bu), ab)
  1.1835 +  | adjustcoeff (l, Le (Add (Mult (Mult (dh, di), cq), bu), ab)) =
  1.1836 +    Le (Add (Mult (Mult (dh, di), cq), bu), ab)
  1.1837 +  | adjustcoeff (l, Le (Sub (bv, bw), ab)) = Le (Sub (bv, bw), ab)
  1.1838 +  | adjustcoeff (l, Le (Mult (bx, by), ab)) = Le (Mult (bx, by), ab)
  1.1839 +  | adjustcoeff (l, Ge (ac, ad)) = Ge (ac, ad)
  1.1840 +  | adjustcoeff (l, Eq (Cst fe, af)) = Eq (Cst fe, af)
  1.1841 +  | adjustcoeff (l, Eq (Var ff, af)) = Eq (Var ff, af)
  1.1842 +  | adjustcoeff (l, Eq (Neg fg, af)) = Eq (Neg fg, af)
  1.1843 +  | adjustcoeff (l, Eq (Add (Cst fw, fi), af)) = Eq (Add (Cst fw, fi), af)
  1.1844 +  | adjustcoeff (l, Eq (Add (Var fx, fi), af)) = Eq (Add (Var fx, fi), af)
  1.1845 +  | adjustcoeff (l, Eq (Add (Neg fy, fi), af)) = Eq (Add (Neg fy, fi), af)
  1.1846 +  | adjustcoeff (l, Eq (Add (Add (fz, ga), fi), af)) =
  1.1847 +    Eq (Add (Add (fz, ga), fi), af)
  1.1848 +  | adjustcoeff (l, Eq (Add (Sub (gb, gc), fi), af)) =
  1.1849 +    Eq (Add (Sub (gb, gc), fi), af)
  1.1850 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Cst hg), fi), af)) =
  1.1851 +    Eq (Add (Mult (Cst go, Cst hg), fi), af)
  1.1852 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Var ib)) =
  1.1853 +    Eq (Add (Mult (Cst go, Var 0), fi), Var ib)
  1.1854 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Neg ic)) =
  1.1855 +    Eq (Add (Mult (Cst go, Var 0), fi), Neg ic)
  1.1856 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie))) =
  1.1857 +    Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie))
  1.1858 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig))) =
  1.1859 +    Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig))
  1.1860 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii))) =
  1.1861 +    Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii))
  1.1862 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var hy), fi), af)) =
  1.1863 +    Eq (Add (Mult (Cst go, Var hy), fi), af)
  1.1864 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Neg hi), fi), af)) =
  1.1865 +    Eq (Add (Mult (Cst go, Neg hi), fi), af)
  1.1866 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af)) =
  1.1867 +    Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af)
  1.1868 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af)) =
  1.1869 +    Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af)
  1.1870 +  | adjustcoeff (l, Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af)) =
  1.1871 +    Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af)
  1.1872 +  | adjustcoeff (l, Eq (Add (Mult (Var gp, ge), fi), af)) =
  1.1873 +    Eq (Add (Mult (Var gp, ge), fi), af)
  1.1874 +  | adjustcoeff (l, Eq (Add (Mult (Neg gq, ge), fi), af)) =
  1.1875 +    Eq (Add (Mult (Neg gq, ge), fi), af)
  1.1876 +  | adjustcoeff (l, Eq (Add (Mult (Add (gr, gs), ge), fi), af)) =
  1.1877 +    Eq (Add (Mult (Add (gr, gs), ge), fi), af)
  1.1878 +  | adjustcoeff (l, Eq (Add (Mult (Sub (gt, gu), ge), fi), af)) =
  1.1879 +    Eq (Add (Mult (Sub (gt, gu), ge), fi), af)
  1.1880 +  | adjustcoeff (l, Eq (Add (Mult (Mult (gv, gw), ge), fi), af)) =
  1.1881 +    Eq (Add (Mult (Mult (gv, gw), ge), fi), af)
  1.1882 +  | adjustcoeff (l, Eq (Sub (fj, fk), af)) = Eq (Sub (fj, fk), af)
  1.1883 +  | adjustcoeff (l, Eq (Mult (fl, fm), af)) = Eq (Mult (fl, fm), af)
  1.1884 +  | adjustcoeff (l, Divides (Cst is, Cst jk)) = Divides (Cst is, Cst jk)
  1.1885 +  | adjustcoeff (l, Divides (Cst is, Var jl)) = Divides (Cst is, Var jl)
  1.1886 +  | adjustcoeff (l, Divides (Cst is, Neg jm)) = Divides (Cst is, Neg jm)
  1.1887 +  | adjustcoeff (l, Divides (Cst is, Add (Cst kc, jo))) =
  1.1888 +    Divides (Cst is, Add (Cst kc, jo))
  1.1889 +  | adjustcoeff (l, Divides (Cst is, Add (Var kd, jo))) =
  1.1890 +    Divides (Cst is, Add (Var kd, jo))
  1.1891 +  | adjustcoeff (l, Divides (Cst is, Add (Neg ke, jo))) =
  1.1892 +    Divides (Cst is, Add (Neg ke, jo))
  1.1893 +  | adjustcoeff (l, Divides (Cst is, Add (Add (kf, kg), jo))) =
  1.1894 +    Divides (Cst is, Add (Add (kf, kg), jo))
  1.1895 +  | adjustcoeff (l, Divides (Cst is, Add (Sub (kh, ki), jo))) =
  1.1896 +    Divides (Cst is, Add (Sub (kh, ki), jo))
  1.1897 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo))) =
  1.1898 +    Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo))
  1.1899 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Var me), jo))) =
  1.1900 +    (if (me = 0)
  1.1901 +      then Divides
  1.1902 +             (Cst (op_div_def1 l ku * is),
  1.1903 +               Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l ku, jo)))
  1.1904 +      else Divides
  1.1905 +             (Cst is,
  1.1906 +               Add (Mult (Cst ku, Var (op_45_def0 me id_1_def0 + 1)), jo)))
  1.1907 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo))) =
  1.1908 +    Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo))
  1.1909 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo))) =
  1.1910 +    Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo))
  1.1911 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo))) =
  1.1912 +    Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo))
  1.1913 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo))) =
  1.1914 +    Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo))
  1.1915 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Var kv, kk), jo))) =
  1.1916 +    Divides (Cst is, Add (Mult (Var kv, kk), jo))
  1.1917 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Neg kw, kk), jo))) =
  1.1918 +    Divides (Cst is, Add (Mult (Neg kw, kk), jo))
  1.1919 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo))) =
  1.1920 +    Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo))
  1.1921 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo))) =
  1.1922 +    Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo))
  1.1923 +  | adjustcoeff (l, Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo))) =
  1.1924 +    Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo))
  1.1925 +  | adjustcoeff (l, Divides (Cst is, Sub (jp, jq))) =
  1.1926 +    Divides (Cst is, Sub (jp, jq))
  1.1927 +  | adjustcoeff (l, Divides (Cst is, Mult (jr, js))) =
  1.1928 +    Divides (Cst is, Mult (jr, js))
  1.1929 +  | adjustcoeff (l, Divides (Var it, ah)) = Divides (Var it, ah)
  1.1930 +  | adjustcoeff (l, Divides (Neg iu, ah)) = Divides (Neg iu, ah)
  1.1931 +  | adjustcoeff (l, Divides (Add (iv, iw), ah)) = Divides (Add (iv, iw), ah)
  1.1932 +  | adjustcoeff (l, Divides (Sub (ix, iy), ah)) = Divides (Sub (ix, iy), ah)
  1.1933 +  | adjustcoeff (l, Divides (Mult (iz, ja), ah)) = Divides (Mult (iz, ja), ah)
  1.1934 +  | adjustcoeff (l, T) = T
  1.1935 +  | adjustcoeff (l, F) = F
  1.1936 +  | adjustcoeff (l, NOT (Lt (mg, mh))) = NOT (Lt (mg, mh))
  1.1937 +  | adjustcoeff (l, NOT (Gt (mi, mj))) = NOT (Gt (mi, mj))
  1.1938 +  | adjustcoeff (l, NOT (Le (mk, ml))) = NOT (Le (mk, ml))
  1.1939 +  | adjustcoeff (l, NOT (Ge (mm, mn))) = NOT (Ge (mm, mn))
  1.1940 +  | adjustcoeff (l, NOT (Eq (Cst oa, mp))) = NOT (Eq (Cst oa, mp))
  1.1941 +  | adjustcoeff (l, NOT (Eq (Var ob, mp))) = NOT (Eq (Var ob, mp))
  1.1942 +  | adjustcoeff (l, NOT (Eq (Neg oc, mp))) = NOT (Eq (Neg oc, mp))
  1.1943 +  | adjustcoeff (l, NOT (Eq (Add (Cst os, oe), mp))) =
  1.1944 +    NOT (Eq (Add (Cst os, oe), mp))
  1.1945 +  | adjustcoeff (l, NOT (Eq (Add (Var ot, oe), mp))) =
  1.1946 +    NOT (Eq (Add (Var ot, oe), mp))
  1.1947 +  | adjustcoeff (l, NOT (Eq (Add (Neg ou, oe), mp))) =
  1.1948 +    NOT (Eq (Add (Neg ou, oe), mp))
  1.1949 +  | adjustcoeff (l, NOT (Eq (Add (Add (ov, ow), oe), mp))) =
  1.1950 +    NOT (Eq (Add (Add (ov, ow), oe), mp))
  1.1951 +  | adjustcoeff (l, NOT (Eq (Add (Sub (ox, oy), oe), mp))) =
  1.1952 +    NOT (Eq (Add (Sub (ox, oy), oe), mp))
  1.1953 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp))) =
  1.1954 +    NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp))
  1.1955 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx))) =
  1.1956 +    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx))
  1.1957 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy))) =
  1.1958 +    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy))
  1.1959 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra)))) =
  1.1960 +    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra)))
  1.1961 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc)))) =
  1.1962 +    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc)))
  1.1963 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re)))) =
  1.1964 +    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re)))
  1.1965 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp))) =
  1.1966 +    NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp))
  1.1967 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp))) =
  1.1968 +    NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp))
  1.1969 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp))) =
  1.1970 +    NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp))
  1.1971 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp))) =
  1.1972 +    NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp))
  1.1973 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp))) =
  1.1974 +    NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp))
  1.1975 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Var pl, pa), oe), mp))) =
  1.1976 +    NOT (Eq (Add (Mult (Var pl, pa), oe), mp))
  1.1977 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Neg pm, pa), oe), mp))) =
  1.1978 +    NOT (Eq (Add (Mult (Neg pm, pa), oe), mp))
  1.1979 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp))) =
  1.1980 +    NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp))
  1.1981 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp))) =
  1.1982 +    NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp))
  1.1983 +  | adjustcoeff (l, NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp))) =
  1.1984 +    NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp))
  1.1985 +  | adjustcoeff (l, NOT (Eq (Sub (of', og), mp))) = NOT (Eq (Sub (of', og), mp))
  1.1986 +  | adjustcoeff (l, NOT (Eq (Mult (oh, oi), mp))) = NOT (Eq (Mult (oh, oi), mp))
  1.1987 +  | adjustcoeff (l, NOT (Divides (Cst ro, Cst sg))) =
  1.1988 +    NOT (Divides (Cst ro, Cst sg))
  1.1989 +  | adjustcoeff (l, NOT (Divides (Cst ro, Var sh))) =
  1.1990 +    NOT (Divides (Cst ro, Var sh))
  1.1991 +  | adjustcoeff (l, NOT (Divides (Cst ro, Neg si))) =
  1.1992 +    NOT (Divides (Cst ro, Neg si))
  1.1993 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Cst sy, sk)))) =
  1.1994 +    NOT (Divides (Cst ro, Add (Cst sy, sk)))
  1.1995 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Var sz, sk)))) =
  1.1996 +    NOT (Divides (Cst ro, Add (Var sz, sk)))
  1.1997 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Neg ta, sk)))) =
  1.1998 +    NOT (Divides (Cst ro, Add (Neg ta, sk)))
  1.1999 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Add (tb, tc), sk)))) =
  1.2000 +    NOT (Divides (Cst ro, Add (Add (tb, tc), sk)))
  1.2001 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Sub (td, te), sk)))) =
  1.2002 +    NOT (Divides (Cst ro, Add (Sub (td, te), sk)))
  1.2003 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk)))) =
  1.2004 +    NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk)))
  1.2005 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Var va), sk)))) =
  1.2006 +    (if (va = 0)
  1.2007 +      then NOT (Divides
  1.2008 +                  (Cst (op_div_def1 l tq * ro),
  1.2009 +                    Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l tq, sk))))
  1.2010 +      else NOT (Divides
  1.2011 +                  (Cst ro,
  1.2012 +                    Add (Mult (Cst tq, Var (op_45_def0 va id_1_def0 + 1)),
  1.2013 +                          sk))))
  1.2014 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk)))) =
  1.2015 +    NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk)))
  1.2016 +  | adjustcoeff
  1.2017 +      (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk)))) =
  1.2018 +    NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk)))
  1.2019 +  | adjustcoeff
  1.2020 +      (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk)))) =
  1.2021 +    NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk)))
  1.2022 +  | adjustcoeff
  1.2023 +      (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk)))) =
  1.2024 +    NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk)))
  1.2025 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk)))) =
  1.2026 +    NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk)))
  1.2027 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk)))) =
  1.2028 +    NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk)))
  1.2029 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk)))) =
  1.2030 +    NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk)))
  1.2031 +  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk)))) =
  1.2032 +    NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk)))
  1.2033 +  | adjustcoeff
  1.2034 +      (l, NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk)))) =
  1.2035 +    NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk)))
  1.2036 +  | adjustcoeff (l, NOT (Divides (Cst ro, Sub (sl, sm)))) =
  1.2037 +    NOT (Divides (Cst ro, Sub (sl, sm)))
  1.2038 +  | adjustcoeff (l, NOT (Divides (Cst ro, Mult (sn, so)))) =
  1.2039 +    NOT (Divides (Cst ro, Mult (sn, so)))
  1.2040 +  | adjustcoeff (l, NOT (Divides (Var rp, mr))) = NOT (Divides (Var rp, mr))
  1.2041 +  | adjustcoeff (l, NOT (Divides (Neg rq, mr))) = NOT (Divides (Neg rq, mr))
  1.2042 +  | adjustcoeff (l, NOT (Divides (Add (rr, rs), mr))) =
  1.2043 +    NOT (Divides (Add (rr, rs), mr))
  1.2044 +  | adjustcoeff (l, NOT (Divides (Sub (rt, ru), mr))) =
  1.2045 +    NOT (Divides (Sub (rt, ru), mr))
  1.2046 +  | adjustcoeff (l, NOT (Divides (Mult (rv, rw), mr))) =
  1.2047 +    NOT (Divides (Mult (rv, rw), mr))
  1.2048 +  | adjustcoeff (l, NOT T) = NOT T
  1.2049 +  | adjustcoeff (l, NOT F) = NOT F
  1.2050 +  | adjustcoeff (l, NOT (NOT ms)) = NOT (NOT ms)
  1.2051 +  | adjustcoeff (l, NOT (And (mt, mu))) = NOT (And (mt, mu))
  1.2052 +  | adjustcoeff (l, NOT (Or (mv, mw))) = NOT (Or (mv, mw))
  1.2053 +  | adjustcoeff (l, NOT (Imp (mx, my))) = NOT (Imp (mx, my))
  1.2054 +  | adjustcoeff (l, NOT (Equ (mz, na))) = NOT (Equ (mz, na))
  1.2055 +  | adjustcoeff (l, NOT (QAll nb)) = NOT (QAll nb)
  1.2056 +  | adjustcoeff (l, NOT (QEx nc)) = NOT (QEx nc)
  1.2057 +  | adjustcoeff (l, Imp (an, ao)) = Imp (an, ao)
  1.2058 +  | adjustcoeff (l, Equ (ap, aq)) = Equ (ap, aq)
  1.2059 +  | adjustcoeff (l, QAll ar) = QAll ar
  1.2060 +  | adjustcoeff (l, QEx as') = QEx as';
  1.2061 +
  1.2062 +fun formlcm (Le (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c
  1.2063 +  | formlcm (Eq (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c
  1.2064 +  | formlcm (NOT p) = formlcm p
  1.2065 +  | formlcm (And (p, q)) = ilcm (formlcm p) (formlcm q)
  1.2066 +  | formlcm (Or (p, q)) = ilcm (formlcm p) (formlcm q)
  1.2067 +  | formlcm (Lt (u, v)) = 1
  1.2068 +  | formlcm (Gt (w, x)) = 1
  1.2069 +  | formlcm (Le (Cst bo, z)) = 1
  1.2070 +  | formlcm (Le (Var bp, z)) = 1
  1.2071 +  | formlcm (Le (Neg bq, z)) = 1
  1.2072 +  | formlcm (Le (Add (Cst cg, bs), z)) = 1
  1.2073 +  | formlcm (Le (Add (Var ch, bs), z)) = 1
  1.2074 +  | formlcm (Le (Add (Neg ci, bs), z)) = 1
  1.2075 +  | formlcm (Le (Add (Add (cj, ck), bs), z)) = 1
  1.2076 +  | formlcm (Le (Add (Sub (cl, cm), bs), z)) = 1
  1.2077 +  | formlcm (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = 1
  1.2078 +  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Var el)) = 1
  1.2079 +  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Neg em)) = 1
  1.2080 +  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Add (en, eo))) = 1
  1.2081 +  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Sub (ep, eq))) = 1
  1.2082 +  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Mult (er, es))) = 1
  1.2083 +  | formlcm (Le (Add (Mult (Cst cy, Var ei ), bs), z)) = 1
  1.2084 +  | formlcm (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = 1
  1.2085 +  | formlcm (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = 1
  1.2086 +  | formlcm (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = 1
  1.2087 +  | formlcm (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = 1
  1.2088 +  | formlcm (Le (Add (Mult (Var cz, co), bs), z)) = 1
  1.2089 +  | formlcm (Le (Add (Mult (Neg da, co), bs), z)) = 1
  1.2090 +  | formlcm (Le (Add (Mult (Add (db, dc), co), bs), z)) = 1
  1.2091 +  | formlcm (Le (Add (Mult (Sub (dd, de), co), bs), z)) = 1
  1.2092 +  | formlcm (Le (Add (Mult (Mult (df, dg), co), bs), z)) = 1
  1.2093 +  | formlcm (Le (Sub (bt, bu), z)) = 1
  1.2094 +  | formlcm (Le (Mult (bv, bw), z)) = 1
  1.2095 +  | formlcm (Ge (aa, ab)) = 1
  1.2096 +  | formlcm (Eq (Cst fc, ad)) = 1
  1.2097 +  | formlcm (Eq (Var fd, ad)) = 1
  1.2098 +  | formlcm (Eq (Neg fe, ad)) = 1
  1.2099 +  | formlcm (Eq (Add (Cst fu, fg), ad)) = 1
  1.2100 +  | formlcm (Eq (Add (Var fv, fg), ad)) = 1
  1.2101 +  | formlcm (Eq (Add (Neg fw, fg), ad)) = 1
  1.2102 +  | formlcm (Eq (Add (Add (fx, fy), fg), ad)) = 1
  1.2103 +  | formlcm (Eq (Add (Sub (fz, ga), fg), ad)) = 1
  1.2104 +  | formlcm (Eq (Add (Mult (Cst gm, Cst he), fg), ad)) = 1
  1.2105 +  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Var hz)) = 1
  1.2106 +  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Neg ia)) = 1
  1.2107 +  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Add (ib, ic))) = 1
  1.2108 +  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Sub (id, ie))) = 1
  1.2109 +  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Mult (if', ig))) = 1
  1.2110 +  | formlcm (Eq (Add (Mult (Cst gm, Var hw), fg), ad)) = 1
  1.2111 +  | formlcm (Eq (Add (Mult (Cst gm, Neg hg), fg), ad)) = 1
  1.2112 +  | formlcm (Eq (Add (Mult (Cst gm, Add (hh, hi)), fg), ad)) = 1
  1.2113 +  | formlcm (Eq (Add (Mult (Cst gm, Sub (hj, hk)), fg), ad)) = 1
  1.2114 +  | formlcm (Eq (Add (Mult (Cst gm, Mult (hl, hm)), fg), ad)) = 1
  1.2115 +  | formlcm (Eq (Add (Mult (Var gn, gc), fg), ad)) = 1
  1.2116 +  | formlcm (Eq (Add (Mult (Neg go, gc), fg), ad)) = 1
  1.2117 +  | formlcm (Eq (Add (Mult (Add (gp, gq), gc), fg), ad)) = 1
  1.2118 +  | formlcm (Eq (Add (Mult (Sub (gr, gs), gc), fg), ad)) = 1
  1.2119 +  | formlcm (Eq (Add (Mult (Mult (gt, gu), gc), fg), ad)) = 1
  1.2120 +  | formlcm (Eq (Sub (fh, fi), ad)) = 1
  1.2121 +  | formlcm (Eq (Mult (fj, fk), ad)) = 1
  1.2122 +  | formlcm (Divides (Cst iq, Cst ji)) = 1
  1.2123 +  | formlcm (Divides (Cst iq, Var jj)) = 1
  1.2124 +  | formlcm (Divides (Cst iq, Neg jk)) = 1
  1.2125 +  | formlcm (Divides (Cst iq, Add (Cst ka, jm))) = 1
  1.2126 +  | formlcm (Divides (Cst iq, Add (Var kb, jm))) = 1
  1.2127 +  | formlcm (Divides (Cst iq, Add (Neg kc, jm))) = 1
  1.2128 +  | formlcm (Divides (Cst iq, Add (Add (kd, ke), jm))) = 1
  1.2129 +  | formlcm (Divides (Cst iq, Add (Sub (kf, kg), jm))) = 1
  1.2130 +  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Cst lk), jm))) = 1
  1.2131 +  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Var mc), jm))) =
  1.2132 +    (if (mc = 0) then abs ks else 1)
  1.2133 +  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Neg lm), jm))) = 1
  1.2134 +  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Add (ln, lo)), jm))) = 1
  1.2135 +  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Sub (lp, lq)), jm))) = 1
  1.2136 +  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Mult (lr, ls)), jm))) = 1
  1.2137 +  | formlcm (Divides (Cst iq, Add (Mult (Var kt, ki), jm))) = 1
  1.2138 +  | formlcm (Divides (Cst iq, Add (Mult (Neg ku, ki), jm))) = 1
  1.2139 +  | formlcm (Divides (Cst iq, Add (Mult (Add (kv, kw), ki), jm))) = 1
  1.2140 +  | formlcm (Divides (Cst iq, Add (Mult (Sub (kx, ky), ki), jm))) = 1
  1.2141 +  | formlcm (Divides (Cst iq, Add (Mult (Mult (kz, la), ki), jm))) = 1
  1.2142 +  | formlcm (Divides (Cst iq, Sub (jn, jo))) = 1
  1.2143 +  | formlcm (Divides (Cst iq, Mult (jp, jq))) = 1
  1.2144 +  | formlcm (Divides (Var ir, af)) = 1
  1.2145 +  | formlcm (Divides (Neg is, af)) = 1
  1.2146 +  | formlcm (Divides (Add (it, iu), af)) = 1
  1.2147 +  | formlcm (Divides (Sub (iv, iw), af)) = 1
  1.2148 +  | formlcm (Divides (Mult (ix, iy), af)) = 1
  1.2149 +  | formlcm T = 1
  1.2150 +  | formlcm F = 1
  1.2151 +  | formlcm (Imp (al, am)) = 1
  1.2152 +  | formlcm (Equ (an, ao)) = 1
  1.2153 +  | formlcm (QAll ap) = 1
  1.2154 +  | formlcm (QEx aq) = 1;
  1.2155 +
  1.2156 +fun unitycoeff p =
  1.2157 +  let val l = formlcm p; val p' = adjustcoeff (l, p)
  1.2158 +  in (if (l = 1) then p'
  1.2159 +       else And (Divides (Cst l, Add (Mult (Cst 1, Var 0), Cst 0)), p'))
  1.2160 +  end;
  1.2161 +
  1.2162 +fun unify p =
  1.2163 +  let val q = unitycoeff p; val B = list_set (bset q); val A = list_set (aset q)
  1.2164 +  in (if op_60_61_def0 (size_def1 B) (size_def1 A) then (q, B)
  1.2165 +       else (mirror q, map lin_neg A))
  1.2166 +  end;
  1.2167 +
  1.2168 +fun cooper p =
  1.2169 +  lift_un (fn q => decrvars (explode_minf (unify q))) (linform (nnf p));
  1.2170 +
  1.2171 +fun pa p = lift_un psimpl (qelim (cooper, p));
  1.2172 +
  1.2173 +val test = pa;
  1.2174 +
  1.2175 +end;