Removed from CVS, since obselete in the new Presburger Method;

--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Jun 11 11:07:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,917 +0,0 @@
-(*  Title:      HOL/Tools/Presburger/cooper_dec.ML
-    ID:         $Id$
-    Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
-
-The Cooper Algorithm decision procedure (intensively inspired by
-J. Harrison). *)
-
-signature COOPER_DEC = 
-sig
-  exception COOPER
-  val mk_number : IntInf.int -> term
-  val zero : term
-  val one : term
-  val dest_number : term -> IntInf.int
-  val is_number : term -> bool
-  val is_arith_rel : term -> bool
-  val linear_cmul : IntInf.int -> term -> term
-  val linear_add : string list -> term -> term -> term 
-  val linear_sub : string list -> term -> term -> term 
-  val linear_neg : term -> term
-  val lint : string list -> term -> term
-  val linform : string list -> term -> term
-  val formlcm : term -> term -> IntInf.int
-  val adjustcoeff : term -> IntInf.int -> term -> term
-  val unitycoeff : term -> term -> term
-  val divlcm : term -> term -> IntInf.int
-  val bset : term -> term -> term list
-  val aset : term -> term -> term list
-  val linrep : string list -> term -> term -> term -> term
-  val list_disj : term list -> term
-  val list_conj : term list -> term
-  val simpl : term -> term
-  val fv : term -> string list
-  val negate : term -> term
-  val operations : (string * (IntInf.int * IntInf.int -> bool)) list
-  val conjuncts : term -> term list
-  val disjuncts : term -> term list
-  val has_bound : term -> bool
-  val minusinf : term -> term -> term
-  val plusinf : term -> term -> term
-  val onatoms : (term -> term) -> term -> term
-  val evalc : term -> term
-  val cooper_w : string list -> term -> (term option * term)
-  val integer_qelim : Term.term -> Term.term
-end;
-
-structure CooperDec : COOPER_DEC =
-struct
-
-(* ========================================================================= *) 
-(* Cooper's algorithm for Presburger arithmetic.                             *) 
-(* ========================================================================= *) 
-exception COOPER;
-
-
-(* ------------------------------------------------------------------------- *) 
-(* Lift operations up to numerals.                                           *) 
-(* ------------------------------------------------------------------------- *) 
- 
-(*Assumption : The construction of atomar formulas in linearl arithmetic is based on 
-relation operations of Type : [IntInf.int,IntInf.int]---> bool *) 
- 
-(* ------------------------------------------------------------------------- *) 
- 
-(*Function is_arith_rel returns true if and only if the term is an atomar presburger 
-formula *) 
-fun is_arith_rel tm = case tm
- of Const(p, Type ("fun", [Type ("IntDef.int", []), Type ("fun", [Type ("IntDef.int", []),
-      Type ("bool", [])])])) $ _ $_ => true
-  | _ => false;
- 
-(*Function is_arith_rel returns true if and only if the term is an operation of the 
-form [int,int]---> int*) 
- 
-val mk_number = HOLogic.mk_number HOLogic.intT;
-val zero = mk_number 0; 
-val one = mk_number 1; 
-fun dest_number t = let
-    val (T, n) = HOLogic.dest_number t
-  in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end;
-val is_number = can dest_number; 
-
-(*maps a unary natural function on a term containing an natural number*) 
-fun numeral1 f n = mk_number (f (dest_number n)); 
- 
-(*maps a binary natural function on 2 term containing  natural numbers*) 
-fun numeral2 f m n = mk_number (f (dest_number m) (dest_number n));
- 
-(* ------------------------------------------------------------------------- *) 
-(* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k          *) 
-(*                                                                           *) 
-(* Note that we're quite strict: the ci must be present even if 1            *) 
-(* (but if 0 we expect the monomial to be omitted) and k must be there       *) 
-(* even if it's zero. Thus, it's a constant iff not an addition term.        *) 
-(* ------------------------------------------------------------------------- *)  
- 
- 
-fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
-  ( case tm of  
-     (Const(@{const_name HOL.plus},T)  $  (Const (@{const_name HOL.times},T1 ) $c1 $  x1) $ rest) => 
-       Const(@{const_name HOL.plus},T) $ ((Const(@{const_name HOL.times},T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) 
-    |_ =>  numeral1 (times n) tm) 
-    end ; 
- 
- 
- 
- 
-(* Whether the first of two items comes earlier in the list  *) 
-fun earlier [] x y = false 
-	|earlier (h::t) x y =if h = y then false 
-              else if h = x then true 
-              	else earlier t x y ; 
- 
-fun earlierv vars (Bound i) (Bound j) = i < j 
-   |earlierv vars (Bound _) _ = true 
-   |earlierv vars _ (Bound _)  = false 
-   |earlierv vars (Free (x,_)) (Free (y,_)) = earlier vars x y; 
- 
- 
-fun linear_add vars tm1 tm2 = 
-  let fun addwith x y = x + y in
- (case (tm1,tm2) of 
-	((Const (@{const_name HOL.plus},T1) $ ( Const(@{const_name HOL.times},T2) $ c1 $  x1) $ rest1),(Const 
-	(@{const_name HOL.plus},T3)$( Const(@{const_name HOL.times},T4) $ c2 $  x2) $ rest2)) => 
-         if x1 = x2 then 
-              let val c = (numeral2 (addwith) c1 c2) 
-	      in 
-              if c = zero then (linear_add vars rest1  rest2)  
-	      else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c $ x1) $ (linear_add vars  rest1 rest2)) 
-              end 
-	   else 
-		if earlierv vars x1 x2 then (Const(@{const_name HOL.plus},T1) $  
-		(Const(@{const_name HOL.times},T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) 
-    	       else (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) 
-   	|((Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ rest1) ,_) => 
-    	  (Const(@{const_name HOL.plus},T1)$ (Const(@{const_name HOL.times},T2) $ c1 $ x1) $ (linear_add vars 
-	  rest1 tm2)) 
-   	|(_, (Const(@{const_name HOL.plus},T1) $(Const(@{const_name HOL.times},T2) $ c2 $ x2) $ rest2)) => 
-      	  (Const(@{const_name HOL.plus},T1) $ (Const(@{const_name HOL.times},T2) $ c2 $ x2) $ (linear_add vars tm1 
-	  rest2)) 
-   	| (_,_) => numeral2 (addwith) tm1 tm2) 
-	 
-	end; 
- 
-(*To obtain the unary - applyed on a formula*) 
- 
-fun linear_neg tm = linear_cmul (0 - 1) tm; 
- 
-(*Substraction of two terms *) 
- 
-fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); 
- 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Linearize a term.                                                         *) 
-(* ------------------------------------------------------------------------- *) 
- 
-(* linearises a term from the point of view of Variable Free (x,T). 
-After this fuction the all expressions containig ths variable will have the form  
- c*Free(x,T) + t where c is a constant ant t is a Term which is not containing 
- Free(x,T)*) 
-  
-fun lint vars tm = if is_number tm then tm else case tm of 
-   (Free (x,T)) =>  (HOLogic.mk_binop @{const_name HOL.plus} ((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1),Free (x,T))), zero)) 
-  |(Bound i) =>  (Const(@{const_name HOL.plus},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ 
-  (Const(@{const_name HOL.times},HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) 
-  |(Const(@{const_name HOL.uminus},_) $ t ) => (linear_neg (lint vars t)) 
-  |(Const(@{const_name HOL.plus},_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) 
-  |(Const(@{const_name HOL.minus},_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) 
-  |(Const (@{const_name HOL.times},_) $ s $ t) => 
-        let val s' = lint vars s  
-            val t' = lint vars t  
-        in 
-        if is_number s' then (linear_cmul (dest_number s') t') 
-        else if is_number t' then (linear_cmul (dest_number t') s') 
- 
-         else raise COOPER
-         end 
-  |_ =>  raise COOPER;
-   
- 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Linearize the atoms in a formula, and eliminate non-strict inequalities.  *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
- 
-fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
-    if is_number c then   
-      let val c' = (mk_number(abs(dest_number c)))  
-      in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) 
-      end 
-    else (warning "Nonlinear term --- Non numeral leftside at dvd"
-      ;raise COOPER)
-  |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
-  |linform vars  (Const(@{const_name Orderings.less},_)$ s $t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
-  |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 
-  |linform vars  (Const(@{const_name Orderings.less_eq},_)$ s $ t ) = 
-        (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) 
-  |linform vars  (Const("op >=",_)$ s $ t ) = 
-        (mkatom vars @{const_name Orderings.less} (Const (@{const_name HOL.minus},HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $ (Const(@{const_name HOL.plus},HOLogic.intT --> HOLogic.intT --> 
-	HOLogic.intT) $s $(mk_number 1)) $ t)) 
- 
-   |linform vars  fm =  fm; 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Post-NNF transformation eliminating negated inequalities.                 *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun posineq fm = case fm of  
- (Const ("Not",_)$(Const(@{const_name Orderings.less},_)$ c $ t)) =>
-   (HOLogic.mk_binrel @{const_name Orderings.less}  (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) 
-  | ( Const ("op &",_) $ p $ q)  => HOLogic.mk_conj (posineq p,posineq q)
-  | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
-  | _ => fm; 
-  
-
-(* ------------------------------------------------------------------------- *) 
-(* Find the LCM of the coefficients of x.                                    *) 
-(* ------------------------------------------------------------------------- *) 
-(*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) 
- 
-fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; 
-fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
- 
-fun formlcm x fm = case fm of 
-    (Const (p,_)$ _ $(Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_)$ c $ y ) $z ) ) =>  if 
-    (is_arith_rel fm) andalso (x = y) then  (abs(dest_number c)) else 1 
-  | ( Const ("Not", _) $p) => formlcm x p 
-  | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
-  | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
-  |  _ => 1; 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Adjust all coefficients of x in formula; fold in reduction to +/- 1.      *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun adjustcoeff x l fm = 
-     case fm of  
-      (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
-      c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
-        let val m = l div (dest_number c) 
-            val n = (if p = @{const_name Orderings.less} then abs(m) else m) 
-            val xtm = HOLogic.mk_binop @{const_name HOL.times} ((mk_number (m div n)), x) 
-	in
-        (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
-	end 
-	else fm 
-  |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) 
-  |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeff x l p) $(adjustcoeff x l q) 
-  |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeff x l p)$ (adjustcoeff x l q) 
-  |_ => fm; 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Hence make coefficient of x one in existential formula.                   *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun unitycoeff x fm = 
-  let val l = formlcm x fm
-      val fm' = adjustcoeff x l fm in
-      if l = 1 then fm' 
-	 else 
-     let val xp = (HOLogic.mk_binop @{const_name HOL.plus}  
-     		((HOLogic.mk_binop @{const_name HOL.times} ((mk_number 1), x )), zero))
-	in 
-      HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm) 
-      end 
-  end; 
- 
-(* adjustcoeffeq l fm adjusts the coeffitients c_i of x  overall in fm to l*)
-(* Here l must be a multiple of all c_i otherwise the obtained formula is not equivalent*)
-(*
-fun adjustcoeffeq x l fm = 
-    case fm of  
-      (Const(p,_) $d $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
-      c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
-        let val m = l div (dest_number c) 
-            val n = (if p = @{const_name Orderings.less} then abs(m) else m)  
-            val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x))
-            in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
-	    end 
-	else fm 
-  |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) 
-  |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeffeq x l p) $(adjustcoeffeq x l q) 
-  |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeffeq x l p)$ (adjustcoeffeq x l q) 
-  |_ => fm;
- 
-
-*)
-
-(* ------------------------------------------------------------------------- *) 
-(* The "minus infinity" version.                                             *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun minusinf x fm = case fm of  
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) => 
-  	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const  
-	 				 else fm 
- 
-  |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z 
-  )) => if (x = y) 
-	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
-	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
-	          else error "minusinf : term not in normal form!!!"
-	else fm
-	 
-  |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) 
-  |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) 
-  |(Const ("op |",_) $ p $ q) => HOLogic.disj $ (minusinf x p) $ (minusinf x q) 
-  |_ => fm; 
-
-(* ------------------------------------------------------------------------- *)
-(* The "Plus infinity" version.                                             *)
-(* ------------------------------------------------------------------------- *)
-
-fun plusinf x fm = case fm of
-    (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
-  	 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
-	 				 else fm
-
-  |(Const(@{const_name Orderings.less},_) $ c $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z
-  )) => if (x = y) 
-	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
-	     else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const
-	     else error "plusinf : term not in normal form!!!"
-	else fm 
-
-  |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p)
-  |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q)
-  |(Const ("op |",_) $ p $ q) => HOLogic.disj $ (plusinf x p) $ (plusinf x q)
-  |_ => fm;
- 
-(* ------------------------------------------------------------------------- *) 
-(* The LCM of all the divisors that involve x.                               *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun divlcm x (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z ) ) =  
-        if x = y then abs(dest_number d) else 1 
-  |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
-  |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
-  |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) 
-  |divlcm x  _ = 1; 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Construct the B-set.                                                      *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun bset x fm = case fm of 
-   (Const ("Not", _) $ p) => if (is_arith_rel p) then  
-          (case p of  
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )  
-	             => if (is_arith_rel p) andalso (x=	y) andalso (c2 = one) andalso (c1 = zero)  
-	                then [linear_neg a] 
-			else  bset x p 
-   	  |_ =>[]) 
-			 
-			else bset x p 
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))]  else [] 
-  |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] 
-  |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) 
-  |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) 
-  |_ => []; 
- 
-(* ------------------------------------------------------------------------- *)
-(* Construct the A-set.                                                      *)
-(* ------------------------------------------------------------------------- *)
-
-fun aset x fm = case fm of
-   (Const ("Not", _) $ p) => if (is_arith_rel p) then
-          (case p of
-	      (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $c2 $y) $a ) )
-	             => if (x=	y) andalso (c2 = one) andalso (c1 = zero)
-	                then [linear_neg a]
-			else  []
-   	  |_ =>[])
-
-			else aset x p
-  |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $c2 $ x) $ a)) =>  if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a]  else []
-  |(Const (@{const_name Orderings.less},_) $ c1$ (Const (@{const_name HOL.plus},_) $(Const (@{const_name HOL.times},_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else []
-  |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
-  |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
-  |_ => [];
-
-
-(* ------------------------------------------------------------------------- *) 
-(* Replace top variable with another linear form, retaining canonicality.    *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun linrep vars x t fm = case fm of  
-   ((Const(p,_)$ d $ (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$ c $ y) $ z))) => 
-      if (x = y) andalso (is_arith_rel fm)  
-      then  
-        let val ct = linear_cmul (dest_number c) t  
-	in (HOLogic.mk_binrel p (d, linear_add vars ct z)) 
-	end 
-	else fm 
-  |(Const ("Not", _) $ p) => HOLogic.Not $ (linrep vars x t p) 
-  |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (linrep vars x t p) $ (linrep vars x t q) 
-  |(Const ("op |",_) $ p $ q) => HOLogic.disj $ (linrep vars x t p) $ (linrep vars x t q) 
-  |_ => fm;
- 
-(* ------------------------------------------------------------------------- *) 
-(* Evaluation of constant expressions.                                       *) 
-(* ------------------------------------------------------------------------- *) 
-
-(* An other implementation of divides, that covers more cases*) 
-
-exception DVD_UNKNOWN
-
-fun dvd_op (d, t) = 
- if not(is_number d) then raise DVD_UNKNOWN
- else let 
-   val dn = dest_number d
-   fun coeffs_of x = case x of 
-     Const(p,_) $ tl $ tr => 
-       if p = @{const_name HOL.plus} then (coeffs_of tl) union (coeffs_of tr)
-          else if p = @{const_name HOL.times} 
-	        then if (is_number tr) 
-		 then [(dest_number tr) * (dest_number tl)] 
-		 else [dest_number tl]
-	        else []
-    |_ => if (is_number t) then [dest_number t]  else []
-   val ts = coeffs_of t
-   in case ts of
-     [] => raise DVD_UNKNOWN
-    |_  => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true
-   end;
-
-
-val operations = 
-  [("op =",op=), (@{const_name Orderings.less},IntInf.<), ("op >",IntInf.>), (@{const_name Orderings.less_eq},IntInf.<=) , 
-   ("op >=",IntInf.>=), 
-   ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
- 
-fun applyoperation (SOME f) (a,b) = f (a, b) 
-    |applyoperation _ (_, _) = false; 
- 
-(*Evaluation of constant atomic formulas*) 
- (*FIXME : This is an optimation but still incorrect !! *)
-(*
-fun evalc_atom at = case at of  
-  (Const (p,_) $ s $ t) =>
-   (if p="Divides.dvd" then 
-     ((if dvd_op(s,t) then HOLogic.true_const
-     else HOLogic.false_const)
-      handle _ => at)
-    else
-  case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const else HOLogic.false_const)  
-    handle _ => at) 
-      | _ =>  at) 
-      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-  case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_number s),(dest_number t))) then 
-    HOLogic.false_const else HOLogic.true_const)  
-    handle _ => at) 
-      | _ =>  at) 
-      | _ =>  at; 
-
-*)
-
-fun evalc_atom at = case at of  
-  (Const (p,_) $ s $ t) =>
-   ( case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const 
-                else HOLogic.false_const)  
-    handle _ => at) 
-      | _ =>  at) 
-      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-  case AList.lookup (op =) operations p of 
-    SOME f => ((if (f ((dest_number s),(dest_number t))) 
-               then HOLogic.false_const else HOLogic.true_const)  
-    handle _ => at) 
-      | _ =>  at) 
-      | _ =>  at; 
-
- (*Function onatoms apllys function f on the atomic formulas involved in a.*) 
- 
-fun onatoms f a = if (is_arith_rel a) then f a else case a of 
- 
-  	(Const ("Not",_) $ p) => if is_arith_rel p then HOLogic.Not $ (f p) 
-				 
-				else HOLogic.Not $ (onatoms f p) 
-  	|(Const ("op &",_) $ p $ q) => HOLogic.conj $ (onatoms f p) $ (onatoms f q) 
-  	|(Const ("op |",_) $ p $ q) => HOLogic.disj $ (onatoms f p) $ (onatoms f q) 
-  	|(Const ("op -->",_) $ p $ q) => HOLogic.imp $ (onatoms f p) $ (onatoms f q) 
-  	|((Const ("op =", Type ("fun",[Type ("bool", []),_]))) $ p $ q) => (Const ("op =", [HOLogic.boolT, HOLogic.boolT] ---> HOLogic.boolT)) $ (onatoms f p) $ (onatoms f q) 
-  	|(Const("All",_) $ Abs(x,T,p)) => Const("All", [HOLogic.intT --> 
-	HOLogic.boolT] ---> HOLogic.boolT)$ Abs (x ,T, (onatoms f p)) 
-  	|(Const("Ex",_) $ Abs(x,T,p)) => Const("Ex", [HOLogic.intT --> HOLogic.boolT]---> HOLogic.boolT) $ Abs( x ,T, (onatoms f p)) 
-  	|_ => a; 
- 
-val evalc = onatoms evalc_atom; 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Hence overall quantifier elimination.                                     *) 
-(* ------------------------------------------------------------------------- *) 
- 
- 
-(*list_disj[conj] makes a disj[conj] of a given list. used with conjucts or disjuncts 
-it liearises iterated conj[disj]unctions. *) 
- 
-fun list_disj [] = HOLogic.false_const
-  | list_disj ps = foldr1 (fn (p, q) => HOLogic.disj $ p $ q) ps;
-
-fun list_conj [] = HOLogic.true_const
-  | list_conj ps = foldr1 (fn (p, q) => HOLogic.conj $ p $ q) ps;
-
-
-(*Simplification of Formulas *) 
- 
-(*Function q_bnd_chk checks if a quantified Formula makes sens : Means if in 
-the body of the existential quantifier there are bound variables to the 
-existential quantifier.*) 
- 
-fun has_bound fm =let fun has_boundh fm i = case fm of 
-		 Bound n => (i = n) 
-		 |Abs (_,_,p) => has_boundh p (i+1) 
-		 |t1 $ t2 => (has_boundh t1 i) orelse (has_boundh t2 i) 
-		 |_ =>false
-
-in  case fm of 
-	Bound _ => true 
-       |Abs (_,_,p) => has_boundh p 0 
-       |t1 $ t2 => (has_bound t1 ) orelse (has_bound t2 ) 
-       |_ =>false
-end;
- 
-(*has_sub_abs checks if in a given Formula there are subformulas which are quantifed 
-too. Is no used no more.*) 
- 
-fun has_sub_abs fm = case fm of  
-		 Abs (_,_,_) => true 
-		 |t1 $ t2 => (has_bound t1 ) orelse (has_bound t2 ) 
-		 |_ =>false ; 
-		  
-(*update_bounds called with i=0 udates the numeration of bounded variables because the 
-formula will not be quantified any more.*) 
- 
-fun update_bounds fm i = case fm of 
-		 Bound n => if n >= i then Bound (n-1) else fm 
-		 |Abs (x,T,p) => Abs(x,T,(update_bounds p (i+1))) 
-		 |t1 $ t2 => (update_bounds t1 i) $ (update_bounds t2 i) 
-		 |_ => fm ; 
- 
-(*psimpl : Simplification of propositions (general purpose)*) 
-fun psimpl1 fm = case fm of 
-    Const("Not",_) $ Const ("False",_) => HOLogic.true_const 
-  | Const("Not",_) $ Const ("True",_) => HOLogic.false_const 
-  | Const("op &",_) $ Const ("False",_) $ q => HOLogic.false_const 
-  | Const("op &",_) $ p $ Const ("False",_)  => HOLogic.false_const 
-  | Const("op &",_) $ Const ("True",_) $ q => q 
-  | Const("op &",_) $ p $ Const ("True",_) => p 
-  | Const("op |",_) $ Const ("False",_) $ q => q 
-  | Const("op |",_) $ p $ Const ("False",_)  => p 
-  | Const("op |",_) $ Const ("True",_) $ q => HOLogic.true_const 
-  | Const("op |",_) $ p $ Const ("True",_)  => HOLogic.true_const 
-  | Const("op -->",_) $ Const ("False",_) $ q => HOLogic.true_const 
-  | Const("op -->",_) $ Const ("True",_) $  q => q 
-  | Const("op -->",_) $ p $ Const ("True",_)  => HOLogic.true_const 
-  | Const("op -->",_) $ p $ Const ("False",_)  => HOLogic.Not $  p 
-  | Const("op =", Type ("fun",[Type ("bool", []),_])) $ Const ("True",_) $ q => q 
-  | Const("op =", Type ("fun",[Type ("bool", []),_])) $ p $ Const ("True",_) => p 
-  | Const("op =", Type ("fun",[Type ("bool", []),_])) $ Const ("False",_) $ q => HOLogic.Not $  q 
-  | Const("op =", Type ("fun",[Type ("bool", []),_])) $ p $ Const ("False",_)  => HOLogic.Not $  p 
-  | _ => fm; 
- 
-fun psimpl fm = case fm of 
-   Const ("Not",_) $ p => psimpl1 (HOLogic.Not $ (psimpl p)) 
-  | Const("op &",_) $ p $ q => psimpl1 (HOLogic.mk_conj (psimpl p,psimpl q)) 
-  | Const("op |",_) $ p $ q => psimpl1 (HOLogic.mk_disj (psimpl p,psimpl q)) 
-  | Const("op -->",_) $ p $ q => psimpl1 (HOLogic.mk_imp(psimpl p,psimpl q)) 
-  | Const("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q => psimpl1 (HOLogic.mk_eq(psimpl p,psimpl q))
-  | _ => fm; 
- 
- 
-(*simpl : Simplification of Terms involving quantifiers too. 
- This function is able to drop out some quantified expressions where there are no 
- bound varaibles.*) 
-  
-fun simpl1 fm  = 
-  case fm of 
-    Const("All",_) $Abs(x,_,p) => if (has_bound fm ) then fm  
-    				else (update_bounds p 0) 
-  | Const("Ex",_) $ Abs (x,_,p) => if has_bound fm then fm  
-    				else (update_bounds p 0) 
-  | _ => psimpl fm; 
- 
-fun simpl fm = case fm of 
-    Const ("Not",_) $ p => simpl1 (HOLogic.Not $(simpl p))  
-  | Const ("op &",_) $ p $ q => simpl1 (HOLogic.mk_conj (simpl p ,simpl q))  
-  | Const ("op |",_) $ p $ q => simpl1 (HOLogic.mk_disj (simpl p ,simpl q ))  
-  | Const ("op -->",_) $ p $ q => simpl1 (HOLogic.mk_imp(simpl p ,simpl q ))  
-  | Const("op =", Type ("fun",[Type ("bool", []),_]))$ p $ q => simpl1 
-  (HOLogic.mk_eq(simpl p ,simpl q ))  
-(*  | Const ("All",Ta) $ Abs(Vn,VT,p) => simpl1(Const("All",Ta) $ 
-  Abs(Vn,VT,simpl p ))  
-  | Const ("Ex",Ta)  $ Abs(Vn,VT,p) => simpl1(Const("Ex",Ta)  $ 
-  Abs(Vn,VT,simpl p ))  
-*)
-  | _ => fm; 
- 
-(* ------------------------------------------------------------------------- *) 
- 
-(* Puts fm into NNF*) 
- 
-fun  nnf fm = if (is_arith_rel fm) then fm  
-else (case fm of 
-  ( Const ("op &",_) $ p $ q)  => HOLogic.conj $ (nnf p) $(nnf q) 
-  | (Const("op |",_) $ p $q) => HOLogic.disj $ (nnf p)$(nnf q) 
-  | (Const ("op -->",_)  $ p $ q) => HOLogic.disj $ (nnf (HOLogic.Not $ p)) $ (nnf q) 
-  | ((Const ("op =", Type ("fun",[Type ("bool", []),_]))) $ p $ q) =>(HOLogic.disj $ (HOLogic.conj $ (nnf p) $ (nnf q)) $ (HOLogic.conj $ (nnf (HOLogic.Not $ p) ) $ (nnf(HOLogic.Not $ q)))) 
-  | (Const ("Not",_)) $ ((Const ("Not",_)) $ p) => (nnf p) 
-  | (Const ("Not",_)) $ (( Const ("op &",_)) $ p $ q) =>HOLogic.disj $ (nnf(HOLogic.Not $ p)) $ (nnf(HOLogic.Not $q)) 
-  | (Const ("Not",_)) $ (( Const ("op |",_)) $ p $ q) =>HOLogic.conj $ (nnf(HOLogic.Not $ p)) $ (nnf(HOLogic.Not $ q)) 
-  | (Const ("Not",_)) $ (( Const ("op -->",_)) $ p $ q ) =>HOLogic.conj $ (nnf p) $(nnf(HOLogic.Not $ q)) 
-  | (Const ("Not",_)) $ ((Const ("op =", Type ("fun",[Type ("bool", []),_]))) $ p $ q ) =>(HOLogic.disj $ (HOLogic.conj $(nnf p) $ (nnf(HOLogic.Not $ q))) $ (HOLogic.conj $(nnf(HOLogic.Not $ p)) $ (nnf q))) 
-  | _ => fm); 
- 
- 
-(* Function remred to remove redundancy in a list while keeping the order of appearance of the 
-elements. but VERY INEFFICIENT!! *) 
- 
-fun remred1 el [] = [] 
-    |remred1 el (h::t) = if el=h then (remred1 el t) else h::(remred1 el t); 
-     
-fun remred [] = [] 
-    |remred (x::l) =  x::(remred1 x (remred l)); 
- 
-(*Makes sure that all free Variables are of the type integer but this function is only 
-used temporarily, this job must be done by the parser later on.*) 
- 
-fun mk_uni_vars T  (node $ rest) = (case node of 
-    Free (name,_) => Free (name,T) $ (mk_uni_vars T rest) 
-    |_=> (mk_uni_vars T node) $ (mk_uni_vars T rest )  ) 
-    |mk_uni_vars T (Free (v,_)) = Free (v,T) 
-    |mk_uni_vars T tm = tm; 
- 
-fun mk_uni_int T (Const (@{const_name HOL.zero},T2)) = if T = T2 then (mk_number 0) else (Const (@{const_name HOL.zero},T2)) 
-    |mk_uni_int T (Const (@{const_name HOL.one},T2)) = if T = T2 then (mk_number 1) else (Const (@{const_name HOL.one},T2)) 
-    |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
-    |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
-    |mk_uni_int T tm = tm; 
- 
-
-(* Minusinfinity Version*)    
-fun myupto (m:IntInf.int) n = if m > n then [] else m::(myupto (m+1) n)
-
-fun coopermi vars1 fm = 
-  case fm of 
-   Const ("Ex",_) $ Abs(x0,T,p0) => 
-   let 
-    val (xn,p1) = Syntax.variant_abs (x0,T,p0) 
-    val x = Free (xn,T)  
-    val vars = (xn::vars1) 
-    val p = unitycoeff x  (posineq (simpl p1))
-    val p_inf = simpl (minusinf x p) 
-    val bset = bset x p 
-    val js = myupto 1 (divlcm x p)
-    fun p_element j b = linrep vars x (linear_add vars b (mk_number j)) p  
-    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) bset)  
-   in (list_disj (map stage js))
-    end 
-  | _ => error "cooper: not an existential formula"; 
- 
-
-
-(* The plusinfinity version of cooper*)
-fun cooperpi vars1 fm =
-  case fm of
-   Const ("Ex",_) $ Abs(x0,T,p0) => let 
-    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
-    val x = Free (xn,T)
-    val vars = (xn::vars1)
-    val p = unitycoeff x  (posineq (simpl p1))
-    val p_inf = simpl (plusinf x p)
-    val aset = aset x p
-    val js = myupto 1 (divlcm x p)
-    fun p_element j a = linrep vars x (linear_sub vars a (mk_number j)) p
-    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) aset)
-   in (list_disj (map stage js))
-   end
-  | _ => error "cooper: not an existential formula";
-  
-
-(* Try to find a withness for the formula *)
-
-fun inf_w mi d vars x p = 
-  let val f = if mi then minusinf else plusinf in
-   case (simpl (minusinf x p)) of
-   Const("True",_)  => (SOME (mk_number 1), HOLogic.true_const)
-  |Const("False",_) => (NONE,HOLogic.false_const)
-  |F => 
-      let 
-      fun h n =
-       case ((simpl o evalc) (linrep vars x (mk_number n) F)) of 
-	Const("True",_) => (SOME (mk_number n),HOLogic.true_const)
-       |F' => if n=1 then (NONE,F')
-	     else let val (rw,rf) = h (n-1) in 
-	       (rw,HOLogic.mk_disj(F',rf))
-	     end
-
-      in (h d)
-      end
-  end;
-
-fun set_w d b st vars x p = let 
-    fun h ns = case ns of 
-    [] => (NONE,HOLogic.false_const)
-   |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of
-      Const("True",_) => (SOME n,HOLogic.true_const)
-      |F' => let val (rw,rf) = h nl 
-             in (rw,HOLogic.mk_disj(F',rf)) 
-	     end)
-    val f = if b then linear_add else linear_sub
-    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_number i)) st)) (myupto 1 d) []
-    in h p_elements
-    end;
-
-fun withness d b st vars x p = case (inf_w b d vars x p) of 
-   (SOME n,_) => (SOME n,HOLogic.true_const)
-  |(NONE,Pinf) => (case (set_w d b st vars x p) of 
-    (SOME n,_) => (SOME n,HOLogic.true_const)
-    |(_,Pst) => (NONE,HOLogic.mk_disj(Pinf,Pst)));
-
-
-
-
-(*Cooper main procedure*) 
-
-exception STAGE_TRUE;
-
-  
-fun cooper vars1 fm =
-  case fm of
-   Const ("Ex",_) $ Abs(x0,T,p0) => let 
-    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
-    val x = Free (xn,T)
-    val vars = (xn::vars1)
-(*     val p = unitycoeff x  (posineq (simpl p1)) *)
-    val p = unitycoeff x  p1 
-    val ast = aset x p
-    val bst = bset x p
-    val js = myupto 1 (divlcm x p)
-    val (p_inf,f,S ) = 
-    if (length bst) <= (length ast) 
-     then (simpl (minusinf x p),linear_add,bst)
-     else (simpl (plusinf x p), linear_sub,ast)
-    fun p_element j a = linrep vars x (f vars a (mk_number j)) p
-    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
-    fun stageh n = ((if n = 0 then []
-	else 
-	let 
-	val nth_stage = simpl (evalc (stage n))
-	in 
-	if (nth_stage = HOLogic.true_const) 
-	  then raise STAGE_TRUE 
-	  else if (nth_stage = HOLogic.false_const) then stageh (n-1)
-	    else nth_stage::(stageh (n-1))
-	end )
-        handle STAGE_TRUE => [HOLogic.true_const])
-    val slist = stageh (divlcm x p)
-   in (list_disj slist)
-   end
-  | _ => error "cooper: not an existential formula";
-
-
-(* A Version of cooper that returns a withness *)
-fun cooper_w vars1 fm =
-  case fm of
-   Const ("Ex",_) $ Abs(x0,T,p0) => let 
-    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
-    val x = Free (xn,T)
-    val vars = (xn::vars1)
-(*     val p = unitycoeff x  (posineq (simpl p1)) *)
-    val p = unitycoeff x  p1 
-    val ast = aset x p
-    val bst = bset x p
-    val d = divlcm x p
-    val (p_inf,S ) = 
-    if (length bst) <= (length ast) 
-     then (true,bst)
-     else (false,ast)
-    in withness d p_inf S vars x p 
-(*    fun p_element j a = linrep vars x (f vars a (mk_number j)) p
-    fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S)
-   in (list_disj (map stage js))
-*)
-   end
-  | _ => error "cooper: not an existential formula";
-
- 
-(* ------------------------------------------------------------------------- *) 
-(* Free variables in terms and formulas.	                             *) 
-(* ------------------------------------------------------------------------- *) 
- 
-fun fvt tml = case tml of 
-    [] => [] 
-  | Free(x,_)::r => x::(fvt r) 
- 
-fun fv fm = fvt (term_frees fm); 
- 
- 
-(* ========================================================================= *) 
-(* Quantifier elimination.                                                   *) 
-(* ========================================================================= *) 
-(*conj[/disj]uncts lists iterated conj[disj]unctions*) 
- 
-fun disjuncts fm = case fm of 
-    Const ("op |",_) $ p $ q => (disjuncts p) @ (disjuncts q) 
-  | _ => [fm]; 
- 
-fun conjuncts fm = case fm of 
-    Const ("op &",_) $p $ q => (conjuncts p) @ (conjuncts q) 
-  | _ => [fm]; 
- 
- 
- 
-(* ------------------------------------------------------------------------- *) 
-(* Lift procedure given literal modifier, formula normalizer & basic quelim. *) 
-(* ------------------------------------------------------------------------- *)
-
-fun lift_qelim afn nfn qfn isat = 
-let 
-fun qelift vars fm = if (isat fm) then afn vars fm 
-else  
-case fm of 
-  Const ("Not",_) $ p => HOLogic.Not $ (qelift vars p) 
-  | Const ("op &",_) $ p $q => HOLogic.conj $ (qelift vars p) $ (qelift vars q) 
-  | Const ("op |",_) $ p $ q => HOLogic.disj $ (qelift vars p) $ (qelift vars q) 
-  | Const ("op -->",_) $ p $ q => HOLogic.imp $ (qelift vars p) $ (qelift vars q) 
-  | Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q)) 
-  | Const ("All",QT) $ Abs(x,T,p) => HOLogic.Not $(qelift vars (Const ("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p)))) 
-  | (e as Const ("Ex",_)) $ Abs (x,T,p)  =>  qfn vars (e$Abs (x,T,(nfn(qelift (x::vars) p))))
-  | _ => fm 
- 
-in (fn fm => qelift (fv fm) fm)
-end; 
-
- 
-(*   
-fun lift_qelim afn nfn qfn isat = 
- let   fun qelim x vars p = 
-  let val cjs = conjuncts p 
-      val (ycjs,ncjs) = List.partition (has_bound) cjs in 
-      (if ycjs = [] then p else 
-                          let val q = (qfn vars ((HOLogic.exists_const HOLogic.intT 
-			  ) $ Abs(x,HOLogic.intT,(list_conj ycjs)))) in 
-                          (fold_rev conj_help ncjs q)  
-			  end) 
-       end 
-    
-  fun qelift vars fm = if (isat fm) then afn vars fm 
-    else  
-    case fm of 
-      Const ("Not",_) $ p => HOLogic.Not $ (qelift vars p) 
-    | Const ("op &",_) $ p $q => HOLogic.conj $ (qelift vars p) $ (qelift vars q) 
-    | Const ("op |",_) $ p $ q => HOLogic.disj $ (qelift vars p) $ (qelift vars q) 
-    | Const ("op -->",_) $ p $ q => HOLogic.imp $ (qelift vars p) $ (qelift vars q) 
-    | Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q)) 
-    | Const ("All",QT) $ Abs(x,T,p) => HOLogic.Not $(qelift vars (Const ("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p)))) 
-    | Const ("Ex",_) $ Abs (x,T,p)  => let  val djs = disjuncts(nfn(qelift (x::vars) p)) in 
-    			list_disj(map (qelim x vars) djs) end 
-    | _ => fm 
- 
-  in (fn fm => simpl(qelift (fv fm) fm)) 
-  end; 
-*)
- 
-(* ------------------------------------------------------------------------- *) 
-(* Cleverer (proposisional) NNF with conditional and literal modification.   *) 
-(* ------------------------------------------------------------------------- *) 
- 
-(*Function Negate used by cnnf, negates a formula p*) 
- 
-fun negate (Const ("Not",_) $ p) = p 
-    |negate p = (HOLogic.Not $ p); 
- 
-fun cnnf lfn = 
-  let fun cnnfh fm = case  fm of 
-      (Const ("op &",_) $ p $ q) => HOLogic.mk_conj(cnnfh p,cnnfh q) 
-    | (Const ("op |",_) $ p $ q) => HOLogic.mk_disj(cnnfh p,cnnfh q) 
-    | (Const ("op -->",_) $ p $q) => HOLogic.mk_disj(cnnfh(HOLogic.Not $ p),cnnfh q) 
-    | (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q) => HOLogic.mk_disj( 
-    		HOLogic.mk_conj(cnnfh p,cnnfh q), 
-		HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh(HOLogic.Not $q))) 
-
-    | (Const ("Not",_) $ (Const("Not",_) $ p)) => cnnfh p 
-    | (Const ("Not",_) $ (Const ("op &",_) $ p $ q)) => HOLogic.mk_disj(cnnfh(HOLogic.Not $ p),cnnfh(HOLogic.Not $ q)) 
-    | (Const ("Not",_) $(Const ("op |",_) $ (Const ("op &",_) $ p $ q) $  
-    			(Const ("op &",_) $ p1 $ r))) => if p1 = negate p then 
-		         HOLogic.mk_disj(  
-			   cnnfh (HOLogic.mk_conj(p,cnnfh(HOLogic.Not $ q))), 
-			   cnnfh (HOLogic.mk_conj(p1,cnnfh(HOLogic.Not $ r)))) 
-			 else  HOLogic.mk_conj(
-			  cnnfh (HOLogic.mk_disj(cnnfh (HOLogic.Not $ p),cnnfh(HOLogic.Not $ q))), 
-			   cnnfh (HOLogic.mk_disj(cnnfh (HOLogic.Not $ p1),cnnfh(HOLogic.Not $ r)))
-			 ) 
-    | (Const ("Not",_) $ (Const ("op |",_) $ p $ q)) => HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh(HOLogic.Not $ q)) 
-    | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) => HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)) 
-    | (Const ("Not",_) $ (Const ("op =",Type ("fun",[Type ("bool", []),_]))  $ p $ q)) => HOLogic.mk_disj(HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)),HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh q)) 
-    | _ => lfn fm  
-in cnnfh
- end; 
- 
-(*End- function the quantifierelimination an decion procedure of presburger formulas.*)   
-
-(*
-val integer_qelim = simpl o evalc o (lift_qelim linform (simpl o (cnnf posineq o evalc)) cooper is_arith_rel) ; 
-*)
-
-
-val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; 
-
-end;

--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Jun 11 11:07:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,988 +0,0 @@
-(*  Title:      HOL/Tools/Presburger/cooper_proof.ML
-    ID:         $Id$
-    Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
-
-File containing the implementation of the proof
-generation for Cooper Algorithm
-*)
-
-
-signature COOPER_PROOF =
-sig
-  val qe_Not : thm
-  val qe_conjI : thm
-  val qe_disjI : thm
-  val qe_impI : thm
-  val qe_eqI : thm
-  val qe_exI : thm
-  val list_to_set : typ -> term list -> term
-  val qe_get_terms : thm -> term * term
-  val cooper_prv  : theory -> term -> term -> thm
-  val proof_of_evalc : theory -> term -> thm
-  val proof_of_cnnf : theory -> term -> (term -> thm) -> thm
-  val proof_of_linform : theory -> string list -> term -> thm
-  val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm
-  val prove_elementar : theory -> string -> term -> thm
-  val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm
-end;
-
-structure CooperProof : COOPER_PROOF =
-struct
-open CooperDec;
-
-val presburger_ss = simpset ()
-  addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"];
-
-val cboolT = ctyp_of HOL.thy HOLogic.boolT;
-
-(*Theorems that will be used later for the proofgeneration*)
-
-val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
-val unity_coeff_ex = thm "unity_coeff_ex";
-
-(* Theorems for proving the adjustment of the coefficients*)
-
-val ac_lt_eq =  thm "ac_lt_eq";
-val ac_eq_eq = thm "ac_eq_eq";
-val ac_dvd_eq = thm "ac_dvd_eq";
-val ac_pi_eq = thm "ac_pi_eq";
-
-(* The logical compination of the sythetised properties*)
-val qe_Not = thm "qe_Not";
-val qe_conjI = thm "qe_conjI";
-val qe_disjI = thm "qe_disjI";
-val qe_impI = thm "qe_impI";
-val qe_eqI = thm "qe_eqI";
-val qe_exI = thm "qe_exI";
-val qe_ALLI = thm "qe_ALLI";
-
-(*Modulo D property for Pminusinf an Plusinf *)
-val fm_modd_minf = thm "fm_modd_minf";
-val not_dvd_modd_minf = thm "not_dvd_modd_minf";
-val dvd_modd_minf = thm "dvd_modd_minf";
-
-val fm_modd_pinf = thm "fm_modd_pinf";
-val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
-val dvd_modd_pinf = thm "dvd_modd_pinf";
-
-(* the minusinfinity proprty*)
-
-val fm_eq_minf = thm "fm_eq_minf";
-val neq_eq_minf = thm "neq_eq_minf";
-val eq_eq_minf = thm "eq_eq_minf";
-val le_eq_minf = thm "le_eq_minf";
-val len_eq_minf = thm "len_eq_minf";
-val not_dvd_eq_minf = thm "not_dvd_eq_minf";
-val dvd_eq_minf = thm "dvd_eq_minf";
-
-(* the Plusinfinity proprty*)
-
-val fm_eq_pinf = thm "fm_eq_pinf";
-val neq_eq_pinf = thm "neq_eq_pinf";
-val eq_eq_pinf = thm "eq_eq_pinf";
-val le_eq_pinf = thm "le_eq_pinf";
-val len_eq_pinf = thm "len_eq_pinf";
-val not_dvd_eq_pinf = thm "not_dvd_eq_pinf";
-val dvd_eq_pinf = thm "dvd_eq_pinf";
-
-(*Logical construction of the Property*)
-val eq_minf_conjI = thm "eq_minf_conjI";
-val eq_minf_disjI = thm "eq_minf_disjI";
-val modd_minf_disjI = thm "modd_minf_disjI";
-val modd_minf_conjI = thm "modd_minf_conjI";
-
-val eq_pinf_conjI = thm "eq_pinf_conjI";
-val eq_pinf_disjI = thm "eq_pinf_disjI";
-val modd_pinf_disjI = thm "modd_pinf_disjI";
-val modd_pinf_conjI = thm "modd_pinf_conjI";
-
-(*Cooper Backwards...*)
-(*Bset*)
-val not_bst_p_fm = thm "not_bst_p_fm";
-val not_bst_p_ne = thm "not_bst_p_ne";
-val not_bst_p_eq = thm "not_bst_p_eq";
-val not_bst_p_gt = thm "not_bst_p_gt";
-val not_bst_p_lt = thm "not_bst_p_lt";
-val not_bst_p_ndvd = thm "not_bst_p_ndvd";
-val not_bst_p_dvd = thm "not_bst_p_dvd";
-
-(*Aset*)
-val not_ast_p_fm = thm "not_ast_p_fm";
-val not_ast_p_ne = thm "not_ast_p_ne";
-val not_ast_p_eq = thm "not_ast_p_eq";
-val not_ast_p_gt = thm "not_ast_p_gt";
-val not_ast_p_lt = thm "not_ast_p_lt";
-val not_ast_p_ndvd = thm "not_ast_p_ndvd";
-val not_ast_p_dvd = thm "not_ast_p_dvd";
-
-(*Logical construction of the prop*)
-(*Bset*)
-val not_bst_p_conjI = thm "not_bst_p_conjI";
-val not_bst_p_disjI = thm "not_bst_p_disjI";
-val not_bst_p_Q_elim = thm "not_bst_p_Q_elim";
-
-(*Aset*)
-val not_ast_p_conjI = thm "not_ast_p_conjI";
-val not_ast_p_disjI = thm "not_ast_p_disjI";
-val not_ast_p_Q_elim = thm "not_ast_p_Q_elim";
-
-(*Cooper*)
-val cppi_eq = thm "cppi_eq";
-val cpmi_eq = thm "cpmi_eq";
-
-(*Others*)
-val simp_from_to = thm "simp_from_to";
-val P_eqtrue = thm "P_eqtrue";
-val P_eqfalse = thm "P_eqfalse";
-
-(*For Proving NNF*)
-
-val nnf_nn = thm "nnf_nn";
-val nnf_im = thm "nnf_im";
-val nnf_eq = thm "nnf_eq";
-val nnf_sdj = thm "nnf_sdj";
-val nnf_ncj = thm "nnf_ncj";
-val nnf_nim = thm "nnf_nim";
-val nnf_neq = thm "nnf_neq";
-val nnf_ndj = thm "nnf_ndj";
-
-(*For Proving term linearizition*)
-val linearize_dvd = thm "linearize_dvd";
-val lf_lt = thm "lf_lt";
-val lf_eq = thm "lf_eq";
-val lf_dvd = thm "lf_dvd";
-
-
-(* ------------------------------------------------------------------------- *)
-(*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
-(*Respectively by their abstract representation Const(@{const_name HOL.one},..) and Const(@{const_name HOL.zero},..)*)
-(*this is necessary because the theorems use this representation.*)
-(* This function should be elminated in next versions...*)
-(* ------------------------------------------------------------------------- *)
-
-fun norm_zero_one fm = case fm of
-  (Const (@{const_name HOL.times},_) $ c $ t) => 
-    if c = one then (norm_zero_one t)
-    else if (dest_number c = ~1) 
-         then (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
-         else (HOLogic.mk_binop @{const_name HOL.times} (norm_zero_one c,norm_zero_one t))
-  |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
-  |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
-  |_ => fm;
-
-(* ------------------------------------------------------------------------- *)
-(*function list to Set, constructs a set containing all elements of a given list.*)
-(* ------------------------------------------------------------------------- *)
-fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in 
-	case l of 
-		[] => Const ("{}",T)
-		|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
-		end;
-		
-(* ------------------------------------------------------------------------- *)
-(* Returns both sides of an equvalence in the theorem*)
-(* ------------------------------------------------------------------------- *)
-fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
-
-(* ------------------------------------------------------------------------- *)
-(*This function proove elementar will be used to generate proofs at
-  runtime*) (*It is thought to prove properties such as a dvd b
-  (essentially) that are only to make at runtime.*)
-(* ------------------------------------------------------------------------- *)
-fun prove_elementar thy s fm2 =
-  Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
-  (case s of
-  (*"ss" like simplification with simpset*)
-  "ss" =>
-    let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex]
-    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
-
-  (*"bl" like blast tactic*)
-  (* Is only used in the harrisons like proof procedure *)
-  | "bl" => [blast_tac HOL_cs 1]
-
-  (*"ed" like Existence disjunctions ...*)
-  (* Is only used in the harrisons like proof procedure *)
-  | "ed" =>
-    let
-      val ex_disj_tacs =
-        let
-          val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1]
-          val tac2 = EVERY[etac exE 1, rtac exI 1,
-            REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1]
-	in [rtac iffI 1,
-          etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
-          REPEAT(EVERY[etac disjE 1, tac2]), tac2]
-        end
-    in ex_disj_tacs end
-
-  | "fa" => [simple_arith_tac 1]
-
-  | "sa" =>
-    let val ss = presburger_ss addsimps zadd_ac
-    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
-
-  (* like Existance Conjunction *)
-  | "ec" =>
-    let val ss = presburger_ss addsimps zadd_ac
-    in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end
-
-  | "ac" =>
-    let val ss = HOL_basic_ss addsimps zadd_ac
-    in [simp_tac ss 1] end
-
-  | "lf" =>
-    let val ss = presburger_ss addsimps zadd_ac
-    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end));
-
-(*=============================================================*)
-(*-------------------------------------------------------------*)
-(*              The new compact model                          *)
-(*-------------------------------------------------------------*)
-(*=============================================================*)
-
-fun thm_of sg decomp t = 
-    let val (ts,recomb) = decomp t 
-    in recomb (map (thm_of sg decomp) ts) 
-    end;
-
-(*==================================================*)
-(*     Compact Version for adjustcoeffeq            *)
-(*==================================================*)
-
-fun decomp_adjustcoeffeq sg x l fm = case fm of
-    (Const("Not",_)$(Const(@{const_name Orderings.less},_) $ zero $(rt as (Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $    c $ y ) $z )))) => 
-     let  
-        val m = l div (dest_number c) 
-        val n = if (x = y) then abs (m) else 1
-        val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div n)*l) ), x)) 
-        val rs = if (x = y) 
-                 then (HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] (mk_number n) (HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul n z) )))) 
-                 else HOLogic.mk_binrel @{const_name Orderings.less} (zero,linear_sub [] one rt )
-        val ck = cterm_of sg (mk_number n)
-        val cc = cterm_of sg c
-        val ct = cterm_of sg z
-        val cx = cterm_of sg y
-        val pre = prove_elementar sg "lf" 
-            (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number n))
-        val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
-        in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
-        end
-
-  |(Const(p,_) $a $( Const (@{const_name HOL.plus}, _)$(Const (@{const_name HOL.times},_) $ 
-      c $ y ) $t )) => 
-   if (is_arith_rel fm) andalso (x = y) 
-   then  
-        let val m = l div (dest_number c) 
-           val k = (if p = @{const_name Orderings.less} then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop @{const_name HOL.times} ((mk_number ((m div k)*l) ), x))
-           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop @{const_name HOL.plus} ( xtm ,( linear_cmul k t) )))) 
-
-           val ck = cterm_of sg (mk_number k)
-           val cc = cterm_of sg c
-           val ct = cterm_of sg t
-           val cx = cterm_of sg x
-           val ca = cterm_of sg a
-
-	   in 
-	case p of
-	  @{const_name Orderings.less} => 
-	let val pre = prove_elementar sg "lf" 
-	    (HOLogic.mk_binrel @{const_name Orderings.less} (zero, mk_number k))
-            val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
-	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
-         end
-
-           |"op =" =>
-	     let val pre = prove_elementar sg "lf" 
-	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
-	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
-	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
-             end
-
-             |"Divides.dvd" =>
-	       let val pre = prove_elementar sg "lf" 
-	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (zero, mk_number k)))
-                   val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
-               in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
-                        
-               end
-              end
-  else ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl)
-
- |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not)
-  |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI)
-  |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI)
-
-  |_ => ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl);
-
-fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
-
-
-
-(*==================================================*)
-(*   Finding rho for modd_minusinfinity             *)
-(*==================================================*)
-fun rho_for_modd_minf x dlcm sg fm1 =
-let
-    (*Some certified Terms*)
-    
-   val ctrue = cterm_of sg HOLogic.true_const
-   val cfalse = cterm_of sg HOLogic.false_const
-   val fm = norm_zero_one fm1
-  in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
-         if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
-           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
-  	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
-	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
-	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
-
-      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
-           if (y=x) andalso (c1 = zero) then 
-            if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
-	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
-	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-  
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
-	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
-		      end
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-      |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
-      c $ y ) $ z))) => 
-         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
-	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
-		      end
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-		
-    
-   |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)
-   end;	 
-(*=========================================================================*)
-(*=========================================================================*)
-fun rho_for_eq_minf x dlcm  sg fm1 =  
-   let
-   val fm = norm_zero_one fm1
-    in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
-         if  (x=y) andalso (c1=zero) andalso (c2=one) 
-	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
-           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
-  	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
-	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
-	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
-
-      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
-           if (y=x) andalso (c1 =zero) then 
-            if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
-	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
-	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
-	 		  val cz = cterm_of sg (norm_zero_one z)
-	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
-		      end
-
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-		
-      |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
-	 		  val cz = cterm_of sg (norm_zero_one z)
-	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
-		      end
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-
-      		
-    |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- end;
-
-(*=====================================================*)
-(*=====================================================*)
-(*=========== minf proofs with the compact version==========*)
-fun decomp_minf_eq x dlcm sg t =  case t of
-   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI)
-   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI)
-   |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t);
-
-fun decomp_minf_modd x dlcm sg t = case t of
-   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI)
-   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI)
-   |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t);
-
-(* -------------------------------------------------------------*)
-(*                    Finding rho for pinf_modd                 *)
-(* -------------------------------------------------------------*)
-fun rho_for_modd_pinf x dlcm sg fm1 = 
-let
-    (*Some certified Terms*)
-    
-  val ctrue = cterm_of sg HOLogic.true_const
-  val cfalse = cterm_of sg HOLogic.false_const
-  val fm = norm_zero_one fm1
- in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
-         if ((x=y) andalso (c1= zero) andalso (c2= one))
-	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
-         else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
-  	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
-	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
-	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-
-      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
-        if ((y=x) andalso (c1 = zero)) then 
-          if (pm1 = one) 
-	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
-	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
-	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-  
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
-	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
-		      end
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-      |(Const("Divides.dvd",_)$ d $ (db as (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $
-      c $ y ) $ z))) => 
-         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero)
-	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
-		      end
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-		
-    
-   |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)
-   end;	
-(* -------------------------------------------------------------*)
-(*                    Finding rho for pinf_eq                 *)
-(* -------------------------------------------------------------*)
-fun rho_for_eq_pinf x dlcm sg fm1 = 
-  let
-					val fm = norm_zero_one fm1
-    in  case fm1 of 
-      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
-         if  (x=y) andalso (c1=zero) andalso (c2=one) 
-	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
-           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-
-      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
-  	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
-	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
-	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
-
-      |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
-           if (y=x) andalso (c1 =zero) then 
-            if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
-	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
-	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
-	 		  val cz = cterm_of sg (norm_zero_one z)
-	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
-		      end
-
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-		
-      |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
-	 		  val cz = cterm_of sg (norm_zero_one z)
-	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
-		      end
-		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-
-      		
-    |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- end;
-
-
-
-fun  minf_proof_of_c sg x dlcm t =
-  let val minf_eqth   = thm_of sg (decomp_minf_eq x dlcm sg) t
-      val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t
-  in (minf_eqth, minf_moddth)
-end;
-
-(*=========== pinf proofs with the compact version==========*)
-fun decomp_pinf_eq x dlcm sg t = case t of
-   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI)
-   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI)
-   |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ;
-
-fun decomp_pinf_modd x dlcm sg t =  case t of
-   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI)
-   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI)
-   |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t);
-
-fun  pinf_proof_of_c sg x dlcm t =
-  let val pinf_eqth   = thm_of sg (decomp_pinf_eq x dlcm sg) t
-      val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t
-  in (pinf_eqth,pinf_moddth)
-end;
-
-
-(* ------------------------------------------------------------------------- *)
-(* Here we generate the theorem for the Bset Property in the simple direction*)
-(* It is just an instantiation*)
-(* ------------------------------------------------------------------------- *)
-(*
-fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm   = 
-  let
-    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cdlcm = cterm_of sg dlcm
-    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
-  in instantiate' [] [SOME cdlcm,SOME cB, SOME cp] (bst_thm)
-end;
-
-fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm = 
-  let
-    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cdlcm = cterm_of sg dlcm
-    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
-  in instantiate' [] [SOME cdlcm,SOME cA, SOME cp] (ast_thm)
-end;
-*)
-
-(* For the generation of atomic Theorems*)
-(* Prove the premisses on runtime and then make RS*)
-(* ------------------------------------------------------------------------- *)
-
-(*========= this is rho ============*)
-fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = 
-  let
-    val cdlcm = cterm_of sg dlcm
-    val cB = cterm_of sg B
-    val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cat = cterm_of sg (norm_zero_one at)
-  in
-  case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
-      if  (x=y) andalso (c1=zero) andalso (c2=one) 
-	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
-        val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero ,dlcm))
-	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
-	 end
-         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
-
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
-     if (is_arith_rel at) andalso (x=y)
-    then let
-      val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_number 1)))
-    in
-      let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const(@{const_name HOL.minus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $ norm_zero_one z) $ HOLogic.mk_number HOLogic.intT 1))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
-	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
-	 end
-       end
-         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
-
-   |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
-        if (y=x) andalso (c1 =zero) then 
-        if pm1 = one then 
-	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
-	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
-	    end
-	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
-	      in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
-	      end
-      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
-
-   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-      if y=x then  
-           let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
- 	     in (instantiate' []  [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
-	     end
-      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
-
-   |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-       if y=x then  
-	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
- 	    in (instantiate' []  [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
-	  end
-      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
-      		
-   |_ => (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
-      		
-    end;
-    
-
-(* ------------------------------------------------------------------------- *)    
-(* Main interpretation function for this backwards dirction*)
-(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
-(*Help Function*)
-(* ------------------------------------------------------------------------- *)
-
-(*==================== Proof with the compact version   *)
-
-fun decomp_nbstp sg x dlcm B fm t = case t of 
-   Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI )
-  |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI)
-  |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t);
-
-fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t =
-  let 
-       val th =  thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t
-      val fma = absfree (xn,xT, norm_zero_one fm)
-  in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
-     in [th,th1] MRS (not_bst_p_Q_elim)
-     end
-  end;
-
-
-(* ------------------------------------------------------------------------- *)    
-(* Protokol interpretation function for the backwards direction for cooper's Theorem*)
-
-(* For the generation of atomic Theorems*)
-(* Prove the premisses on runtime and then make RS*)
-(* ------------------------------------------------------------------------- *)
-(*========= this is rho ============*)
-fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = 
-  let
-    val cdlcm = cterm_of sg dlcm
-    val cA = cterm_of sg A
-    val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
-    val cat = cterm_of sg (norm_zero_one at)
-  in
-  case at of 
-   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z))) => 
-      if  (x=y) andalso (c1=zero) andalso (c2=one) 
-	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
-	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
-		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
-	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
-	 end
-         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
-
-   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const (@{const_name HOL.plus}, T) $(Const (@{const_name HOL.times},_) $ c2 $ y) $z)) =>
-     if (is_arith_rel at) andalso (x=y)
-	then let val ast_z = norm_zero_one (linear_sub [] one z )
-	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
-	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const(@{const_name HOL.plus},T) $ (Const(@{const_name HOL.uminus},HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ one))
-		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
-	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
-       end
-         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
-
-   |(Const(@{const_name Orderings.less},_) $ c1 $(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times},_) $ pm1 $ y ) $ z )) =>
-        if (y=x) andalso (c1 =zero) then 
-        if pm1 = (mk_number ~1) then 
-	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
-              val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm))
-	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
-	    end
-	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero, dlcm))
-	      in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
-	      end
-      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
-
-   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-      if y=x then  
-           let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
- 	     in (instantiate' []  [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
-	     end
-      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
-
-   |(Const("Divides.dvd",_)$ d $ (Const (@{const_name HOL.plus},_) $ (Const (@{const_name HOL.times},_) $ c $ y ) $ z)) => 
-       if y=x then  
-	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop @{const_name Divides.mod} (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
- 	    in (instantiate' []  [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
-	  end
-      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
-      		
-   |_ => (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
-      		
-    end;
-
-(* ------------------------------------------------------------------------ *)
-(* Main interpretation function for this backwards dirction*)
-(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
-(*Help Function*)
-(* ------------------------------------------------------------------------- *)
-
-fun decomp_nastp sg x dlcm A fm t = case t of 
-   Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI )
-  |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI)
-  |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t);
-
-fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t =
-  let 
-       val th =  thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t
-      val fma = absfree (xn,xT, norm_zero_one fm)
-  in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
-     in [th,th1] MRS (not_ast_p_Q_elim)
-     end
-  end;
-
-
-(* -------------------------------*)
-(* Finding rho and beta for evalc *)
-(* -------------------------------*)
-
-fun rho_for_evalc sg at = case at of  
-    (Const (p,_) $ s $ t) =>(  
-    case AList.lookup (op =) operations p of 
-        SOME f => 
-           ((if (f ((dest_number s),(dest_number t))) 
-             then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
-             else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))  
-		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
-        | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
-     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-       case AList.lookup (op =) operations p of 
-         SOME f => 
-           ((if (f ((dest_number s),(dest_number t))) 
-             then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
-             else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))  
-		      handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) 
-         | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) 
-     | _ =>   instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl;
-
-
-(*=========================================================*)
-fun decomp_evalc sg t = case t of
-   (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
-   |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
-   |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
-   |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
-   |_ => ([], fn [] => rho_for_evalc sg t);
-
-
-fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm;
-
-(*==================================================*)
-(*     Proof of linform with the compact model      *)
-(*==================================================*)
-
-
-fun decomp_linform sg vars t = case t of
-   (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
-   |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
-   |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
-   |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
-   |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
-   |(Const("Divides.dvd",_)$d$r) => 
-     if is_number d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
-     else (warning "Nonlinear Term --- Non numeral leftside at dvd";
-       raise COOPER)
-   |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
-
-fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
-
-(* ------------------------------------------------------------------------- *)
-(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
-(* ------------------------------------------------------------------------- *)
-fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
-  (* Get the Bset thm*)
-  let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm 
-      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
-      val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
-  in (dpos,minf_eqth,nbstpthm,minf_moddth)
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
-(* ------------------------------------------------------------------------- *)
-fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
-  let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
-      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel @{const_name Orderings.less} (zero,dlcm));
-      val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
-  in (dpos,pinf_eqth,nastpthm,pinf_moddth)
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Interpretaion of Protocols of the cooper procedure : full version*)
-(* ------------------------------------------------------------------------- *)
-fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of
-  "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm 
-	      in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq)
-           end
-  |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm
-	       in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq)
-                end
- |_ => error "parameter error";
-
-(* ------------------------------------------------------------------------- *)
-(* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*)
-(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
-(* ------------------------------------------------------------------------- *)
-
-(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*)
-(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *)
-
-fun cooper_prv sg (x as Free(xn,xT)) efm = let 
-   (* lfm_thm : efm = linearized form of efm*)
-   val lfm_thm = proof_of_linform sg [xn] efm
-   (*efm2 is the linearized form of efm *) 
-   val efm2 = snd(qe_get_terms lfm_thm)
-   (* l is the lcm of all coefficients of x *)
-   val l = formlcm x efm2
-   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
-   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
-   (* fm is efm2 with adjusted coefficients of x *)
-   val fm = snd (qe_get_terms ac_thm)
-  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
-   val  cfm = unitycoeff x fm
-   (*afm is fm where c*x is replaced by 1*x or -1*x *)
-   val afm = adjustcoeff x l fm
-   (* P = %x.afm*)
-   val P = absfree(xn,xT,afm)
-   (* This simpset allows the elimination of the sets in bex {1..d} *)
-   val ss = presburger_ss addsimps
-     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
-   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
-   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
-   (* e_ac_thm : Ex x. efm = EX x. fm*)
-   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
-   (* A and B set of the formula*)
-   val A = aset x cfm
-   val B = bset x cfm
-   (* the divlcm (delta) of the formula*)
-   val dlcm = mk_number (divlcm x cfm)
-   (* Which set is smaller to generate the (hoepfully) shorter proof*)
-   val cms = if ((length A) < (length B )) then "pi" else "mi"
-(*   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
-   (* synthesize the proof of cooper's theorem*)
-    (* cp_thm: EX x. cfm = Q*)
-   val cp_thm =  cooper_thm sg cms x cfm dlcm A B
-   (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
-   (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
-(*
-   val _ = prth cp_thm
-   val _ = writeln "Expanding the bounded EX..."
-*)
-   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
-(*
-   val _ = writeln "Expanded" *)
-   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
-   val (lsuth,rsuth) = qe_get_terms (uth)
-   (* lseacth = EX x. efm; rseacth = EX x. fm*)
-   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
-   (* lscth = EX x. cfm; rscth = Q' *)
-   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
-   (* u_c_thm: EX x. P(l*x) = Q'*)
-   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
-   (* result: EX x. efm = Q'*)
- in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
-   end
-|cooper_prv _ _ _ =  error "Parameters format";
-
-(* **************************************** *)
-(*    An Other Version of cooper proving    *)
-(*     by giving a withness for EX          *)
-(* **************************************** *)
-
-
-
-fun cooper_prv_w sg (x as Free(xn,xT)) efm = let 
-   (* lfm_thm : efm = linearized form of efm*)
-   val lfm_thm = proof_of_linform sg [xn] efm
-   (*efm2 is the linearized form of efm *) 
-   val efm2 = snd(qe_get_terms lfm_thm)
-   (* l is the lcm of all coefficients of x *)
-   val l = formlcm x efm2
-   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
-   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
-   (* fm is efm2 with adjusted coefficients of x *)
-   val fm = snd (qe_get_terms ac_thm)
-  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
-   val  cfm = unitycoeff x fm
-   (*afm is fm where c*x is replaced by 1*x or -1*x *)
-   val afm = adjustcoeff x l fm
-   (* P = %x.afm*)
-   val P = absfree(xn,xT,afm)
-   (* This simpset allows the elimination of the sets in bex {1..d} *)
-   val ss = presburger_ss addsimps
-     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
-   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
-   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_number l))] (unity_coeff_ex)
-   (* e_ac_thm : Ex x. efm = EX x. fm*)
-   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
-   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
-   val (lsuth,rsuth) = qe_get_terms (uth)
-   (* lseacth = EX x. efm; rseacth = EX x. fm*)
-   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
-
-   val (w,rs) = cooper_w [] cfm
-   val exp_cp_thm =  case w of 
-     (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
-    SOME n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
-   |_ => let 
-    (* A and B set of the formula*)
-    val A = aset x cfm
-    val B = bset x cfm
-    (* the divlcm (delta) of the formula*)
-    val dlcm = mk_number (divlcm x cfm)
-    (* Which set is smaller to generate the (hoepfully) shorter proof*)
-    val cms = if ((length A) < (length B )) then "pi" else "mi"
-    (* synthesize the proof of cooper's theorem*)
-     (* cp_thm: EX x. cfm = Q*)
-    val cp_thm = cooper_thm sg cms x cfm dlcm A B
-     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
-    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
-    in refl RS (simplify ss (cp_thm RSN (2,trans)))
-    end
-   (* lscth = EX x. cfm; rscth = Q' *)
-   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
-   (* u_c_thm: EX x. P(l*x) = Q'*)
-   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
-   (* result: EX x. efm = Q'*)
- in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
-   end
-|cooper_prv_w _ _ _ =  error "Parameters format";
-
-
-
-fun decomp_cnnf sg lfnp P = case P of 
-     Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
-   |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS  qe_disjI)
-   |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn)
-   |Const("Not",_) $ (Const(opn,T) $ p $ q) => 
-     if opn = "op |" 
-      then case (p,q) of 
-         (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
-          if r1 = negate r 
-          then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],fn [th1_1,th1_2,th2_1,th2_2] => [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
-
-          else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
-        |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
-      else (
-         case (opn,T) of 
-           ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj )
-           |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim )
-           |("op =",Type ("fun",[Type ("bool", []),_])) => 
-           ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq)
-            |(_,_) => ([], fn [] => lfnp P)
-)
-
-   |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im)
-
-   |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
-     ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq )
-   |_ => ([], fn [] => lfnp P);
-
-
-
-
-fun proof_of_cnnf sg p lfnp = 
- let val th1 = thm_of sg (decomp_cnnf sg lfnp) p
-     val rs = snd(qe_get_terms th1)
-     val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs))
-  in [th1,th2] MRS trans
-  end;
-
-end;
-

--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Mon Jun 11 11:07:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-(* $Id$ *)
-(* The oracle for Presburger arithmetic based on the verified Code *)
-    (* in HOL/ex/Reflected_Presburger.thy *)
-
-structure ReflectedCooper =
-struct
-
-open Generated;
-(* pseudo reification : term -> intterm *)
-
-fun i_of_term vs t =  case t of
-    Free(xn,xT) => (case AList.lookup (op =) vs t of 
-        NONE   => error "Variable not found in the list!!"
-      | SOME n => Var n)
-  | Const(@{const_name HOL.zero},iT) => Cst 0
-  | Const(@{const_name HOL.one},iT) => Cst 1
-  | Bound i => Var (nat (IntInf.fromInt i))
-  | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
-  | Const (@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-  | Const (@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-  | Const (@{const_name HOL.times},_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2)
-  | Const (@{const_name Numeral.number_of},_)$t' => Cst (HOLogic.dest_numeral t')
-  | _ => error "i_of_term: unknown term";
-
-(* pseudo reification : term -> QF *)
-fun qf_of_term vs t = case t of 
-	Const("True",_) => T
-      | Const("False",_) => F
-      | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
-      | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
-      | Const ("Divides.dvd",_)$t1$t2 => 
-	Divides(i_of_term vs t1,i_of_term vs t2)
-      | Const("op =",eqT)$t1$t2 => 
-	if (domain_type eqT = HOLogic.intT)
-	then let val i1 = i_of_term vs t1
-		 val i2 = i_of_term vs t2
-	     in	Eq (i1,i2)
-	     end 
-	else Equ(qf_of_term vs t1,qf_of_term vs t2)
-      | Const("op &",_)$t1$t2 => And(qf_of_term vs t1,qf_of_term vs t2)
-      | Const("op |",_)$t1$t2 => Or(qf_of_term vs t1,qf_of_term vs t2)
-      | Const("op -->",_)$t1$t2 => Imp(qf_of_term vs t1,qf_of_term vs t2)
-      | Const("Not",_)$t' => NOT(qf_of_term vs t')
-      | Const("Ex",_)$Abs(xn,xT,p) => 
-	QEx(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p)
-      | Const("All",_)$Abs(xn,xT,p) => 
-	QAll(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p)
-      | _ => error "qf_of_term : unknown term!";
-
-(*
-fun parse thy s = term_of (Thm.read_cterm thy (s, HOLogic.boolT));
-
-val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i";
-*)
-fun zip [] [] = []
-  | zip (x::xs) (y::ys) = (x,y)::(zip xs ys);
-
-
-fun start_vs t =
-    let val fs = term_frees t
-    in zip fs (map (nat o IntInf.fromInt) (0 upto  (length fs - 1)))
-    end ;
-
-(* transform intterm and QF back to terms *)
-val iT = HOLogic.intT;
-val bT = HOLogic.boolT;
-fun myassoc2 l v =
-    case l of
-	[] => NONE
-      | (x,v')::xs => if v = v' then SOME x
-		      else myassoc2 xs v;
-
-fun term_of_i vs t =
-    case t of 
-	Cst i => CooperDec.mk_number i
-      | Var n => valOf (myassoc2 vs n)
-      | Neg t' => Const(@{const_name HOL.uminus},iT --> iT)$(term_of_i vs t')
-      | Add(t1,t2) => Const(@{const_name HOL.plus},[iT,iT] ---> iT)$
-			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Sub(t1,t2) => Const(@{const_name HOL.minus},[iT,iT] ---> iT)$
-			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Mult(t1,t2) => Const(@{const_name HOL.times},[iT,iT] ---> iT)$
-			   (term_of_i vs t1)$(term_of_i vs t2);
-
-fun term_of_qf vs t = 
-    case t of 
-	T => HOLogic.true_const 
-      | F => HOLogic.false_const
-      | Lt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
-			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Le(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
-			  (term_of_i vs t1)$(term_of_i vs t2)
-      | Gt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$
-			   (term_of_i vs t2)$(term_of_i vs t1)
-      | Ge(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$
-			  (term_of_i vs t2)$(term_of_i vs t1)
-      | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
-			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Divides(t1,t2) => Const("Divides.dvd",[iT,iT] ---> bT)$
-			       (term_of_i vs t1)$(term_of_i vs t2)
-      | NOT t' => HOLogic.Not$(term_of_qf vs t')
-      | And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2)
-      | Or(t1,t2) => HOLogic.disj$(term_of_qf vs t1)$(term_of_qf vs t2)
-      | Imp(t1,t2) => HOLogic.imp$(term_of_qf vs t1)$(term_of_qf vs t2)
-      | Equ(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf vs t1)$
-					   (term_of_qf vs t2)
-      | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
-
-(* The oracle *)
-fun presburger_oracle thy t =
-    let val vs = start_vs t
-	val result = lift_un (term_of_qf vs) (pa (qf_of_term vs t))
-    in 
-    case result of 
-	None => raise CooperDec.COOPER
-      | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t'))
-    end ;
- 
-end;

--- a/src/HOL/Tools/Presburger/reflected_presburger.ML	Mon Jun 11 11:07:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2172 +0,0 @@
-(* $Id$ *)
-
-    (* Caution: This file should not be modified. *)
-    (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
-fun nat (i:IntInf.int) = if i < 0 then 0 else i : IntInf.int;
-structure Generated =
-struct
-
-datatype intterm = Cst of IntInf.int | Var of IntInf.int | Neg of intterm
-  | Add of intterm * intterm | Sub of intterm * intterm
-  | Mult of intterm * intterm;
-
-datatype QF = Lt of intterm * intterm | Gt of intterm * intterm
-  | Le of intterm * intterm | Ge of intterm * intterm | Eq of intterm * intterm
-  | Divides of intterm * intterm | T | F | NOT of QF | And of QF * QF
-  | Or of QF * QF | Imp of QF * QF | Equ of QF * QF | QAll of QF | QEx of QF;
-
-datatype 'a option = None | Some of 'a;
-
-fun lift_un c None = None
-  | lift_un c (Some p) = Some (c p);
-
-fun lift_bin (c, (Some a, Some b)) = Some (c a b)
-  | lift_bin (c, (None, y)) = None
-  | lift_bin (c, (Some y, None)) = None;
-
-fun lift_qe qe None = None
-  | lift_qe qe (Some p) = qe p;
-
-fun qelim (qe, QAll p) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe, p))))
-  | qelim (qe, QEx p) = lift_qe qe (qelim (qe, p))
-  | qelim (qe, And (p, q)) =
-    lift_bin ((fn x => fn xa => And (x, xa)), (qelim (qe, p), qelim (qe, q)))
-  | qelim (qe, Or (p, q)) =
-    lift_bin ((fn x => fn xa => Or (x, xa)), (qelim (qe, p), qelim (qe, q)))
-  | qelim (qe, Imp (p, q)) =
-    lift_bin ((fn x => fn xa => Imp (x, xa)), (qelim (qe, p), qelim (qe, q)))
-  | qelim (qe, Equ (p, q)) =
-    lift_bin ((fn x => fn xa => Equ (x, xa)), (qelim (qe, p), qelim (qe, q)))
-  | qelim (qe, NOT p) = lift_un NOT (qelim (qe, p))
-  | qelim (qe, Lt (w, x)) = Some (Lt (w, x))
-  | qelim (qe, Gt (y, z)) = Some (Gt (y, z))
-  | qelim (qe, Le (aa, ab)) = Some (Le (aa, ab))
-  | qelim (qe, Ge (ac, ad)) = Some (Ge (ac, ad))
-  | qelim (qe, Eq (ae, af)) = Some (Eq (ae, af))
-  | qelim (qe, Divides (ag, ah)) = Some (Divides (ag, ah))
-  | qelim (qe, T) = Some T
-  | qelim (qe, F) = Some F;
-
-fun lin_mul (c, Cst i) = Cst (c * i)
-  | lin_mul (c, Add (Mult (Cst c', Var n), r)) =
-    (if (c = 0) then Cst 0
-      else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
-
-fun op_60_def0 m n = IntInf.< (m,n);
-
-fun op_60_61_def0 m n = not (op_60_def0 n m);
-
-fun lin_add (Add (Mult (Cst c1, Var n1), r1), Add (Mult (Cst c2, Var n2), r2)) =
-    (if (n1 = n2)
-      then let val c = Cst (c1 + c2)
-           in (if ((c1 + c2) = 0) then lin_add (r1, r2)
-                else Add (Mult (c, Var n1), lin_add (r1, r2)))
-           end
-      else (if op_60_61_def0 n1 n2
-             then Add (Mult (Cst c1, Var n1),
-                        lin_add (r1, Add (Mult (Cst c2, Var n2), r2)))
-             else Add (Mult (Cst c2, Var n2),
-                        lin_add (Add (Mult (Cst c1, Var n1), r1), r2))))
-  | lin_add (Add (Mult (Cst c1, Var n1), r1), Cst b) =
-    Add (Mult (Cst c1, Var n1), lin_add (r1, Cst b))
-  | lin_add (Cst x, Add (Mult (Cst c2, Var n2), r2)) =
-    Add (Mult (Cst c2, Var n2), lin_add (Cst x, r2))
-  | lin_add (Cst b1, Cst b2) = Cst (b1 + b2);
-
-fun lin_neg i = lin_mul (~1, i);
-
-fun linearize (Cst b) = Some (Cst b)
-  | linearize (Var n) = Some (Add (Mult (Cst 1, Var n), Cst 0))
-  | linearize (Neg i) = lift_un lin_neg (linearize i)
-  | linearize (Add (i, j)) =
-    lift_bin ((fn x => fn y => lin_add (x, y)), (linearize i, linearize j))
-  | linearize (Sub (i, j)) =
-    lift_bin
-      ((fn x => fn y => lin_add (x, lin_neg y)), (linearize i, linearize j))
-  | linearize (Mult (i, j)) =
-    (case linearize i of None => None
-      | Some x =>
-          (case x of
-            Cst xa =>
-              (case linearize j of None => None
-                | Some x => Some (lin_mul (xa, x)))
-            | Var xa =>
-                (case linearize j of None => None
-                  | Some xa =>
-                      (case xa of Cst xa => Some (lin_mul (xa, x))
-                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
-                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
-            | Neg xa =>
-                (case linearize j of None => None
-                  | Some xa =>
-                      (case xa of Cst xa => Some (lin_mul (xa, x))
-                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
-                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
-            | Add (xa, xb) =>
-                (case linearize j of None => None
-                  | Some xa =>
-                      (case xa of Cst xa => Some (lin_mul (xa, x))
-                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
-                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
-            | Sub (xa, xb) =>
-                (case linearize j of None => None
-                  | Some xa =>
-                      (case xa of Cst xa => Some (lin_mul (xa, x))
-                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
-                        | Sub (xa, xb) => None | Mult (xa, xb) => None))
-            | Mult (xa, xb) =>
-                (case linearize j of None => None
-                  | Some xa =>
-                      (case xa of Cst xa => Some (lin_mul (xa, x))
-                        | Var xa => None | Neg xa => None | Add (xa, xb) => None
-                        | Sub (xa, xb) => None | Mult (xa, xb) => None))));
-
-fun linform (Le (it1, it2)) =
-    lift_bin
-      ((fn x => fn y => Le (lin_add (x, lin_neg y), Cst 0)),
-        (linearize it1, linearize it2))
-  | linform (Eq (it1, it2)) =
-    lift_bin
-      ((fn x => fn y => Eq (lin_add (x, lin_neg y), Cst 0)),
-        (linearize it1, linearize it2))
-  | linform (Divides (d, t)) =
-    (case linearize d of None => None
-      | Some x =>
-          (case x of
-            Cst xa =>
-              (if (xa = 0) then None
-                else (case linearize t of None => None
-                       | Some xa => Some (Divides (x, xa))))
-            | Var xa => None | Neg xa => None | Add (xa, xb) => None
-            | Sub (xa, xb) => None | Mult (xa, xb) => None))
-  | linform T = Some T
-  | linform F = Some F
-  | linform (NOT p) = lift_un NOT (linform p)
-  | linform (And (p, q)) =
-    lift_bin ((fn f => fn g => And (f, g)), (linform p, linform q))
-  | linform (Or (p, q)) =
-    lift_bin ((fn f => fn g => Or (f, g)), (linform p, linform q));
-
-fun nnf (Lt (it1, it2)) = Le (Sub (it1, it2), Cst (~ 1))
-  | nnf (Gt (it1, it2)) = Le (Sub (it2, it1), Cst (~ 1))
-  | nnf (Le (it1, it2)) = Le (it1, it2)
-  | nnf (Ge (it1, it2)) = Le (it2, it1)
-  | nnf (Eq (it1, it2)) = Eq (it2, it1)
-  | nnf (Divides (d, t)) = Divides (d, t)
-  | nnf T = T
-  | nnf F = F
-  | nnf (And (p, q)) = And (nnf p, nnf q)
-  | nnf (Or (p, q)) = Or (nnf p, nnf q)
-  | nnf (Imp (p, q)) = Or (nnf (NOT p), nnf q)
-  | nnf (Equ (p, q)) = Or (And (nnf p, nnf q), And (nnf (NOT p), nnf (NOT q)))
-  | nnf (NOT (Lt (it1, it2))) = Le (it2, it1)
-  | nnf (NOT (Gt (it1, it2))) = Le (it1, it2)
-  | nnf (NOT (Le (it1, it2))) = Le (Sub (it2, it1), Cst (~ 1))
-  | nnf (NOT (Ge (it1, it2))) = Le (Sub (it1, it2), Cst (~ 1))
-  | nnf (NOT (Eq (it1, it2))) = NOT (Eq (it1, it2))
-  | nnf (NOT (Divides (d, t))) = NOT (Divides (d, t))
-  | nnf (NOT T) = F
-  | nnf (NOT F) = T
-  | nnf (NOT (NOT p)) = nnf p
-  | nnf (NOT (And (p, q))) = Or (nnf (NOT p), nnf (NOT q))
-  | nnf (NOT (Or (p, q))) = And (nnf (NOT p), nnf (NOT q))
-  | nnf (NOT (Imp (p, q))) = And (nnf p, nnf (NOT q))
-  | nnf (NOT (Equ (p, q))) =
-    Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
-
-fun op_45_def2 z w =  IntInf.+ (z,~ w);
-
-fun op_45_def0 m n = nat (op_45_def2 (m) (n));
-
-val id_1_def0 : IntInf.int = (0 + 1);
-
-fun decrvarsI (Cst i) = Cst i
-  | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
-  | decrvarsI (Neg a) = Neg (decrvarsI a)
-  | decrvarsI (Add (a, b)) = Add (decrvarsI a, decrvarsI b)
-  | decrvarsI (Sub (a, b)) = Sub (decrvarsI a, decrvarsI b)
-  | decrvarsI (Mult (a, b)) = Mult (decrvarsI a, decrvarsI b);
-
-fun decrvars (Lt (a, b)) = Lt (decrvarsI a, decrvarsI b)
-  | decrvars (Gt (a, b)) = Gt (decrvarsI a, decrvarsI b)
-  | decrvars (Le (a, b)) = Le (decrvarsI a, decrvarsI b)
-  | decrvars (Ge (a, b)) = Ge (decrvarsI a, decrvarsI b)
-  | decrvars (Eq (a, b)) = Eq (decrvarsI a, decrvarsI b)
-  | decrvars (Divides (a, b)) = Divides (decrvarsI a, decrvarsI b)
-  | decrvars T = T
-  | decrvars F = F
-  | decrvars (NOT p) = NOT (decrvars p)
-  | decrvars (And (p, q)) = And (decrvars p, decrvars q)
-  | decrvars (Or (p, q)) = Or (decrvars p, decrvars q)
-  | decrvars (Imp (p, q)) = Imp (decrvars p, decrvars q)
-  | decrvars (Equ (p, q)) = Equ (decrvars p, decrvars q);
-
-fun op_64 [] ys = ys
-  | op_64 (x :: xs) ys = (x :: op_64 xs ys);
-
-fun map f [] = []
-  | map f (x :: xs) = (f x :: map f xs);
-
-fun iupto (i:IntInf.int, j:IntInf.int) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
-
-fun all_sums (j:IntInf.int, []) = []
-  | all_sums (j, (i :: is)) =
-    op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
-
-fun split x = (fn p => x (fst p) (snd p));
-
-fun negateSnd x = split (fn q => fn r => (q, IntInf.~ r)) x;
-
-fun adjust b =
-  (fn (q:IntInf.int, r:IntInf.int) =>
-    (if (0 <= op_45_def2 r b) then ((((2:IntInf.int) * q) + (1:IntInf.int)), op_45_def2 r b)
-      else (((2:IntInf.int) * q), r)));
-
-fun negDivAlg (a:IntInf.int, b:IntInf.int) =
-    (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
-      else adjust b (negDivAlg (a, (2 * b))));
-
-fun posDivAlg (a:IntInf.int, b:IntInf.int) =
-    (if ((a < b) orelse (b <= 0)) then (0, a)
-      else adjust b (posDivAlg (a, (2 * b))));
-
-fun divAlg x =
-  split (fn a:IntInf.int => fn b:IntInf.int =>
-          (if (0 <= a)
-            then (if (0 <= b) then posDivAlg (a, b)
-                   else (if (a = 0) then (0, 0)
-                          else negateSnd (negDivAlg (~ a, ~ b))))
-            else (if (0 < b) then negDivAlg (a, b)
-                   else negateSnd (posDivAlg (~ a, ~ b)))))
-    x;
-
-fun op_mod_def1 a b = snd (divAlg (a, b));
-
-fun op_dvd m n = (op_mod_def1 n m = 0);
-
-fun psimpl (Le (l, r)) =
-    (case lift_bin
-            ((fn x => fn y => lin_add (x, lin_neg y)),
-              (linearize l, linearize r)) of
-      None => Le (l, r)
-      | Some x =>
-          (case x of Cst xa => (if (xa <= 0) then T else F)
-            | Var xa => Le (x, Cst 0) | Neg xa => Le (x, Cst 0)
-            | Add (xa, xb) => Le (x, Cst 0) | Sub (xa, xb) => Le (x, Cst 0)
-            | Mult (xa, xb) => Le (x, Cst 0)))
-  | psimpl (Eq (l, r)) =
-    (case lift_bin
-            ((fn x => fn y => lin_add (x, lin_neg y)),
-              (linearize l, linearize r)) of
-      None => Eq (l, r)
-      | Some x =>
-          (case x of Cst xa => (if (xa = 0) then T else F)
-            | Var xa => Eq (x, Cst 0) | Neg xa => Eq (x, Cst 0)
-            | Add (xa, xb) => Eq (x, Cst 0) | Sub (xa, xb) => Eq (x, Cst 0)
-            | Mult (xa, xb) => Eq (x, Cst 0)))
-  | psimpl (Divides (Cst d, t)) =
-    (case linearize t of None => Divides (Cst d, t)
-      | Some x =>
-          (case x of Cst xa => (if op_dvd d xa then T else F)
-            | Var xa => Divides (Cst d, x) | Neg xa => Divides (Cst d, x)
-            | Add (xa, xb) => Divides (Cst d, x)
-            | Sub (xa, xb) => Divides (Cst d, x)
-            | Mult (xa, xb) => Divides (Cst d, x)))
-  | psimpl (Equ (p, q)) =
-    let val p' = psimpl p; val q' = psimpl q
-    in (case p' of
-         Lt (x, xa) =>
-           (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-             | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-             | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-             | T => p' | F => NOT p' | NOT x => Equ (p', q')
-             | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-             | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-             | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Gt (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Le (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Ge (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Eq (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Divides (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | T => q'
-         | F => (case q' of Lt (x, xa) => NOT q' | Gt (x, xa) => NOT q'
-                  | Le (x, xa) => NOT q' | Ge (x, xa) => NOT q'
-                  | Eq (x, xa) => NOT q' | Divides (x, xa) => NOT q' | T => F
-                  | F => T | NOT x => x | And (x, xa) => NOT q'
-                  | Or (x, xa) => NOT q' | Imp (x, xa) => NOT q'
-                  | Equ (x, xa) => NOT q' | QAll x => NOT q' | QEx x => NOT q')
-         | NOT x =>
-             (case q' of Lt (xa, xb) => Equ (p', q')
-               | Gt (xa, xb) => Equ (p', q') | Le (xa, xb) => Equ (p', q')
-               | Ge (xa, xb) => Equ (p', q') | Eq (xa, xb) => Equ (p', q')
-               | Divides (xa, xb) => Equ (p', q') | T => p' | F => x
-               | NOT xa => Equ (x, xa) | And (xa, xb) => Equ (p', q')
-               | Or (xa, xb) => Equ (p', q') | Imp (xa, xb) => Equ (p', q')
-               | Equ (xa, xb) => Equ (p', q') | QAll xa => Equ (p', q')
-               | QEx xa => Equ (p', q'))
-         | And (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Or (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Imp (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | Equ (x, xa) =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | QAll x =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q'))
-         | QEx x =>
-             (case q' of Lt (x, xa) => Equ (p', q') | Gt (x, xa) => Equ (p', q')
-               | Le (x, xa) => Equ (p', q') | Ge (x, xa) => Equ (p', q')
-               | Eq (x, xa) => Equ (p', q') | Divides (x, xa) => Equ (p', q')
-               | T => p' | F => NOT p' | NOT x => Equ (p', q')
-               | And (x, xa) => Equ (p', q') | Or (x, xa) => Equ (p', q')
-               | Imp (x, xa) => Equ (p', q') | Equ (x, xa) => Equ (p', q')
-               | QAll x => Equ (p', q') | QEx x => Equ (p', q')))
-    end
-  | psimpl (NOT p) =
-    let val p' = psimpl p
-    in (case p' of Lt (x, xa) => NOT p' | Gt (x, xa) => NOT p'
-         | Le (x, xa) => NOT p' | Ge (x, xa) => NOT p' | Eq (x, xa) => NOT p'
-         | Divides (x, xa) => NOT p' | T => F | F => T | NOT x => x
-         | And (x, xa) => NOT p' | Or (x, xa) => NOT p' | Imp (x, xa) => NOT p'
-         | Equ (x, xa) => NOT p' | QAll x => NOT p' | QEx x => NOT p')
-    end
-  | psimpl (Lt (u, v)) = Lt (u, v)
-  | psimpl (Gt (w, x)) = Gt (w, x)
-  | psimpl (Ge (aa, ab)) = Ge (aa, ab)
-  | psimpl (Divides (Var bp, af)) = Divides (Var bp, af)
-  | psimpl (Divides (Neg bq, af)) = Divides (Neg bq, af)
-  | psimpl (Divides (Add (br, bs), af)) = Divides (Add (br, bs), af)
-  | psimpl (Divides (Sub (bt, bu), af)) = Divides (Sub (bt, bu), af)
-  | psimpl (Divides (Mult (bv, bw), af)) = Divides (Mult (bv, bw), af)
-  | psimpl T = T
-  | psimpl F = F
-  | psimpl (QAll ap) = QAll ap
-  | psimpl (QEx aq) = QEx aq
-  | psimpl (And (p, q)) =
-    let val p' = psimpl p
-    in (case p' of
-         Lt (x, xa) =>
-           let val q' = psimpl q
-           in (case q' of Lt (x, xa) => And (p', q')
-                | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                | Divides (x, xa) => And (p', q') | T => p' | F => F
-                | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                | QEx x => And (p', q'))
-           end
-         | Gt (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | Le (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | Ge (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | Eq (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | Divides (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | T => psimpl q | F => F
-         | NOT x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | And (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | Or (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | Imp (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | Equ (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | QAll x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end
-         | QEx x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => And (p', q')
-                  | Gt (x, xa) => And (p', q') | Le (x, xa) => And (p', q')
-                  | Ge (x, xa) => And (p', q') | Eq (x, xa) => And (p', q')
-                  | Divides (x, xa) => And (p', q') | T => p' | F => F
-                  | NOT x => And (p', q') | And (x, xa) => And (p', q')
-                  | Or (x, xa) => And (p', q') | Imp (x, xa) => And (p', q')
-                  | Equ (x, xa) => And (p', q') | QAll x => And (p', q')
-                  | QEx x => And (p', q'))
-             end)
-    end
-  | psimpl (Or (p, q)) =
-    let val p' = psimpl p
-    in (case p' of
-         Lt (x, xa) =>
-           let val q' = psimpl q
-           in (case q' of Lt (x, xa) => Or (p', q') | Gt (x, xa) => Or (p', q')
-                | Le (x, xa) => Or (p', q') | Ge (x, xa) => Or (p', q')
-                | Eq (x, xa) => Or (p', q') | Divides (x, xa) => Or (p', q')
-                | T => T | F => p' | NOT x => Or (p', q')
-                | And (x, xa) => Or (p', q') | Or (x, xa) => Or (p', q')
-                | Imp (x, xa) => Or (p', q') | Equ (x, xa) => Or (p', q')
-                | QAll x => Or (p', q') | QEx x => Or (p', q'))
-           end
-         | Gt (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | Le (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | Ge (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | Eq (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | Divides (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | T => T | F => psimpl q
-         | NOT x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | And (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | Or (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | Imp (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | Equ (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | QAll x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end
-         | QEx x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Or (p', q')
-                  | Gt (x, xa) => Or (p', q') | Le (x, xa) => Or (p', q')
-                  | Ge (x, xa) => Or (p', q') | Eq (x, xa) => Or (p', q')
-                  | Divides (x, xa) => Or (p', q') | T => T | F => p'
-                  | NOT x => Or (p', q') | And (x, xa) => Or (p', q')
-                  | Or (x, xa) => Or (p', q') | Imp (x, xa) => Or (p', q')
-                  | Equ (x, xa) => Or (p', q') | QAll x => Or (p', q')
-                  | QEx x => Or (p', q'))
-             end)
-    end
-  | psimpl (Imp (p, q)) =
-    let val p' = psimpl p
-    in (case p' of
-         Lt (x, xa) =>
-           let val q' = psimpl q
-           in (case q' of Lt (x, xa) => Imp (p', q')
-                | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                | QEx x => Imp (p', q'))
-           end
-         | Gt (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | Le (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | Ge (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | Eq (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | Divides (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | T => psimpl q | F => T
-         | NOT x =>
-             let val q' = psimpl q
-             in (case q' of Lt (xa, xb) => Or (x, q')
-                  | Gt (xa, xb) => Or (x, q') | Le (xa, xb) => Or (x, q')
-                  | Ge (xa, xb) => Or (x, q') | Eq (xa, xb) => Or (x, q')
-                  | Divides (xa, xb) => Or (x, q') | T => T | F => x
-                  | NOT xa => Or (x, q') | And (xa, xb) => Or (x, q')
-                  | Or (xa, xb) => Or (x, q') | Imp (xa, xb) => Or (x, q')
-                  | Equ (xa, xb) => Or (x, q') | QAll xa => Or (x, q')
-                  | QEx xa => Or (x, q'))
-             end
-         | And (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | Or (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | Imp (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | Equ (x, xa) =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | QAll x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end
-         | QEx x =>
-             let val q' = psimpl q
-             in (case q' of Lt (x, xa) => Imp (p', q')
-                  | Gt (x, xa) => Imp (p', q') | Le (x, xa) => Imp (p', q')
-                  | Ge (x, xa) => Imp (p', q') | Eq (x, xa) => Imp (p', q')
-                  | Divides (x, xa) => Imp (p', q') | T => T | F => NOT p'
-                  | NOT x => Imp (p', q') | And (x, xa) => Imp (p', q')
-                  | Or (x, xa) => Imp (p', q') | Imp (x, xa) => Imp (p', q')
-                  | Equ (x, xa) => Imp (p', q') | QAll x => Imp (p', q')
-                  | QEx x => Imp (p', q'))
-             end)
-    end;
-
-fun subst_it i (Cst b) = Cst b
-  | subst_it i (Var n) = (if (n = 0) then i else Var n)
-  | subst_it i (Neg it) = Neg (subst_it i it)
-  | subst_it i (Add (it1, it2)) = Add (subst_it i it1, subst_it i it2)
-  | subst_it i (Sub (it1, it2)) = Sub (subst_it i it1, subst_it i it2)
-  | subst_it i (Mult (it1, it2)) = Mult (subst_it i it1, subst_it i it2);
-
-fun subst_p i (Le (it1, it2)) = Le (subst_it i it1, subst_it i it2)
-  | subst_p i (Lt (it1, it2)) = Lt (subst_it i it1, subst_it i it2)
-  | subst_p i (Ge (it1, it2)) = Ge (subst_it i it1, subst_it i it2)
-  | subst_p i (Gt (it1, it2)) = Gt (subst_it i it1, subst_it i it2)
-  | subst_p i (Eq (it1, it2)) = Eq (subst_it i it1, subst_it i it2)
-  | subst_p i (Divides (d, t)) = Divides (subst_it i d, subst_it i t)
-  | subst_p i T = T
-  | subst_p i F = F
-  | subst_p i (And (p, q)) = And (subst_p i p, subst_p i q)
-  | subst_p i (Or (p, q)) = Or (subst_p i p, subst_p i q)
-  | subst_p i (Imp (p, q)) = Imp (subst_p i p, subst_p i q)
-  | subst_p i (Equ (p, q)) = Equ (subst_p i p, subst_p i q)
-  | subst_p i (NOT p) = NOT (subst_p i p);
-
-fun explode_disj ([], p) = F
-  | explode_disj ((i :: is), p) =
-    let val pi = psimpl (subst_p i p)
-    in (case pi of
-         Lt (x, xa) =>
-           let val r = explode_disj (is, p)
-           in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                | T => T | F => pi | NOT x => Or (pi, r)
-                | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-           end
-         | Gt (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | Le (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | Ge (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | Eq (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | Divides (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | T => T | F => explode_disj (is, p)
-         | NOT x =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | And (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | Or (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | Imp (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | Equ (x, xa) =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | QAll x =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end
-         | QEx x =>
-             let val r = explode_disj (is, p)
-             in (case r of Lt (x, xa) => Or (pi, r) | Gt (x, xa) => Or (pi, r)
-                  | Le (x, xa) => Or (pi, r) | Ge (x, xa) => Or (pi, r)
-                  | Eq (x, xa) => Or (pi, r) | Divides (x, xa) => Or (pi, r)
-                  | T => T | F => pi | NOT x => Or (pi, r)
-                  | And (x, xa) => Or (pi, r) | Or (x, xa) => Or (pi, r)
-                  | Imp (x, xa) => Or (pi, r) | Equ (x, xa) => Or (pi, r)
-                  | QAll x => Or (pi, r) | QEx x => Or (pi, r))
-             end)
-    end;
-
-fun minusinf (And (p, q)) = And (minusinf p, minusinf q)
-  | minusinf (Or (p, q)) = Or (minusinf p, minusinf q)
-  | minusinf (Lt (u, v)) = Lt (u, v)
-  | minusinf (Gt (w, x)) = Gt (w, x)
-  | minusinf (Le (Cst bo, z)) = Le (Cst bo, z)
-  | minusinf (Le (Var bp, z)) = Le (Var bp, z)
-  | minusinf (Le (Neg bq, z)) = Le (Neg bq, z)
-  | minusinf (Le (Add (Cst cg, bs), z)) = Le (Add (Cst cg, bs), z)
-  | minusinf (Le (Add (Var ch, bs), z)) = Le (Add (Var ch, bs), z)
-  | minusinf (Le (Add (Neg ci, bs), z)) = Le (Add (Neg ci, bs), z)
-  | minusinf (Le (Add (Add (cj, ck), bs), z)) = Le (Add (Add (cj, ck), bs), z)
-  | minusinf (Le (Add (Sub (cl, cm), bs), z)) = Le (Add (Sub (cl, cm), bs), z)
-  | minusinf (Le (Add (Mult (Cst cy, Cst dq), bs), z)) =
-    Le (Add (Mult (Cst cy, Cst dq), bs), z)
-  | minusinf (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
-    (if (ei = 0) then (if (cy < 0) then F else T)
-      else Le (Add (Mult (Cst cy, Var (op_45_def0 ei id_1_def0 + 1)), bs), z))
-  | minusinf (Le (Add (Mult (Cst cy, Neg ds), bs), z)) =
-    Le (Add (Mult (Cst cy, Neg ds), bs), z)
-  | minusinf (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) =
-    Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)
-  | minusinf (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) =
-    Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)
-  | minusinf (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) =
-    Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)
-  | minusinf (Le (Add (Mult (Var cz, co), bs), z)) =
-    Le (Add (Mult (Var cz, co), bs), z)
-  | minusinf (Le (Add (Mult (Neg da, co), bs), z)) =
-    Le (Add (Mult (Neg da, co), bs), z)
-  | minusinf (Le (Add (Mult (Add (db, dc), co), bs), z)) =
-    Le (Add (Mult (Add (db, dc), co), bs), z)
-  | minusinf (Le (Add (Mult (Sub (dd, de), co), bs), z)) =
-    Le (Add (Mult (Sub (dd, de), co), bs), z)
-  | minusinf (Le (Add (Mult (Mult (df, dg), co), bs), z)) =
-    Le (Add (Mult (Mult (df, dg), co), bs), z)
-  | minusinf (Le (Sub (bt, bu), z)) = Le (Sub (bt, bu), z)
-  | minusinf (Le (Mult (bv, bw), z)) = Le (Mult (bv, bw), z)
-  | minusinf (Ge (aa, ab)) = Ge (aa, ab)
-  | minusinf (Eq (Cst ek, ad)) = Eq (Cst ek, ad)
-  | minusinf (Eq (Var el, ad)) = Eq (Var el, ad)
-  | minusinf (Eq (Neg em, ad)) = Eq (Neg em, ad)
-  | minusinf (Eq (Add (Cst fc, eo), ad)) = Eq (Add (Cst fc, eo), ad)
-  | minusinf (Eq (Add (Var fd, eo), ad)) = Eq (Add (Var fd, eo), ad)
-  | minusinf (Eq (Add (Neg fe, eo), ad)) = Eq (Add (Neg fe, eo), ad)
-  | minusinf (Eq (Add (Add (ff, fg), eo), ad)) = Eq (Add (Add (ff, fg), eo), ad)
-  | minusinf (Eq (Add (Sub (fh, fi), eo), ad)) = Eq (Add (Sub (fh, fi), eo), ad)
-  | minusinf (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) =
-    Eq (Add (Mult (Cst fu, Cst gm), eo), ad)
-  | minusinf (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
-    (if (he = 0) then F
-      else Eq (Add (Mult (Cst fu, Var (op_45_def0 he id_1_def0 + 1)), eo), ad))
-  | minusinf (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) =
-    Eq (Add (Mult (Cst fu, Neg go), eo), ad)
-  | minusinf (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) =
-    Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)
-  | minusinf (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) =
-    Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)
-  | minusinf (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) =
-    Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)
-  | minusinf (Eq (Add (Mult (Var fv, fk), eo), ad)) =
-    Eq (Add (Mult (Var fv, fk), eo), ad)
-  | minusinf (Eq (Add (Mult (Neg fw, fk), eo), ad)) =
-    Eq (Add (Mult (Neg fw, fk), eo), ad)
-  | minusinf (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) =
-    Eq (Add (Mult (Add (fx, fy), fk), eo), ad)
-  | minusinf (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) =
-    Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)
-  | minusinf (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) =
-    Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)
-  | minusinf (Eq (Sub (ep, eq), ad)) = Eq (Sub (ep, eq), ad)
-  | minusinf (Eq (Mult (er, es), ad)) = Eq (Mult (er, es), ad)
-  | minusinf (Divides (ae, af)) = Divides (ae, af)
-  | minusinf T = T
-  | minusinf F = F
-  | minusinf (NOT (Lt (hg, hh))) = NOT (Lt (hg, hh))
-  | minusinf (NOT (Gt (hi, hj))) = NOT (Gt (hi, hj))
-  | minusinf (NOT (Le (hk, hl))) = NOT (Le (hk, hl))
-  | minusinf (NOT (Ge (hm, hn))) = NOT (Ge (hm, hn))
-  | minusinf (NOT (Eq (Cst ja, hp))) = NOT (Eq (Cst ja, hp))
-  | minusinf (NOT (Eq (Var jb, hp))) = NOT (Eq (Var jb, hp))
-  | minusinf (NOT (Eq (Neg jc, hp))) = NOT (Eq (Neg jc, hp))
-  | minusinf (NOT (Eq (Add (Cst js, je), hp))) = NOT (Eq (Add (Cst js, je), hp))
-  | minusinf (NOT (Eq (Add (Var jt, je), hp))) = NOT (Eq (Add (Var jt, je), hp))
-  | minusinf (NOT (Eq (Add (Neg ju, je), hp))) = NOT (Eq (Add (Neg ju, je), hp))
-  | minusinf (NOT (Eq (Add (Add (jv, jw), je), hp))) =
-    NOT (Eq (Add (Add (jv, jw), je), hp))
-  | minusinf (NOT (Eq (Add (Sub (jx, jy), je), hp))) =
-    NOT (Eq (Add (Sub (jx, jy), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) =
-    NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
-    (if (lu = 0) then T
-      else NOT (Eq (Add (Mult (Cst kk, Var (op_45_def0 lu id_1_def0 + 1)), je),
-                     hp)))
-  | minusinf (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) =
-    NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) =
-    NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) =
-    NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) =
-    NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) =
-    NOT (Eq (Add (Mult (Var kl, ka), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) =
-    NOT (Eq (Add (Mult (Neg km, ka), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) =
-    NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) =
-    NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))
-  | minusinf (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) =
-    NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))
-  | minusinf (NOT (Eq (Sub (jf, jg), hp))) = NOT (Eq (Sub (jf, jg), hp))
-  | minusinf (NOT (Eq (Mult (jh, ji), hp))) = NOT (Eq (Mult (jh, ji), hp))
-  | minusinf (NOT (Divides (hq, hr))) = NOT (Divides (hq, hr))
-  | minusinf (NOT T) = NOT T
-  | minusinf (NOT F) = NOT F
-  | minusinf (NOT (NOT hs)) = NOT (NOT hs)
-  | minusinf (NOT (And (ht, hu))) = NOT (And (ht, hu))
-  | minusinf (NOT (Or (hv, hw))) = NOT (Or (hv, hw))
-  | minusinf (NOT (Imp (hx, hy))) = NOT (Imp (hx, hy))
-  | minusinf (NOT (Equ (hz, ia))) = NOT (Equ (hz, ia))
-  | minusinf (NOT (QAll ib)) = NOT (QAll ib)
-  | minusinf (NOT (QEx ic)) = NOT (QEx ic)
-  | minusinf (Imp (al, am)) = Imp (al, am)
-  | minusinf (Equ (an, ao)) = Equ (an, ao)
-  | minusinf (QAll ap) = QAll ap
-  | minusinf (QEx aq) = QEx aq;
-
-fun abs (i:IntInf.int) = (if (i < 0) then IntInf.~ i else i);
-
-fun op_div_def1 a b = fst (divAlg (a, b));
-
-fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
-
-fun ngcd (m:IntInf.int, n:IntInf.int) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
-
-fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
-
-fun ilcm (a:IntInf.int) (b:IntInf.int) = op_div_def1 (a * b) (igcd (a, b));
-
-fun divlcm (NOT p) = divlcm p
-  | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
-  | divlcm (Or (p, q)) = ilcm (divlcm p) (divlcm q)
-  | divlcm (Lt (u, v)) = 1
-  | divlcm (Gt (w, x)) = 1
-  | divlcm (Le (y, z)) = 1
-  | divlcm (Ge (aa, ab)) = 1
-  | divlcm (Eq (ac, ad)) = 1
-  | divlcm (Divides (Cst bo, Cst cg)) = 1
-  | divlcm (Divides (Cst bo, Var ch)) = 1
-  | divlcm (Divides (Cst bo, Neg ci)) = 1
-  | divlcm (Divides (Cst bo, Add (Cst cy, ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Var cz, ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Neg da, ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Add (db, dc), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Sub (dd, de), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Cst ei), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Var fa), ck))) =
-    (if (fa = 0) then abs bo else 1)
-  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Neg ek), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Add (el, em)), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Sub (en, eo)), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Cst dq, Mult (ep, eq)), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Var dr, dg), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Neg ds, dg), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Add (dt, du), dg), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Sub (dv, dw), dg), ck))) = 1
-  | divlcm (Divides (Cst bo, Add (Mult (Mult (dx, dy), dg), ck))) = 1
-  | divlcm (Divides (Cst bo, Sub (cl, cm))) = 1
-  | divlcm (Divides (Cst bo, Mult (cn, co))) = 1
-  | divlcm (Divides (Var bp, af)) = 1
-  | divlcm (Divides (Neg bq, af)) = 1
-  | divlcm (Divides (Add (br, bs), af)) = 1
-  | divlcm (Divides (Sub (bt, bu), af)) = 1
-  | divlcm (Divides (Mult (bv, bw), af)) = 1
-  | divlcm T = 1
-  | divlcm F = 1
-  | divlcm (Imp (al, am)) = 1
-  | divlcm (Equ (an, ao)) = 1
-  | divlcm (QAll ap) = 1
-  | divlcm (QEx aq) = 1;
-
-fun explode_minf (q, B) =
-    let val d = divlcm q; val pm = minusinf q;
-        val dj1 = explode_disj (map (fn x => Cst x) (iupto (1, d)), pm)
-    in (case dj1 of
-         Lt (x, xa) =>
-           let val dj2 = explode_disj (all_sums (d, B), q)
-           in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                | QEx x => Or (dj1, dj2))
-           end
-         | Gt (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | Le (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | Ge (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | Eq (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | Divides (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | T => T | F => explode_disj (all_sums (d, B), q)
-         | NOT x =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | And (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | Or (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | Imp (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | Equ (x, xa) =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | QAll x =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end
-         | QEx x =>
-             let val dj2 = explode_disj (all_sums (d, B), q)
-             in (case dj2 of Lt (x, xa) => Or (dj1, dj2)
-                  | Gt (x, xa) => Or (dj1, dj2) | Le (x, xa) => Or (dj1, dj2)
-                  | Ge (x, xa) => Or (dj1, dj2) | Eq (x, xa) => Or (dj1, dj2)
-                  | Divides (x, xa) => Or (dj1, dj2) | T => T | F => dj1
-                  | NOT x => Or (dj1, dj2) | And (x, xa) => Or (dj1, dj2)
-                  | Or (x, xa) => Or (dj1, dj2) | Imp (x, xa) => Or (dj1, dj2)
-                  | Equ (x, xa) => Or (dj1, dj2) | QAll x => Or (dj1, dj2)
-                  | QEx x => Or (dj1, dj2))
-             end)
-    end;
-
-fun mirror (And (p, q)) = And (mirror p, mirror q)
-  | mirror (Or (p, q)) = Or (mirror p, mirror q)
-  | mirror (Lt (u, v)) = Lt (u, v)
-  | mirror (Gt (w, x)) = Gt (w, x)
-  | mirror (Le (Cst bp, aa)) = Le (Cst bp, aa)
-  | mirror (Le (Var bq, aa)) = Le (Var bq, aa)
-  | mirror (Le (Neg br, aa)) = Le (Neg br, aa)
-  | mirror (Le (Add (Cst ch, bt), aa)) = Le (Add (Cst ch, bt), aa)
-  | mirror (Le (Add (Var ci, bt), aa)) = Le (Add (Var ci, bt), aa)
-  | mirror (Le (Add (Neg cj, bt), aa)) = Le (Add (Neg cj, bt), aa)
-  | mirror (Le (Add (Add (ck, cl), bt), aa)) = Le (Add (Add (ck, cl), bt), aa)
-  | mirror (Le (Add (Sub (cm, cn), bt), aa)) = Le (Add (Sub (cm, cn), bt), aa)
-  | mirror (Le (Add (Mult (Cst cz, Cst dr), bt), aa)) =
-    Le (Add (Mult (Cst cz, Cst dr), bt), aa)
-  | mirror (Le (Add (Mult (Cst cz, Var ej), bt), aa)) =
-    (if (ej = 0) then Le (Add (Mult (Cst (~ cz), Var 0), bt), aa)
-      else Le (Add (Mult (Cst cz, Var (op_45_def0 ej id_1_def0 + 1)), bt), aa))
-  | mirror (Le (Add (Mult (Cst cz, Neg dt), bt), aa)) =
-    Le (Add (Mult (Cst cz, Neg dt), bt), aa)
-  | mirror (Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)) =
-    Le (Add (Mult (Cst cz, Add (du, dv)), bt), aa)
-  | mirror (Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)) =
-    Le (Add (Mult (Cst cz, Sub (dw, dx)), bt), aa)
-  | mirror (Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)) =
-    Le (Add (Mult (Cst cz, Mult (dy, dz)), bt), aa)
-  | mirror (Le (Add (Mult (Var da, cp), bt), aa)) =
-    Le (Add (Mult (Var da, cp), bt), aa)
-  | mirror (Le (Add (Mult (Neg db, cp), bt), aa)) =
-    Le (Add (Mult (Neg db, cp), bt), aa)
-  | mirror (Le (Add (Mult (Add (dc, dd), cp), bt), aa)) =
-    Le (Add (Mult (Add (dc, dd), cp), bt), aa)
-  | mirror (Le (Add (Mult (Sub (de, df), cp), bt), aa)) =
-    Le (Add (Mult (Sub (de, df), cp), bt), aa)
-  | mirror (Le (Add (Mult (Mult (dg, dh), cp), bt), aa)) =
-    Le (Add (Mult (Mult (dg, dh), cp), bt), aa)
-  | mirror (Le (Sub (bu, bv), aa)) = Le (Sub (bu, bv), aa)
-  | mirror (Le (Mult (bw, bx), aa)) = Le (Mult (bw, bx), aa)
-  | mirror (Ge (ab, ac)) = Ge (ab, ac)
-  | mirror (Eq (Cst el, ae)) = Eq (Cst el, ae)
-  | mirror (Eq (Var em, ae)) = Eq (Var em, ae)
-  | mirror (Eq (Neg en, ae)) = Eq (Neg en, ae)
-  | mirror (Eq (Add (Cst fd, ep), ae)) = Eq (Add (Cst fd, ep), ae)
-  | mirror (Eq (Add (Var fe, ep), ae)) = Eq (Add (Var fe, ep), ae)
-  | mirror (Eq (Add (Neg ff, ep), ae)) = Eq (Add (Neg ff, ep), ae)
-  | mirror (Eq (Add (Add (fg, fh), ep), ae)) = Eq (Add (Add (fg, fh), ep), ae)
-  | mirror (Eq (Add (Sub (fi, fj), ep), ae)) = Eq (Add (Sub (fi, fj), ep), ae)
-  | mirror (Eq (Add (Mult (Cst fv, Cst gn), ep), ae)) =
-    Eq (Add (Mult (Cst fv, Cst gn), ep), ae)
-  | mirror (Eq (Add (Mult (Cst fv, Var hf), ep), ae)) =
-    (if (hf = 0) then Eq (Add (Mult (Cst (~ fv), Var 0), ep), ae)
-      else Eq (Add (Mult (Cst fv, Var (op_45_def0 hf id_1_def0 + 1)), ep), ae))
-  | mirror (Eq (Add (Mult (Cst fv, Neg gp), ep), ae)) =
-    Eq (Add (Mult (Cst fv, Neg gp), ep), ae)
-  | mirror (Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)) =
-    Eq (Add (Mult (Cst fv, Add (gq, gr)), ep), ae)
-  | mirror (Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)) =
-    Eq (Add (Mult (Cst fv, Sub (gs, gt)), ep), ae)
-  | mirror (Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)) =
-    Eq (Add (Mult (Cst fv, Mult (gu, gv)), ep), ae)
-  | mirror (Eq (Add (Mult (Var fw, fl), ep), ae)) =
-    Eq (Add (Mult (Var fw, fl), ep), ae)
-  | mirror (Eq (Add (Mult (Neg fx, fl), ep), ae)) =
-    Eq (Add (Mult (Neg fx, fl), ep), ae)
-  | mirror (Eq (Add (Mult (Add (fy, fz), fl), ep), ae)) =
-    Eq (Add (Mult (Add (fy, fz), fl), ep), ae)
-  | mirror (Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)) =
-    Eq (Add (Mult (Sub (ga, gb), fl), ep), ae)
-  | mirror (Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)) =
-    Eq (Add (Mult (Mult (gc, gd), fl), ep), ae)
-  | mirror (Eq (Sub (eq, er), ae)) = Eq (Sub (eq, er), ae)
-  | mirror (Eq (Mult (es, et), ae)) = Eq (Mult (es, et), ae)
-  | mirror (Divides (Cst hh, Cst hz)) = Divides (Cst hh, Cst hz)
-  | mirror (Divides (Cst hh, Var ia)) = Divides (Cst hh, Var ia)
-  | mirror (Divides (Cst hh, Neg ib)) = Divides (Cst hh, Neg ib)
-  | mirror (Divides (Cst hh, Add (Cst ir, id))) =
-    Divides (Cst hh, Add (Cst ir, id))
-  | mirror (Divides (Cst hh, Add (Var is, id))) =
-    Divides (Cst hh, Add (Var is, id))
-  | mirror (Divides (Cst hh, Add (Neg it, id))) =
-    Divides (Cst hh, Add (Neg it, id))
-  | mirror (Divides (Cst hh, Add (Add (iu, iv), id))) =
-    Divides (Cst hh, Add (Add (iu, iv), id))
-  | mirror (Divides (Cst hh, Add (Sub (iw, ix), id))) =
-    Divides (Cst hh, Add (Sub (iw, ix), id))
-  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))) =
-    Divides (Cst hh, Add (Mult (Cst jj, Cst kb), id))
-  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Var kt), id))) =
-    (if (kt = 0) then Divides (Cst hh, Add (Mult (Cst (~ jj), Var 0), id))
-      else Divides
-             (Cst hh,
-               Add (Mult (Cst jj, Var (op_45_def0 kt id_1_def0 + 1)), id)))
-  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))) =
-    Divides (Cst hh, Add (Mult (Cst jj, Neg kd), id))
-  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))) =
-    Divides (Cst hh, Add (Mult (Cst jj, Add (ke, kf)), id))
-  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))) =
-    Divides (Cst hh, Add (Mult (Cst jj, Sub (kg, kh)), id))
-  | mirror (Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))) =
-    Divides (Cst hh, Add (Mult (Cst jj, Mult (ki, kj)), id))
-  | mirror (Divides (Cst hh, Add (Mult (Var jk, iz), id))) =
-    Divides (Cst hh, Add (Mult (Var jk, iz), id))
-  | mirror (Divides (Cst hh, Add (Mult (Neg jl, iz), id))) =
-    Divides (Cst hh, Add (Mult (Neg jl, iz), id))
-  | mirror (Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))) =
-    Divides (Cst hh, Add (Mult (Add (jm, jn), iz), id))
-  | mirror (Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))) =
-    Divides (Cst hh, Add (Mult (Sub (jo, jp), iz), id))
-  | mirror (Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))) =
-    Divides (Cst hh, Add (Mult (Mult (jq, jr), iz), id))
-  | mirror (Divides (Cst hh, Sub (ie, if'))) = Divides (Cst hh, Sub (ie, if'))
-  | mirror (Divides (Cst hh, Mult (ig, ih))) = Divides (Cst hh, Mult (ig, ih))
-  | mirror (Divides (Var hi, ag)) = Divides (Var hi, ag)
-  | mirror (Divides (Neg hj, ag)) = Divides (Neg hj, ag)
-  | mirror (Divides (Add (hk, hl), ag)) = Divides (Add (hk, hl), ag)
-  | mirror (Divides (Sub (hm, hn), ag)) = Divides (Sub (hm, hn), ag)
-  | mirror (Divides (Mult (ho, hp), ag)) = Divides (Mult (ho, hp), ag)
-  | mirror T = T
-  | mirror F = F
-  | mirror (NOT (Lt (kv, kw))) = NOT (Lt (kv, kw))
-  | mirror (NOT (Gt (kx, ky))) = NOT (Gt (kx, ky))
-  | mirror (NOT (Le (kz, la))) = NOT (Le (kz, la))
-  | mirror (NOT (Ge (lb, lc))) = NOT (Ge (lb, lc))
-  | mirror (NOT (Eq (Cst mp, le))) = NOT (Eq (Cst mp, le))
-  | mirror (NOT (Eq (Var mq, le))) = NOT (Eq (Var mq, le))
-  | mirror (NOT (Eq (Neg mr, le))) = NOT (Eq (Neg mr, le))
-  | mirror (NOT (Eq (Add (Cst nh, mt), le))) = NOT (Eq (Add (Cst nh, mt), le))
-  | mirror (NOT (Eq (Add (Var ni, mt), le))) = NOT (Eq (Add (Var ni, mt), le))
-  | mirror (NOT (Eq (Add (Neg nj, mt), le))) = NOT (Eq (Add (Neg nj, mt), le))
-  | mirror (NOT (Eq (Add (Add (nk, nl), mt), le))) =
-    NOT (Eq (Add (Add (nk, nl), mt), le))
-  | mirror (NOT (Eq (Add (Sub (nm, nn), mt), le))) =
-    NOT (Eq (Add (Sub (nm, nn), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))) =
-    NOT (Eq (Add (Mult (Cst nz, Cst or), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Cst nz, Var pj), mt), le))) =
-    (if (pj = 0) then NOT (Eq (Add (Mult (Cst (~ nz), Var 0), mt), le))
-      else NOT (Eq (Add (Mult (Cst nz, Var (op_45_def0 pj id_1_def0 + 1)), mt),
-                     le)))
-  | mirror (NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))) =
-    NOT (Eq (Add (Mult (Cst nz, Neg ot), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))) =
-    NOT (Eq (Add (Mult (Cst nz, Add (ou, ov)), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))) =
-    NOT (Eq (Add (Mult (Cst nz, Sub (ow, ox)), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))) =
-    NOT (Eq (Add (Mult (Cst nz, Mult (oy, oz)), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Var oa, np), mt), le))) =
-    NOT (Eq (Add (Mult (Var oa, np), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Neg ob, np), mt), le))) =
-    NOT (Eq (Add (Mult (Neg ob, np), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))) =
-    NOT (Eq (Add (Mult (Add (oc, od), np), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))) =
-    NOT (Eq (Add (Mult (Sub (oe, of'), np), mt), le))
-  | mirror (NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))) =
-    NOT (Eq (Add (Mult (Mult (og, oh), np), mt), le))
-  | mirror (NOT (Eq (Sub (mu, mv), le))) = NOT (Eq (Sub (mu, mv), le))
-  | mirror (NOT (Eq (Mult (mw, mx), le))) = NOT (Eq (Mult (mw, mx), le))
-  | mirror (NOT (Divides (Cst pl, Cst qd))) = NOT (Divides (Cst pl, Cst qd))
-  | mirror (NOT (Divides (Cst pl, Var qe))) = NOT (Divides (Cst pl, Var qe))
-  | mirror (NOT (Divides (Cst pl, Neg qf))) = NOT (Divides (Cst pl, Neg qf))
-  | mirror (NOT (Divides (Cst pl, Add (Cst qv, qh)))) =
-    NOT (Divides (Cst pl, Add (Cst qv, qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Var qw, qh)))) =
-    NOT (Divides (Cst pl, Add (Var qw, qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Neg qx, qh)))) =
-    NOT (Divides (Cst pl, Add (Neg qx, qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))) =
-    NOT (Divides (Cst pl, Add (Add (qy, qz), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))) =
-    NOT (Divides (Cst pl, Add (Sub (ra, rb), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Cst rn, Cst sf), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Var sx), qh)))) =
-    (if (sx = 0)
-      then NOT (Divides (Cst pl, Add (Mult (Cst (~ rn), Var 0), qh)))
-      else NOT (Divides
-                  (Cst pl,
-                    Add (Mult (Cst rn, Var (op_45_def0 sx id_1_def0 + 1)),
-                          qh))))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Cst rn, Neg sh), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Cst rn, Add (si, sj)), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Cst rn, Sub (sk, sl)), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Cst rn, Mult (sm, sn)), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Var ro, rd), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Neg rp, rd), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Add (rq, rr), rd), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Sub (rs, rt), rd), qh)))
-  | mirror (NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))) =
-    NOT (Divides (Cst pl, Add (Mult (Mult (ru, rv), rd), qh)))
-  | mirror (NOT (Divides (Cst pl, Sub (qi, qj)))) =
-    NOT (Divides (Cst pl, Sub (qi, qj)))
-  | mirror (NOT (Divides (Cst pl, Mult (qk, ql)))) =
-    NOT (Divides (Cst pl, Mult (qk, ql)))
-  | mirror (NOT (Divides (Var pm, lg))) = NOT (Divides (Var pm, lg))
-  | mirror (NOT (Divides (Neg pn, lg))) = NOT (Divides (Neg pn, lg))
-  | mirror (NOT (Divides (Add (po, pp), lg))) = NOT (Divides (Add (po, pp), lg))
-  | mirror (NOT (Divides (Sub (pq, pr), lg))) = NOT (Divides (Sub (pq, pr), lg))
-  | mirror (NOT (Divides (Mult (ps, pt), lg))) =
-    NOT (Divides (Mult (ps, pt), lg))
-  | mirror (NOT T) = NOT T
-  | mirror (NOT F) = NOT F
-  | mirror (NOT (NOT lh)) = NOT (NOT lh)
-  | mirror (NOT (And (li, lj))) = NOT (And (li, lj))
-  | mirror (NOT (Or (lk, ll))) = NOT (Or (lk, ll))
-  | mirror (NOT (Imp (lm, ln))) = NOT (Imp (lm, ln))
-  | mirror (NOT (Equ (lo, lp))) = NOT (Equ (lo, lp))
-  | mirror (NOT (QAll lq)) = NOT (QAll lq)
-  | mirror (NOT (QEx lr)) = NOT (QEx lr)
-  | mirror (Imp (am, an)) = Imp (am, an)
-  | mirror (Equ (ao, ap)) = Equ (ao, ap)
-  | mirror (QAll aq) = QAll aq
-  | mirror (QEx ar) = QEx ar;
-
-fun op_43_def0 m n = nat ((m) + (n));
-
-fun size_def1 [] = (0:IntInf.int)
-  | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
-
-fun aset (And (p, q)) = op_64 (aset p) (aset q)
-  | aset (Or (p, q)) = op_64 (aset p) (aset q)
-  | aset (Lt (u, v)) = []
-  | aset (Gt (w, x)) = []
-  | aset (Le (Cst bo, z)) = []
-  | aset (Le (Var bp, z)) = []
-  | aset (Le (Neg bq, z)) = []
-  | aset (Le (Add (Cst cg, bs), z)) = []
-  | aset (Le (Add (Var ch, bs), z)) = []
-  | aset (Le (Add (Neg ci, bs), z)) = []
-  | aset (Le (Add (Add (cj, ck), bs), z)) = []
-  | aset (Le (Add (Sub (cl, cm), bs), z)) = []
-  | aset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
-  | aset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
-    (if (ei = 0)
-      then (if (cy < 0) then [lin_add (bs, Cst 1)]
-             else [lin_neg bs, lin_add (lin_neg bs, Cst 1)])
-      else [])
-  | aset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = []
-  | aset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = []
-  | aset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = []
-  | aset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = []
-  | aset (Le (Add (Mult (Var cz, co), bs), z)) = []
-  | aset (Le (Add (Mult (Neg da, co), bs), z)) = []
-  | aset (Le (Add (Mult (Add (db, dc), co), bs), z)) = []
-  | aset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = []
-  | aset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = []
-  | aset (Le (Sub (bt, bu), z)) = []
-  | aset (Le (Mult (bv, bw), z)) = []
-  | aset (Ge (aa, ab)) = []
-  | aset (Eq (Cst ek, ad)) = []
-  | aset (Eq (Var el, ad)) = []
-  | aset (Eq (Neg em, ad)) = []
-  | aset (Eq (Add (Cst fc, eo), ad)) = []
-  | aset (Eq (Add (Var fd, eo), ad)) = []
-  | aset (Eq (Add (Neg fe, eo), ad)) = []
-  | aset (Eq (Add (Add (ff, fg), eo), ad)) = []
-  | aset (Eq (Add (Sub (fh, fi), eo), ad)) = []
-  | aset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = []
-  | aset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
-    (if (he = 0)
-      then (if (fu < 0) then [lin_add (eo, Cst 1)]
-             else [lin_add (lin_neg eo, Cst 1)])
-      else [])
-  | aset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = []
-  | aset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = []
-  | aset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = []
-  | aset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = []
-  | aset (Eq (Add (Mult (Var fv, fk), eo), ad)) = []
-  | aset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = []
-  | aset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = []
-  | aset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = []
-  | aset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = []
-  | aset (Eq (Sub (ep, eq), ad)) = []
-  | aset (Eq (Mult (er, es), ad)) = []
-  | aset (Divides (ae, af)) = []
-  | aset T = []
-  | aset F = []
-  | aset (NOT (Lt (hg, hh))) = []
-  | aset (NOT (Gt (hi, hj))) = []
-  | aset (NOT (Le (hk, hl))) = []
-  | aset (NOT (Ge (hm, hn))) = []
-  | aset (NOT (Eq (Cst ja, hp))) = []
-  | aset (NOT (Eq (Var jb, hp))) = []
-  | aset (NOT (Eq (Neg jc, hp))) = []
-  | aset (NOT (Eq (Add (Cst js, je), hp))) = []
-  | aset (NOT (Eq (Add (Var jt, je), hp))) = []
-  | aset (NOT (Eq (Add (Neg ju, je), hp))) = []
-  | aset (NOT (Eq (Add (Add (jv, jw), je), hp))) = []
-  | aset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
-    (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else [])
-  | aset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = []
-  | aset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = []
-  | aset (NOT (Eq (Sub (jf, jg), hp))) = []
-  | aset (NOT (Eq (Mult (jh, ji), hp))) = []
-  | aset (NOT (Divides (hq, hr))) = []
-  | aset (NOT T) = []
-  | aset (NOT F) = []
-  | aset (NOT (NOT hs)) = []
-  | aset (NOT (And (ht, hu))) = []
-  | aset (NOT (Or (hv, hw))) = []
-  | aset (NOT (Imp (hx, hy))) = []
-  | aset (NOT (Equ (hz, ia))) = []
-  | aset (NOT (QAll ib)) = []
-  | aset (NOT (QEx ic)) = []
-  | aset (Imp (al, am)) = []
-  | aset (Equ (an, ao)) = []
-  | aset (QAll ap) = []
-  | aset (QEx aq) = [];
-
-fun op_mem x [] = false
-  | op_mem x (y :: ys) = (if (y = x) then true else op_mem x ys);
-
-fun list_insert x xs = (if op_mem x xs then xs else (x :: xs));
-
-fun list_set [] = []
-  | list_set (x :: xs) = list_insert x (list_set xs);
-
-fun bset (And (p, q)) = op_64 (bset p) (bset q)
-  | bset (Or (p, q)) = op_64 (bset p) (bset q)
-  | bset (Lt (u, v)) = []
-  | bset (Gt (w, x)) = []
-  | bset (Le (Cst bo, z)) = []
-  | bset (Le (Var bp, z)) = []
-  | bset (Le (Neg bq, z)) = []
-  | bset (Le (Add (Cst cg, bs), z)) = []
-  | bset (Le (Add (Var ch, bs), z)) = []
-  | bset (Le (Add (Neg ci, bs), z)) = []
-  | bset (Le (Add (Add (cj, ck), bs), z)) = []
-  | bset (Le (Add (Sub (cl, cm), bs), z)) = []
-  | bset (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = []
-  | bset (Le (Add (Mult (Cst cy, Var ei), bs), z)) =
-    (if (ei = 0)
-      then (if (cy < 0) then [lin_add (bs, Cst ~1), bs]
-             else [lin_add (lin_neg bs, Cst ~1)])
-      else [])
-  | bset (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = []
-  | bset (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = []
-  | bset (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = []
-  | bset (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = []
-  | bset (Le (Add (Mult (Var cz, co), bs), z)) = []
-  | bset (Le (Add (Mult (Neg da, co), bs), z)) = []
-  | bset (Le (Add (Mult (Add (db, dc), co), bs), z)) = []
-  | bset (Le (Add (Mult (Sub (dd, de), co), bs), z)) = []
-  | bset (Le (Add (Mult (Mult (df, dg), co), bs), z)) = []
-  | bset (Le (Sub (bt, bu), z)) = []
-  | bset (Le (Mult (bv, bw), z)) = []
-  | bset (Ge (aa, ab)) = []
-  | bset (Eq (Cst ek, ad)) = []
-  | bset (Eq (Var el, ad)) = []
-  | bset (Eq (Neg em, ad)) = []
-  | bset (Eq (Add (Cst fc, eo), ad)) = []
-  | bset (Eq (Add (Var fd, eo), ad)) = []
-  | bset (Eq (Add (Neg fe, eo), ad)) = []
-  | bset (Eq (Add (Add (ff, fg), eo), ad)) = []
-  | bset (Eq (Add (Sub (fh, fi), eo), ad)) = []
-  | bset (Eq (Add (Mult (Cst fu, Cst gm), eo), ad)) = []
-  | bset (Eq (Add (Mult (Cst fu, Var he), eo), ad)) =
-    (if (he = 0)
-      then (if (fu < 0) then [lin_add (eo, Cst ~1)]
-             else [lin_add (lin_neg eo, Cst ~1)])
-      else [])
-  | bset (Eq (Add (Mult (Cst fu, Neg go), eo), ad)) = []
-  | bset (Eq (Add (Mult (Cst fu, Add (gp, gq)), eo), ad)) = []
-  | bset (Eq (Add (Mult (Cst fu, Sub (gr, gs)), eo), ad)) = []
-  | bset (Eq (Add (Mult (Cst fu, Mult (gt, gu)), eo), ad)) = []
-  | bset (Eq (Add (Mult (Var fv, fk), eo), ad)) = []
-  | bset (Eq (Add (Mult (Neg fw, fk), eo), ad)) = []
-  | bset (Eq (Add (Mult (Add (fx, fy), fk), eo), ad)) = []
-  | bset (Eq (Add (Mult (Sub (fz, ga), fk), eo), ad)) = []
-  | bset (Eq (Add (Mult (Mult (gb, gc), fk), eo), ad)) = []
-  | bset (Eq (Sub (ep, eq), ad)) = []
-  | bset (Eq (Mult (er, es), ad)) = []
-  | bset (Divides (ae, af)) = []
-  | bset T = []
-  | bset F = []
-  | bset (NOT (Lt (hg, hh))) = []
-  | bset (NOT (Gt (hi, hj))) = []
-  | bset (NOT (Le (hk, hl))) = []
-  | bset (NOT (Ge (hm, hn))) = []
-  | bset (NOT (Eq (Cst ja, hp))) = []
-  | bset (NOT (Eq (Var jb, hp))) = []
-  | bset (NOT (Eq (Neg jc, hp))) = []
-  | bset (NOT (Eq (Add (Cst js, je), hp))) = []
-  | bset (NOT (Eq (Add (Var jt, je), hp))) = []
-  | bset (NOT (Eq (Add (Neg ju, je), hp))) = []
-  | bset (NOT (Eq (Add (Add (jv, jw), je), hp))) = []
-  | bset (NOT (Eq (Add (Sub (jx, jy), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Cst kk, Cst lc), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Cst kk, Var lu), je), hp))) =
-    (if (lu = 0) then (if (kk < 0) then [je] else [lin_neg je]) else [])
-  | bset (NOT (Eq (Add (Mult (Cst kk, Neg le), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Cst kk, Add (lf, lg)), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Cst kk, Sub (lh, li)), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Cst kk, Mult (lj, lk)), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Var kl, ka), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Neg km, ka), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Add (kn, ko), ka), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Sub (kp, kq), ka), je), hp))) = []
-  | bset (NOT (Eq (Add (Mult (Mult (kr, ks), ka), je), hp))) = []
-  | bset (NOT (Eq (Sub (jf, jg), hp))) = []
-  | bset (NOT (Eq (Mult (jh, ji), hp))) = []
-  | bset (NOT (Divides (hq, hr))) = []
-  | bset (NOT T) = []
-  | bset (NOT F) = []
-  | bset (NOT (NOT hs)) = []
-  | bset (NOT (And (ht, hu))) = []
-  | bset (NOT (Or (hv, hw))) = []
-  | bset (NOT (Imp (hx, hy))) = []
-  | bset (NOT (Equ (hz, ia))) = []
-  | bset (NOT (QAll ib)) = []
-  | bset (NOT (QEx ic)) = []
-  | bset (Imp (al, am)) = []
-  | bset (Equ (an, ao)) = []
-  | bset (QAll ap) = []
-  | bset (QEx aq) = [];
-
-fun adjustcoeff (l:IntInf.int, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
-    (if (c <= 0)
-      then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)),
-                Cst 0)
-      else Le (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0))
-  | adjustcoeff (l, Eq (Add (Mult (Cst c, Var 0), r), Cst i)) =
-    Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0)
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst c, Var 0), r), Cst i))) =
-    NOT (Eq (Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l c, r)), Cst 0))
-  | adjustcoeff (l, And (p, q)) = And (adjustcoeff (l, p), adjustcoeff (l, q))
-  | adjustcoeff (l, Or (p, q)) = Or (adjustcoeff (l, p), adjustcoeff (l, q))
-  | adjustcoeff (l, Lt (w, x)) = Lt (w, x)
-  | adjustcoeff (l, Gt (y, z)) = Gt (y, z)
-  | adjustcoeff (l, Le (Cst bq, ab)) = Le (Cst bq, ab)
-  | adjustcoeff (l, Le (Var br, ab)) = Le (Var br, ab)
-  | adjustcoeff (l, Le (Neg bs, ab)) = Le (Neg bs, ab)
-  | adjustcoeff (l, Le (Add (Cst ci, bu), ab)) = Le (Add (Cst ci, bu), ab)
-  | adjustcoeff (l, Le (Add (Var cj, bu), ab)) = Le (Add (Var cj, bu), ab)
-  | adjustcoeff (l, Le (Add (Neg ck, bu), ab)) = Le (Add (Neg ck, bu), ab)
-  | adjustcoeff (l, Le (Add (Add (cl, cm), bu), ab)) =
-    Le (Add (Add (cl, cm), bu), ab)
-  | adjustcoeff (l, Le (Add (Sub (cn, co), bu), ab)) =
-    Le (Add (Sub (cn, co), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Cst ds), bu), ab)) =
-    Le (Add (Mult (Cst da, Cst ds), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Var en)) =
-    Le (Add (Mult (Cst da, Var 0), bu), Var en)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Neg eo)) =
-    Le (Add (Mult (Cst da, Var 0), bu), Neg eo)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq))) =
-    Le (Add (Mult (Cst da, Var 0), bu), Add (ep, eq))
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es))) =
-    Le (Add (Mult (Cst da, Var 0), bu), Sub (er, es))
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu))) =
-    Le (Add (Mult (Cst da, Var 0), bu), Mult (et, eu))
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Var ek), bu), ab)) =
-    Le (Add (Mult (Cst da, Var ek), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Neg du), bu), ab)) =
-    Le (Add (Mult (Cst da, Neg du), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab)) =
-    Le (Add (Mult (Cst da, Add (dv, dw)), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab)) =
-    Le (Add (Mult (Cst da, Sub (dx, dy)), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab)) =
-    Le (Add (Mult (Cst da, Mult (dz, ea)), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Var db, cq), bu), ab)) =
-    Le (Add (Mult (Var db, cq), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Neg dc, cq), bu), ab)) =
-    Le (Add (Mult (Neg dc, cq), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Add (dd, de), cq), bu), ab)) =
-    Le (Add (Mult (Add (dd, de), cq), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Sub (df, dg), cq), bu), ab)) =
-    Le (Add (Mult (Sub (df, dg), cq), bu), ab)
-  | adjustcoeff (l, Le (Add (Mult (Mult (dh, di), cq), bu), ab)) =
-    Le (Add (Mult (Mult (dh, di), cq), bu), ab)
-  | adjustcoeff (l, Le (Sub (bv, bw), ab)) = Le (Sub (bv, bw), ab)
-  | adjustcoeff (l, Le (Mult (bx, by), ab)) = Le (Mult (bx, by), ab)
-  | adjustcoeff (l, Ge (ac, ad)) = Ge (ac, ad)
-  | adjustcoeff (l, Eq (Cst fe, af)) = Eq (Cst fe, af)
-  | adjustcoeff (l, Eq (Var ff, af)) = Eq (Var ff, af)
-  | adjustcoeff (l, Eq (Neg fg, af)) = Eq (Neg fg, af)
-  | adjustcoeff (l, Eq (Add (Cst fw, fi), af)) = Eq (Add (Cst fw, fi), af)
-  | adjustcoeff (l, Eq (Add (Var fx, fi), af)) = Eq (Add (Var fx, fi), af)
-  | adjustcoeff (l, Eq (Add (Neg fy, fi), af)) = Eq (Add (Neg fy, fi), af)
-  | adjustcoeff (l, Eq (Add (Add (fz, ga), fi), af)) =
-    Eq (Add (Add (fz, ga), fi), af)
-  | adjustcoeff (l, Eq (Add (Sub (gb, gc), fi), af)) =
-    Eq (Add (Sub (gb, gc), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Cst hg), fi), af)) =
-    Eq (Add (Mult (Cst go, Cst hg), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Var ib)) =
-    Eq (Add (Mult (Cst go, Var 0), fi), Var ib)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Neg ic)) =
-    Eq (Add (Mult (Cst go, Var 0), fi), Neg ic)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie))) =
-    Eq (Add (Mult (Cst go, Var 0), fi), Add (id, ie))
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig))) =
-    Eq (Add (Mult (Cst go, Var 0), fi), Sub (if', ig))
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii))) =
-    Eq (Add (Mult (Cst go, Var 0), fi), Mult (ih, ii))
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Var hy), fi), af)) =
-    Eq (Add (Mult (Cst go, Var hy), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Neg hi), fi), af)) =
-    Eq (Add (Mult (Cst go, Neg hi), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af)) =
-    Eq (Add (Mult (Cst go, Add (hj, hk)), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af)) =
-    Eq (Add (Mult (Cst go, Sub (hl, hm)), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af)) =
-    Eq (Add (Mult (Cst go, Mult (hn, ho)), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Var gp, ge), fi), af)) =
-    Eq (Add (Mult (Var gp, ge), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Neg gq, ge), fi), af)) =
-    Eq (Add (Mult (Neg gq, ge), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Add (gr, gs), ge), fi), af)) =
-    Eq (Add (Mult (Add (gr, gs), ge), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Sub (gt, gu), ge), fi), af)) =
-    Eq (Add (Mult (Sub (gt, gu), ge), fi), af)
-  | adjustcoeff (l, Eq (Add (Mult (Mult (gv, gw), ge), fi), af)) =
-    Eq (Add (Mult (Mult (gv, gw), ge), fi), af)
-  | adjustcoeff (l, Eq (Sub (fj, fk), af)) = Eq (Sub (fj, fk), af)
-  | adjustcoeff (l, Eq (Mult (fl, fm), af)) = Eq (Mult (fl, fm), af)
-  | adjustcoeff (l, Divides (Cst is, Cst jk)) = Divides (Cst is, Cst jk)
-  | adjustcoeff (l, Divides (Cst is, Var jl)) = Divides (Cst is, Var jl)
-  | adjustcoeff (l, Divides (Cst is, Neg jm)) = Divides (Cst is, Neg jm)
-  | adjustcoeff (l, Divides (Cst is, Add (Cst kc, jo))) =
-    Divides (Cst is, Add (Cst kc, jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Var kd, jo))) =
-    Divides (Cst is, Add (Var kd, jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Neg ke, jo))) =
-    Divides (Cst is, Add (Neg ke, jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Add (kf, kg), jo))) =
-    Divides (Cst is, Add (Add (kf, kg), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Sub (kh, ki), jo))) =
-    Divides (Cst is, Add (Sub (kh, ki), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo))) =
-    Divides (Cst is, Add (Mult (Cst ku, Cst lm), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Var me), jo))) =
-    (if (me = 0)
-      then Divides
-             (Cst (op_div_def1 l ku * is),
-               Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l ku, jo)))
-      else Divides
-             (Cst is,
-               Add (Mult (Cst ku, Var (op_45_def0 me id_1_def0 + 1)), jo)))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo))) =
-    Divides (Cst is, Add (Mult (Cst ku, Neg lo), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo))) =
-    Divides (Cst is, Add (Mult (Cst ku, Add (lp, lq)), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo))) =
-    Divides (Cst is, Add (Mult (Cst ku, Sub (lr, ls)), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo))) =
-    Divides (Cst is, Add (Mult (Cst ku, Mult (lt, lu)), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Var kv, kk), jo))) =
-    Divides (Cst is, Add (Mult (Var kv, kk), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Neg kw, kk), jo))) =
-    Divides (Cst is, Add (Mult (Neg kw, kk), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo))) =
-    Divides (Cst is, Add (Mult (Add (kx, ky), kk), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo))) =
-    Divides (Cst is, Add (Mult (Sub (kz, la), kk), jo))
-  | adjustcoeff (l, Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo))) =
-    Divides (Cst is, Add (Mult (Mult (lb, lc), kk), jo))
-  | adjustcoeff (l, Divides (Cst is, Sub (jp, jq))) =
-    Divides (Cst is, Sub (jp, jq))
-  | adjustcoeff (l, Divides (Cst is, Mult (jr, js))) =
-    Divides (Cst is, Mult (jr, js))
-  | adjustcoeff (l, Divides (Var it, ah)) = Divides (Var it, ah)
-  | adjustcoeff (l, Divides (Neg iu, ah)) = Divides (Neg iu, ah)
-  | adjustcoeff (l, Divides (Add (iv, iw), ah)) = Divides (Add (iv, iw), ah)
-  | adjustcoeff (l, Divides (Sub (ix, iy), ah)) = Divides (Sub (ix, iy), ah)
-  | adjustcoeff (l, Divides (Mult (iz, ja), ah)) = Divides (Mult (iz, ja), ah)
-  | adjustcoeff (l, T) = T
-  | adjustcoeff (l, F) = F
-  | adjustcoeff (l, NOT (Lt (mg, mh))) = NOT (Lt (mg, mh))
-  | adjustcoeff (l, NOT (Gt (mi, mj))) = NOT (Gt (mi, mj))
-  | adjustcoeff (l, NOT (Le (mk, ml))) = NOT (Le (mk, ml))
-  | adjustcoeff (l, NOT (Ge (mm, mn))) = NOT (Ge (mm, mn))
-  | adjustcoeff (l, NOT (Eq (Cst oa, mp))) = NOT (Eq (Cst oa, mp))
-  | adjustcoeff (l, NOT (Eq (Var ob, mp))) = NOT (Eq (Var ob, mp))
-  | adjustcoeff (l, NOT (Eq (Neg oc, mp))) = NOT (Eq (Neg oc, mp))
-  | adjustcoeff (l, NOT (Eq (Add (Cst os, oe), mp))) =
-    NOT (Eq (Add (Cst os, oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Var ot, oe), mp))) =
-    NOT (Eq (Add (Var ot, oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Neg ou, oe), mp))) =
-    NOT (Eq (Add (Neg ou, oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Add (ov, ow), oe), mp))) =
-    NOT (Eq (Add (Add (ov, ow), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Sub (ox, oy), oe), mp))) =
-    NOT (Eq (Add (Sub (ox, oy), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp))) =
-    NOT (Eq (Add (Mult (Cst pk, Cst qc), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx))) =
-    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Var qx))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy))) =
-    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Neg qy))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra)))) =
-    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Add (qz, ra)))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc)))) =
-    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Sub (rb, rc)))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re)))) =
-    NOT (Eq (Add (Mult (Cst pk, Var 0), oe), Mult (rd, re)))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp))) =
-    NOT (Eq (Add (Mult (Cst pk, Var qu), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp))) =
-    NOT (Eq (Add (Mult (Cst pk, Neg qe), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp))) =
-    NOT (Eq (Add (Mult (Cst pk, Add (qf, qg)), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp))) =
-    NOT (Eq (Add (Mult (Cst pk, Sub (qh, qi)), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp))) =
-    NOT (Eq (Add (Mult (Cst pk, Mult (qj, qk)), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Var pl, pa), oe), mp))) =
-    NOT (Eq (Add (Mult (Var pl, pa), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Neg pm, pa), oe), mp))) =
-    NOT (Eq (Add (Mult (Neg pm, pa), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp))) =
-    NOT (Eq (Add (Mult (Add (pn, po), pa), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp))) =
-    NOT (Eq (Add (Mult (Sub (pp, pq), pa), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp))) =
-    NOT (Eq (Add (Mult (Mult (pr, ps), pa), oe), mp))
-  | adjustcoeff (l, NOT (Eq (Sub (of', og), mp))) = NOT (Eq (Sub (of', og), mp))
-  | adjustcoeff (l, NOT (Eq (Mult (oh, oi), mp))) = NOT (Eq (Mult (oh, oi), mp))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Cst sg))) =
-    NOT (Divides (Cst ro, Cst sg))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Var sh))) =
-    NOT (Divides (Cst ro, Var sh))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Neg si))) =
-    NOT (Divides (Cst ro, Neg si))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Cst sy, sk)))) =
-    NOT (Divides (Cst ro, Add (Cst sy, sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Var sz, sk)))) =
-    NOT (Divides (Cst ro, Add (Var sz, sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Neg ta, sk)))) =
-    NOT (Divides (Cst ro, Add (Neg ta, sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Add (tb, tc), sk)))) =
-    NOT (Divides (Cst ro, Add (Add (tb, tc), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Sub (td, te), sk)))) =
-    NOT (Divides (Cst ro, Add (Sub (td, te), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Cst tq, Cst ui), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Var va), sk)))) =
-    (if (va = 0)
-      then NOT (Divides
-                  (Cst (op_div_def1 l tq * ro),
-                    Add (Mult (Cst 1, Var 0), lin_mul (op_div_def1 l tq, sk))))
-      else NOT (Divides
-                  (Cst ro,
-                    Add (Mult (Cst tq, Var (op_45_def0 va id_1_def0 + 1)),
-                          sk))))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Cst tq, Neg uk), sk)))
-  | adjustcoeff
-      (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Cst tq, Add (ul, um)), sk)))
-  | adjustcoeff
-      (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Cst tq, Sub (un, uo)), sk)))
-  | adjustcoeff
-      (l, NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Cst tq, Mult (up, uq)), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Var tr, tg), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Neg ts, tg), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Add (tt, tu), tg), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Sub (tv, tw), tg), sk)))
-  | adjustcoeff
-      (l, NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk)))) =
-    NOT (Divides (Cst ro, Add (Mult (Mult (tx, ty), tg), sk)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Sub (sl, sm)))) =
-    NOT (Divides (Cst ro, Sub (sl, sm)))
-  | adjustcoeff (l, NOT (Divides (Cst ro, Mult (sn, so)))) =
-    NOT (Divides (Cst ro, Mult (sn, so)))
-  | adjustcoeff (l, NOT (Divides (Var rp, mr))) = NOT (Divides (Var rp, mr))
-  | adjustcoeff (l, NOT (Divides (Neg rq, mr))) = NOT (Divides (Neg rq, mr))
-  | adjustcoeff (l, NOT (Divides (Add (rr, rs), mr))) =
-    NOT (Divides (Add (rr, rs), mr))
-  | adjustcoeff (l, NOT (Divides (Sub (rt, ru), mr))) =
-    NOT (Divides (Sub (rt, ru), mr))
-  | adjustcoeff (l, NOT (Divides (Mult (rv, rw), mr))) =
-    NOT (Divides (Mult (rv, rw), mr))
-  | adjustcoeff (l, NOT T) = NOT T
-  | adjustcoeff (l, NOT F) = NOT F
-  | adjustcoeff (l, NOT (NOT ms)) = NOT (NOT ms)
-  | adjustcoeff (l, NOT (And (mt, mu))) = NOT (And (mt, mu))
-  | adjustcoeff (l, NOT (Or (mv, mw))) = NOT (Or (mv, mw))
-  | adjustcoeff (l, NOT (Imp (mx, my))) = NOT (Imp (mx, my))
-  | adjustcoeff (l, NOT (Equ (mz, na))) = NOT (Equ (mz, na))
-  | adjustcoeff (l, NOT (QAll nb)) = NOT (QAll nb)
-  | adjustcoeff (l, NOT (QEx nc)) = NOT (QEx nc)
-  | adjustcoeff (l, Imp (an, ao)) = Imp (an, ao)
-  | adjustcoeff (l, Equ (ap, aq)) = Equ (ap, aq)
-  | adjustcoeff (l, QAll ar) = QAll ar
-  | adjustcoeff (l, QEx as') = QEx as';
-
-fun formlcm (Le (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c
-  | formlcm (Eq (Add (Mult (Cst c, Var 0), r), Cst i)) = abs c
-  | formlcm (NOT p) = formlcm p
-  | formlcm (And (p, q)) = ilcm (formlcm p) (formlcm q)
-  | formlcm (Or (p, q)) = ilcm (formlcm p) (formlcm q)
-  | formlcm (Lt (u, v)) = 1
-  | formlcm (Gt (w, x)) = 1
-  | formlcm (Le (Cst bo, z)) = 1
-  | formlcm (Le (Var bp, z)) = 1
-  | formlcm (Le (Neg bq, z)) = 1
-  | formlcm (Le (Add (Cst cg, bs), z)) = 1
-  | formlcm (Le (Add (Var ch, bs), z)) = 1
-  | formlcm (Le (Add (Neg ci, bs), z)) = 1
-  | formlcm (Le (Add (Add (cj, ck), bs), z)) = 1
-  | formlcm (Le (Add (Sub (cl, cm), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Cst dq), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Var el)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Neg em)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Add (en, eo))) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Sub (ep, eq))) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Var 0), bs), Mult (er, es))) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Var ei ), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Neg ds), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Add (dt, du)), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Sub (dv, dw)), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Cst cy, Mult (dx, dy)), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Var cz, co), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Neg da, co), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Add (db, dc), co), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Sub (dd, de), co), bs), z)) = 1
-  | formlcm (Le (Add (Mult (Mult (df, dg), co), bs), z)) = 1
-  | formlcm (Le (Sub (bt, bu), z)) = 1
-  | formlcm (Le (Mult (bv, bw), z)) = 1
-  | formlcm (Ge (aa, ab)) = 1
-  | formlcm (Eq (Cst fc, ad)) = 1
-  | formlcm (Eq (Var fd, ad)) = 1
-  | formlcm (Eq (Neg fe, ad)) = 1
-  | formlcm (Eq (Add (Cst fu, fg), ad)) = 1
-  | formlcm (Eq (Add (Var fv, fg), ad)) = 1
-  | formlcm (Eq (Add (Neg fw, fg), ad)) = 1
-  | formlcm (Eq (Add (Add (fx, fy), fg), ad)) = 1
-  | formlcm (Eq (Add (Sub (fz, ga), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Cst he), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Var hz)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Neg ia)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Add (ib, ic))) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Sub (id, ie))) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Var 0), fg), Mult (if', ig))) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Var hw), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Neg hg), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Add (hh, hi)), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Sub (hj, hk)), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Cst gm, Mult (hl, hm)), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Var gn, gc), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Neg go, gc), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Add (gp, gq), gc), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Sub (gr, gs), gc), fg), ad)) = 1
-  | formlcm (Eq (Add (Mult (Mult (gt, gu), gc), fg), ad)) = 1
-  | formlcm (Eq (Sub (fh, fi), ad)) = 1
-  | formlcm (Eq (Mult (fj, fk), ad)) = 1
-  | formlcm (Divides (Cst iq, Cst ji)) = 1
-  | formlcm (Divides (Cst iq, Var jj)) = 1
-  | formlcm (Divides (Cst iq, Neg jk)) = 1
-  | formlcm (Divides (Cst iq, Add (Cst ka, jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Var kb, jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Neg kc, jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Add (kd, ke), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Sub (kf, kg), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Cst lk), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Var mc), jm))) =
-    (if (mc = 0) then abs ks else 1)
-  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Neg lm), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Add (ln, lo)), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Sub (lp, lq)), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Cst ks, Mult (lr, ls)), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Var kt, ki), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Neg ku, ki), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Add (kv, kw), ki), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Sub (kx, ky), ki), jm))) = 1
-  | formlcm (Divides (Cst iq, Add (Mult (Mult (kz, la), ki), jm))) = 1
-  | formlcm (Divides (Cst iq, Sub (jn, jo))) = 1
-  | formlcm (Divides (Cst iq, Mult (jp, jq))) = 1
-  | formlcm (Divides (Var ir, af)) = 1
-  | formlcm (Divides (Neg is, af)) = 1
-  | formlcm (Divides (Add (it, iu), af)) = 1
-  | formlcm (Divides (Sub (iv, iw), af)) = 1
-  | formlcm (Divides (Mult (ix, iy), af)) = 1
-  | formlcm T = 1
-  | formlcm F = 1
-  | formlcm (Imp (al, am)) = 1
-  | formlcm (Equ (an, ao)) = 1
-  | formlcm (QAll ap) = 1
-  | formlcm (QEx aq) = 1;
-
-fun unitycoeff p =
-  let val l = formlcm p; val p' = adjustcoeff (l, p)
-  in (if (l = 1) then p'
-       else And (Divides (Cst l, Add (Mult (Cst 1, Var 0), Cst 0)), p'))
-  end;
-
-fun unify p =
-  let val q = unitycoeff p; val B = list_set (bset q); val A = list_set (aset q)
-  in (if op_60_61_def0 (size_def1 B) (size_def1 A) then (q, B)
-       else (mirror q, map lin_neg A))
-  end;
-
-fun cooper p =
-  lift_un (fn q => decrvars (explode_minf (unify q))) (linform (nnf p));
-
-fun pa p = lift_un psimpl (qelim (cooper, p));
-
-val test = pa;
-
-end;