# HG changeset patch
# User haftmann
# Date 1234807895 -3600
# Node ID 2138ff0ec94a86119e4fa55349558b8629b0c39b
# Parent  a0e54cf21fd499ff9e65bdf7d99871dbee547522
re-generated

diff -r a0e54cf21fd4 -r 2138ff0ec94a src/HOL/Tools/Qelim/generated_cooper.ML
--- a/src/HOL/Tools/Qelim/generated_cooper.ML	Mon Feb 16 19:11:16 2009 +0100
+++ b/src/HOL/Tools/Qelim/generated_cooper.ML	Mon Feb 16 19:11:35 2009 +0100
@@ -15,13 +15,13 @@
 
 fun divmod n m = (if eqop eq_nat m 0 then (0, n) else IntInf.divMod (n, m));
 
-fun snd (a, y) = y;
+fun snd (a, b) = b;
 
 fun mod_nat m n = snd (divmod m n);
 
 fun gcd m n = (if eqop eq_nat n 0 then m else gcd n (mod_nat m n));
 
-fun fst (y, b) = y;
+fun fst (a, b) = a;
 
 fun div_nat m n = fst (divmod m n);
 
@@ -48,7 +48,7 @@
 fun map f [] = []
   | map f (x :: xs) = f x :: map f xs;
 
-fun append [] y = y
+fun append [] ys = ys
   | append (x :: xs) ys = x :: append xs ys;
 
 fun disjuncts (Or (p, q)) = append (disjuncts p) (disjuncts q)
@@ -105,53 +105,53 @@
     (Le num) = f4 num
   | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19
     (Lt num) = f3 num
-  | fm_case f1 y f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
-    = y
-  | fm_case y f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
-    = y;
+  | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
+    = f2
+  | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
+    = f1;
 
-fun eq_num (Mul (cb, dc)) (Sub (ae, be)) = false
-  | eq_num (Mul (cb, dc)) (Add (ae, be)) = false
-  | eq_num (Sub (cc, dc)) (Add (ae, be)) = false
-  | eq_num (Mul (bd, cc)) (Neg ae) = false
-  | eq_num (Sub (be, cc)) (Neg ae) = false
-  | eq_num (Add (be, cc)) (Neg ae) = false
-  | eq_num (Mul (db, ea)) (Cn (ac, bd, cc)) = false
-  | eq_num (Sub (dc, ea)) (Cn (ac, bd, cc)) = false
-  | eq_num (Add (dc, ea)) (Cn (ac, bd, cc)) = false
-  | eq_num (Neg dc) (Cn (ac, bd, cc)) = false
-  | eq_num (Mul (bd, cc)) (Bound ac) = false
-  | eq_num (Sub (be, cc)) (Bound ac) = false
-  | eq_num (Add (be, cc)) (Bound ac) = false
-  | eq_num (Neg be) (Bound ac) = false
-  | eq_num (Cn (bc, cb, dc)) (Bound ac) = false
-  | eq_num (Mul (bd, cc)) (C ad) = false
-  | eq_num (Sub (be, cc)) (C ad) = false
-  | eq_num (Add (be, cc)) (C ad) = false
-  | eq_num (Neg be) (C ad) = false
-  | eq_num (Cn (bc, cb, dc)) (C ad) = false
-  | eq_num (Bound bc) (C ad) = false
-  | eq_num (Sub (ab, bb)) (Mul (c, da)) = false
-  | eq_num (Add (ab, bb)) (Mul (c, da)) = false
-  | eq_num (Add (ab, bb)) (Sub (ca, da)) = false
-  | eq_num (Neg ab) (Mul (ba, ca)) = false
-  | eq_num (Neg ab) (Sub (bb, ca)) = false
-  | eq_num (Neg ab) (Add (bb, ca)) = false
-  | eq_num (Cn (a, ba, ca)) (Mul (d, e)) = false
-  | eq_num (Cn (a, ba, ca)) (Sub (da, e)) = false
-  | eq_num (Cn (a, ba, ca)) (Add (da, e)) = false
-  | eq_num (Cn (a, ba, ca)) (Neg da) = false
-  | eq_num (Bound a) (Mul (ba, ca)) = false
-  | eq_num (Bound a) (Sub (bb, ca)) = false
-  | eq_num (Bound a) (Add (bb, ca)) = false
-  | eq_num (Bound a) (Neg bb) = false
-  | eq_num (Bound a) (Cn (b, c, da)) = false
-  | eq_num (C aa) (Mul (ba, ca)) = false
-  | eq_num (C aa) (Sub (bb, ca)) = false
-  | eq_num (C aa) (Add (bb, ca)) = false
-  | eq_num (C aa) (Neg bb) = false
-  | eq_num (C aa) (Cn (b, c, da)) = false
-  | eq_num (C aa) (Bound b) = false
+fun eq_num (Mul (c, d)) (Sub (a, b)) = false
+  | eq_num (Mul (c, d)) (Add (a, b)) = false
+  | eq_num (Sub (c, d)) (Add (a, b)) = false
+  | eq_num (Mul (b, c)) (Neg a) = false
+  | eq_num (Sub (b, c)) (Neg a) = false
+  | eq_num (Add (b, c)) (Neg a) = false
+  | eq_num (Mul (d, e)) (Cn (a, b, c)) = false
+  | eq_num (Sub (d, e)) (Cn (a, b, c)) = false
+  | eq_num (Add (d, e)) (Cn (a, b, c)) = false
+  | eq_num (Neg d) (Cn (a, b, c)) = false
+  | eq_num (Mul (b, c)) (Bound a) = false
+  | eq_num (Sub (b, c)) (Bound a) = false
+  | eq_num (Add (b, c)) (Bound a) = false
+  | eq_num (Neg b) (Bound a) = false
+  | eq_num (Cn (b, c, d)) (Bound a) = false
+  | eq_num (Mul (b, c)) (C a) = false
+  | eq_num (Sub (b, c)) (C a) = false
+  | eq_num (Add (b, c)) (C a) = false
+  | eq_num (Neg b) (C a) = false
+  | eq_num (Cn (b, c, d)) (C a) = false
+  | eq_num (Bound b) (C a) = false
+  | eq_num (Sub (a, b)) (Mul (c, d)) = false
+  | eq_num (Add (a, b)) (Mul (c, d)) = false
+  | eq_num (Add (a, b)) (Sub (c, d)) = false
+  | eq_num (Neg a) (Mul (b, c)) = false
+  | eq_num (Neg a) (Sub (b, c)) = false
+  | eq_num (Neg a) (Add (b, c)) = false
+  | eq_num (Cn (a, b, c)) (Mul (d, e)) = false
+  | eq_num (Cn (a, b, c)) (Sub (d, e)) = false
+  | eq_num (Cn (a, b, c)) (Add (d, e)) = false
+  | eq_num (Cn (a, b, c)) (Neg d) = false
+  | eq_num (Bound a) (Mul (b, c)) = false
+  | eq_num (Bound a) (Sub (b, c)) = false
+  | eq_num (Bound a) (Add (b, c)) = false
+  | eq_num (Bound a) (Neg b) = false
+  | eq_num (Bound a) (Cn (b, c, d)) = false
+  | eq_num (C a) (Mul (b, c)) = false
+  | eq_num (C a) (Sub (b, c)) = false
+  | eq_num (C a) (Add (b, c)) = false
+  | eq_num (C a) (Neg b) = false
+  | eq_num (C a) (Cn (b, c, d)) = false
+  | eq_num (C a) (Bound b) = false
   | eq_num (Mul (inta, num)) (Mul (int', num')) =
     ((inta : IntInf.int) = int') andalso eq_num num num'
   | eq_num (Sub (num1, num2)) (Sub (num1', num2')) =
@@ -165,347 +165,347 @@
   | eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat')
   | eq_num (C inta) (C int') = ((inta : IntInf.int) = int');
 
-fun eq_fm (NClosed bd) (Closed ad) = false
-  | eq_fm (NClosed bd) (A af) = false
-  | eq_fm (Closed bd) (A af) = false
-  | eq_fm (NClosed bd) (E af) = false
-  | eq_fm (Closed bd) (E af) = false
-  | eq_fm (A bf) (E af) = false
-  | eq_fm (NClosed cd) (Iff (af, bf)) = false
-  | eq_fm (Closed cd) (Iff (af, bf)) = false
-  | eq_fm (A cf) (Iff (af, bf)) = false
-  | eq_fm (E cf) (Iff (af, bf)) = false
-  | eq_fm (NClosed cd) (Imp (af, bf)) = false
-  | eq_fm (Closed cd) (Imp (af, bf)) = false
-  | eq_fm (A cf) (Imp (af, bf)) = false
-  | eq_fm (E cf) (Imp (af, bf)) = false
-  | eq_fm (Iff (cf, db)) (Imp (af, bf)) = false
-  | eq_fm (NClosed cd) (Or (af, bf)) = false
-  | eq_fm (Closed cd) (Or (af, bf)) = false
-  | eq_fm (A cf) (Or (af, bf)) = false
-  | eq_fm (E cf) (Or (af, bf)) = false
-  | eq_fm (Iff (cf, db)) (Or (af, bf)) = false
-  | eq_fm (Imp (cf, db)) (Or (af, bf)) = false
-  | eq_fm (NClosed cd) (And (af, bf)) = false
-  | eq_fm (Closed cd) (And (af, bf)) = false
-  | eq_fm (A cf) (And (af, bf)) = false
-  | eq_fm (E cf) (And (af, bf)) = false
-  | eq_fm (Iff (cf, db)) (And (af, bf)) = false
-  | eq_fm (Imp (cf, db)) (And (af, bf)) = false
-  | eq_fm (Or (cf, db)) (And (af, bf)) = false
-  | eq_fm (NClosed bd) (Not af) = false
-  | eq_fm (Closed bd) (Not af) = false
-  | eq_fm (A bf) (Not af) = false
-  | eq_fm (E bf) (Not af) = false
-  | eq_fm (Iff (bf, cf)) (Not af) = false
-  | eq_fm (Imp (bf, cf)) (Not af) = false
-  | eq_fm (Or (bf, cf)) (Not af) = false
-  | eq_fm (And (bf, cf)) (Not af) = false
-  | eq_fm (NClosed cd) (NDvd (ae, bg)) = false
-  | eq_fm (Closed cd) (NDvd (ae, bg)) = false
-  | eq_fm (A cf) (NDvd (ae, bg)) = false
-  | eq_fm (E cf) (NDvd (ae, bg)) = false
-  | eq_fm (Iff (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (Imp (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (Or (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (And (cf, db)) (NDvd (ae, bg)) = false
-  | eq_fm (Not cf) (NDvd (ae, bg)) = false
-  | eq_fm (NClosed cd) (Dvd (ae, bg)) = false
-  | eq_fm (Closed cd) (Dvd (ae, bg)) = false
-  | eq_fm (A cf) (Dvd (ae, bg)) = false
-  | eq_fm (E cf) (Dvd (ae, bg)) = false
-  | eq_fm (Iff (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (Imp (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (Or (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (And (cf, db)) (Dvd (ae, bg)) = false
-  | eq_fm (Not cf) (Dvd (ae, bg)) = false
-  | eq_fm (NDvd (ce, dc)) (Dvd (ae, bg)) = false
-  | eq_fm (NClosed bd) (NEq ag) = false
-  | eq_fm (Closed bd) (NEq ag) = false
-  | eq_fm (A bf) (NEq ag) = false
-  | eq_fm (E bf) (NEq ag) = false
-  | eq_fm (Iff (bf, cf)) (NEq ag) = false
-  | eq_fm (Imp (bf, cf)) (NEq ag) = false
-  | eq_fm (Or (bf, cf)) (NEq ag) = false
-  | eq_fm (And (bf, cf)) (NEq ag) = false
-  | eq_fm (Not bf) (NEq ag) = false
-  | eq_fm (NDvd (be, cg)) (NEq ag) = false
-  | eq_fm (Dvd (be, cg)) (NEq ag) = false
-  | eq_fm (NClosed bd) (Eq ag) = false
-  | eq_fm (Closed bd) (Eq ag) = false
-  | eq_fm (A bf) (Eq ag) = false
-  | eq_fm (E bf) (Eq ag) = false
-  | eq_fm (Iff (bf, cf)) (Eq ag) = false
-  | eq_fm (Imp (bf, cf)) (Eq ag) = false
-  | eq_fm (Or (bf, cf)) (Eq ag) = false
-  | eq_fm (And (bf, cf)) (Eq ag) = false
-  | eq_fm (Not bf) (Eq ag) = false
-  | eq_fm (NDvd (be, cg)) (Eq ag) = false
-  | eq_fm (Dvd (be, cg)) (Eq ag) = false
-  | eq_fm (NEq bg) (Eq ag) = false
-  | eq_fm (NClosed bd) (Ge ag) = false
-  | eq_fm (Closed bd) (Ge ag) = false
-  | eq_fm (A bf) (Ge ag) = false
-  | eq_fm (E bf) (Ge ag) = false
-  | eq_fm (Iff (bf, cf)) (Ge ag) = false
-  | eq_fm (Imp (bf, cf)) (Ge ag) = false
-  | eq_fm (Or (bf, cf)) (Ge ag) = false
-  | eq_fm (And (bf, cf)) (Ge ag) = false
-  | eq_fm (Not bf) (Ge ag) = false
-  | eq_fm (NDvd (be, cg)) (Ge ag) = false
-  | eq_fm (Dvd (be, cg)) (Ge ag) = false
-  | eq_fm (NEq bg) (Ge ag) = false
-  | eq_fm (Eq bg) (Ge ag) = false
-  | eq_fm (NClosed bd) (Gt ag) = false
-  | eq_fm (Closed bd) (Gt ag) = false
-  | eq_fm (A bf) (Gt ag) = false
-  | eq_fm (E bf) (Gt ag) = false
-  | eq_fm (Iff (bf, cf)) (Gt ag) = false
-  | eq_fm (Imp (bf, cf)) (Gt ag) = false
-  | eq_fm (Or (bf, cf)) (Gt ag) = false
-  | eq_fm (And (bf, cf)) (Gt ag) = false
-  | eq_fm (Not bf) (Gt ag) = false
-  | eq_fm (NDvd (be, cg)) (Gt ag) = false
-  | eq_fm (Dvd (be, cg)) (Gt ag) = false
-  | eq_fm (NEq bg) (Gt ag) = false
-  | eq_fm (Eq bg) (Gt ag) = false
-  | eq_fm (Ge bg) (Gt ag) = false
-  | eq_fm (NClosed bd) (Le ag) = false
-  | eq_fm (Closed bd) (Le ag) = false
-  | eq_fm (A bf) (Le ag) = false
-  | eq_fm (E bf) (Le ag) = false
-  | eq_fm (Iff (bf, cf)) (Le ag) = false
-  | eq_fm (Imp (bf, cf)) (Le ag) = false
-  | eq_fm (Or (bf, cf)) (Le ag) = false
-  | eq_fm (And (bf, cf)) (Le ag) = false
-  | eq_fm (Not bf) (Le ag) = false
-  | eq_fm (NDvd (be, cg)) (Le ag) = false
-  | eq_fm (Dvd (be, cg)) (Le ag) = false
-  | eq_fm (NEq bg) (Le ag) = false
-  | eq_fm (Eq bg) (Le ag) = false
-  | eq_fm (Ge bg) (Le ag) = false
-  | eq_fm (Gt bg) (Le ag) = false
-  | eq_fm (NClosed bd) (Lt ag) = false
-  | eq_fm (Closed bd) (Lt ag) = false
-  | eq_fm (A bf) (Lt ag) = false
-  | eq_fm (E bf) (Lt ag) = false
-  | eq_fm (Iff (bf, cf)) (Lt ag) = false
-  | eq_fm (Imp (bf, cf)) (Lt ag) = false
-  | eq_fm (Or (bf, cf)) (Lt ag) = false
-  | eq_fm (And (bf, cf)) (Lt ag) = false
-  | eq_fm (Not bf) (Lt ag) = false
-  | eq_fm (NDvd (be, cg)) (Lt ag) = false
-  | eq_fm (Dvd (be, cg)) (Lt ag) = false
-  | eq_fm (NEq bg) (Lt ag) = false
-  | eq_fm (Eq bg) (Lt ag) = false
-  | eq_fm (Ge bg) (Lt ag) = false
-  | eq_fm (Gt bg) (Lt ag) = false
-  | eq_fm (Le bg) (Lt ag) = false
-  | eq_fm (NClosed ad) F = false
-  | eq_fm (Closed ad) F = false
-  | eq_fm (A af) F = false
-  | eq_fm (E af) F = false
-  | eq_fm (Iff (af, bf)) F = false
-  | eq_fm (Imp (af, bf)) F = false
-  | eq_fm (Or (af, bf)) F = false
-  | eq_fm (And (af, bf)) F = false
-  | eq_fm (Not af) F = false
-  | eq_fm (NDvd (ae, bg)) F = false
-  | eq_fm (Dvd (ae, bg)) F = false
-  | eq_fm (NEq ag) F = false
-  | eq_fm (Eq ag) F = false
-  | eq_fm (Ge ag) F = false
-  | eq_fm (Gt ag) F = false
-  | eq_fm (Le ag) F = false
-  | eq_fm (Lt ag) F = false
-  | eq_fm (NClosed ad) T = false
-  | eq_fm (Closed ad) T = false
-  | eq_fm (A af) T = false
-  | eq_fm (E af) T = false
-  | eq_fm (Iff (af, bf)) T = false
-  | eq_fm (Imp (af, bf)) T = false
-  | eq_fm (Or (af, bf)) T = false
-  | eq_fm (And (af, bf)) T = false
-  | eq_fm (Not af) T = false
-  | eq_fm (NDvd (ae, bg)) T = false
-  | eq_fm (Dvd (ae, bg)) T = false
-  | eq_fm (NEq ag) T = false
-  | eq_fm (Eq ag) T = false
-  | eq_fm (Ge ag) T = false
-  | eq_fm (Gt ag) T = false
-  | eq_fm (Le ag) T = false
-  | eq_fm (Lt ag) T = false
+fun eq_fm (NClosed b) (Closed a) = false
+  | eq_fm (NClosed b) (A a) = false
+  | eq_fm (Closed b) (A a) = false
+  | eq_fm (NClosed b) (E a) = false
+  | eq_fm (Closed b) (E a) = false
+  | eq_fm (A b) (E a) = false
+  | eq_fm (NClosed c) (Iff (a, b)) = false
+  | eq_fm (Closed c) (Iff (a, b)) = false
+  | eq_fm (A c) (Iff (a, b)) = false
+  | eq_fm (E c) (Iff (a, b)) = false
+  | eq_fm (NClosed c) (Imp (a, b)) = false
+  | eq_fm (Closed c) (Imp (a, b)) = false
+  | eq_fm (A c) (Imp (a, b)) = false
+  | eq_fm (E c) (Imp (a, b)) = false
+  | eq_fm (Iff (c, d)) (Imp (a, b)) = false
+  | eq_fm (NClosed c) (Or (a, b)) = false
+  | eq_fm (Closed c) (Or (a, b)) = false
+  | eq_fm (A c) (Or (a, b)) = false
+  | eq_fm (E c) (Or (a, b)) = false
+  | eq_fm (Iff (c, d)) (Or (a, b)) = false
+  | eq_fm (Imp (c, d)) (Or (a, b)) = false
+  | eq_fm (NClosed c) (And (a, b)) = false
+  | eq_fm (Closed c) (And (a, b)) = false
+  | eq_fm (A c) (And (a, b)) = false
+  | eq_fm (E c) (And (a, b)) = false
+  | eq_fm (Iff (c, d)) (And (a, b)) = false
+  | eq_fm (Imp (c, d)) (And (a, b)) = false
+  | eq_fm (Or (c, d)) (And (a, b)) = false
+  | eq_fm (NClosed b) (Not a) = false
+  | eq_fm (Closed b) (Not a) = false
+  | eq_fm (A b) (Not a) = false
+  | eq_fm (E b) (Not a) = false
+  | eq_fm (Iff (b, c)) (Not a) = false
+  | eq_fm (Imp (b, c)) (Not a) = false
+  | eq_fm (Or (b, c)) (Not a) = false
+  | eq_fm (And (b, c)) (Not a) = false
+  | eq_fm (NClosed c) (NDvd (a, b)) = false
+  | eq_fm (Closed c) (NDvd (a, b)) = false
+  | eq_fm (A c) (NDvd (a, b)) = false
+  | eq_fm (E c) (NDvd (a, b)) = false
+  | eq_fm (Iff (c, d)) (NDvd (a, b)) = false
+  | eq_fm (Imp (c, d)) (NDvd (a, b)) = false
+  | eq_fm (Or (c, d)) (NDvd (a, b)) = false
+  | eq_fm (And (c, d)) (NDvd (a, b)) = false
+  | eq_fm (Not c) (NDvd (a, b)) = false
+  | eq_fm (NClosed c) (Dvd (a, b)) = false
+  | eq_fm (Closed c) (Dvd (a, b)) = false
+  | eq_fm (A c) (Dvd (a, b)) = false
+  | eq_fm (E c) (Dvd (a, b)) = false
+  | eq_fm (Iff (c, d)) (Dvd (a, b)) = false
+  | eq_fm (Imp (c, d)) (Dvd (a, b)) = false
+  | eq_fm (Or (c, d)) (Dvd (a, b)) = false
+  | eq_fm (And (c, d)) (Dvd (a, b)) = false
+  | eq_fm (Not c) (Dvd (a, b)) = false
+  | eq_fm (NDvd (c, d)) (Dvd (a, b)) = false
+  | eq_fm (NClosed b) (NEq a) = false
+  | eq_fm (Closed b) (NEq a) = false
+  | eq_fm (A b) (NEq a) = false
+  | eq_fm (E b) (NEq a) = false
+  | eq_fm (Iff (b, c)) (NEq a) = false
+  | eq_fm (Imp (b, c)) (NEq a) = false
+  | eq_fm (Or (b, c)) (NEq a) = false
+  | eq_fm (And (b, c)) (NEq a) = false
+  | eq_fm (Not b) (NEq a) = false
+  | eq_fm (NDvd (b, c)) (NEq a) = false
+  | eq_fm (Dvd (b, c)) (NEq a) = false
+  | eq_fm (NClosed b) (Eq a) = false
+  | eq_fm (Closed b) (Eq a) = false
+  | eq_fm (A b) (Eq a) = false
+  | eq_fm (E b) (Eq a) = false
+  | eq_fm (Iff (b, c)) (Eq a) = false
+  | eq_fm (Imp (b, c)) (Eq a) = false
+  | eq_fm (Or (b, c)) (Eq a) = false
+  | eq_fm (And (b, c)) (Eq a) = false
+  | eq_fm (Not b) (Eq a) = false
+  | eq_fm (NDvd (b, c)) (Eq a) = false
+  | eq_fm (Dvd (b, c)) (Eq a) = false
+  | eq_fm (NEq b) (Eq a) = false
+  | eq_fm (NClosed b) (Ge a) = false
+  | eq_fm (Closed b) (Ge a) = false
+  | eq_fm (A b) (Ge a) = false
+  | eq_fm (E b) (Ge a) = false
+  | eq_fm (Iff (b, c)) (Ge a) = false
+  | eq_fm (Imp (b, c)) (Ge a) = false
+  | eq_fm (Or (b, c)) (Ge a) = false
+  | eq_fm (And (b, c)) (Ge a) = false
+  | eq_fm (Not b) (Ge a) = false
+  | eq_fm (NDvd (b, c)) (Ge a) = false
+  | eq_fm (Dvd (b, c)) (Ge a) = false
+  | eq_fm (NEq b) (Ge a) = false
+  | eq_fm (Eq b) (Ge a) = false
+  | eq_fm (NClosed b) (Gt a) = false
+  | eq_fm (Closed b) (Gt a) = false
+  | eq_fm (A b) (Gt a) = false
+  | eq_fm (E b) (Gt a) = false
+  | eq_fm (Iff (b, c)) (Gt a) = false
+  | eq_fm (Imp (b, c)) (Gt a) = false
+  | eq_fm (Or (b, c)) (Gt a) = false
+  | eq_fm (And (b, c)) (Gt a) = false
+  | eq_fm (Not b) (Gt a) = false
+  | eq_fm (NDvd (b, c)) (Gt a) = false
+  | eq_fm (Dvd (b, c)) (Gt a) = false
+  | eq_fm (NEq b) (Gt a) = false
+  | eq_fm (Eq b) (Gt a) = false
+  | eq_fm (Ge b) (Gt a) = false
+  | eq_fm (NClosed b) (Le a) = false
+  | eq_fm (Closed b) (Le a) = false
+  | eq_fm (A b) (Le a) = false
+  | eq_fm (E b) (Le a) = false
+  | eq_fm (Iff (b, c)) (Le a) = false
+  | eq_fm (Imp (b, c)) (Le a) = false
+  | eq_fm (Or (b, c)) (Le a) = false
+  | eq_fm (And (b, c)) (Le a) = false
+  | eq_fm (Not b) (Le a) = false
+  | eq_fm (NDvd (b, c)) (Le a) = false
+  | eq_fm (Dvd (b, c)) (Le a) = false
+  | eq_fm (NEq b) (Le a) = false
+  | eq_fm (Eq b) (Le a) = false
+  | eq_fm (Ge b) (Le a) = false
+  | eq_fm (Gt b) (Le a) = false
+  | eq_fm (NClosed b) (Lt a) = false
+  | eq_fm (Closed b) (Lt a) = false
+  | eq_fm (A b) (Lt a) = false
+  | eq_fm (E b) (Lt a) = false
+  | eq_fm (Iff (b, c)) (Lt a) = false
+  | eq_fm (Imp (b, c)) (Lt a) = false
+  | eq_fm (Or (b, c)) (Lt a) = false
+  | eq_fm (And (b, c)) (Lt a) = false
+  | eq_fm (Not b) (Lt a) = false
+  | eq_fm (NDvd (b, c)) (Lt a) = false
+  | eq_fm (Dvd (b, c)) (Lt a) = false
+  | eq_fm (NEq b) (Lt a) = false
+  | eq_fm (Eq b) (Lt a) = false
+  | eq_fm (Ge b) (Lt a) = false
+  | eq_fm (Gt b) (Lt a) = false
+  | eq_fm (Le b) (Lt a) = false
+  | eq_fm (NClosed a) F = false
+  | eq_fm (Closed a) F = false
+  | eq_fm (A a) F = false
+  | eq_fm (E a) F = false
+  | eq_fm (Iff (a, b)) F = false
+  | eq_fm (Imp (a, b)) F = false
+  | eq_fm (Or (a, b)) F = false
+  | eq_fm (And (a, b)) F = false
+  | eq_fm (Not a) F = false
+  | eq_fm (NDvd (a, b)) F = false
+  | eq_fm (Dvd (a, b)) F = false
+  | eq_fm (NEq a) F = false
+  | eq_fm (Eq a) F = false
+  | eq_fm (Ge a) F = false
+  | eq_fm (Gt a) F = false
+  | eq_fm (Le a) F = false
+  | eq_fm (Lt a) F = false
+  | eq_fm (NClosed a) T = false
+  | eq_fm (Closed a) T = false
+  | eq_fm (A a) T = false
+  | eq_fm (E a) T = false
+  | eq_fm (Iff (a, b)) T = false
+  | eq_fm (Imp (a, b)) T = false
+  | eq_fm (Or (a, b)) T = false
+  | eq_fm (And (a, b)) T = false
+  | eq_fm (Not a) T = false
+  | eq_fm (NDvd (a, b)) T = false
+  | eq_fm (Dvd (a, b)) T = false
+  | eq_fm (NEq a) T = false
+  | eq_fm (Eq a) T = false
+  | eq_fm (Ge a) T = false
+  | eq_fm (Gt a) T = false
+  | eq_fm (Le a) T = false
+  | eq_fm (Lt a) T = false
   | eq_fm F T = false
   | eq_fm (Closed a) (NClosed b) = false
-  | eq_fm (A ab) (NClosed b) = false
-  | eq_fm (A ab) (Closed b) = false
-  | eq_fm (E ab) (NClosed b) = false
-  | eq_fm (E ab) (Closed b) = false
-  | eq_fm (E ab) (A bb) = false
-  | eq_fm (Iff (ab, bb)) (NClosed c) = false
-  | eq_fm (Iff (ab, bb)) (Closed c) = false
-  | eq_fm (Iff (ab, bb)) (A cb) = false
-  | eq_fm (Iff (ab, bb)) (E cb) = false
-  | eq_fm (Imp (ab, bb)) (NClosed c) = false
-  | eq_fm (Imp (ab, bb)) (Closed c) = false
-  | eq_fm (Imp (ab, bb)) (A cb) = false
-  | eq_fm (Imp (ab, bb)) (E cb) = false
-  | eq_fm (Imp (ab, bb)) (Iff (cb, d)) = false
-  | eq_fm (Or (ab, bb)) (NClosed c) = false
-  | eq_fm (Or (ab, bb)) (Closed c) = false
-  | eq_fm (Or (ab, bb)) (A cb) = false
-  | eq_fm (Or (ab, bb)) (E cb) = false
-  | eq_fm (Or (ab, bb)) (Iff (cb, d)) = false
-  | eq_fm (Or (ab, bb)) (Imp (cb, d)) = false
-  | eq_fm (And (ab, bb)) (NClosed c) = false
-  | eq_fm (And (ab, bb)) (Closed c) = false
-  | eq_fm (And (ab, bb)) (A cb) = false
-  | eq_fm (And (ab, bb)) (E cb) = false
-  | eq_fm (And (ab, bb)) (Iff (cb, d)) = false
-  | eq_fm (And (ab, bb)) (Imp (cb, d)) = false
-  | eq_fm (And (ab, bb)) (Or (cb, d)) = false
-  | eq_fm (Not ab) (NClosed b) = false
-  | eq_fm (Not ab) (Closed b) = false
-  | eq_fm (Not ab) (A bb) = false
-  | eq_fm (Not ab) (E bb) = false
-  | eq_fm (Not ab) (Iff (bb, cb)) = false
-  | eq_fm (Not ab) (Imp (bb, cb)) = false
-  | eq_fm (Not ab) (Or (bb, cb)) = false
-  | eq_fm (Not ab) (And (bb, cb)) = false
-  | eq_fm (NDvd (aa, bc)) (NClosed c) = false
-  | eq_fm (NDvd (aa, bc)) (Closed c) = false
-  | eq_fm (NDvd (aa, bc)) (A cb) = false
-  | eq_fm (NDvd (aa, bc)) (E cb) = false
-  | eq_fm (NDvd (aa, bc)) (Iff (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (Imp (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (Or (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (And (cb, d)) = false
-  | eq_fm (NDvd (aa, bc)) (Not cb) = false
-  | eq_fm (Dvd (aa, bc)) (NClosed c) = false
-  | eq_fm (Dvd (aa, bc)) (Closed c) = false
-  | eq_fm (Dvd (aa, bc)) (A cb) = false
-  | eq_fm (Dvd (aa, bc)) (E cb) = false
-  | eq_fm (Dvd (aa, bc)) (Iff (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (Imp (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (Or (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (And (cb, d)) = false
-  | eq_fm (Dvd (aa, bc)) (Not cb) = false
-  | eq_fm (Dvd (aa, bc)) (NDvd (ca, da)) = false
-  | eq_fm (NEq ac) (NClosed b) = false
-  | eq_fm (NEq ac) (Closed b) = false
-  | eq_fm (NEq ac) (A bb) = false
-  | eq_fm (NEq ac) (E bb) = false
-  | eq_fm (NEq ac) (Iff (bb, cb)) = false
-  | eq_fm (NEq ac) (Imp (bb, cb)) = false
-  | eq_fm (NEq ac) (Or (bb, cb)) = false
-  | eq_fm (NEq ac) (And (bb, cb)) = false
-  | eq_fm (NEq ac) (Not bb) = false
-  | eq_fm (NEq ac) (NDvd (ba, cc)) = false
-  | eq_fm (NEq ac) (Dvd (ba, cc)) = false
-  | eq_fm (Eq ac) (NClosed b) = false
-  | eq_fm (Eq ac) (Closed b) = false
-  | eq_fm (Eq ac) (A bb) = false
-  | eq_fm (Eq ac) (E bb) = false
-  | eq_fm (Eq ac) (Iff (bb, cb)) = false
-  | eq_fm (Eq ac) (Imp (bb, cb)) = false
-  | eq_fm (Eq ac) (Or (bb, cb)) = false
-  | eq_fm (Eq ac) (And (bb, cb)) = false
-  | eq_fm (Eq ac) (Not bb) = false
-  | eq_fm (Eq ac) (NDvd (ba, cc)) = false
-  | eq_fm (Eq ac) (Dvd (ba, cc)) = false
-  | eq_fm (Eq ac) (NEq bc) = false
-  | eq_fm (Ge ac) (NClosed b) = false
-  | eq_fm (Ge ac) (Closed b) = false
-  | eq_fm (Ge ac) (A bb) = false
-  | eq_fm (Ge ac) (E bb) = false
-  | eq_fm (Ge ac) (Iff (bb, cb)) = false
-  | eq_fm (Ge ac) (Imp (bb, cb)) = false
-  | eq_fm (Ge ac) (Or (bb, cb)) = false
-  | eq_fm (Ge ac) (And (bb, cb)) = false
-  | eq_fm (Ge ac) (Not bb) = false
-  | eq_fm (Ge ac) (NDvd (ba, cc)) = false
-  | eq_fm (Ge ac) (Dvd (ba, cc)) = false
-  | eq_fm (Ge ac) (NEq bc) = false
-  | eq_fm (Ge ac) (Eq bc) = false
-  | eq_fm (Gt ac) (NClosed b) = false
-  | eq_fm (Gt ac) (Closed b) = false
-  | eq_fm (Gt ac) (A bb) = false
-  | eq_fm (Gt ac) (E bb) = false
-  | eq_fm (Gt ac) (Iff (bb, cb)) = false
-  | eq_fm (Gt ac) (Imp (bb, cb)) = false
-  | eq_fm (Gt ac) (Or (bb, cb)) = false
-  | eq_fm (Gt ac) (And (bb, cb)) = false
-  | eq_fm (Gt ac) (Not bb) = false
-  | eq_fm (Gt ac) (NDvd (ba, cc)) = false
-  | eq_fm (Gt ac) (Dvd (ba, cc)) = false
-  | eq_fm (Gt ac) (NEq bc) = false
-  | eq_fm (Gt ac) (Eq bc) = false
-  | eq_fm (Gt ac) (Ge bc) = false
-  | eq_fm (Le ac) (NClosed b) = false
-  | eq_fm (Le ac) (Closed b) = false
-  | eq_fm (Le ac) (A bb) = false
-  | eq_fm (Le ac) (E bb) = false
-  | eq_fm (Le ac) (Iff (bb, cb)) = false
-  | eq_fm (Le ac) (Imp (bb, cb)) = false
-  | eq_fm (Le ac) (Or (bb, cb)) = false
-  | eq_fm (Le ac) (And (bb, cb)) = false
-  | eq_fm (Le ac) (Not bb) = false
-  | eq_fm (Le ac) (NDvd (ba, cc)) = false
-  | eq_fm (Le ac) (Dvd (ba, cc)) = false
-  | eq_fm (Le ac) (NEq bc) = false
-  | eq_fm (Le ac) (Eq bc) = false
-  | eq_fm (Le ac) (Ge bc) = false
-  | eq_fm (Le ac) (Gt bc) = false
-  | eq_fm (Lt ac) (NClosed b) = false
-  | eq_fm (Lt ac) (Closed b) = false
-  | eq_fm (Lt ac) (A bb) = false
-  | eq_fm (Lt ac) (E bb) = false
-  | eq_fm (Lt ac) (Iff (bb, cb)) = false
-  | eq_fm (Lt ac) (Imp (bb, cb)) = false
-  | eq_fm (Lt ac) (Or (bb, cb)) = false
-  | eq_fm (Lt ac) (And (bb, cb)) = false
-  | eq_fm (Lt ac) (Not bb) = false
-  | eq_fm (Lt ac) (NDvd (ba, cc)) = false
-  | eq_fm (Lt ac) (Dvd (ba, cc)) = false
-  | eq_fm (Lt ac) (NEq bc) = false
-  | eq_fm (Lt ac) (Eq bc) = false
-  | eq_fm (Lt ac) (Ge bc) = false
-  | eq_fm (Lt ac) (Gt bc) = false
-  | eq_fm (Lt ac) (Le bc) = false
+  | eq_fm (A a) (NClosed b) = false
+  | eq_fm (A a) (Closed b) = false
+  | eq_fm (E a) (NClosed b) = false
+  | eq_fm (E a) (Closed b) = false
+  | eq_fm (E a) (A b) = false
+  | eq_fm (Iff (a, b)) (NClosed c) = false
+  | eq_fm (Iff (a, b)) (Closed c) = false
+  | eq_fm (Iff (a, b)) (A c) = false
+  | eq_fm (Iff (a, b)) (E c) = false
+  | eq_fm (Imp (a, b)) (NClosed c) = false
+  | eq_fm (Imp (a, b)) (Closed c) = false
+  | eq_fm (Imp (a, b)) (A c) = false
+  | eq_fm (Imp (a, b)) (E c) = false
+  | eq_fm (Imp (a, b)) (Iff (c, d)) = false
+  | eq_fm (Or (a, b)) (NClosed c) = false
+  | eq_fm (Or (a, b)) (Closed c) = false
+  | eq_fm (Or (a, b)) (A c) = false
+  | eq_fm (Or (a, b)) (E c) = false
+  | eq_fm (Or (a, b)) (Iff (c, d)) = false
+  | eq_fm (Or (a, b)) (Imp (c, d)) = false
+  | eq_fm (And (a, b)) (NClosed c) = false
+  | eq_fm (And (a, b)) (Closed c) = false
+  | eq_fm (And (a, b)) (A c) = false
+  | eq_fm (And (a, b)) (E c) = false
+  | eq_fm (And (a, b)) (Iff (c, d)) = false
+  | eq_fm (And (a, b)) (Imp (c, d)) = false
+  | eq_fm (And (a, b)) (Or (c, d)) = false
+  | eq_fm (Not a) (NClosed b) = false
+  | eq_fm (Not a) (Closed b) = false
+  | eq_fm (Not a) (A b) = false
+  | eq_fm (Not a) (E b) = false
+  | eq_fm (Not a) (Iff (b, c)) = false
+  | eq_fm (Not a) (Imp (b, c)) = false
+  | eq_fm (Not a) (Or (b, c)) = false
+  | eq_fm (Not a) (And (b, c)) = false
+  | eq_fm (NDvd (a, b)) (NClosed c) = false
+  | eq_fm (NDvd (a, b)) (Closed c) = false
+  | eq_fm (NDvd (a, b)) (A c) = false
+  | eq_fm (NDvd (a, b)) (E c) = false
+  | eq_fm (NDvd (a, b)) (Iff (c, d)) = false
+  | eq_fm (NDvd (a, b)) (Imp (c, d)) = false
+  | eq_fm (NDvd (a, b)) (Or (c, d)) = false
+  | eq_fm (NDvd (a, b)) (And (c, d)) = false
+  | eq_fm (NDvd (a, b)) (Not c) = false
+  | eq_fm (Dvd (a, b)) (NClosed c) = false
+  | eq_fm (Dvd (a, b)) (Closed c) = false
+  | eq_fm (Dvd (a, b)) (A c) = false
+  | eq_fm (Dvd (a, b)) (E c) = false
+  | eq_fm (Dvd (a, b)) (Iff (c, d)) = false
+  | eq_fm (Dvd (a, b)) (Imp (c, d)) = false
+  | eq_fm (Dvd (a, b)) (Or (c, d)) = false
+  | eq_fm (Dvd (a, b)) (And (c, d)) = false
+  | eq_fm (Dvd (a, b)) (Not c) = false
+  | eq_fm (Dvd (a, b)) (NDvd (c, d)) = false
+  | eq_fm (NEq a) (NClosed b) = false
+  | eq_fm (NEq a) (Closed b) = false
+  | eq_fm (NEq a) (A b) = false
+  | eq_fm (NEq a) (E b) = false
+  | eq_fm (NEq a) (Iff (b, c)) = false
+  | eq_fm (NEq a) (Imp (b, c)) = false
+  | eq_fm (NEq a) (Or (b, c)) = false
+  | eq_fm (NEq a) (And (b, c)) = false
+  | eq_fm (NEq a) (Not b) = false
+  | eq_fm (NEq a) (NDvd (b, c)) = false
+  | eq_fm (NEq a) (Dvd (b, c)) = false
+  | eq_fm (Eq a) (NClosed b) = false
+  | eq_fm (Eq a) (Closed b) = false
+  | eq_fm (Eq a) (A b) = false
+  | eq_fm (Eq a) (E b) = false
+  | eq_fm (Eq a) (Iff (b, c)) = false
+  | eq_fm (Eq a) (Imp (b, c)) = false
+  | eq_fm (Eq a) (Or (b, c)) = false
+  | eq_fm (Eq a) (And (b, c)) = false
+  | eq_fm (Eq a) (Not b) = false
+  | eq_fm (Eq a) (NDvd (b, c)) = false
+  | eq_fm (Eq a) (Dvd (b, c)) = false
+  | eq_fm (Eq a) (NEq b) = false
+  | eq_fm (Ge a) (NClosed b) = false
+  | eq_fm (Ge a) (Closed b) = false
+  | eq_fm (Ge a) (A b) = false
+  | eq_fm (Ge a) (E b) = false
+  | eq_fm (Ge a) (Iff (b, c)) = false
+  | eq_fm (Ge a) (Imp (b, c)) = false
+  | eq_fm (Ge a) (Or (b, c)) = false
+  | eq_fm (Ge a) (And (b, c)) = false
+  | eq_fm (Ge a) (Not b) = false
+  | eq_fm (Ge a) (NDvd (b, c)) = false
+  | eq_fm (Ge a) (Dvd (b, c)) = false
+  | eq_fm (Ge a) (NEq b) = false
+  | eq_fm (Ge a) (Eq b) = false
+  | eq_fm (Gt a) (NClosed b) = false
+  | eq_fm (Gt a) (Closed b) = false
+  | eq_fm (Gt a) (A b) = false
+  | eq_fm (Gt a) (E b) = false
+  | eq_fm (Gt a) (Iff (b, c)) = false
+  | eq_fm (Gt a) (Imp (b, c)) = false
+  | eq_fm (Gt a) (Or (b, c)) = false
+  | eq_fm (Gt a) (And (b, c)) = false
+  | eq_fm (Gt a) (Not b) = false
+  | eq_fm (Gt a) (NDvd (b, c)) = false
+  | eq_fm (Gt a) (Dvd (b, c)) = false
+  | eq_fm (Gt a) (NEq b) = false
+  | eq_fm (Gt a) (Eq b) = false
+  | eq_fm (Gt a) (Ge b) = false
+  | eq_fm (Le a) (NClosed b) = false
+  | eq_fm (Le a) (Closed b) = false
+  | eq_fm (Le a) (A b) = false
+  | eq_fm (Le a) (E b) = false
+  | eq_fm (Le a) (Iff (b, c)) = false
+  | eq_fm (Le a) (Imp (b, c)) = false
+  | eq_fm (Le a) (Or (b, c)) = false
+  | eq_fm (Le a) (And (b, c)) = false
+  | eq_fm (Le a) (Not b) = false
+  | eq_fm (Le a) (NDvd (b, c)) = false
+  | eq_fm (Le a) (Dvd (b, c)) = false
+  | eq_fm (Le a) (NEq b) = false
+  | eq_fm (Le a) (Eq b) = false
+  | eq_fm (Le a) (Ge b) = false
+  | eq_fm (Le a) (Gt b) = false
+  | eq_fm (Lt a) (NClosed b) = false
+  | eq_fm (Lt a) (Closed b) = false
+  | eq_fm (Lt a) (A b) = false
+  | eq_fm (Lt a) (E b) = false
+  | eq_fm (Lt a) (Iff (b, c)) = false
+  | eq_fm (Lt a) (Imp (b, c)) = false
+  | eq_fm (Lt a) (Or (b, c)) = false
+  | eq_fm (Lt a) (And (b, c)) = false
+  | eq_fm (Lt a) (Not b) = false
+  | eq_fm (Lt a) (NDvd (b, c)) = false
+  | eq_fm (Lt a) (Dvd (b, c)) = false
+  | eq_fm (Lt a) (NEq b) = false
+  | eq_fm (Lt a) (Eq b) = false
+  | eq_fm (Lt a) (Ge b) = false
+  | eq_fm (Lt a) (Gt b) = false
+  | eq_fm (Lt a) (Le b) = false
   | eq_fm F (NClosed a) = false
   | eq_fm F (Closed a) = false
-  | eq_fm F (A ab) = false
-  | eq_fm F (E ab) = false
-  | eq_fm F (Iff (ab, bb)) = false
-  | eq_fm F (Imp (ab, bb)) = false
-  | eq_fm F (Or (ab, bb)) = false
-  | eq_fm F (And (ab, bb)) = false
-  | eq_fm F (Not ab) = false
-  | eq_fm F (NDvd (aa, bc)) = false
-  | eq_fm F (Dvd (aa, bc)) = false
-  | eq_fm F (NEq ac) = false
-  | eq_fm F (Eq ac) = false
-  | eq_fm F (Ge ac) = false
-  | eq_fm F (Gt ac) = false
-  | eq_fm F (Le ac) = false
-  | eq_fm F (Lt ac) = false
+  | eq_fm F (A a) = false
+  | eq_fm F (E a) = false
+  | eq_fm F (Iff (a, b)) = false
+  | eq_fm F (Imp (a, b)) = false
+  | eq_fm F (Or (a, b)) = false
+  | eq_fm F (And (a, b)) = false
+  | eq_fm F (Not a) = false
+  | eq_fm F (NDvd (a, b)) = false
+  | eq_fm F (Dvd (a, b)) = false
+  | eq_fm F (NEq a) = false
+  | eq_fm F (Eq a) = false
+  | eq_fm F (Ge a) = false
+  | eq_fm F (Gt a) = false
+  | eq_fm F (Le a) = false
+  | eq_fm F (Lt a) = false
   | eq_fm T (NClosed a) = false
   | eq_fm T (Closed a) = false
-  | eq_fm T (A ab) = false
-  | eq_fm T (E ab) = false
-  | eq_fm T (Iff (ab, bb)) = false
-  | eq_fm T (Imp (ab, bb)) = false
-  | eq_fm T (Or (ab, bb)) = false
-  | eq_fm T (And (ab, bb)) = false
-  | eq_fm T (Not ab) = false
-  | eq_fm T (NDvd (aa, bc)) = false
-  | eq_fm T (Dvd (aa, bc)) = false
-  | eq_fm T (NEq ac) = false
-  | eq_fm T (Eq ac) = false
-  | eq_fm T (Ge ac) = false
-  | eq_fm T (Gt ac) = false
-  | eq_fm T (Le ac) = false
-  | eq_fm T (Lt ac) = false
+  | eq_fm T (A a) = false
+  | eq_fm T (E a) = false
+  | eq_fm T (Iff (a, b)) = false
+  | eq_fm T (Imp (a, b)) = false
+  | eq_fm T (Or (a, b)) = false
+  | eq_fm T (And (a, b)) = false
+  | eq_fm T (Not a) = false
+  | eq_fm T (NDvd (a, b)) = false
+  | eq_fm T (Dvd (a, b)) = false
+  | eq_fm T (NEq a) = false
+  | eq_fm T (Eq a) = false
+  | eq_fm T (Ge a) = false
+  | eq_fm T (Gt a) = false
+  | eq_fm T (Le a) = false
+  | eq_fm T (Lt a) = false
   | eq_fm T F = false
   | eq_fm (NClosed nat) (NClosed nat') = ((nat : IntInf.int) = nat')
   | eq_fm (Closed nat) (Closed nat') = ((nat : IntInf.int) = nat')
@@ -554,7 +554,7 @@
                      | NClosed nat => Or (f p, q))
                 end));
 
-fun foldr f [] y = y
+fun foldr f [] a = a
   | foldr f (x :: xs) a = f x (foldr f xs a);
 
 fun evaldjf f ps = foldr (djf f) ps F;
@@ -607,9 +607,9 @@
   | numsubst0 t (Add (a, b)) = Add (numsubst0 t a, numsubst0 t b)
   | numsubst0 t (Sub (a, b)) = Sub (numsubst0 t a, numsubst0 t b)
   | numsubst0 t (Mul (i, a)) = Mul (i, numsubst0 t a)
-  | numsubst0 ta (Cn (v, ia, aa)) =
-    (if eqop eq_nat v 0 then Add (Mul (ia, ta), numsubst0 ta aa)
-      else Cn (suc (minus_nat v 1), ia, numsubst0 ta aa));
+  | numsubst0 t (Cn (v, i, a)) =
+    (if eqop eq_nat v 0 then Add (Mul (i, t), numsubst0 t a)
+      else Cn (suc (minus_nat v 1), i, numsubst0 t a));
 
 fun subst0 t T = T
   | subst0 t F = F
@@ -691,36 +691,35 @@
   | minusinf (NEq (Cn (hm, c, e))) =
     (if eqop eq_nat hm 0 then T else NEq (Cn (suc (minus_nat hm 1), c, e)));
 
-fun adjust b =
-  (fn a as (q, r) =>
-    (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
-      then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
-             IntInf.- (r, b))
-      else (IntInf.* ((2 : IntInf.int), q), r)));
+val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
 
-fun negDivAlg a b =
-  (if IntInf.<= ((0 : IntInf.int), IntInf.+ (a, b)) orelse
-        IntInf.<= (b, (0 : IntInf.int))
-    then ((~1 : IntInf.int), IntInf.+ (a, b))
-    else adjust b (negDivAlg a (IntInf.* ((2 : IntInf.int), b))));
+fun sgn_int i =
+  (if eqop eq_int i (0 : IntInf.int) then (0 : IntInf.int)
+    else (if IntInf.< ((0 : IntInf.int), i) then (1 : IntInf.int)
+           else IntInf.~ (1 : IntInf.int)));
 
 fun apsnd f (x, y) = (x, f y);
 
-val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
-
-fun posDivAlg a b =
-  (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
-    then ((0 : IntInf.int), a)
-    else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
-
-fun divmoda a b =
-  (if IntInf.<= ((0 : IntInf.int), a)
-    then (if IntInf.<= ((0 : IntInf.int), b) then posDivAlg a b
-           else (if eqop eq_int a (0 : IntInf.int)
-                  then ((0 : IntInf.int), (0 : IntInf.int))
-                  else apsnd IntInf.~ (negDivAlg (IntInf.~ a) (IntInf.~ b))))
-    else (if IntInf.< ((0 : IntInf.int), b) then negDivAlg a b
-           else apsnd IntInf.~ (posDivAlg (IntInf.~ a) (IntInf.~ b))));
+fun divmoda k l =
+  (if eqop eq_int k (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int))
+    else (if eqop eq_int l (0 : IntInf.int) then ((0 : IntInf.int), k)
+           else apsnd (fn a => IntInf.* (sgn_int l, a))
+                  (if eqop eq_int (sgn_int k) (sgn_int l)
+                    then (fn k => fn l => IntInf.divMod (IntInf.abs k,
+                           IntInf.abs l))
+                           k l
+                    else let
+                           val a =
+                             (fn k => fn l => IntInf.divMod (IntInf.abs k,
+                               IntInf.abs l))
+                               k l;
+                           val (r, s) = a;
+                         in
+                           (if eqop eq_int s (0 : IntInf.int)
+                             then (IntInf.~ r, (0 : IntInf.int))
+                             else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
+                                    IntInf.- (abs_int l, s)))
+                         end)));
 
 fun mod_int a b = snd (divmoda a b);
 
@@ -823,23 +822,23 @@
       else nummul i (simpnum t))
   | simpnum (Cn (v, va, vb)) = Cn (v, va, vb);
 
-fun nota (Not y) = y
+fun nota (Not p) = p
   | nota T = F
   | nota F = T
-  | nota (Lt vc) = Not (Lt vc)
-  | nota (Le vc) = Not (Le vc)
-  | nota (Gt vc) = Not (Gt vc)
-  | nota (Ge vc) = Not (Ge vc)
-  | nota (Eq vc) = Not (Eq vc)
-  | nota (NEq vc) = Not (NEq vc)
-  | nota (Dvd (va, vab)) = Not (Dvd (va, vab))
-  | nota (NDvd (va, vab)) = Not (NDvd (va, vab))
-  | nota (And (vb, vaa)) = Not (And (vb, vaa))
-  | nota (Or (vb, vaa)) = Not (Or (vb, vaa))
-  | nota (Imp (vb, vaa)) = Not (Imp (vb, vaa))
-  | nota (Iff (vb, vaa)) = Not (Iff (vb, vaa))
-  | nota (E vb) = Not (E vb)
-  | nota (A vb) = Not (A vb)
+  | nota (Lt v) = Not (Lt v)
+  | nota (Le v) = Not (Le v)
+  | nota (Gt v) = Not (Gt v)
+  | nota (Ge v) = Not (Ge v)
+  | nota (Eq v) = Not (Eq v)
+  | nota (NEq v) = Not (NEq v)
+  | nota (Dvd (v, va)) = Not (Dvd (v, va))
+  | nota (NDvd (v, va)) = Not (NDvd (v, va))
+  | nota (And (v, va)) = Not (And (v, va))
+  | nota (Or (v, va)) = Not (Or (v, va))
+  | nota (Imp (v, va)) = Not (Imp (v, va))
+  | nota (Iff (v, va)) = Not (Iff (v, va))
+  | nota (E v) = Not (E v)
+  | nota (A v) = Not (A v)
   | nota (Closed v) = Not (Closed v)
   | nota (NClosed v) = Not (NClosed v);
 
@@ -1184,7 +1183,7 @@
   | delta (Le v) = (1 : IntInf.int)
   | delta (Gt w) = (1 : IntInf.int)
   | delta (Ge x) = (1 : IntInf.int)
-  | delta (Eq ya) = (1 : IntInf.int)
+  | delta (Eq y) = (1 : IntInf.int)
   | delta (NEq z) = (1 : IntInf.int)
   | delta (Dvd (aa, C bo)) = (1 : IntInf.int)
   | delta (Dvd (aa, Bound bp)) = (1 : IntInf.int)
@@ -1205,10 +1204,10 @@
   | delta (A ao) = (1 : IntInf.int)
   | delta (Closed ap) = (1 : IntInf.int)
   | delta (NClosed aq) = (1 : IntInf.int)
-  | delta (Dvd (b, Cn (cm, c, e))) =
-    (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
-  | delta (NDvd (b, Cn (dm, c, e))) =
-    (if eqop eq_nat dm 0 then b else (1 : IntInf.int));
+  | delta (Dvd (i, Cn (cm, c, e))) =
+    (if eqop eq_nat cm 0 then i else (1 : IntInf.int))
+  | delta (NDvd (i, Cn (dm, c, e))) =
+    (if eqop eq_nat dm 0 then i else (1 : IntInf.int));
 
 fun div_int a b = fst (divmoda a b);
 
@@ -1367,22 +1366,22 @@
   | zeta (A ao) = (1 : IntInf.int)
   | zeta (Closed ap) = (1 : IntInf.int)
   | zeta (NClosed aq) = (1 : IntInf.int)
-  | zeta (Lt (Cn (cm, b, e))) =
-    (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
-  | zeta (Le (Cn (dm, b, e))) =
-    (if eqop eq_nat dm 0 then b else (1 : IntInf.int))
-  | zeta (Gt (Cn (em, b, e))) =
-    (if eqop eq_nat em 0 then b else (1 : IntInf.int))
-  | zeta (Ge (Cn (fm, b, e))) =
-    (if eqop eq_nat fm 0 then b else (1 : IntInf.int))
-  | zeta (Eq (Cn (gm, b, e))) =
-    (if eqop eq_nat gm 0 then b else (1 : IntInf.int))
-  | zeta (NEq (Cn (hm, b, e))) =
-    (if eqop eq_nat hm 0 then b else (1 : IntInf.int))
-  | zeta (Dvd (i, Cn (im, b, e))) =
-    (if eqop eq_nat im 0 then b else (1 : IntInf.int))
-  | zeta (NDvd (i, Cn (jm, b, e))) =
-    (if eqop eq_nat jm 0 then b else (1 : IntInf.int));
+  | zeta (Lt (Cn (cm, c, e))) =
+    (if eqop eq_nat cm 0 then c else (1 : IntInf.int))
+  | zeta (Le (Cn (dm, c, e))) =
+    (if eqop eq_nat dm 0 then c else (1 : IntInf.int))
+  | zeta (Gt (Cn (em, c, e))) =
+    (if eqop eq_nat em 0 then c else (1 : IntInf.int))
+  | zeta (Ge (Cn (fm, c, e))) =
+    (if eqop eq_nat fm 0 then c else (1 : IntInf.int))
+  | zeta (Eq (Cn (gm, c, e))) =
+    (if eqop eq_nat gm 0 then c else (1 : IntInf.int))
+  | zeta (NEq (Cn (hm, c, e))) =
+    (if eqop eq_nat hm 0 then c else (1 : IntInf.int))
+  | zeta (Dvd (i, Cn (im, c, e))) =
+    (if eqop eq_nat im 0 then c else (1 : IntInf.int))
+  | zeta (NDvd (i, Cn (jm, c, e))) =
+    (if eqop eq_nat jm 0 then c else (1 : IntInf.int));
 
 fun zsplit0 (C c) = ((0 : IntInf.int), C c)
   | zsplit0 (Bound n) =
@@ -1691,4 +1690,16 @@
   (if IntInf.<= (i, (0 : IntInf.int)) then n
     else nat_aux (IntInf.- (i, (1 : IntInf.int))) (suc n));
 
+fun adjust b =
+  (fn a as (q, r) =>
+    (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
+      then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
+             IntInf.- (r, b))
+      else (IntInf.* ((2 : IntInf.int), q), r)));
+
+fun posDivAlg a b =
+  (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
+    then ((0 : IntInf.int), a)
+    else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
+
 end; (*struct GeneratedCooper*)