src/HOL/Integ/reflected_presburger.ML
author chaieb
Wed Sep 14 23:00:03 2005 +0200 (2005-09-14)
changeset 17390 df2b53a66937
parent 17378 105519771c67
child 17401 9147c880ada6
permissions -rw-r--r--
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
chaieb@17378
     1
(* $Id$ *)
chaieb@17378
     2
chaieb@17378
     3
    (* Caution: This file should not be modified. *)
chaieb@17378
     4
    (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
chaieb@17390
     5
fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i;
chaieb@17378
     6
structure Generated =
chaieb@17378
     7
struct
chaieb@17378
     8
chaieb@17390
     9
datatype intterm = Cst of IntInf.int | Var of IntInf.int | Neg of intterm
chaieb@17378
    10
  | Add of intterm * intterm | Sub of intterm * intterm
chaieb@17378
    11
  | Mult of intterm * intterm;
chaieb@17378
    12
chaieb@17378
    13
datatype QF = Lt of intterm * intterm | Gt of intterm * intterm
chaieb@17378
    14
  | Le of intterm * intterm | Ge of intterm * intterm | Eq of intterm * intterm
chaieb@17378
    15
  | Divides of intterm * intterm | T | F | NOT of QF | And of QF * QF
chaieb@17378
    16
  | Or of QF * QF | Imp of QF * QF | Equ of QF * QF | QAll of QF | QEx of QF;
chaieb@17378
    17
chaieb@17378
    18
datatype 'a option = None | Some of 'a;
chaieb@17378
    19
chaieb@17378
    20
fun lift_un c None = None
chaieb@17378
    21
  | lift_un c (Some p) = Some (c p);
chaieb@17378
    22
chaieb@17378
    23
fun lift_bin (c, (Some a, Some b)) = Some (c a b)
chaieb@17378
    24
  | lift_bin (c, (None, y)) = None
chaieb@17378
    25
  | lift_bin (c, (Some y, None)) = None;
chaieb@17378
    26
chaieb@17378
    27
fun lift_qe qe None = None
chaieb@17378
    28
  | lift_qe qe (Some p) = qe p;
chaieb@17378
    29
chaieb@17378
    30
fun qelim (qe, QAll p) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe, p))))
chaieb@17378
    31
  | qelim (qe, QEx p) = lift_qe qe (qelim (qe, p))
chaieb@17378
    32
  | qelim (qe, And (p, q)) =
chaieb@17378
    33
    lift_bin ((fn x => fn xa => And (x, xa)), (qelim (qe, p), qelim (qe, q)))
chaieb@17378
    34
  | qelim (qe, Or (p, q)) =
chaieb@17378
    35
    lift_bin ((fn x => fn xa => Or (x, xa)), (qelim (qe, p), qelim (qe, q)))
chaieb@17378
    36
  | qelim (qe, Imp (p, q)) =
chaieb@17378
    37
    lift_bin ((fn x => fn xa => Imp (x, xa)), (qelim (qe, p), qelim (qe, q)))
chaieb@17378
    38
  | qelim (qe, Equ (p, q)) =
chaieb@17378
    39
    lift_bin ((fn x => fn xa => Equ (x, xa)), (qelim (qe, p), qelim (qe, q)))
chaieb@17378
    40
  | qelim (qe, NOT p) = lift_un NOT (qelim (qe, p))
chaieb@17378
    41
  | qelim (qe, Lt (w, x)) = Some (Lt (w, x))
chaieb@17378
    42
  | qelim (qe, Gt (y, z)) = Some (Gt (y, z))
chaieb@17378
    43
  | qelim (qe, Le (aa, ab)) = Some (Le (aa, ab))
chaieb@17378
    44
  | qelim (qe, Ge (ac, ad)) = Some (Ge (ac, ad))
chaieb@17378
    45
  | qelim (qe, Eq (ae, af)) = Some (Eq (ae, af))
chaieb@17378
    46
  | qelim (qe, Divides (ag, ah)) = Some (Divides (ag, ah))
chaieb@17378
    47
  | qelim (qe, T) = Some T
chaieb@17378
    48
  | qelim (qe, F) = Some F;
chaieb@17378
    49
chaieb@17378
    50
fun lin_mul (c, Cst i) = Cst (c * i)
chaieb@17378
    51
  | lin_mul (c, Add (Mult (Cst c', Var n), r)) =
chaieb@17378
    52
    (if (c = 0) then Cst 0
chaieb@17378
    53
      else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
chaieb@17378
    54
chaieb@17378
    55
fun op_60_def0 m n = ((m) < (n));
chaieb@17378
    56
chaieb@17378
    57
fun op_60_61_def0 m n = not (op_60_def0 n m);
chaieb@17378
    58
chaieb@17378
    59
fun lin_add (Add (Mult (Cst c1, Var n1), r1), Add (Mult (Cst c2, Var n2), r2)) =
chaieb@17378
    60
    (if (n1 = n2)
chaieb@17378
    61
      then let val c = Cst (c1 + c2)
chaieb@17378
    62
           in (if ((c1 + c2) = 0) then lin_add (r1, r2)
chaieb@17378
    63
                else Add (Mult (c, Var n1), lin_add (r1, r2)))
chaieb@17378
    64
           end
chaieb@17378
    65
      else (if op_60_61_def0 n1 n2
chaieb@17378
    66
             then Add (Mult (Cst c1, Var n1),
chaieb@17378
    67
                        lin_add (r1, Add (Mult (Cst c2, Var n2), r2)))
chaieb@17378
    68
             else Add (Mult (Cst c2, Var n2),
chaieb@17378
    69
                        lin_add (Add (Mult (Cst c1, Var n1), r1), r2))))
chaieb@17378
    70
  | lin_add (Add (Mult (Cst c1, Var n1), r1), Cst b) =
chaieb@17378
    71
    Add (Mult (Cst c1, Var n1), lin_add (r1, Cst b))
chaieb@17378
    72
  | lin_add (Cst x, Add (Mult (Cst c2, Var n2), r2)) =
chaieb@17378
    73
    Add (Mult (Cst c2, Var n2), lin_add (Cst x, r2))
chaieb@17378
    74
  | lin_add (Cst b1, Cst b2) = Cst (b1 + b2);
chaieb@17378
    75
chaieb@17378
    76
fun lin_neg i = lin_mul (~1, i);
chaieb@17378
    77
chaieb@17378
    78
fun linearize (Cst b) = Some (Cst b)
chaieb@17378
    79
  | linearize (Var n) = Some (Add (Mult (Cst 1, Var n), Cst 0))
chaieb@17378
    80
  | linearize (Neg i) = lift_un lin_neg (linearize i)
chaieb@17378
    81
  | linearize (Add (i, j)) =
chaieb@17378
    82
    lift_bin ((fn x => fn y => lin_add (x, y)), (linearize i, linearize j))
chaieb@17378
    83
  | linearize (Sub (i, j)) =
chaieb@17378
    84
    lift_bin
chaieb@17378
    85
      ((fn x => fn y => lin_add (x, lin_neg y)), (linearize i, linearize j))
chaieb@17378
    86
  | linearize (Mult (i, j)) =
chaieb@17378
    87
    (case linearize i of None => None
chaieb@17378
    88
      | Some x =>
chaieb@17378
    89
          (case x of
chaieb@17378
    90
            Cst xa =>
chaieb@17378
    91
              (case linearize j of None => None
chaieb@17378
    92
                | Some x => Some (lin_mul (xa, x)))
chaieb@17378
    93
            | Var xa =>
chaieb@17378
    94
                (case linearize j of None => None
chaieb@17378
    95
                  | Some xa =>
chaieb@17378
    96
                      (case xa of Cst xa => Some (lin_mul (xa, x))
chaieb@17378
    97
                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
chaieb@17378
    98
                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
chaieb@17378
    99
            | Neg xa =>
chaieb@17378
   100
                (case linearize j of None => None
chaieb@17378
   101
                  | Some xa =>
chaieb@17378
   102
                      (case xa of Cst xa => Some (lin_mul (xa, x))
chaieb@17378
   103
                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
chaieb@17378
   104
                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
chaieb@17378
   105
            | Add (xa, xb) =>
chaieb@17378
   106
                (case linearize j of None => None
chaieb@17378
   107
                  | Some xa =>
chaieb@17378
   108
                      (case xa of Cst xa => Some (lin_mul (xa, x))
chaieb@17378
   109
                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
chaieb@17378
   110
                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
chaieb@17378
   111
            | Sub (xa, xb) =>
chaieb@17378
   112
                (case linearize j of None => None
chaieb@17378
   113
                  | Some xa =>
chaieb@17378
   114
                      (case xa of Cst xa => Some (lin_mul (xa, x))
chaieb@17378
   115
                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
chaieb@17378
   116
                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
chaieb@17378
   117
            | Mult (xa, xb) =>
chaieb@17378
   118
                (case linearize j of None => None
chaieb@17378
   119
                  | Some xa =>
chaieb@17378
   120
                      (case xa of Cst xa => Some (lin_mul (xa, x))
chaieb@17378
   121
                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
chaieb@17378
   122
                        | Sub (xa, xb) => None | Mult (xa, xb) => None))));
chaieb@17378
   123
chaieb@17378
   124
fun linform (Le (it1, it2)) =
chaieb@17378
   125
    lift_bin
chaieb@17378
   126
      ((fn x => fn y => Le (lin_add (x, lin_neg y), Cst 0)),
chaieb@17378
   127
        (linearize it1, linearize it2))
chaieb@17378
   128
  | linform (Eq (it1, it2)) =
chaieb@17378
   129
    lift_bin
chaieb@17378
   130
      ((fn x => fn y => Eq (lin_add (x, lin_neg y), Cst 0)),
chaieb@17378
   131
        (linearize it1, linearize it2))
chaieb@17378
   132
  | linform (Divides (d, t)) =
chaieb@17378
   133
    (case linearize d of None => None
chaieb@17378
   134
      | Some x =>
chaieb@17378
   135
          (case x of
chaieb@17378
   136
            Cst xa =>
chaieb@17378
   137
              (if (xa = 0) then None
chaieb@17378
   138
                else (case linearize t of None => None
chaieb@17378
   139
                       | Some xa => Some (Divides (x, xa))))
chaieb@17378
   140
            | Var xa => None | Neg xa => None | Add (xa, xb) => None
chaieb@17378
   141
            | Sub (xa, xb) => None | Mult (xa, xb) => None))
chaieb@17378
   142
  | linform T = Some T
chaieb@17378
   143
  | linform F = Some F
chaieb@17378
   144
  | linform (NOT p) = lift_un NOT (linform p)
chaieb@17378
   145
  | linform (And (p, q)) =
chaieb@17378
   146
    lift_bin ((fn f => fn g => And (f, g)), (linform p, linform q))
chaieb@17378
   147
  | linform (Or (p, q)) =
chaieb@17378
   148
    lift_bin ((fn f => fn g => Or (f, g)), (linform p, linform q));
chaieb@17378
   149
chaieb@17378
   150
fun nnf (Lt (it1, it2)) = Le (Sub (it1, it2), Cst (~ 1))
chaieb@17378
   151
  | nnf (Gt (it1, it2)) = Le (Sub (it2, it1), Cst (~ 1))
chaieb@17378
   152
  | nnf (Le (it1, it2)) = Le (it1, it2)
chaieb@17378
   153
  | nnf (Ge (it1, it2)) = Le (it2, it1)
chaieb@17378
   154
  | nnf (Eq (it1, it2)) = Eq (it2, it1)
chaieb@17378
   155
  | nnf (Divides (d, t)) = Divides (d, t)
chaieb@17378
   156
  | nnf T = T
chaieb@17378
   157
  | nnf F = F
chaieb@17378
   158
  | nnf (And (p, q)) = And (nnf p, nnf q)
chaieb@17378
   159
  | nnf (Or (p, q)) = Or (nnf p, nnf q)
chaieb@17378
   160
  | nnf (Imp (p, q)) = Or (nnf (NOT p), nnf q)
chaieb@17378
   161
  | nnf (Equ (p, q)) = Or (And (nnf p, nnf q), And (nnf (NOT p), nnf (NOT q)))
chaieb@17378
   162
  | nnf (NOT (Lt (it1, it2))) = Le (it2, it1)
chaieb@17378
   163
  | nnf (NOT (Gt (it1, it2))) = Le (it1, it2)
chaieb@17378
   164
  | nnf (NOT (Le (it1, it2))) = Le (Sub (it2, it1), Cst (~ 1))
chaieb@17378
   165
  | nnf (NOT (Ge (it1, it2))) = Le (Sub (it1, it2), Cst (~ 1))
chaieb@17378
   166
  | nnf (NOT (Eq (it1, it2))) = NOT (Eq (it1, it2))
chaieb@17378
   167
  | nnf (NOT (Divides (d, t))) = NOT (Divides (d, t))
chaieb@17378
   168
  | nnf (NOT T) = F
chaieb@17378
   169
  | nnf (NOT F) = T
chaieb@17378
   170
  | nnf (NOT (NOT p)) = nnf p
chaieb@17378
   171
  | nnf (NOT (And (p, q))) = Or (nnf (NOT p), nnf (NOT q))
chaieb@17378
   172
  | nnf (NOT (Or (p, q))) = And (nnf (NOT p), nnf (NOT q))
chaieb@17378
   173
  | nnf (NOT (Imp (p, q))) = And (nnf p, nnf (NOT q))
chaieb@17378
   174
  | nnf (NOT (Equ (p, q))) =
chaieb@17378
   175
    Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
chaieb@17378
   176
chaieb@17378
   177
fun op_45_def2 z w = (z + ~ w);
chaieb@17378
   178
chaieb@17378
   179
fun op_45_def0 m n = nat (op_45_def2 (m) (n));
chaieb@17378
   180
chaieb@17390
   181
val id_1_def0 : IntInf.int = (0 + 1);
chaieb@17378
   182
chaieb@17378
   183
fun decrvarsI (Cst i) = Cst i
chaieb@17378
   184
  | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
chaieb@17378
   185
  | decrvarsI (Neg a) = Neg (decrvarsI a)
chaieb@17378
   186
  | decrvarsI (Add (a, b)) = Add (decrvarsI a, decrvarsI b)
chaieb@17378
   187
  | decrvarsI (Sub (a, b)) = Sub (decrvarsI a, decrvarsI b)
chaieb@17378
   188
  | decrvarsI (Mult (a, b)) = Mult (decrvarsI a, decrvarsI b);
chaieb@17378
   189
chaieb@17378
   190
fun decrvars (Lt (a, b)) = Lt (decrvarsI a, decrvarsI b)
chaieb@17378
   191
  | decrvars (Gt (a, b)) = Gt (decrvarsI a, decrvarsI b)
chaieb@17378
   192
  | decrvars (Le (a, b)) = Le (decrvarsI a, decrvarsI b)
chaieb@17378
   193
  | decrvars (Ge (a, b)) = Ge (decrvarsI a, decrvarsI b)
chaieb@17378
   194
  | decrvars (Eq (a, b)) = Eq (decrvarsI a, decrvarsI b)
chaieb@17378
   195
  | decrvars (Divides (a, b)) = Divides (decrvarsI a, decrvarsI b)
chaieb@17378
   196
  | decrvars T = T
chaieb@17378
   197
  | decrvars F = F
chaieb@17378
   198
  | decrvars (NOT p) = NOT (decrvars p)
chaieb@17378
   199
  | decrvars (And (p, q)) = And (decrvars p, decrvars q)
chaieb@17378
   200
  | decrvars (Or (p, q)) = Or (decrvars p, decrvars q)
chaieb@17378
   201
  | decrvars (Imp (p, q)) = Imp (decrvars p, decrvars q)
chaieb@17378
   202
  | decrvars (Equ (p, q)) = Equ (decrvars p, decrvars q);
chaieb@17378
   203
chaieb@17378
   204
fun op_64 [] ys = ys
chaieb@17378
   205
  | op_64 (x :: xs) ys = (x :: op_64 xs ys);
chaieb@17378
   206
chaieb@17378
   207
fun map f [] = []
chaieb@17378
   208
  | map f (x :: xs) = (f x :: map f xs);
chaieb@17378
   209
chaieb@17390
   210
fun iupto (i:IntInf.int, j:IntInf.int) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
chaieb@17378
   211
chaieb@17390
   212
fun all_sums (j:IntInf.int, []) = []
chaieb@17378
   213
  | all_sums (j, (i :: is)) =
chaieb@17378
   214
    op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
chaieb@17378
   215
chaieb@17378
   216
fun split x = (fn p => x (fst p) (snd p));
chaieb@17378
   217
chaieb@17378
   218
fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
chaieb@17378
   219
chaieb@17378
   220
fun adjust b =
chaieb@17390
   221
  (fn (q:IntInf.int, r:IntInf.int) =>
chaieb@17390
   222
    (if (0 <= op_45_def2 r b) then ((((2:IntInf.int) * q) + (1:IntInf.int)), op_45_def2 r b)
chaieb@17390
   223
      else (((2:IntInf.int) * q), r)));
chaieb@17378
   224
chaieb@17390
   225
fun negDivAlg (a:IntInf.int, b:IntInf.int) =
chaieb@17378
   226
    (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
chaieb@17378
   227
      else adjust b (negDivAlg (a, (2 * b))));
chaieb@17378
   228
chaieb@17390
   229
fun posDivAlg (a:IntInf.int, b:IntInf.int) =
chaieb@17378
   230
    (if ((a < b) orelse (b <= 0)) then (0, a)
chaieb@17378
   231
      else adjust b (posDivAlg (a, (2 * b))));
chaieb@17378
   232
chaieb@17378
   233
fun divAlg x =
chaieb@17390
   234
  split (fn a:IntInf.int => fn b:IntInf.int =>
chaieb@17378
   235
          (if (0 <= a)
chaieb@17378
   236
            then (if (0 <= b) then posDivAlg (a, b)
chaieb@17378
   237
                   else (if (a = 0) then (0, 0)
chaieb@17378
   238
                          else negateSnd (negDivAlg (~ a, ~ b))))
chaieb@17378
   239
            else (if (0 < b) then negDivAlg (a, b)
chaieb@17378
   240
                   else negateSnd (posDivAlg (~ a, ~ b)))))
chaieb@17378
   241
    x;
chaieb@17378
   242
chaieb@17390
   243
fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
chaieb@17378
   244
chaieb@17378
   245
fun op_dvd m n = (op_mod_def1 n m = 0);
chaieb@17378
   246
chaieb@17378
   247
fun psimpl (Le (l, r)) =
chaieb@17378
   248
    (case lift_bin
chaieb@17378
   249
            ((fn x => fn y => lin_add (x, lin_neg y)),
chaieb@17378
   250
              (linearize l, linearize r)) of
chaieb@17378
   251
      None => Le (l, r)
chaieb@17378
   252
      | Some x =>
chaieb@17378
   253
          (case x of Cst xa => (if (xa <= 0) then T else F)
chaieb@17378
   254
            | Var xa => Le (x, Cst 0) | Neg xa => Le (x, Cst 0)
chaieb@17378
   255
            | Add (xa, xb) => Le (x, Cst 0) | Sub (xa, xb) => Le (x, Cst 0)
chaieb@17378
   256
            | Mult (xa, xb) => Le (x, Cst 0)))
chaieb@17378
   257
  | psimpl (Eq (l, r)) =
chaieb@17378
   258
    (case lift_bin
chaieb@17378
   259
            ((fn x => fn y => lin_add (x, lin_neg y)),
chaieb@17378
   260
              (linearize l, linearize r)) of
chaieb@17378
   261
      None => Eq (l, r)
chaieb@17378
   262
      | Some x =>
chaieb@17378
   263
          (case x of Cst xa => (if (xa = 0) then T else F)
chaieb@17378
   264
            | Var xa => Eq (x, Cst 0) | Neg xa => Eq (x, Cst 0)
chaieb@17378
   265
            | Add (xa, xb) => Eq (x, Cst 0) | Sub (xa, xb) => Eq (x, Cst 0)
chaieb@17378
   266
            | Mult (xa, xb) => Eq (x, Cst 0)))
chaieb@17378
   267
  | psimpl (Divides (Cst d, t)) =
chaieb@17378
   268
    (case linearize t of None => Divides (Cst d, t)
chaieb@17378
   269
      | Some x =>
chaieb@17378
   270
          (case x of Cst xa => (if op_dvd d xa then T else F)
chaieb@17378
   271
            | Var xa => Divides (Cst d, x) | Neg xa => Divides (Cst d, x)
chaieb@17378
   272
            | Add (xa, xb) => Divides (Cst d, x)
chaieb@17378
   273
            | Sub (xa, xb) => Divides (Cst d, x)
chaieb@17378
   274
            | Mult (xa, xb) => Divides (Cst d, x)))
chaieb@17378
   275
  | psimpl (Equ (p, q)) =
chaieb@17378
   276
    let val p' = psimpl p; val q' = psimpl q
chaieb@17378
   277
    in (case p' of
chaieb@17378
   278
         Lt (x, xa) =>
chaieb@17378
   279
           (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   280
             | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   281
             | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   282
             | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   283
             | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   284
             | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   285
             | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   286
         | Gt (x, xa) =>
chaieb@17378
   287
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   288
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   289
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   290
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   291
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   292
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   293
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   294
         | Le (x, xa) =>
chaieb@17378
   295
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   296
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   297
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   298
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   299
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   300
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   301
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   302
         | Ge (x, xa) =>
chaieb@17378
   303
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   304
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   305
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   306
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   307
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   308
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   309
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   310
         | Eq (x, xa) =>
chaieb@17378
   311
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   312
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   313
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   314
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   315
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   316
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   317
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   318
         | Divides (x, xa) =>
chaieb@17378
   319
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   320
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   321
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   322
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   323
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   324
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   325
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   326
         | T => q'
chaieb@17378
   327
         | F => (case q' of Lt (x, xa) => NOT q' | Gt (x, xa) => NOT q'
chaieb@17378
   328
                  | Le (x, xa) => NOT q' | Ge (x, xa) => NOT q'
chaieb@17378
   329
                  | Eq (x, xa) => NOT q' | Divides (x, xa) => NOT q' | T => F
chaieb@17378
   330
                  | F => T | NOT x => x | And (x, xa) => NOT q'
chaieb@17378
   331
                  | Or (x, xa) => NOT q' | Imp (x, xa) => NOT q'
chaieb@17378
   332
                  | Equ (x, xa) => NOT q' | QAll x => NOT q' | QEx x => NOT q')
chaieb@17378
   333
         | NOT x =>
chaieb@17378
   334
             (case q' of Lt (xa, xb) => Equ (p', q')
chaieb@17378
   335
               | Gt (xa, xb) => Equ (p', q') | Le (xa, xb) => Equ (p', q')
chaieb@17378
   336
               | Ge (xa, xb) => Equ (p', q') | Eq (xa, xb) => Equ (p', q')
chaieb@17378
   337
               | Divides (xa, xb) => Equ (p', q') | T => p' | F => x
chaieb@17378
   338
               | NOT xa => Equ (x, xa) | And (xa, xb) => Equ (p', q')
chaieb@17378
   339
               | Or (xa, xb) => Equ (p', q') | Imp (xa, xb) => Equ (p', q')
chaieb@17378
   340
               | Equ (xa, xb) => Equ (p', q') | QAll xa => Equ (p', q')
chaieb@17378
   341
               | QEx xa => Equ (p', q'))
chaieb@17378
   342
         | And (x, xa) =>
chaieb@17378
   343
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   344
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   345
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   346
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   347
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   348
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   349
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   350
         | Or (x, xa) =>
chaieb@17378
   351
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   352
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   353
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   354
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   355
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   356
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   357
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   358
         | Imp (x, xa) =>
chaieb@17378
   359
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   360
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   361
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   362
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   363
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   364
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   365
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   366
         | Equ (x, xa) =>
chaieb@17378
   367
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   368
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   369
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   370
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   371
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   372
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   373
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   374
         | QAll x =>
chaieb@17378
   375
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   376
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   377
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   378
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   379
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   380
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   381
               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
chaieb@17378
   382
         | QEx x =>
chaieb@17378
   383
             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
chaieb@17378
   384
               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
chaieb@17378
   385
               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
chaieb@17378
   386
               | T => p' | F => NOT p' | NOT x => Equ (p', q')
chaieb@17378
   387
               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
chaieb@17378
   388
               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
chaieb@17378
   389
               | QAll x => Equ (p', q') | QEx x => Equ (p', q')))
chaieb@17378
   390
    end
chaieb@17378
   391
  | psimpl (NOT p) =
chaieb@17378
   392
    let val p' = psimpl p
chaieb@17378
   393
    in (case p' of Lt (x, xa) => NOT p' | Gt (x, xa) => NOT p'
chaieb@17378
   394
         | Le (x, xa) => NOT p' | Ge (x, xa) => NOT p' | Eq (x, xa) => NOT p'
chaieb@17378
   395
         | Divides (x, xa) => NOT p' | T => F | F => T | NOT x => x
chaieb@17378
   396
         | And (x, xa) => NOT p' | Or (x, xa) => NOT p' | Imp (x, xa) => NOT p'
chaieb@17378
   397
         | Equ (x, xa) => NOT p' | QAll x => NOT p' | QEx x => NOT p')
chaieb@17378
   398
    end
chaieb@17378
   399
  | psimpl (Lt (u, v)) = Lt (u, v)
chaieb@17378
   400
  | psimpl (Gt (w, x)) = Gt (w, x)
chaieb@17378
   401
  | psimpl (Ge (aa, ab)) = Ge (aa, ab)
chaieb@17378
   402
  | psimpl (Divides (Var bp, af)) = Divides (Var bp, af)
chaieb@17378
   403
  | psimpl (Divides (Neg bq, af)) = Divides (Neg bq, af)
chaieb@17378
   404
  | psimpl (Divides (Add (br, bs), af)) = Divides (Add (br, bs), af)
chaieb@17378
   405
  | psimpl (Divides (Sub (bt, bu), af)) = Divides (Sub (bt, bu), af)
chaieb@17378
   406
  | psimpl (Divides (Mult (bv, bw), af)) = Divides (Mult (bv, bw), af)
chaieb@17378
   407
  | psimpl T = T
chaieb@17378
   408
  | psimpl F = F
chaieb@17378
   409
  | psimpl (QAll ap) = QAll ap
chaieb@17378
   410
  | psimpl (QEx aq) = QEx aq
chaieb@17378
   411
  | psimpl (And (p, q)) =
chaieb@17378
   412
    let val p' = psimpl p
chaieb@17378
   413
    in (case p' of
chaieb@17378
   414
         Lt (x, xa) =>
chaieb@17378
   415
           let val q' = psimpl q
chaieb@17378
   416
           in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   417
                | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   418
                | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   419
                | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   420
                | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   421
                | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   422
                | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   423
                | QEx x => And (p', q'))
chaieb@17378
   424
           end
chaieb@17378
   425
         | Gt (x, xa) =>
chaieb@17378
   426
             let val q' = psimpl q
chaieb@17378
   427
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   428
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   429
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   430
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   431
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   432
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   433
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   434
                  | QEx x => And (p', q'))
chaieb@17378
   435
             end
chaieb@17378
   436
         | Le (x, xa) =>
chaieb@17378
   437
             let val q' = psimpl q
chaieb@17378
   438
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   439
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   440
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   441
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   442
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   443
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   444
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   445
                  | QEx x => And (p', q'))
chaieb@17378
   446
             end
chaieb@17378
   447
         | Ge (x, xa) =>
chaieb@17378
   448
             let val q' = psimpl q
chaieb@17378
   449
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   450
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   451
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   452
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   453
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   454
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   455
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   456
                  | QEx x => And (p', q'))
chaieb@17378
   457
             end
chaieb@17378
   458
         | Eq (x, xa) =>
chaieb@17378
   459
             let val q' = psimpl q
chaieb@17378
   460
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   461
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   462
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   463
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   464
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   465
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   466
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   467
                  | QEx x => And (p', q'))
chaieb@17378
   468
             end
chaieb@17378
   469
         | Divides (x, xa) =>
chaieb@17378
   470
             let val q' = psimpl q
chaieb@17378
   471
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   472
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   473
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   474
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   475
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   476
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   477
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   478
                  | QEx x => And (p', q'))
chaieb@17378
   479
             end
chaieb@17378
   480
         | T => psimpl q | F => F
chaieb@17378
   481
         | NOT x =>
chaieb@17378
   482
             let val q' = psimpl q
chaieb@17378
   483
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   484
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   485
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   486
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   487
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   488
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   489
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   490
                  | QEx x => And (p', q'))
chaieb@17378
   491
             end
chaieb@17378
   492
         | And (x, xa) =>
chaieb@17378
   493
             let val q' = psimpl q
chaieb@17378
   494
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   495
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   496
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   497
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   498
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   499
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   500
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   501
                  | QEx x => And (p', q'))
chaieb@17378
   502
             end
chaieb@17378
   503
         | Or (x, xa) =>
chaieb@17378
   504
             let val q' = psimpl q
chaieb@17378
   505
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   506
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   507
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   508
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   509
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   510
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   511
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   512
                  | QEx x => And (p', q'))
chaieb@17378
   513
             end
chaieb@17378
   514
         | Imp (x, xa) =>
chaieb@17378
   515
             let val q' = psimpl q
chaieb@17378
   516
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   517
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   518
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   519
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   520
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   521
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   522
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   523
                  | QEx x => And (p', q'))
chaieb@17378
   524
             end
chaieb@17378
   525
         | Equ (x, xa) =>
chaieb@17378
   526
             let val q' = psimpl q
chaieb@17378
   527
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   528
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   529
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   530
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   531
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   532
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   533
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   534
                  | QEx x => And (p', q'))
chaieb@17378
   535
             end
chaieb@17378
   536
         | QAll x =>
chaieb@17378
   537
             let val q' = psimpl q
chaieb@17378
   538
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   539
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   540
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   541
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   542
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   543
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   544
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   545
                  | QEx x => And (p', q'))
chaieb@17378
   546
             end
chaieb@17378
   547
         | QEx x =>
chaieb@17378
   548
             let val q' = psimpl q
chaieb@17378
   549
             in (case q' of Lt (x, xa) => And (p', q')
chaieb@17378
   550
                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
chaieb@17378
   551
                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
chaieb@17378
   552
                  | Divides (x, xa) => And (p', q') | T => p' | F => F
chaieb@17378
   553
                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
chaieb@17378
   554
                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
chaieb@17378
   555
                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
chaieb@17378
   556
                  | QEx x => And (p', q'))
chaieb@17378
   557
             end)
chaieb@17378
   558
    end
chaieb@17378
   559
  | psimpl (Or (p, q)) =
chaieb@17378
   560
    let val p' = psimpl p
chaieb@17378
   561
    in (case p' of
chaieb@17378
   562
         Lt (x, xa) =>
chaieb@17378
   563
           let val q' = psimpl q
chaieb@17378
   564
           in (case q' of Lt (x, xa) => Or (p', q') | Gt (x, xa) => Or (p', q')
chaieb@17378
   565
                | Le (x, xa) => Or (p', q') | Ge (x, xa) => Or (p', q')
chaieb@17378
   566
                | Eq (x, xa) => Or (p', q') | Divides (x, xa) => Or (p', q')
chaieb@17378
   567
                | T => T | F => p' | NOT x => Or (p', q')
chaieb@17378
   568
                | And (x, xa) => Or (p', q') | Or (x, xa) => Or (p', q')
chaieb@17378
   569
                | Imp (x, xa) => Or (p', q') | Equ (x, xa) => Or (p', q')
chaieb@17378
   570
                | QAll x => Or (p', q') | QEx x => Or (p', q'))
chaieb@17378
   571
           end
chaieb@17378
   572
         | Gt (x, xa) =>
chaieb@17378
   573
             let val q' = psimpl q
chaieb@17378
   574
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   575
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   576
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   577
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   578
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   579
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   580
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   581
                  | QEx x => Or (p', q'))
chaieb@17378
   582
             end
chaieb@17378
   583
         | Le (x, xa) =>
chaieb@17378
   584
             let val q' = psimpl q
chaieb@17378
   585
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   586
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   587
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   588
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   589
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   590
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   591
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   592
                  | QEx x => Or (p', q'))
chaieb@17378
   593
             end
chaieb@17378
   594
         | Ge (x, xa) =>
chaieb@17378
   595
             let val q' = psimpl q
chaieb@17378
   596
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   597
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   598
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   599
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   600
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   601
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   602
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   603
                  | QEx x => Or (p', q'))
chaieb@17378
   604
             end
chaieb@17378
   605
         | Eq (x, xa) =>
chaieb@17378
   606
             let val q' = psimpl q
chaieb@17378
   607
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   608
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   609
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   610
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   611
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   612
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   613
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   614
                  | QEx x => Or (p', q'))
chaieb@17378
   615
             end
chaieb@17378
   616
         | Divides (x, xa) =>
chaieb@17378
   617
             let val q' = psimpl q
chaieb@17378
   618
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   619
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   620
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   621
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   622
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   623
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   624
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   625
                  | QEx x => Or (p', q'))
chaieb@17378
   626
             end
chaieb@17378
   627
         | T => T | F => psimpl q
chaieb@17378
   628
         | NOT x =>
chaieb@17378
   629
             let val q' = psimpl q
chaieb@17378
   630
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   631
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   632
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   633
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   634
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   635
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   636
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   637
                  | QEx x => Or (p', q'))
chaieb@17378
   638
             end
chaieb@17378
   639
         | And (x, xa) =>
chaieb@17378
   640
             let val q' = psimpl q
chaieb@17378
   641
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   642
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   643
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   644
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   645
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   646
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   647
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   648
                  | QEx x => Or (p', q'))
chaieb@17378
   649
             end
chaieb@17378
   650
         | Or (x, xa) =>
chaieb@17378
   651
             let val q' = psimpl q
chaieb@17378
   652
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   653
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   654
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   655
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   656
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   657
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   658
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   659
                  | QEx x => Or (p', q'))
chaieb@17378
   660
             end
chaieb@17378
   661
         | Imp (x, xa) =>
chaieb@17378
   662
             let val q' = psimpl q
chaieb@17378
   663
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   664
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   665
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   666
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   667
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   668
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   669
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   670
                  | QEx x => Or (p', q'))
chaieb@17378
   671
             end
chaieb@17378
   672
         | Equ (x, xa) =>
chaieb@17378
   673
             let val q' = psimpl q
chaieb@17378
   674
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   675
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   676
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   677
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   678
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   679
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   680
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   681
                  | QEx x => Or (p', q'))
chaieb@17378
   682
             end
chaieb@17378
   683
         | QAll x =>
chaieb@17378
   684
             let val q' = psimpl q
chaieb@17378
   685
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   686
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   687
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   688
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   689
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   690
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   691
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   692
                  | QEx x => Or (p', q'))
chaieb@17378
   693
             end
chaieb@17378
   694
         | QEx x =>
chaieb@17378
   695
             let val q' = psimpl q
chaieb@17378
   696
             in (case q' of Lt (x, xa) => Or (p', q')
chaieb@17378
   697
                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
chaieb@17378
   698
                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
chaieb@17378
   699
                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
chaieb@17378
   700
                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
chaieb@17378
   701
                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
chaieb@17378
   702
                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
chaieb@17378
   703
                  | QEx x => Or (p', q'))
chaieb@17378
   704
             end)
chaieb@17378
   705
    end
chaieb@17378
   706
  | psimpl (Imp (p, q)) =
chaieb@17378
   707
    let val p' = psimpl p
chaieb@17378
   708
    in (case p' of
chaieb@17378
   709
         Lt (x, xa) =>
chaieb@17378
   710
           let val q' = psimpl q
chaieb@17378
   711
           in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   712
                | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   713
                | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   714
                | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   715
                | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   716
                | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   717
                | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   718
                | QEx x => Imp (p', q'))
chaieb@17378
   719
           end
chaieb@17378
   720
         | Gt (x, xa) =>
chaieb@17378
   721
             let val q' = psimpl q
chaieb@17378
   722
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   723
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   724
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   725
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   726
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   727
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   728
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   729
                  | QEx x => Imp (p', q'))
chaieb@17378
   730
             end
chaieb@17378
   731
         | Le (x, xa) =>
chaieb@17378
   732
             let val q' = psimpl q
chaieb@17378
   733
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   734
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   735
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   736
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   737
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   738
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   739
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   740
                  | QEx x => Imp (p', q'))
chaieb@17378
   741
             end
chaieb@17378
   742
         | Ge (x, xa) =>
chaieb@17378
   743
             let val q' = psimpl q
chaieb@17378
   744
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   745
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   746
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   747
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   748
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   749
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   750
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   751
                  | QEx x => Imp (p', q'))
chaieb@17378
   752
             end
chaieb@17378
   753
         | Eq (x, xa) =>
chaieb@17378
   754
             let val q' = psimpl q
chaieb@17378
   755
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   756
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   757
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   758
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   759
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   760
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   761
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   762
                  | QEx x => Imp (p', q'))
chaieb@17378
   763
             end
chaieb@17378
   764
         | Divides (x, xa) =>
chaieb@17378
   765
             let val q' = psimpl q
chaieb@17378
   766
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   767
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   768
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   769
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   770
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   771
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   772
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   773
                  | QEx x => Imp (p', q'))
chaieb@17378
   774
             end
chaieb@17378
   775
         | T => psimpl q | F => T
chaieb@17378
   776
         | NOT x =>
chaieb@17378
   777
             let val q' = psimpl q
chaieb@17378
   778
             in (case q' of Lt (xa, xb) => Or (x, q')
chaieb@17378
   779
                  | Gt (xa, xb) => Or (x, q') | Le (xa, xb) => Or (x, q')
chaieb@17378
   780
                  | Ge (xa, xb) => Or (x, q') | Eq (xa, xb) => Or (x, q')
chaieb@17378
   781
                  | Divides (xa, xb) => Or (x, q') | T => T | F => x
chaieb@17378
   782
                  | NOT xa => Or (x, q') | And (xa, xb) => Or (x, q')
chaieb@17378
   783
                  | Or (xa, xb) => Or (x, q') | Imp (xa, xb) => Or (x, q')
chaieb@17378
   784
                  | Equ (xa, xb) => Or (x, q') | QAll xa => Or (x, q')
chaieb@17378
   785
                  | QEx xa => Or (x, q'))
chaieb@17378
   786
             end
chaieb@17378
   787
         | And (x, xa) =>
chaieb@17378
   788
             let val q' = psimpl q
chaieb@17378
   789
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   790
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   791
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   792
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   793
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   794
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   795
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   796
                  | QEx x => Imp (p', q'))
chaieb@17378
   797
             end
chaieb@17378
   798
         | Or (x, xa) =>
chaieb@17378
   799
             let val q' = psimpl q
chaieb@17378
   800
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   801
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   802
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   803
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   804
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   805
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   806
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   807
                  | QEx x => Imp (p', q'))
chaieb@17378
   808
             end
chaieb@17378
   809
         | Imp (x, xa) =>
chaieb@17378
   810
             let val q' = psimpl q
chaieb@17378
   811
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   812
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   813
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   814
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   815
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   816
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   817
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   818
                  | QEx x => Imp (p', q'))
chaieb@17378
   819
             end
chaieb@17378
   820
         | Equ (x, xa) =>
chaieb@17378
   821
             let val q' = psimpl q
chaieb@17378
   822
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   823
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   824
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   825
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   826
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   827
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   828
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   829
                  | QEx x => Imp (p', q'))
chaieb@17378
   830
             end
chaieb@17378
   831
         | QAll x =>
chaieb@17378
   832
             let val q' = psimpl q
chaieb@17378
   833
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   834
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   835
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   836
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   837
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   838
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   839
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   840
                  | QEx x => Imp (p', q'))
chaieb@17378
   841
             end
chaieb@17378
   842
         | QEx x =>
chaieb@17378
   843
             let val q' = psimpl q
chaieb@17378
   844
             in (case q' of Lt (x, xa) => Imp (p', q')
chaieb@17378
   845
                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
chaieb@17378
   846
                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
chaieb@17378
   847
                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
chaieb@17378
   848
                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
chaieb@17378
   849
                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
chaieb@17378
   850
                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
chaieb@17378
   851
                  | QEx x => Imp (p', q'))
chaieb@17378
   852
             end)
chaieb@17378
   853
    end;
chaieb@17378
   854
chaieb@17378
   855
fun subst_it i (Cst b) = Cst b
chaieb@17378
   856
  | subst_it i (Var n) = (if (n = 0) then i else Var n)
chaieb@17378
   857
  | subst_it i (Neg it) = Neg (subst_it i it)
chaieb@17378
   858
  | subst_it i (Add (it1, it2)) = Add (subst_it i it1, subst_it i it2)
chaieb@17378
   859
  | subst_it i (Sub (it1, it2)) = Sub (subst_it i it1, subst_it i it2)
chaieb@17378
   860
  | subst_it i (Mult (it1, it2)) = Mult (subst_it i it1, subst_it i it2);
chaieb@17378
   861
chaieb@17378
   862
fun subst_p i (Le (it1, it2)) = Le (subst_it i it1, subst_it i it2)
chaieb@17378
   863
  | subst_p i (Lt (it1, it2)) = Lt (subst_it i it1, subst_it i it2)
chaieb@17378
   864
  | subst_p i (Ge (it1, it2)) = Ge (subst_it i it1, subst_it i it2)
chaieb@17378
   865
  | subst_p i (Gt (it1, it2)) = Gt (subst_it i it1, subst_it i it2)
chaieb@17378
   866
  | subst_p i (Eq (it1, it2)) = Eq (subst_it i it1, subst_it i it2)
chaieb@17378
   867
  | subst_p i (Divides (d, t)) = Divides (subst_it i d, subst_it i t)
chaieb@17378
   868
  | subst_p i T = T
chaieb@17378
   869
  | subst_p i F = F
chaieb@17378
   870
  | subst_p i (And (p, q)) = And (subst_p i p, subst_p i q)
chaieb@17378
   871
  | subst_p i (Or (p, q)) = Or (subst_p i p, subst_p i q)
chaieb@17378
   872
  | subst_p i (Imp (p, q)) = Imp (subst_p i p, subst_p i q)
chaieb@17378
   873
  | subst_p i (Equ (p, q)) = Equ (subst_p i p, subst_p i q)
chaieb@17378
   874
  | subst_p i (NOT p) = NOT (subst_p i p);
chaieb@17378
   875
chaieb@17378
   876
fun explode_disj ([], p) = F
chaieb@17378
   877
  | explode_disj ((i :: is), p) =
chaieb@17378
   878
    let val pi = psimpl (subst_p i p)
chaieb@17378
   879
    in (case pi of
chaieb@17378
   880
         Lt (x, xa) =>
chaieb@17378
   881
           let val r = explode_disj (is, p)
chaieb@17378
   882
           in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   883
                | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   884
                | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   885
                | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   886
                | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   887
                | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   888
                | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   889
           end
chaieb@17378
   890
         | Gt (x, xa) =>
chaieb@17378
   891
             let val r = explode_disj (is, p)
chaieb@17378
   892
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   893
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   894
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   895
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   896
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   897
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   898
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   899
             end
chaieb@17378
   900
         | Le (x, xa) =>
chaieb@17378
   901
             let val r = explode_disj (is, p)
chaieb@17378
   902
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   903
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   904
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   905
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   906
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   907
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   908
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   909
             end
chaieb@17378
   910
         | Ge (x, xa) =>
chaieb@17378
   911
             let val r = explode_disj (is, p)
chaieb@17378
   912
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   913
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   914
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   915
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   916
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   917
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   918
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   919
             end
chaieb@17378
   920
         | Eq (x, xa) =>
chaieb@17378
   921
             let val r = explode_disj (is, p)
chaieb@17378
   922
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   923
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   924
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   925
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   926
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   927
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   928
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   929
             end
chaieb@17378
   930
         | Divides (x, xa) =>
chaieb@17378
   931
             let val r = explode_disj (is, p)
chaieb@17378
   932
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   933
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   934
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   935
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   936
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   937
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   938
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   939
             end
chaieb@17378
   940
         | T => T | F => explode_disj (is, p)
chaieb@17378
   941
         | NOT x =>
chaieb@17378
   942
             let val r = explode_disj (is, p)
chaieb@17378
   943
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   944
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   945
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   946
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   947
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   948
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   949
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   950
             end
chaieb@17378
   951
         | And (x, xa) =>
chaieb@17378
   952
             let val r = explode_disj (is, p)
chaieb@17378
   953
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   954
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   955
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   956
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   957
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   958
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   959
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   960
             end
chaieb@17378
   961
         | Or (x, xa) =>
chaieb@17378
   962
             let val r = explode_disj (is, p)
chaieb@17378
   963
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   964
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   965
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   966
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   967
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   968
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   969
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   970
             end
chaieb@17378
   971
         | Imp (x, xa) =>
chaieb@17378
   972
             let val r = explode_disj (is, p)
chaieb@17378
   973
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   974
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   975
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   976
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   977
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   978
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   979
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   980
             end
chaieb@17378
   981
         | Equ (x, xa) =>
chaieb@17378
   982
             let val r = explode_disj (is, p)
chaieb@17378
   983
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   984
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   985
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   986
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   987
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   988
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   989
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
   990
             end
chaieb@17378
   991
         | QAll x =>
chaieb@17378
   992
             let val r = explode_disj (is, p)
chaieb@17378
   993
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
   994
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
   995
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
   996
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
   997
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
   998
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
   999
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
  1000
             end
chaieb@17378
  1001
         | QEx x =>
chaieb@17378
  1002
             let val r = explode_disj (is, p)
chaieb@17378
  1003
             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
chaieb@17378
  1004
                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
chaieb@17378
  1005
                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
chaieb@17378
  1006
                  | T => T | F => pi | NOT x => Or (pi, r)
chaieb@17378
  1007
                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
chaieb@17378
  1008
                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
chaieb@17378
  1009
                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
chaieb@17378
  1010
             end)
chaieb@17378
  1011
    end;
chaieb@17378
  1012
chaieb@17378
  1013
fun minusinf (And (p, q)) = And (minusinf p, minusinf q)
chaieb@17378
  1014
  | minusinf (Or (p, q)) = Or (minusinf p, minusinf q)
chaieb@17378
  1015
  | minusinf (Lt (u, v)) = Lt (u, v)
chaieb@17378
  1016
  | minusinf (Gt (w, x)) = Gt (w, x)
chaieb@17378
  1017
  | minusinf (Le (Cst bo, z)) = Le (Cst bo, z)
chaieb@17378
  1018
  | minusinf (Le (Var bp, z)) = Le (Var bp, z)
chaieb@17378
  1019
  | minusinf (Le (Neg bq, z)) = Le (Neg bq, z)
chaieb@17378
  1020
  | minusinf (Le (Add (Cst cg, bs), z)) = Le (Add (Cst cg, bs), z)
chaieb@17378
  1021
  | minusinf (Le (Add (Var ch, bs), z)) = Le (Add (Var ch, bs), z)
chaieb@17378
  1022
  | minusinf (Le (Add (Neg ci, bs), z)) = Le (Add (Neg ci, bs), z)
chaieb@17378
  1023
  | minusinf (Le (Add (Add (cj, ck), bs), z)) = Le (Add (Add (cj, ck), bs), z)
chaieb@17378
  1024
  | minusinf (Le (Add (Sub (cl, cm), bs), z)) = Le (Add (Sub (cl, cm), bs), z)
chaieb@17378
  1025
  | minusinf (Le (Add (Mult (Cst cy, Cst dq), bs), z)) =
chaieb@17378
  1026
    Le (Add (Mult (Cst cy, Cst dq), bs), z)
chaieb@17378
  1027
  | minusinf (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
chaieb@17378
  1028
    (if (ei = 0) then (if (cy < 0) then F else T)
chaieb@17378
  1029
      else Le (Add (Mult (Cst cy, Var (op_45_def0 ei id_1_def0 + 1)), bs), z))
chaieb@17378
  1030
  | minusinf (Le (Add (Mult (Cst cy, Neg ds), bs), z)) =
chaieb@17378
  1031
    Le (Add (Mult (Cst cy, Neg ds), bs), z)
chaieb@17378
  1032
  | minusinf (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) =
chaieb@17378
  1033
    Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)
chaieb@17378
  1034
  | minusinf (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) =
chaieb@17378
  1035
    Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)
chaieb@17378
  1036
  | minusinf (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) =
chaieb@17378
  1037
    Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)
chaieb@17378
  1038
  | minusinf (Le (Add (Mult (Var cz, co), bs), z)) =
chaieb@17378
  1039
    Le (Add (Mult (Var cz, co), bs), z)
chaieb@17378
  1040
  | minusinf (Le (Add (Mult (Neg da, co), bs), z)) =
chaieb@17378
  1041
    Le (Add (Mult (Neg da, co), bs), z)
chaieb@17378
  1042
  | minusinf (Le (Add (Mult (Add (db, dc), co), bs), z)) =
chaieb@17378
  1043
    Le (Add (Mult (Add (db, dc), co), bs), z)
chaieb@17378
  1044
  | minusinf (Le (Add (Mult (Sub (dd, de), co), bs), z)) =
chaieb@17378
  1045
    Le (Add (Mult (Sub (dd, de), co), bs), z)
chaieb@17378
  1046
  | minusinf (Le (Add (Mult (Mult (df, dg), co), bs), z)) =
chaieb@17378
  1047
    Le (Add (Mult (Mult (df, dg), co), bs), z)
chaieb@17378
  1048
  | minusinf (Le (Sub (bt, bu), z)) = Le (Sub (bt, bu), z)
chaieb@17378
  1049
  | minusinf (Le (Mult (bv, bw), z)) = Le (Mult (bv, bw), z)
chaieb@17378
  1050
  | minusinf (Ge (aa, ab)) = Ge (aa, ab)
chaieb@17378
  1051
  | minusinf (Eq (Cst ek, ad)) = Eq (Cst ek, ad)
chaieb@17378
  1052
  | minusinf (Eq (Var el, ad)) = Eq (Var el, ad)
chaieb@17378
  1053
  | minusinf (Eq (Neg em, ad)) = Eq (Neg em, ad)
chaieb@17378
  1054
  | minusinf (Eq (Add (Cst fc, eo), ad)) = Eq (Add (Cst fc, eo), ad)
chaieb@17378
  1055
  | minusinf (Eq (Add (Var fd, eo), ad)) = Eq (Add (Var fd, eo), ad)
chaieb@17378
  1056
  | minusinf (Eq (Add (Neg fe, eo), ad)) = Eq (Add (Neg fe, eo), ad)
chaieb@17378
  1057
  | minusinf (Eq (Add (Add (ff, fg), eo), ad)) = Eq (Add (Add (ff, fg), eo), ad)
chaieb@17378
  1058
  | minusinf (Eq (Add (Sub (fh, fi), eo), ad)) = Eq (Add (Sub (fh, fi), eo), ad)
chaieb@17378
  1059
  | minusinf (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) =
chaieb@17378
  1060
    Eq (Add (Mult (Cst fu, Cst gm), eo), ad)
chaieb@17378
  1061
  | minusinf (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
chaieb@17378
  1062
    (if (he = 0) then F
chaieb@17378
  1063
      else Eq (Add (Mult (Cst fu, Var (op_45_def0 he id_1_def0 + 1)), eo), ad))
chaieb@17378
  1064
  | minusinf (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) =
chaieb@17378
  1065
    Eq (Add (Mult (Cst fu, Neg go), eo), ad)
chaieb@17378
  1066
  | minusinf (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) =
chaieb@17378
  1067
    Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)
chaieb@17378
  1068
  | minusinf (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) =
chaieb@17378
  1069
    Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)
chaieb@17378
  1070
  | minusinf (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) =
chaieb@17378
  1071
    Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)
chaieb@17378
  1072
  | minusinf (Eq (Add (Mult (Var fv, fk), eo), ad)) =
chaieb@17378
  1073
    Eq (Add (Mult (Var fv, fk), eo), ad)
chaieb@17378
  1074
  | minusinf (Eq (Add (Mult (Neg fw, fk), eo), ad)) =
chaieb@17378
  1075
    Eq (Add (Mult (Neg fw, fk), eo), ad)
chaieb@17378
  1076
  | minusinf (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) =
chaieb@17378
  1077
    Eq (Add (Mult (Add (fx, fy), fk), eo), ad)
chaieb@17378
  1078
  | minusinf (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) =
chaieb@17378
  1079
    Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)
chaieb@17378
  1080
  | minusinf (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) =
chaieb@17378
  1081
    Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)
chaieb@17378
  1082
  | minusinf (Eq (Sub (ep, eq), ad)) = Eq (Sub (ep, eq), ad)
chaieb@17378
  1083
  | minusinf (Eq (Mult (er, es), ad)) = Eq (Mult (er, es), ad)
chaieb@17378
  1084
  | minusinf (Divides (ae, af)) = Divides (ae, af)
chaieb@17378
  1085
  | minusinf T = T
chaieb@17378
  1086
  | minusinf F = F
chaieb@17378
  1087
  | minusinf (NOT (Lt (hg, hh))) = NOT (Lt (hg, hh))
chaieb@17378
  1088
  | minusinf (NOT (Gt (hi, hj))) = NOT (Gt (hi, hj))
chaieb@17378
  1089
  | minusinf (NOT (Le (hk, hl))) = NOT (Le (hk, hl))
chaieb@17378
  1090
  | minusinf (NOT (Ge (hm, hn))) = NOT (Ge (hm, hn))
chaieb@17378
  1091
  | minusinf (NOT (Eq (Cst ja, hp))) = NOT (Eq (Cst ja, hp))
chaieb@17378
  1092
  | minusinf (NOT (Eq (Var jb, hp))) = NOT (Eq (Var jb, hp))
chaieb@17378
  1093
  | minusinf (NOT (Eq (Neg jc, hp))) = NOT (Eq (Neg jc, hp))
chaieb@17378
  1094
  | minusinf (NOT (Eq (Add (Cst js, je), hp))) = NOT (Eq (Add (Cst js, je), hp))
chaieb@17378
  1095
  | minusinf (NOT (Eq (Add (Var jt, je), hp))) = NOT (Eq (Add (Var jt, je), hp))
chaieb@17378
  1096
  | minusinf (NOT (Eq (Add (Neg ju, je), hp))) = NOT (Eq (Add (Neg ju, je), hp))
chaieb@17378
  1097
  | minusinf (NOT (Eq (Add (Add (jv, jw), je), hp))) =
chaieb@17378
  1098
    NOT (Eq (Add (Add (jv, jw), je), hp))
chaieb@17378
  1099
  | minusinf (NOT (Eq (Add (Sub (jx, jy), je), hp))) =
chaieb@17378
  1100
    NOT (Eq (Add (Sub (jx, jy), je), hp))
chaieb@17378
  1101
  | minusinf (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) =
chaieb@17378
  1102
    NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))
chaieb@17378
  1103
  | minusinf (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
chaieb@17378
  1104
    (if (lu = 0) then T
chaieb@17378
  1105
      else NOT (Eq (Add (Mult (Cst kk, Var (op_45_def0 lu id_1_def0 + 1)), je),
chaieb@17378
  1106
                     hp)))
chaieb@17378
  1107
  | minusinf (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) =
chaieb@17378
  1108
    NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))
chaieb@17378
  1109
  | minusinf (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) =
chaieb@17378
  1110
    NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))
chaieb@17378
  1111
  | minusinf (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) =
chaieb@17378
  1112
    NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))
chaieb@17378
  1113
  | minusinf (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) =
chaieb@17378
  1114
    NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))
chaieb@17378
  1115
  | minusinf (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) =
chaieb@17378
  1116
    NOT (Eq (Add (Mult (Var kl, ka), je), hp))
chaieb@17378
  1117
  | minusinf (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) =
chaieb@17378
  1118
    NOT (Eq (Add (Mult (Neg km, ka), je), hp))
chaieb@17378
  1119
  | minusinf (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) =
chaieb@17378
  1120
    NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))
chaieb@17378
  1121
  | minusinf (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) =
chaieb@17378
  1122
    NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))
chaieb@17378
  1123
  | minusinf (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) =
chaieb@17378
  1124
    NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))
chaieb@17378
  1125
  | minusinf (NOT (Eq (Sub (jf, jg), hp))) = NOT (Eq (Sub (jf, jg), hp))
chaieb@17378
  1126
  | minusinf (NOT (Eq (Mult (jh, ji), hp))) = NOT (Eq (Mult (jh, ji), hp))
chaieb@17378
  1127
  | minusinf (NOT (Divides (hq, hr))) = NOT (Divides (hq, hr))
chaieb@17378
  1128
  | minusinf (NOT T) = NOT T
chaieb@17378
  1129
  | minusinf (NOT F) = NOT F
chaieb@17378
  1130
  | minusinf (NOT (NOT hs)) = NOT (NOT hs)
chaieb@17378
  1131
  | minusinf (NOT (And (ht, hu))) = NOT (And (ht, hu))
chaieb@17378
  1132
  | minusinf (NOT (Or (hv, hw))) = NOT (Or (hv, hw))
chaieb@17378
  1133
  | minusinf (NOT (Imp (hx, hy))) = NOT (Imp (hx, hy))
chaieb@17378
  1134
  | minusinf (NOT (Equ (hz, ia))) = NOT (Equ (hz, ia))
chaieb@17378
  1135
  | minusinf (NOT (QAll ib)) = NOT (QAll ib)
chaieb@17378
  1136
  | minusinf (NOT (QEx ic)) = NOT (QEx ic)
chaieb@17378
  1137
  | minusinf (Imp (al, am)) = Imp (al, am)
chaieb@17378
  1138
  | minusinf (Equ (an, ao)) = Equ (an, ao)
chaieb@17378
  1139
  | minusinf (QAll ap) = QAll ap
chaieb@17378
  1140
  | minusinf (QEx aq) = QEx aq;
chaieb@17378
  1141
chaieb@17390
  1142
fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
chaieb@17378
  1143
chaieb@17390
  1144
fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
chaieb@17378
  1145
chaieb@17378
  1146
fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
chaieb@17378
  1147
chaieb@17390
  1148
fun ngcd (m:IntInf.int, n:IntInf.int) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
chaieb@17378
  1149
chaieb@17378
  1150
fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
chaieb@17378
  1151
chaieb@17390
  1152
fun ilcm (a:IntInf.int) (b:IntInf.int) = op_div_def1 (a * b) (igcd (a, b));
chaieb@17378
  1153
chaieb@17378
  1154
fun divlcm (NOT p) = divlcm p
chaieb@17378
  1155
  | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
chaieb@17378
  1156
  | divlcm (Or (p, q)) = ilcm (divlcm p) (divlcm q)
chaieb@17378
  1157
  | divlcm (Lt (u, v)) = 1
chaieb@17378
  1158
  | divlcm (Gt (w, x)) = 1
chaieb@17378
  1159
  | divlcm (Le (y, z)) = 1
chaieb@17378
  1160
  | divlcm (Ge (aa, ab)) = 1
chaieb@17378
  1161
  | divlcm (Eq (ac, ad)) = 1
chaieb@17378
  1162
  | divlcm (Divides (Cst bo, Cst cg)) = 1
chaieb@17378
  1163
  | divlcm (Divides (Cst bo, Var ch)) = 1
chaieb@17378
  1164
  | divlcm (Divides (Cst bo, Neg ci)) = 1
chaieb@17378
  1165
  | divlcm (Divides (Cst bo, Add (Cst cy, ck))) = 1
chaieb@17378
  1166
  | divlcm (Divides (Cst bo, Add (Var cz, ck))) = 1
chaieb@17378
  1167
  | divlcm (Divides (Cst bo, Add (Neg da, ck))) = 1
chaieb@17378
  1168
  | divlcm (Divides (Cst bo, Add (Add (db, dc), ck))) = 1
chaieb@17378
  1169
  | divlcm (Divides (Cst bo, Add (Sub (dd, de), ck))) = 1
chaieb@17378
  1170
  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Cst ei), ck))) = 1
chaieb@17378
  1171
  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Var fa), ck))) =
chaieb@17378
  1172
    (if (fa = 0) then abs bo else 1)
chaieb@17378
  1173
  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Neg ek), ck))) = 1
chaieb@17378
  1174
  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Add (el, em)), ck))) = 1
chaieb@17378
  1175
  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Sub (en, eo)), ck))) = 1
chaieb@17378
  1176
  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Mult (ep, eq)), ck))) = 1
chaieb@17378
  1177
  | divlcm (Divides (Cst bo, Add (Mult (Var dr, dg), ck))) = 1
chaieb@17378
  1178
  | divlcm (Divides (Cst bo, Add (Mult (Neg ds, dg), ck))) = 1
chaieb@17378
  1179
  | divlcm (Divides (Cst bo, Add (Mult (Add (dt, du), dg), ck))) = 1
chaieb@17378
  1180
  | divlcm (Divides (Cst bo, Add (Mult (Sub (dv, dw), dg), ck))) = 1
chaieb@17378
  1181
  | divlcm (Divides (Cst bo, Add (Mult (Mult (dx, dy), dg), ck))) = 1
chaieb@17378
  1182
  | divlcm (Divides (Cst bo, Sub (cl, cm))) = 1
chaieb@17378
  1183
  | divlcm (Divides (Cst bo, Mult (cn, co))) = 1
chaieb@17378
  1184
  | divlcm (Divides (Var bp, af)) = 1
chaieb@17378
  1185
  | divlcm (Divides (Neg bq, af)) = 1
chaieb@17378
  1186
  | divlcm (Divides (Add (br, bs), af)) = 1
chaieb@17378
  1187
  | divlcm (Divides (Sub (bt, bu), af)) = 1
chaieb@17378
  1188
  | divlcm (Divides (Mult (bv, bw), af)) = 1
chaieb@17378
  1189
  | divlcm T = 1
chaieb@17378
  1190
  | divlcm F = 1
chaieb@17378
  1191
  | divlcm (Imp (al, am)) = 1
chaieb@17378
  1192
  | divlcm (Equ (an, ao)) = 1
chaieb@17378
  1193
  | divlcm (QAll ap) = 1
chaieb@17378
  1194
  | divlcm (QEx aq) = 1;
chaieb@17378
  1195
chaieb@17378
  1196
fun explode_minf (q, B) =
chaieb@17378
  1197
    let val d = divlcm q; val pm = minusinf q;
chaieb@17378
  1198
        val dj1 = explode_disj (map (fn x => Cst x) (iupto (1, d)), pm)
chaieb@17378
  1199
    in (case dj1 of
chaieb@17378
  1200
         Lt (x, xa) =>
chaieb@17378
  1201
           let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1202
           in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1203
                | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1204
                | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1205
                | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1206
                | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1207
                | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1208
                | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1209
                | QEx x => Or (dj1, dj2))
chaieb@17378
  1210
           end
chaieb@17378
  1211
         | Gt (x, xa) =>
chaieb@17378
  1212
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1213
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1214
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1215
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1216
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1217
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1218
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1219
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1220
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1221
             end
chaieb@17378
  1222
         | Le (x, xa) =>
chaieb@17378
  1223
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1224
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1225
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1226
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1227
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1228
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1229
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1230
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1231
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1232
             end
chaieb@17378
  1233
         | Ge (x, xa) =>
chaieb@17378
  1234
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1235
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1236
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1237
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1238
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1239
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1240
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1241
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1242
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1243
             end
chaieb@17378
  1244
         | Eq (x, xa) =>
chaieb@17378
  1245
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1246
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1247
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1248
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1249
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1250
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1251
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1252
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1253
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1254
             end
chaieb@17378
  1255
         | Divides (x, xa) =>
chaieb@17378
  1256
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1257
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1258
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1259
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1260
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1261
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1262
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1263
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1264
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1265
             end
chaieb@17378
  1266
         | T => T | F => explode_disj (all_sums (d, B), q)
chaieb@17378
  1267
         | NOT x =>
chaieb@17378
  1268
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1269
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1270
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1271
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1272
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1273
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1274
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1275
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1276
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1277
             end
chaieb@17378
  1278
         | And (x, xa) =>
chaieb@17378
  1279
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1280
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1281
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1282
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1283
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1284
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1285
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1286
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1287
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1288
             end
chaieb@17378
  1289
         | Or (x, xa) =>
chaieb@17378
  1290
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1291
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1292
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1293
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1294
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1295
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1296
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1297
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1298
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1299
             end
chaieb@17378
  1300
         | Imp (x, xa) =>
chaieb@17378
  1301
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1302
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1303
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1304
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1305
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1306
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1307
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1308
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1309
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1310
             end
chaieb@17378
  1311
         | Equ (x, xa) =>
chaieb@17378
  1312
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1313
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1314
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1315
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1316
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1317
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1318
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1319
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1320
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1321
             end
chaieb@17378
  1322
         | QAll x =>
chaieb@17378
  1323
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1324
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1325
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1326
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1327
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1328
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1329
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1330
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1331
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1332
             end
chaieb@17378
  1333
         | QEx x =>
chaieb@17378
  1334
             let val dj2 = explode_disj (all_sums (d, B), q)
chaieb@17378
  1335
             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
chaieb@17378
  1336
                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
chaieb@17378
  1337
                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
chaieb@17378
  1338
                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
chaieb@17378
  1339
                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
chaieb@17378
  1340
                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
chaieb@17378
  1341
                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
chaieb@17378
  1342
                  | QEx x => Or (dj1, dj2))
chaieb@17378
  1343
             end)
chaieb@17378
  1344
    end;
chaieb@17378
  1345
chaieb@17378
  1346
fun mirror (And (p, q)) = And (mirror p, mirror q)
chaieb@17378
  1347
  | mirror (Or (p, q)) = Or (mirror p, mirror q)
chaieb@17378
  1348
  | mirror (Lt (u, v)) = Lt (u, v)
chaieb@17378
  1349
  | mirror (Gt (w, x)) = Gt (w, x)
chaieb@17378
  1350
  | mirror (Le (Cst bp, aa)) = Le (Cst bp, aa)
chaieb@17378
  1351
  | mirror (Le (Var bq, aa)) = Le (Var bq, aa)
chaieb@17378
  1352
  | mirror (Le (Neg br, aa)) = Le (Neg br, aa)
chaieb@17378
  1353
  | mirror (Le (Add (Cst ch, bt), aa)) = Le (Add (Cst ch, bt), aa)
chaieb@17378
  1354
  | mirror (Le (Add (Var ci, bt), aa)) = Le (Add (Var ci, bt), aa)
chaieb@17378
  1355
  | mirror (Le (Add (Neg cj, bt), aa)) = Le (Add (Neg cj, bt), aa)
chaieb@17378
  1356
  | mirror (Le (Add (Add (ck, cl), bt), aa)) = Le (Add (Add (ck, cl), bt), aa)
chaieb@17378
  1357
  | mirror (Le (Add (Sub (cm, cn), bt), aa)) = Le (Add (Sub (cm, cn), bt), aa)
chaieb@17378
  1358
  | mirror (Le (Add (Mult (Cst cz, Cst dr), bt), aa)) =
chaieb@17378
  1359
    Le (Add (Mult (Cst cz, Cst dr), bt), aa)
chaieb@17378
  1360
  | mirror (Le (Add (Mult (Cst cz, Var ej), bt), aa)) =
chaieb@17378
  1361
    (if (ej = 0) then Le (Add (Mult (Cst (~ cz), Var 0), bt), aa)
chaieb@17378
  1362
      else Le (Add (Mult (Cst cz, Var (op_45_def0 ej id_1_def0 + 1)), bt), aa))
chaieb@17378
  1363
  | mirror (Le (Add (Mult (Cst cz, Neg dt), bt), aa)) =
chaieb@17378
  1364
    Le (Add (Mult (Cst cz, Neg dt), bt), aa)
chaieb@17378
  1365
  | mirror (Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)) =
chaieb@17378
  1366
    Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)
chaieb@17378
  1367
  | mirror (Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)) =
chaieb@17378
  1368
    Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)
chaieb@17378
  1369
  | mirror (Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)) =
chaieb@17378
  1370
    Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)
chaieb@17378
  1371
  | mirror (Le (Add (Mult (Var da, cp), bt), aa)) =
chaieb@17378
  1372
    Le (Add (Mult (Var da, cp), bt), aa)
chaieb@17378
  1373
  | mirror (Le (Add (Mult (Neg db, cp), bt), aa)) =
chaieb@17378
  1374
    Le (Add (Mult (Neg db, cp), bt), aa)
chaieb@17378
  1375
  | mirror (Le (Add (Mult (Add (dc, dd), cp), bt), aa)) =
chaieb@17378
  1376
    Le (Add (Mult (Add (dc, dd), cp), bt), aa)
chaieb@17378
  1377
  | mirror (Le (Add (Mult (Sub (de, df), cp), bt), aa)) =
chaieb@17378
  1378
    Le (Add (Mult (Sub (de, df), cp), bt), aa)
chaieb@17378
  1379
  | mirror (Le (Add (Mult (Mult (dg, dh), cp), bt), aa)) =
chaieb@17378
  1380
    Le (Add (Mult (Mult (dg, dh), cp), bt), aa)
chaieb@17378
  1381
  | mirror (Le (Sub (bu, bv), aa)) = Le (Sub (bu, bv), aa)
chaieb@17378
  1382
  | mirror (Le (Mult (bw, bx), aa)) = Le (Mult (bw, bx), aa)
chaieb@17378
  1383
  | mirror (Ge (ab, ac)) = Ge (ab, ac)
chaieb@17378
  1384
  | mirror (Eq (Cst el, ae)) = Eq (Cst el, ae)
chaieb@17378
  1385
  | mirror (Eq (Var em, ae)) = Eq (Var em, ae)
chaieb@17378
  1386
  | mirror (Eq (Neg en, ae)) = Eq (Neg en, ae)
chaieb@17378
  1387
  | mirror (Eq (Add (Cst fd, ep), ae)) = Eq (Add (Cst fd, ep), ae)
chaieb@17378
  1388
  | mirror (Eq (Add (Var fe, ep), ae)) = Eq (Add (Var fe, ep), ae)
chaieb@17378
  1389
  | mirror (Eq (Add (Neg ff, ep), ae)) = Eq (Add (Neg ff, ep), ae)
chaieb@17378
  1390
  | mirror (Eq (Add (Add (fg, fh), ep), ae)) = Eq (Add (Add (fg, fh), ep), ae)
chaieb@17378
  1391
  | mirror (Eq (Add (Sub (fi, fj), ep), ae)) = Eq (Add (Sub (fi, fj), ep), ae)
chaieb@17378
  1392
  | mirror (Eq (Add (Mult (Cst fv, Cst gn), ep), ae)) =
chaieb@17378
  1393
    Eq (Add (Mult (Cst fv, Cst gn), ep), ae)
chaieb@17378
  1394
  | mirror (Eq (Add (Mult (Cst fv, Var hf), ep), ae)) =
chaieb@17378
  1395
    (if (hf = 0) then Eq (Add (Mult (Cst (~ fv), Var 0), ep), ae)
chaieb@17378
  1396
      else Eq (Add (Mult (Cst fv, Var (op_45_def0 hf id_1_def0 + 1)), ep), ae))
chaieb@17378
  1397
  | mirror (Eq (Add (Mult (Cst fv, Neg gp), ep), ae)) =
chaieb@17378
  1398
    Eq (Add (Mult (Cst fv, Neg gp), ep), ae)
chaieb@17378
  1399
  | mirror (Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)) =
chaieb@17378
  1400
    Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)
chaieb@17378
  1401
  | mirror (Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)) =
chaieb@17378
  1402
    Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)
chaieb@17378
  1403
  | mirror (Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)) =
chaieb@17378
  1404
    Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)
chaieb@17378
  1405
  | mirror (Eq (Add (Mult (Var fw, fl), ep), ae)) =
chaieb@17378
  1406
    Eq (Add (Mult (Var fw, fl), ep), ae)
chaieb@17378
  1407
  | mirror (Eq (Add (Mult (Neg fx, fl), ep), ae)) =
chaieb@17378
  1408
    Eq (Add (Mult (Neg fx, fl), ep), ae)
chaieb@17378
  1409
  | mirror (Eq (Add (Mult (Add (fy, fz), fl), ep), ae)) =
chaieb@17378
  1410
    Eq (Add (Mult (Add (fy, fz), fl), ep), ae)
chaieb@17378
  1411
  | mirror (Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)) =
chaieb@17378
  1412
    Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)
chaieb@17378
  1413
  | mirror (Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)) =
chaieb@17378
  1414
    Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)
chaieb@17378
  1415
  | mirror (Eq (Sub (eq, er), ae)) = Eq (Sub (eq, er), ae)
chaieb@17378
  1416
  | mirror (Eq (Mult (es, et), ae)) = Eq (Mult (es, et), ae)
chaieb@17378
  1417
  | mirror (Divides (Cst hh, Cst hz)) = Divides (Cst hh, Cst hz)
chaieb@17378
  1418
  | mirror (Divides (Cst hh, Var ia)) = Divides (Cst hh, Var ia)
chaieb@17378
  1419
  | mirror (Divides (Cst hh, Neg ib)) = Divides (Cst hh, Neg ib)
chaieb@17378
  1420
  | mirror (Divides (Cst hh, Add (Cst ir, id))) =
chaieb@17378
  1421
    Divides (Cst hh, Add (Cst ir, id))
chaieb@17378
  1422
  | mirror (Divides (Cst hh, Add (Var is, id))) =
chaieb@17378
  1423
    Divides (Cst hh, Add (Var is, id))
chaieb@17378
  1424
  | mirror (Divides (Cst hh, Add (Neg it, id))) =
chaieb@17378
  1425
    Divides (Cst hh, Add (Neg it, id))
chaieb@17378
  1426
  | mirror (Divides (Cst hh, Add (Add (iu, iv), id))) =
chaieb@17378
  1427
    Divides (Cst hh, Add (Add (iu, iv), id))
chaieb@17378
  1428
  | mirror (Divides (Cst hh, Add (Sub (iw, ix), id))) =
chaieb@17378
  1429
    Divides (Cst hh, Add (Sub (iw, ix), id))
chaieb@17378
  1430
  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))) =
chaieb@17378
  1431
    Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))
chaieb@17378
  1432
  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Var kt), id))) =
chaieb@17378
  1433
    (if (kt = 0) then Divides (Cst hh, Add (Mult (Cst (~ jj), Var 0), id))
chaieb@17378
  1434
      else Divides
chaieb@17378
  1435
             (Cst hh,
chaieb@17378
  1436
               Add (Mult (Cst jj, Var (op_45_def0 kt id_1_def0 + 1)), id)))
chaieb@17378
  1437
  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))) =
chaieb@17378
  1438
    Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))
chaieb@17378
  1439
  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))) =
chaieb@17378
  1440
    Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))
chaieb@17378
  1441
  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))) =
chaieb@17378
  1442
    Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))
chaieb@17378
  1443
  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))) =
chaieb@17378
  1444
    Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))
chaieb@17378
  1445
  | mirror (Divides (Cst hh, Add (Mult (Var jk, iz), id))) =
chaieb@17378
  1446
    Divides (Cst hh, Add (Mult (Var jk, iz), id))
chaieb@17378
  1447
  | mirror (Divides (Cst hh, Add (Mult (Neg jl, iz), id))) =
chaieb@17378
  1448
    Divides (Cst hh, Add (Mult (Neg jl, iz), id))
chaieb@17378
  1449
  | mirror (Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))) =
chaieb@17378
  1450
    Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))
chaieb@17378
  1451
  | mirror (Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))) =
chaieb@17378
  1452
    Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))
chaieb@17378
  1453
  | mirror (Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))) =
chaieb@17378
  1454
    Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))
chaieb@17378
  1455
  | mirror (Divides (Cst hh, Sub (ie, if'))) = Divides (Cst hh, Sub (ie, if'))
chaieb@17378
  1456
  | mirror (Divides (Cst hh, Mult (ig, ih))) = Divides (Cst hh, Mult (ig, ih))
chaieb@17378
  1457
  | mirror (Divides (Var hi, ag)) = Divides (Var hi, ag)
chaieb@17378
  1458
  | mirror (Divides (Neg hj, ag)) = Divides (Neg hj, ag)
chaieb@17378
  1459
  | mirror (Divides (Add (hk, hl), ag)) = Divides (Add (hk, hl), ag)
chaieb@17378
  1460
  | mirror (Divides (Sub (hm, hn), ag)) = Divides (Sub (hm, hn), ag)
chaieb@17378
  1461
  | mirror (Divides (Mult (ho, hp), ag)) = Divides (Mult (ho, hp), ag)
chaieb@17378
  1462
  | mirror T = T
chaieb@17378
  1463
  | mirror F = F
chaieb@17378
  1464
  | mirror (NOT (Lt (kv, kw))) = NOT (Lt (kv, kw))
chaieb@17378
  1465
  | mirror (NOT (Gt (kx, ky))) = NOT (Gt (kx, ky))
chaieb@17378
  1466
  | mirror (NOT (Le (kz, la))) = NOT (Le (kz, la))
chaieb@17378
  1467
  | mirror (NOT (Ge (lb, lc))) = NOT (Ge (lb, lc))
chaieb@17378
  1468
  | mirror (NOT (Eq (Cst mp, le))) = NOT (Eq (Cst mp, le))
chaieb@17378
  1469
  | mirror (NOT (Eq (Var mq, le))) = NOT (Eq (Var mq, le))
chaieb@17378
  1470
  | mirror (NOT (Eq (Neg mr, le))) = NOT (Eq (Neg mr, le))
chaieb@17378
  1471
  | mirror (NOT (Eq (Add (Cst nh, mt), le))) = NOT (Eq (Add (Cst nh, mt), le))
chaieb@17378
  1472
  | mirror (NOT (Eq (Add (Var ni, mt), le))) = NOT (Eq (Add (Var ni, mt), le))
chaieb@17378
  1473
  | mirror (NOT (Eq (Add (Neg nj, mt), le))) = NOT (Eq (Add (Neg nj, mt), le))
chaieb@17378
  1474
  | mirror (NOT (Eq (Add (Add (nk, nl), mt), le))) =
chaieb@17378
  1475
    NOT (Eq (Add (Add (nk, nl), mt), le))
chaieb@17378
  1476
  | mirror (NOT (Eq (Add (Sub (nm, nn), mt), le))) =
chaieb@17378
  1477
    NOT (Eq (Add (Sub (nm, nn), mt), le))
chaieb@17378
  1478
  | mirror (NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))) =
chaieb@17378
  1479
    NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))
chaieb@17378
  1480
  | mirror (NOT (Eq (Add (Mult (Cst nz, Var pj), mt), le))) =
chaieb@17378
  1481
    (if (pj = 0) then NOT (Eq (Add (Mult (Cst (~ nz), Var 0), mt), le))
chaieb@17378
  1482
      else NOT (Eq (Add (Mult (Cst nz, Var (op_45_def0 pj id_1_def0 + 1)), mt),
chaieb@17378
  1483
                     le)))
chaieb@17378
  1484
  | mirror (NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))) =
chaieb@17378
  1485
    NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))
chaieb@17378
  1486
  | mirror (NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))) =
chaieb@17378
  1487
    NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))
chaieb@17378
  1488
  | mirror (NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))) =
chaieb@17378
  1489
    NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))
chaieb@17378
  1490
  | mirror (NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))) =
chaieb@17378
  1491
    NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))
chaieb@17378
  1492
  | mirror (NOT (Eq (Add (Mult (Var oa, np), mt), le))) =
chaieb@17378
  1493
    NOT (Eq (Add (Mult (Var oa, np), mt), le))
chaieb@17378
  1494
  | mirror (NOT (Eq (Add (Mult (Neg ob, np), mt), le))) =
chaieb@17378
  1495
    NOT (Eq (Add (Mult (Neg ob, np), mt), le))
chaieb@17378
  1496
  | mirror (NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))) =
chaieb@17378
  1497
    NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))
chaieb@17378
  1498
  | mirror (NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))) =
chaieb@17378
  1499
    NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))
chaieb@17378
  1500
  | mirror (NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))) =
chaieb@17378
  1501
    NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))
chaieb@17378
  1502
  | mirror (NOT (Eq (Sub (mu, mv), le))) = NOT (Eq (Sub (mu, mv), le))
chaieb@17378
  1503
  | mirror (NOT (Eq (Mult (mw, mx), le))) = NOT (Eq (Mult (mw, mx), le))
chaieb@17378
  1504
  | mirror (NOT (Divides (Cst pl, Cst qd))) = NOT (Divides (Cst pl, Cst qd))
chaieb@17378
  1505
  | mirror (NOT (Divides (Cst pl, Var qe))) = NOT (Divides (Cst pl, Var qe))
chaieb@17378
  1506
  | mirror (NOT (Divides (Cst pl, Neg qf))) = NOT (Divides (Cst pl, Neg qf))
chaieb@17378
  1507
  | mirror (NOT (Divides (Cst pl, Add (Cst qv, qh)))) =
chaieb@17378
  1508
    NOT (Divides (Cst pl, Add (Cst qv, qh)))
chaieb@17378
  1509
  | mirror (NOT (Divides (Cst pl, Add (Var qw, qh)))) =
chaieb@17378
  1510
    NOT (Divides (Cst pl, Add (Var qw, qh)))
chaieb@17378
  1511
  | mirror (NOT (Divides (Cst pl, Add (Neg qx, qh)))) =
chaieb@17378
  1512
    NOT (Divides (Cst pl, Add (Neg qx, qh)))
chaieb@17378
  1513
  | mirror (NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))) =
chaieb@17378
  1514
    NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))
chaieb@17378
  1515
  | mirror (NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))) =
chaieb@17378
  1516
    NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))
chaieb@17378
  1517
  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))) =
chaieb@17378
  1518
    NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))
chaieb@17378
  1519
  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Var sx), qh)))) =
chaieb@17378
  1520
    (if (sx = 0)
chaieb@17378
  1521
      then NOT (Divides (Cst pl, Add (Mult (Cst (~ rn), Var 0), qh)))
chaieb@17378
  1522
      else NOT (Divides
chaieb@17378
  1523
                  (Cst pl,
chaieb@17378
  1524
                    Add (Mult (Cst rn, Var (op_45_def0 sx id_1_def0 + 1)),
chaieb@17378
  1525
                          qh))))
chaieb@17378
  1526
  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))) =
chaieb@17378
  1527
    NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))
chaieb@17378
  1528
  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))) =
chaieb@17378
  1529
    NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))
chaieb@17378
  1530
  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))) =
chaieb@17378
  1531
    NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))
chaieb@17378
  1532
  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))) =
chaieb@17378
  1533
    NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))
chaieb@17378
  1534
  | mirror (NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))) =
chaieb@17378
  1535
    NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))
chaieb@17378
  1536
  | mirror (NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))) =
chaieb@17378
  1537
    NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))
chaieb@17378
  1538
  | mirror (NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))) =
chaieb@17378
  1539
    NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))
chaieb@17378
  1540
  | mirror (NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))) =
chaieb@17378
  1541
    NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))
chaieb@17378
  1542
  | mirror (NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))) =
chaieb@17378
  1543
    NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))
chaieb@17378
  1544
  | mirror (NOT (Divides (Cst pl, Sub (qi, qj)))) =
chaieb@17378
  1545
    NOT (Divides (Cst pl, Sub (qi, qj)))
chaieb@17378
  1546
  | mirror (NOT (Divides (Cst pl, Mult (qk, ql)))) =
chaieb@17378
  1547
    NOT (Divides (Cst pl, Mult (qk, ql)))
chaieb@17378
  1548
  | mirror (NOT (Divides (Var pm, lg))) = NOT (Divides (Var pm, lg))
chaieb@17378
  1549
  | mirror (NOT (Divides (Neg pn, lg))) = NOT (Divides (Neg pn, lg))
chaieb@17378
  1550
  | mirror (NOT (Divides (Add (po, pp), lg))) = NOT (Divides (Add (po, pp), lg))
chaieb@17378
  1551
  | mirror (NOT (Divides (Sub (pq, pr), lg))) = NOT (Divides (Sub (pq, pr), lg))
chaieb@17378
  1552
  | mirror (NOT (Divides (Mult (ps, pt), lg))) =
chaieb@17378
  1553
    NOT (Divides (Mult (ps, pt), lg))
chaieb@17378
  1554
  | mirror (NOT T) = NOT T
chaieb@17378
  1555
  | mirror (NOT F) = NOT F
chaieb@17378
  1556
  | mirror (NOT (NOT lh)) = NOT (NOT lh)
chaieb@17378
  1557
  | mirror (NOT (And (li, lj))) = NOT (And (li, lj))
chaieb@17378
  1558
  | mirror (NOT (Or (lk, ll))) = NOT (Or (lk, ll))
chaieb@17378
  1559
  | mirror (NOT (Imp (lm, ln))) = NOT (Imp (lm, ln))
chaieb@17378
  1560
  | mirror (NOT (Equ (lo, lp))) = NOT (Equ (lo, lp))
chaieb@17378
  1561
  | mirror (NOT (QAll lq)) = NOT (QAll lq)
chaieb@17378
  1562
  | mirror (NOT (QEx lr)) = NOT (QEx lr)
chaieb@17378
  1563
  | mirror (Imp (am, an)) = Imp (am, an)
chaieb@17378
  1564
  | mirror (Equ (ao, ap)) = Equ (ao, ap)
chaieb@17378
  1565
  | mirror (QAll aq) = QAll aq
chaieb@17378
  1566
  | mirror (QEx ar) = QEx ar;
chaieb@17378
  1567
chaieb@17378
  1568
fun op_43_def0 m n = nat ((m) + (n));
chaieb@17378
  1569
chaieb@17390
  1570
fun size_def1 [] = (0:IntInf.int)
chaieb@17378
  1571
  | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
chaieb@17378
  1572
chaieb@17378
  1573
fun aset (And (p, q)) = op_64 (aset p) (aset q)
chaieb@17378
  1574
  | aset (Or (p, q)) = op_64 (aset p) (aset q)
chaieb@17378
  1575
  | aset (Lt (u, v)) = []
chaieb@17378
  1576
  | aset (Gt (w, x)) = []
chaieb@17378
  1577
  | aset (Le (Cst bo, z)) = []
chaieb@17378
  1578
  | aset (Le (Var bp, z)) = []
chaieb@17378
  1579
  | aset (Le (Neg bq, z)) = []
chaieb@17378
  1580
  | aset (Le (Add (Cst cg, bs), z)) = []
chaieb@17378
  1581
  | aset (Le (Add (Var ch, bs), z)) = []
chaieb@17378
  1582
  | aset (Le (Add (Neg ci, bs), z)) = []
chaieb@17378
  1583
  | aset (Le (Add (Add (cj, ck), bs), z)) = []
chaieb@17378
  1584
  | aset (Le (Add (Sub (cl, cm), bs), z)) = []
chaieb@17378
  1585
  | aset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
chaieb@17378
  1586
  | aset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
chaieb@17378
  1587
    (if (ei = 0)
chaieb@17378
  1588
      then (if (cy < 0) then [lin_add (bs, Cst 1)]
chaieb@17378
  1589
             else [lin_neg bs, lin_add (lin_neg bs, Cst 1)])
chaieb@17378
  1590
      else [])
chaieb@17378
  1591
  | aset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = []
chaieb@17378
  1592
  | aset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = []
chaieb@17378
  1593
  | aset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = []
chaieb@17378
  1594
  | aset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = []
chaieb@17378
  1595
  | aset (Le (Add (Mult (Var cz, co), bs), z)) = []
chaieb@17378
  1596
  | aset (Le (Add (Mult (Neg da, co), bs), z)) = []
chaieb@17378
  1597
  | aset (Le (Add (Mult (Add (db, dc), co), bs), z)) = []
chaieb@17378
  1598
  | aset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = []
chaieb@17378
  1599
  | aset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = []
chaieb@17378
  1600
  | aset (Le (Sub (bt, bu), z)) = []
chaieb@17378
  1601
  | aset (Le (Mult (bv, bw), z)) = []
chaieb@17378
  1602
  | aset (Ge (aa, ab)) = []
chaieb@17378
  1603
  | aset (Eq (Cst ek, ad)) = []
chaieb@17378
  1604
  | aset (Eq (Var el, ad)) = []
chaieb@17378
  1605
  | aset (Eq (Neg em, ad)) = []
chaieb@17378
  1606
  | aset (Eq (Add (Cst fc, eo), ad)) = []
chaieb@17378
  1607
  | aset (Eq (Add (Var fd, eo), ad)) = []
chaieb@17378
  1608
  | aset (Eq (Add (Neg fe, eo), ad)) = []
chaieb@17378
  1609
  | aset (Eq (Add (Add (ff, fg), eo), ad)) = []
chaieb@17378
  1610
  | aset (Eq (Add (Sub (fh, fi), eo), ad)) = []
chaieb@17378
  1611
  | aset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = []
chaieb@17378
  1612
  | aset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
chaieb@17378
  1613
    (if (he = 0)
chaieb@17378
  1614
      then (if (fu < 0) then [lin_add (eo, Cst 1)]
chaieb@17378
  1615
             else [lin_add (lin_neg eo, Cst 1)])
chaieb@17378
  1616
      else [])
chaieb@17378
  1617
  | aset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = []
chaieb@17378
  1618
  | aset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = []
chaieb@17378
  1619
  | aset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = []
chaieb@17378
  1620
  | aset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = []
chaieb@17378
  1621
  | aset (Eq (Add (Mult (Var fv, fk), eo), ad)) = []
chaieb@17378
  1622
  | aset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = []
chaieb@17378
  1623
  | aset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = []
chaieb@17378
  1624
  | aset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = []
chaieb@17378
  1625
  | aset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = []
chaieb@17378
  1626
  | aset (Eq (Sub (ep, eq), ad)) = []
chaieb@17378
  1627
  | aset (Eq (Mult (er, es), ad)) = []
chaieb@17378
  1628
  | aset (Divides (ae, af)) = []
chaieb@17378
  1629
  | aset T = []
chaieb@17378
  1630
  | aset F = []
chaieb@17378
  1631
  | aset (NOT (Lt (hg, hh))) = []
chaieb@17378
  1632
  | aset (NOT (Gt (hi, hj))) = []
chaieb@17378
  1633
  | aset (NOT (Le (hk, hl))) = []
chaieb@17378
  1634
  | aset (NOT (Ge (hm, hn))) = []
chaieb@17378
  1635
  | aset (NOT (Eq (Cst ja, hp))) = []
chaieb@17378
  1636
  | aset (NOT (Eq (Var jb, hp))) = []
chaieb@17378
  1637
  | aset (NOT (Eq (Neg jc, hp))) = []
chaieb@17378
  1638
  | aset (NOT (Eq (Add (Cst js, je), hp))) = []
chaieb@17378
  1639
  | aset (NOT (Eq (Add (Var jt, je), hp))) = []
chaieb@17378
  1640
  | aset (NOT (Eq (Add (Neg ju, je), hp))) = []
chaieb@17378
  1641
  | aset (NOT (Eq (Add (Add (jv, jw), je), hp))) = []
chaieb@17378
  1642
  | aset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = []
chaieb@17378
  1643
  | aset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = []
chaieb@17378
  1644
  | aset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
chaieb@17378
  1645
    (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else [])
chaieb@17378
  1646
  | aset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = []
chaieb@17378
  1647
  | aset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = []
chaieb@17378
  1648
  | aset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = []
chaieb@17378
  1649
  | aset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = []
chaieb@17378
  1650
  | aset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = []
chaieb@17378
  1651
  | aset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = []
chaieb@17378
  1652
  | aset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = []
chaieb@17378
  1653
  | aset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = []
chaieb@17378
  1654
  | aset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = []
chaieb@17378
  1655
  | aset (NOT (Eq (Sub (jf, jg), hp))) = []
chaieb@17378
  1656
  | aset (NOT (Eq (Mult (jh, ji), hp))) = []
chaieb@17378
  1657
  | aset (NOT (Divides (hq, hr))) = []
chaieb@17378
  1658
  | aset (NOT T) = []
chaieb@17378
  1659
  | aset (NOT F) = []
chaieb@17378
  1660
  | aset (NOT (NOT hs)) = []
chaieb@17378
  1661
  | aset (NOT (And (ht, hu))) = []
chaieb@17378
  1662
  | aset (NOT (Or (hv, hw))) = []
chaieb@17378
  1663
  | aset (NOT (Imp (hx, hy))) = []
chaieb@17378
  1664
  | aset (NOT (Equ (hz, ia))) = []
chaieb@17378
  1665
  | aset (NOT (QAll ib)) = []
chaieb@17378
  1666
  | aset (NOT (QEx ic)) = []
chaieb@17378
  1667
  | aset (Imp (al, am)) = []
chaieb@17378
  1668
  | aset (Equ (an, ao)) = []
chaieb@17378
  1669
  | aset (QAll ap) = []
chaieb@17378
  1670
  | aset (QEx aq) = [];
chaieb@17378
  1671
chaieb@17378
  1672
fun op_mem x [] = false
chaieb@17378
  1673
  | op_mem x (y :: ys) = (if (y = x) then true else op_mem x ys);
chaieb@17378
  1674
chaieb@17378
  1675
fun list_insert x xs = (if op_mem x xs then xs else (x :: xs));
chaieb@17378
  1676
chaieb@17378
  1677
fun list_set [] = []
chaieb@17378
  1678
  | list_set (x :: xs) = list_insert x (list_set xs);
chaieb@17378
  1679
chaieb@17378
  1680
fun bset (And (p, q)) = op_64 (bset p) (bset q)
chaieb@17378
  1681
  | bset (Or (p, q)) = op_64 (bset p) (bset q)
chaieb@17378
  1682
  | bset (Lt (u, v)) = []
chaieb@17378
  1683
  | bset (Gt (w, x)) = []
chaieb@17378
  1684
  | bset (Le (Cst bo, z)) = []
chaieb@17378
  1685
  | bset (Le (Var bp, z)) = []
chaieb@17378
  1686
  | bset (Le (Neg bq, z)) = []
chaieb@17378
  1687
  | bset (Le (Add (Cst cg, bs), z)) = []
chaieb@17378
  1688
  | bset (Le (Add (Var ch, bs), z)) = []
chaieb@17378
  1689
  | bset (Le (Add (Neg ci, bs), z)) = []
chaieb@17378
  1690
  | bset (Le (Add (Add (cj, ck), bs), z)) = []
chaieb@17378
  1691
  | bset (Le (Add (Sub (cl, cm), bs), z)) = []
chaieb@17378
  1692
  | bset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
chaieb@17378
  1693
  | bset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
chaieb@17378
  1694
    (if (ei = 0)
chaieb@17378
  1695
      then (if (cy < 0) then [lin_add (bs, Cst ~1), bs]
chaieb@17378
  1696
             else [lin_add (lin_neg bs, Cst ~1)])