# HG changeset patch
# User noschinl
# Date 1433316769 -7200
# Node ID 2e1c1968b38e15be06f008aa6107e24ee6b41dc8
# Parent  ccafd7d193e7d7b65797c6d62d9bd4be37549b56# Parent  838025c6e278d2daed6d1fe4a301a06125f1383b
merged

diff -r ccafd7d193e7 -r 2e1c1968b38e NEWS
--- a/NEWS	Tue Jun 02 13:14:36 2015 +0200
+++ b/NEWS	Wed Jun 03 09:32:49 2015 +0200
@@ -13,6 +13,17 @@
 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
 
 
+*** Pure ***
+
+* Abbreviations in type classes now carry proper sort constraint.
+Rare INCOMPATIBILITY in situations where the previous misbehaviour
+has been exploited previously.
+
+* Refinement of user-space type system in type classes: pseudo-local
+operations behave more similar to abbreviations.  Potential
+INCOMPATIBILITY in exotic situations.
+
+
 *** HOL ***
 
 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
@@ -25,6 +36,14 @@
 * Nitpick:
   - Removed "check_potential" and "check_genuine" options.
 
+* Constants Fields.divide (... / ...) and Divides.div (... div ...)
+are logically unified to Rings.divide in syntactic type class
+Rings.divide, with particular infix syntax added as abbreviations
+in classes Fields.inverse and Divides.div respectively.  INCOMPATIBILITY,
+instantiatios must refer to Rings.divide rather than the former
+separate constants, and infix syntax is usually not available during
+instantiation.
+
 
 New in Isabelle2015 (May 2015)
 ------------------------------
diff -r ccafd7d193e7 -r 2e1c1968b38e src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -325,7 +325,7 @@
 @{const abs} & @{typeof abs}\\
 @{const sgn} & @{typeof sgn}\\
 @{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
-@{const div_class.div} & @{typeof "div_class.div"}\\
+@{const Rings.divide} & @{typeof Rings.divide}\\
 @{const div_class.mod} & @{typeof "div_class.mod"}\\
 \end{supertabular}
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -150,11 +150,11 @@
 instantiation integer :: "{ring_div, equal, linordered_idom}"
 begin
 
-lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
-  is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
   .
 
-declare div_integer.rep_eq [simp]
+declare divide_integer.rep_eq [simp]
 
 lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
@@ -709,11 +709,11 @@
 instantiation natural :: "{semiring_div, equal, linordered_semiring}"
 begin
 
-lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
-  is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
+lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
   .
 
-declare div_natural.rep_eq [simp]
+declare divide_natural.rep_eq [simp]
 
 lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Complex.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -70,7 +70,7 @@
   "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
 | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
 
-definition "x / (y\<Colon>complex) = x * inverse y"
+definition "divide x (y\<Colon>complex) = x * inverse y"
 
 instance
   by intro_classes
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -710,7 +710,7 @@
 
 fun dest_frac ct =
   case Thm.term_of ct of
-    Const (@{const_name Fields.divide},_) $ a $ b=>
+    Const (@{const_name Rings.divide},_) $ a $ b=>
       Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -4033,7 +4033,7 @@
       @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
   | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) =
       @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
-  | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) =
+  | num_of_term ps (Const (@{const_name Rings.divide}, _) $ a $ b) =
       mk_C (dest_num a, dest_num b)
   | num_of_term ps t =
       (case try_dest_num t of
@@ -4087,7 +4087,7 @@
         (if d = 1 then HOLogic.mk_number T c
         else if d = 0 then Const (@{const_name Groups.zero}, T)
         else
-          Const (@{const_name Fields.divide}, binopT T) $
+          Const (@{const_name Rings.divide}, binopT T) $
             HOLogic.mk_number T c $ HOLogic.mk_number T d)
       end
   | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Divides.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -11,10 +11,15 @@
 
 subsection {* Syntactic division operations *}
 
-class div = dvd +
-  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
-    and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
-
+class div = dvd + divide +
+  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
+begin
+
+abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
+where
+  "op div \<equiv> divide"
+
+end
 
 subsection {* Abstract division in commutative semirings. *}
 
@@ -26,7 +31,13 @@
     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
 begin
 
-subclass semiring_no_zero_divisors ..
+subclass semidom_divide
+proof
+  fix b a
+  assume "b \<noteq> 0"
+  then show "a * b div b = a"
+    using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
+qed simp
 
 lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
   "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
@@ -102,11 +113,13 @@
   "(b * c + a) mod b = a mod b"
   by (simp add: add.commute)
 
-lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
-  using div_mult_self2 [of b 0 a] by simp
-
-lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
-  using div_mult_self1 [of b 0 a] by simp
+lemma div_mult_self1_is_id:
+  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
+  by (fact nonzero_mult_divide_cancel_left)
+
+lemma div_mult_self2_is_id:
+  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+  by (fact nonzero_mult_divide_cancel_right)
 
 lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
   using mod_mult_self2 [of 0 b a] by simp
@@ -434,21 +447,21 @@
 next
   assume "b div a = c"
   then have "b div a * a = c * a" by simp
-  moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self)
+  moreover from `a dvd b` have "b div a * a = b" by simp
   ultimately show "b = c * a" by simp
 qed
    
 lemma dvd_div_div_eq_mult:
   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
-  using assms by (auto simp add: mult.commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)
+  using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
 
 end
 
 class ring_div = comm_ring_1 + semiring_div
 begin
 
-subclass idom ..
+subclass idom_divide ..
 
 text {* Negation respects modular equivalence. *}
 
@@ -951,19 +964,26 @@
   shows "divmod_nat m n = qr"
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
 
+instantiation nat :: "Divides.div"
+begin
+
+definition divide_nat where
+  div_nat_def: "divide m n = fst (divmod_nat m n)"
+
+definition mod_nat where
+  "m mod n = snd (divmod_nat m n)"
+  
+instance ..
+
+end
+
 instantiation nat :: semiring_div
 begin
 
-definition div_nat where
-  "m div n = fst (divmod_nat m n)"
-
 lemma fst_divmod_nat [simp]:
   "fst (divmod_nat m n) = m div n"
   by (simp add: div_nat_def)
 
-definition mod_nat where
-  "m mod n = snd (divmod_nat m n)"
-
 lemma snd_divmod_nat [simp]:
   "snd (divmod_nat m n) = m mod n"
   by (simp add: mod_nat_def)
@@ -1069,7 +1089,7 @@
 ML {*
 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
 (
-  val div_name = @{const_name div};
+  val div_name = @{const_name divide};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
@@ -1184,18 +1204,23 @@
   "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
 by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
 
-lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
-  apply (cut_tac m = q and n = c in mod_less_divisor)
-  apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
-  apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
-  apply (simp add: add_mult_distrib2)
-  done
-
 lemma divmod_nat_rel_mult2_eq:
-  "divmod_nat_rel a b (q, r)
-   \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
-by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
-
+  assumes "divmod_nat_rel a b (q, r)"
+  shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
+proof -
+  { assume "r < b" and "0 < c" 
+    then have "b * (q mod c) + r < b * c"
+      apply (cut_tac m = q and n = c in mod_less_divisor)
+      apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
+      apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
+      apply (simp add: add_mult_distrib2)
+      done
+    then have "r + b * (q mod c) < b * c"
+      by (simp add: ac_simps)
+  } with assms show ?thesis
+    by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
+qed
+    
 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
 
@@ -1583,8 +1608,16 @@
   using odd_succ_div_two [of n] by simp
 
 lemma odd_two_times_div_two_nat [simp]:
-  "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
-  using odd_two_times_div_two_succ [of n] by simp
+  assumes "odd n"
+  shows "2 * (n div 2) = n - (1 :: nat)"
+proof -
+  from assms have "2 * (n div 2) + 1 = n"
+    by (rule odd_two_times_div_two_succ)
+  then have "Suc (2 * (n div 2)) - 1 = n - 1"
+    by simp
+  then show ?thesis
+    by simp
+qed
 
 lemma odd_Suc_minus_one [simp]:
   "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
@@ -1669,24 +1702,24 @@
 instantiation int :: Divides.div
 begin
 
-definition div_int where
-  "a div b = fst (divmod_int a b)"
+definition divide_int where
+  div_int_def: "divide a b = fst (divmod_int a b)"
+
+definition mod_int where
+  "a mod b = snd (divmod_int a b)"
+
+instance ..
+
+end
 
 lemma fst_divmod_int [simp]:
   "fst (divmod_int a b) = a div b"
   by (simp add: div_int_def)
 
-definition mod_int where
-  "a mod b = snd (divmod_int a b)"
-
 lemma snd_divmod_int [simp]:
   "snd (divmod_int a b) = a mod b"
   by (simp add: mod_int_def)
 
-instance ..
-
-end
-
 lemma divmod_int_mod_div:
   "divmod_int p q = (p div q, p mod q)"
   by (simp add: prod_eq_iff)
@@ -1909,7 +1942,7 @@
 ML {*
 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
 (
-  val div_name = @{const_name div};
+  val div_name = @{const_name Rings.divide};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Enum.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -585,12 +585,11 @@
 definition [simp]: "Groups.one = a\<^sub>1"
 definition [simp]: "op + = (\<lambda>_ _. a\<^sub>1)"
 definition [simp]: "op * = (\<lambda>_ _. a\<^sub>1)"
-definition [simp]: "op div = (\<lambda>_ _. a\<^sub>1)" 
 definition [simp]: "op mod = (\<lambda>_ _. a\<^sub>1)" 
 definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
 definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
 definition [simp]: "inverse = (\<lambda>_. a\<^sub>1)"
-definition [simp]: "op / = (\<lambda>_ _. a\<^sub>1)"
+definition [simp]: "divide = (\<lambda>_ _. a\<^sub>1)"
 
 instance by intro_classes(simp_all add: less_finite_1_def)
 end
@@ -691,15 +690,14 @@
 definition "op - = (op + :: finite_2 \<Rightarrow> _)"
 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
 definition "inverse = (\<lambda>x :: finite_2. x)"
-definition "op / = (op * :: finite_2 \<Rightarrow> _)"
+definition "divide = (op * :: finite_2 \<Rightarrow> _)"
 definition "abs = (\<lambda>x :: finite_2. x)"
-definition "op div = (op / :: finite_2 \<Rightarrow> _)"
 definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
 definition "sgn = (\<lambda>x :: finite_2. x)"
 instance
 by intro_classes
   (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
-       inverse_finite_2_def divide_finite_2_def abs_finite_2_def div_finite_2_def mod_finite_2_def sgn_finite_2_def
+       inverse_finite_2_def divide_finite_2_def abs_finite_2_def mod_finite_2_def sgn_finite_2_def
      split: finite_2.splits)
 end
 
@@ -819,15 +817,14 @@
 definition "x - y = x + (- y :: finite_3)"
 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
 definition "inverse = (\<lambda>x :: finite_3. x)" 
-definition "x / y = x * inverse (y :: finite_3)"
+definition "divide x y = x * inverse (y :: finite_3)"
 definition "abs = (\<lambda>x :: finite_3. x)"
-definition "op div = (op / :: finite_3 \<Rightarrow> _)"
 definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
 definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
 instance
 by intro_classes
   (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
-       inverse_finite_3_def divide_finite_3_def abs_finite_3_def div_finite_3_def mod_finite_3_def sgn_finite_3_def
+       inverse_finite_3_def divide_finite_3_def abs_finite_3_def mod_finite_3_def sgn_finite_3_def
        less_finite_3_def
      split: finite_3.splits)
 end
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Fields.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -19,35 +19,16 @@
   A division ring is like a field, but without the commutativity requirement.
 *}
 
-class inverse =
+class inverse = divide +
   fixes inverse :: "'a \<Rightarrow> 'a"
-    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-
-
-context semiring
 begin
-
-lemma [field_simps]:
-  shows distrib_left_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
-    and distrib_right_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
-  by (rule distrib_left distrib_right)+
+  
+abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
+where
+  "inverse_divide \<equiv> divide"
 
 end
 
-context ring
-begin
-
-lemma [field_simps]:
-  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
-    and right_diff_distrib_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
-  by (rule left_diff_distrib right_diff_distrib)+
-
-end
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-
 text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
 
 named_theorems divide_simps "rewrite rules to eliminate divisions"
@@ -240,7 +221,7 @@
   "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
   by (simp add: divide_diff_eq_iff[symmetric])
 
-lemma divide_zero [simp]:
+lemma division_ring_divide_zero [simp]:
   "a / 0 = 0"
   by (simp add: divide_inverse)
 
@@ -319,18 +300,31 @@
     by (fact field_inverse_zero) 
 qed
 
-subclass idom ..
+subclass idom_divide
+proof
+  fix b a
+  assume "b \<noteq> 0"
+  then show "a * b / b = a"
+    by (simp add: divide_inverse ac_simps)
+next
+  fix a
+  show "a / 0 = 0"
+    by (simp add: divide_inverse)
+qed
 
 text{*There is no slick version using division by zero.*}
 lemma inverse_add:
-  "[| a \<noteq> 0;  b \<noteq> 0 |]
-   ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
-by (simp add: division_ring_inverse_add ac_simps)
+  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
+  by (simp add: division_ring_inverse_add ac_simps)
 
 lemma nonzero_mult_divide_mult_cancel_left [simp]:
-assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
-proof -
-  have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
+  assumes [simp]: "c \<noteq> 0"
+  shows "(c * a) / (c * b) = a / b"
+proof (cases "b = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
   also have "... =  a * inverse b * (inverse c * c)"
     by (simp only: ac_simps)
@@ -339,8 +333,8 @@
 qed
 
 lemma nonzero_mult_divide_mult_cancel_right [simp]:
-  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
-by (simp add: mult.commute [of _ c])
+  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
+  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
 
 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   by (simp add: divide_inverse ac_simps)
@@ -359,29 +353,21 @@
 
 text{*Special Cancellation Simprules for Division*}
 
-lemma nonzero_mult_divide_cancel_right [simp]:
-  "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
-  using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
-
-lemma nonzero_mult_divide_cancel_left [simp]:
-  "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
-using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
-
 lemma nonzero_divide_mult_cancel_right [simp]:
-  "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
-using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
+  "b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a"
+  using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp
 
 lemma nonzero_divide_mult_cancel_left [simp]:
-  "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
-using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
+  "a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b"
+  using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp
 
 lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
-  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
-using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps)
+  "c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b"
+  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
 
 lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
-  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
-using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
+  "c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b"
+  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
 
 lemma diff_frac_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
@@ -445,7 +431,7 @@
 
 lemma mult_divide_mult_cancel_left_if [simp]:
   shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
-  by (simp add: mult_divide_mult_cancel_left)
+  by simp
 
 
 text {* Division and Unary Minus *}
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -1153,10 +1153,29 @@
   shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
   using assms by (induct A) (auto simp: no_zero_divisors)
 
-lemma (in field) setprod_diff1:
-  "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
-    (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
-  by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
+lemma (in semidom_divide) setprod_diff1:
+  assumes "finite A" and "f a \<noteq> 0"
+  shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
+proof (cases "a \<notin> A")
+  case True then show ?thesis by simp
+next
+  case False with assms show ?thesis
+  proof (induct A rule: finite_induct)
+    case empty then show ?case by simp
+  next
+    case (insert b B)
+    then show ?case
+    proof (cases "a = b")
+      case True with insert show ?thesis by simp
+    next
+      case False with insert have "a \<in> B" by simp
+      def C \<equiv> "B - {a}"
+      with `finite B` `a \<in> B`
+        have *: "B = insert a C" "finite C" "a \<notin> C" by auto
+      with insert show ?thesis by (auto simp add: insert_commute ac_simps)
+    qed
+  qed
+qed
 
 lemma (in field) setprod_inversef: 
   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Bit.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -117,7 +117,7 @@
   "inverse x = (x :: bit)"
 
 definition divide_bit_def [simp]:
-  "x / y = (x * y :: bit)"
+  "divide x y = (x * y :: bit)"
 
 lemmas field_bit_defs =
   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
@@ -201,4 +201,3 @@
 hide_const (open) set
 
 end
-
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Extended.thy
--- a/src/HOL/Library/Extended.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Extended.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -25,7 +25,7 @@
 case_of_simps less_eq_extended_case: less_eq_extended.simps
 
 definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
-"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
+"((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)"
 
 instance
   by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -1403,7 +1403,7 @@
   by (auto intro: ereal_cases)
 termination by (relation "{}") simp
 
-definition "x / y = x * inverse (y :: ereal)"
+definition "divide x y = x * inverse (y :: ereal)"
 
 instance ..
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -241,9 +241,9 @@
     by (simp add: Fract_def inverse_fract_def UN_fractrel)
 qed
 
-definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
+definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
 
-lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
+lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
   by (simp add: divide_fract_def)
 
 instance
@@ -255,7 +255,7 @@
       (simp_all add: fract_expand eq_fract mult.commute)
 next
   fix q r :: "'a fract"
-  show "q / r = q * inverse r" by (simp add: divide_fract_def)
+  show "divide q r = q * inverse r" by (simp add: divide_fract_def)
 next
   show "inverse 0 = (0:: 'a fract)"
     by (simp add: fract_expand) (simp add: fract_collapse)
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Function_Division.thy
--- a/src/HOL/Library/Function_Division.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Function_Division.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -15,7 +15,7 @@
 
 definition "inverse f = inverse \<circ> f"
 
-definition "(f / g) = (\<lambda>x. f x / g x)"
+definition "divide f g = (\<lambda>x. f x / g x)"
 
 instance ..
 
@@ -63,4 +63,3 @@
 *}
 
 end
-
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -336,10 +336,19 @@
 
 lemma set_decode_plus_power_2:
   "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
- apply (induct n arbitrary: z, simp_all)
-  apply (rule set_eqI, induct_tac x, simp, simp)
- apply (rule set_eqI, induct_tac x, simp, simp add: add.commute)
-done
+proof (induct n arbitrary: z)
+  case 0 show ?case
+  proof (rule set_eqI)
+    fix q show "q \<in> set_decode (2 ^ 0 + z) \<longleftrightarrow> q \<in> insert 0 (set_decode z)"
+      by (induct q) (insert 0, simp_all)
+  qed
+next
+  case (Suc n) show ?case
+  proof (rule set_eqI)
+    fix q show "q \<in> set_decode (2 ^ Suc n + z) \<longleftrightarrow> q \<in> insert (Suc n) (set_decode z)"
+      by (induct q) (insert Suc, simp_all)
+  qed
+qed
 
 lemma finite_set_decode [simp]: "finite (set_decode n)"
 apply (induct n rule: nat_less_induct)
@@ -389,4 +398,3 @@
 qed
 
 end
-
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Old_SMT/old_smt_normalize.ML
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -429,7 +429,7 @@
     @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
 
   val mult_nat_ops =
-    [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
+    [@{const times (nat)}, @{const divide (nat)}, @{const mod (nat)}]
 
   val nat_ops = simple_nat_ops @ mult_nat_ops
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Old_SMT/old_z3_interface.ML
--- a/src/HOL/Library/Old_SMT/old_z3_interface.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -41,7 +41,7 @@
         has_datatypes=true}
     end
 
-  fun is_div_mod @{const div (int)} = true
+  fun is_div_mod @{const divide (int)} = true
     | is_div_mod @{const mod (int)} = true
     | is_div_mod _ = false
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -1360,14 +1360,14 @@
 instantiation poly :: (field) ring_div
 begin
 
-definition div_poly where
-  "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
+definition divide_poly where
+  div_poly_def: "divide x y = (THE q. \<exists>r. pdivmod_rel x y q r)"
 
 definition mod_poly where
   "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
 
 lemma div_poly_eq:
-  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
+  "pdivmod_rel x y q r \<Longrightarrow> divide x y = q"
 unfolding div_poly_def
 by (fast elim: pdivmod_rel_unique_div)
 
@@ -1377,7 +1377,7 @@
 by (fast elim: pdivmod_rel_unique_mod)
 
 lemma pdivmod_rel:
-  "pdivmod_rel x y (x div y) (x mod y)"
+  "pdivmod_rel x y (divide x y) (x mod y)"
 proof -
   from pdivmod_rel_exists
     obtain q r where "pdivmod_rel x y q r" by fast
@@ -1387,41 +1387,41 @@
 
 instance proof
   fix x y :: "'a poly"
-  show "x div y * y + x mod y = x"
+  show "divide x y * y + x mod y = x"
     using pdivmod_rel [of x y]
     by (simp add: pdivmod_rel_def)
 next
   fix x :: "'a poly"
   have "pdivmod_rel x 0 0 x"
     by (rule pdivmod_rel_by_0)
-  thus "x div 0 = 0"
+  thus "divide x 0 = 0"
     by (rule div_poly_eq)
 next
   fix y :: "'a poly"
   have "pdivmod_rel 0 y 0 0"
     by (rule pdivmod_rel_0)
-  thus "0 div y = 0"
+  thus "divide 0 y = 0"
     by (rule div_poly_eq)
 next
   fix x y z :: "'a poly"
   assume "y \<noteq> 0"
-  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
+  hence "pdivmod_rel (x + z * y) y (z + divide x y) (x mod y)"
     using pdivmod_rel [of x y]
     by (simp add: pdivmod_rel_def distrib_right)
-  thus "(x + z * y) div y = z + x div y"
+  thus "divide (x + z * y) y = z + divide x y"
     by (rule div_poly_eq)
 next
   fix x y z :: "'a poly"
   assume "x \<noteq> 0"
-  show "(x * y) div (x * z) = y div z"
+  show "divide (x * y) (x * z) = divide y z"
   proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
     have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
       by (rule pdivmod_rel_by_0)
-    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
+    then have [simp]: "\<And>x::'a poly. divide x 0 = 0"
       by (rule div_poly_eq)
     have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
       by (rule pdivmod_rel_0)
-    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
+    then have [simp]: "\<And>x::'a poly. divide 0 x = 0"
       by (rule div_poly_eq)
     case False then show ?thesis by auto
   next
@@ -1430,8 +1430,8 @@
     have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
       by (auto simp add: pdivmod_rel_def algebra_simps)
         (rule classical, simp add: degree_mult_eq)
-    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
-    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
+    moreover from pdivmod_rel have "pdivmod_rel y z (divide y z) (y mod z)" .
+    ultimately have "pdivmod_rel (x * y) (x * z) (divide y z) (x * (y mod z))" .
     then show ?thesis by (simp add: div_poly_eq)
   qed
 qed
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -53,7 +53,7 @@
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
 setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
 
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}] *}
 
 section {* Arithmetic operations *}
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -283,14 +283,13 @@
    (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
    (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
    (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
-   (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
-   (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
+      (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
    (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
    (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
-   (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
+   (@{const_name Rings.divide}, @{typ "prop => prop => prop"}),
    (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
    (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -505,11 +505,18 @@
 
 end
 
-instantiation star :: (inverse) inverse
+instantiation star :: (divide) divide
 begin
 
 definition
-  star_divide_def:  "(op /) \<equiv> *f2* (op /)"
+  star_divide_def:  "divide \<equiv> *f2* divide"
+
+instance ..
+
+end
+
+instantiation star :: (inverse) inverse
+begin
 
 definition
   star_inverse_def: "inverse \<equiv> *f* inverse"
@@ -524,9 +531,6 @@
 begin
 
 definition
-  star_div_def:     "(op div) \<equiv> *f2* (op div)"
-
-definition
   star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
 
 instance ..
@@ -551,7 +555,7 @@
   star_add_def      star_diff_def     star_minus_def
   star_mult_def     star_divide_def   star_inverse_def
   star_le_def       star_less_def     star_abs_def       star_sgn_def
-  star_div_def      star_mod_def
+  star_mod_def
 
 text {* Class operations preserve standard elements *}
 
@@ -573,7 +577,7 @@
 lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
 by (simp add: star_mult_def)
 
-lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
+lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> divide x y \<in> Standard"
 by (simp add: star_divide_def)
 
 lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
@@ -582,17 +586,14 @@
 lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
 by (simp add: star_abs_def)
 
-lemma Standard_div: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x div y \<in> Standard"
-by (simp add: star_div_def)
-
 lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
 by (simp add: star_mod_def)
 
 lemmas Standard_simps [simp] =
   Standard_zero  Standard_one
-  Standard_add  Standard_diff  Standard_minus
+  Standard_add   Standard_diff    Standard_minus
   Standard_mult  Standard_divide  Standard_inverse
-  Standard_abs  Standard_div  Standard_mod
+  Standard_abs   Standard_mod
 
 text {* @{term star_of} preserves class operations *}
 
@@ -614,9 +615,6 @@
 lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
 by transfer (rule refl)
 
-lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
-by transfer (rule refl)
-
 lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
 by transfer (rule refl)
 
@@ -665,7 +663,7 @@
 lemmas star_of_simps [simp] =
   star_of_add     star_of_diff    star_of_minus
   star_of_mult    star_of_divide  star_of_inverse
-  star_of_div     star_of_mod     star_of_abs
+  star_of_mod     star_of_abs
   star_of_zero    star_of_one
   star_of_less    star_of_le      star_of_eq
   star_of_0_less  star_of_0_le    star_of_0_eq
@@ -855,6 +853,13 @@
 instance star :: (ring_1) ring_1 ..
 instance star :: (comm_ring_1) comm_ring_1 ..
 instance star :: (semidom) semidom ..
+instance star :: (semidom_divide) semidom_divide
+proof
+  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+    by transfer simp
+  show "\<And>a :: 'a star. divide a 0 = 0"
+    by transfer simp
+qed
 instance star :: (semiring_div) semiring_div
 apply intro_classes
 apply(transfer, rule mod_div_equality)
@@ -867,6 +872,7 @@
 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
 instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
 instance star :: (idom) idom .. 
+instance star :: (idom_divide) idom_divide ..
 
 instance star :: (division_ring) division_ring
 apply (intro_classes)
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -1484,6 +1484,14 @@
 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
 
+lemma of_nat_neq_0 [simp]:
+  "of_nat (Suc n) \<noteq> 0"
+  unfolding of_nat_eq_0_iff by simp
+
+lemma of_nat_0_neq [simp]:
+  "0 \<noteq> of_nat (Suc n)"
+  unfolding of_nat_0_eq_iff by simp  
+  
 end
 
 context linordered_semidom
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Parity.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -118,75 +118,60 @@
 subsection {* Instances for @{typ nat} and @{typ int} *}
 
 lemma even_Suc_Suc_iff [simp]:
-  "even (Suc (Suc n)) \<longleftrightarrow> even n"
+  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
   using dvd_add_triv_right_iff [of 2 n] by simp
 
 lemma even_Suc [simp]:
-  "even (Suc n) \<longleftrightarrow> odd n"
+  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
   by (induct n) auto
 
 lemma even_diff_nat [simp]:
   fixes m n :: nat
-  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
+  shows "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
 proof (cases "n \<le> m")
   case True
   then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
-  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
-  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
+  moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
+  ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
   then show ?thesis by auto
 next
   case False
   then show ?thesis by simp
 qed 
   
-lemma even_diff_iff [simp]:
-  fixes k l :: int
-  shows "even (k - l) \<longleftrightarrow> even (k + l)"
-  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
-
-lemma even_abs_add_iff [simp]:
-  fixes k l :: int
-  shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
-  by (cases "k \<ge> 0") (simp_all add: ac_simps)
-
-lemma even_add_abs_iff [simp]:
-  fixes k l :: int
-  shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
-  using even_abs_add_iff [of l k] by (simp add: ac_simps)
-
 instance nat :: semiring_parity
 proof
-  show "odd (1 :: nat)"
+  show "\<not> 2 dvd (1 :: nat)"
     by (rule notI, erule dvdE) simp
 next
   fix m n :: nat
-  assume "odd m"
-  moreover assume "odd n"
-  ultimately have *: "even (Suc m) \<and> even (Suc n)"
+  assume "\<not> 2 dvd m"
+  moreover assume "\<not> 2 dvd n"
+  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
     by simp
-  then have "even (Suc m + Suc n)"
+  then have "2 dvd (Suc m + Suc n)"
     by (blast intro: dvd_add)
   also have "Suc m + Suc n = m + n + 2"
     by simp
-  finally show "even (m + n)"
+  finally show "2 dvd (m + n)"
     using dvd_add_triv_right_iff [of 2 "m + n"] by simp
 next
   fix m n :: nat
-  assume *: "even (m * n)"
-  show "even m \<or> even n"
+  assume *: "2 dvd (m * n)"
+  show "2 dvd m \<or> 2 dvd n"
   proof (rule disjCI)
-    assume "odd n"
-    then have "even (Suc n)" by simp
+    assume "\<not> 2 dvd n"
+    then have "2 dvd (Suc n)" by simp
     then obtain r where "Suc n = 2 * r" ..
     moreover from * obtain s where "m * n = 2 * s" ..
     then have "2 * s + m = m * Suc n" by simp
     ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
     then have "m = 2 * (m * r - s)" by simp
-    then show "even m" ..
+    then show "2 dvd m" ..
   qed
 next
   fix n :: nat
-  assume "odd n"
+  assume "\<not> 2 dvd n"
   then show "\<exists>m. n = m + 1"
     by (cases n) simp_all
 qed
@@ -194,23 +179,38 @@
 lemma odd_pos: 
   "odd (n :: nat) \<Longrightarrow> 0 < n"
   by (auto elim: oddE)
-  
+
+lemma even_diff_iff [simp]:
+  fixes k l :: int
+  shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
+  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+
+lemma even_abs_add_iff [simp]:
+  fixes k l :: int
+  shows "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
+  by (cases "k \<ge> 0") (simp_all add: ac_simps)
+
+lemma even_add_abs_iff [simp]:
+  fixes k l :: int
+  shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
+  using even_abs_add_iff [of l k] by (simp add: ac_simps)
+
 instance int :: ring_parity
 proof
-  show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
+  show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
   fix k l :: int
-  assume "odd k"
-  moreover assume "odd l"
-  ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
+  assume "\<not> 2 dvd k"
+  moreover assume "\<not> 2 dvd l"
+  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
     by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
-  then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
+  then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
     by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
-  then show "even (k + l)"
+  then show "2 dvd (k + l)"
     by simp
 next
   fix k l :: int
-  assume "even (k * l)"
-  then show "even k \<or> even l"
+  assume "2 dvd (k * l)"
+  then show "2 dvd k \<or> 2 dvd l"
     by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
 next
   fix k :: int
@@ -352,4 +352,3 @@
 ]
 
 end
-
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Rat.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -162,9 +162,9 @@
   by transfer simp
 
 definition
-  divide_rat_def: "q / r = q * inverse (r::rat)"
+  divide_rat_def: "divide q r = q * inverse (r::rat)"
 
-lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
+lemma divide_rat [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
   by (simp add: divide_rat_def)
 
 instance proof
@@ -191,7 +191,7 @@
     by transfer simp
   { assume "q \<noteq> 0" thus "inverse q * q = 1"
     by transfer simp }
-  show "q / r = q * inverse r"
+  show "divide q r = q * inverse r"
     by (fact divide_rat_def)
   show "inverse 0 = (0::rat)"
     by transfer simp
@@ -1158,8 +1158,8 @@
         val {mant = i, exp = n} = Lexicon.read_float str;
         val exp = Syntax.const @{const_syntax Power.power};
         val ten = Numeral.mk_number_syntax 10;
-        val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;;
-      in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end;
+        val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;
+      in Syntax.const @{const_syntax Fields.inverse_divide} $ Numeral.mk_number_syntax i $ exp10 end;
 
     fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
       | float_tr [t as Const (str, _)] = mk_frac str
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Real.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -438,7 +438,7 @@
   "x - y = (x::real) + - y"
 
 definition
-  "x / y = (x::real) * inverse y"
+  "divide x y = (x::real) * inverse y"
 
 lemma add_Real:
   assumes X: "cauchy X" and Y: "cauchy Y"
@@ -501,7 +501,7 @@
     apply (rule_tac x=k in exI, clarify)
     apply (drule_tac x=n in spec, simp)
     done
-  show "a / b = a * inverse b"
+  show "divide a b = a * inverse b"
     by (rule divide_real_def)
   show "inverse (0::real) = 0"
     by transfer (simp add: realrel_def)
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Rings.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -558,6 +558,46 @@
   \end{itemize}
 *}
 
+class divide =
+  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+context semiring
+begin
+
+lemma [field_simps]:
+  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
+  by (rule distrib_left distrib_right)+
+
+end
+
+context ring
+begin
+
+lemma [field_simps]:
+  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
+  by (rule left_diff_distrib right_diff_distrib)+
+
+end
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+class semidom_divide = semidom + divide +
+  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+  assumes divide_zero [simp]: "divide a 0 = 0"
+begin
+
+lemma nonzero_mult_divide_cancel_left [simp]:
+  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
+  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
+
+end
+
+class idom_divide = idom + semidom_divide
+
 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/SMT_Examples/SMT_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Wed Jun 03 09:32:49 2015 +0200
@@ -4415,6 +4415,1608 @@
 (let ((@x128 (asserted $x127)))
 (unit-resolution @x128 @x546 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
+0f7f4a10f8a84029fd3a6efddc4408fa429b0cda 113 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x228 (mod x$ 2)))
+(let ((?x262 (* (- 1) ?x228)))
+(let ((?x31 (mod$ x$ 2)))
+(let ((?x263 (+ ?x31 ?x262)))
+(let (($x280 (>= ?x263 0)))
+(let (($x264 (= ?x263 0)))
+(let (($x205 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x181 (forall ((?v0 Int) (?v1 Int) )(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))))
+))
+(let ((?x136 (mod ?1 ?0)))
+(let ((?x93 (* (- 1) ?0)))
+(let ((?x90 (* (- 1) ?1)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?0 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?0 0)))
+(let ((?x175 (ite $x78 ?1 ?x170)))
+(let ((?x135 (mod$ ?1 ?0)))
+(let (($x178 (= ?x135 ?x175)))
+(let (($x142 (forall ((?v0 Int) (?v1 Int) )(let (($x78 (= ?v1 0)))
+(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x140)))))
+))
+(let (($x164 (forall ((?v0 Int) (?v1 Int) )(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let ((?x136 (mod ?v0 ?v1)))
+(let (($x79 (< 0 ?v1)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let (($x78 (= ?v1 0)))
+(let ((?x158 (ite $x78 ?v0 ?x155)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x158))))))))))))
+))
+(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
+(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
+(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
+(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
+(let (($x79 (< 0 ?0)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let ((?x158 (ite $x78 ?1 ?x155)))
+(let (($x161 (= ?x135 ?x158)))
+(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
+(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
+(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
+(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
+(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
+(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
+(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
+(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
+(let (($x270 (or (not $x205) $x264)))
+(let ((?x225 (* (- 1) 2)))
+(let ((?x224 (* (- 1) x$)))
+(let ((?x226 (mod ?x224 ?x225)))
+(let ((?x227 (* (- 1) ?x226)))
+(let (($x223 (<= 2 0)))
+(let ((?x229 (ite $x223 ?x227 ?x228)))
+(let (($x222 (= 2 0)))
+(let ((?x230 (ite $x222 x$ ?x229)))
+(let (($x231 (= ?x31 ?x230)))
+(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
+(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
+(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
+(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
+(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
+(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
+(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
+(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
+(let ((@x337 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
+(let (($x305 (>= ?x228 0)))
+(let (($x64 (>= ?x31 0)))
+(let (($x67 (not $x64)))
+(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
+(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
+(let ((?x32 (* 2 ?x31)))
+(let ((?x47 (+ 1 x$ ?x32)))
+(let (($x52 (<= (+ 1 x$) ?x47)))
+(let (($x55 (not $x52)))
+(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
+(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
+(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
+(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
+(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
+(let ((@x74 (mp (asserted $x36) @x73 $x67)))
+((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x337 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+fa5abc269019f00f5093218b287856c2a08c0adf 112 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x224 (mod x$ 2)))
+(let (($x318 (>= ?x224 2)))
+(let (($x319 (not $x318)))
+(let ((?x258 (* (- 1) ?x224)))
+(let ((?x29 (mod$ x$ 2)))
+(let ((?x259 (+ ?x29 ?x258)))
+(let (($x275 (<= ?x259 0)))
+(let (($x260 (= ?x259 0)))
+(let (($x201 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x177 (forall ((?v0 Int) (?v1 Int) )(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))))
+))
+(let ((?x132 (mod ?1 ?0)))
+(let ((?x89 (* (- 1) ?0)))
+(let ((?x86 (* (- 1) ?1)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?0 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?0 0)))
+(let ((?x171 (ite $x74 ?1 ?x166)))
+(let ((?x131 (mod$ ?1 ?0)))
+(let (($x174 (= ?x131 ?x171)))
+(let (($x138 (forall ((?v0 Int) (?v1 Int) )(let (($x74 (= ?v1 0)))
+(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x136)))))
+))
+(let (($x160 (forall ((?v0 Int) (?v1 Int) )(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let ((?x132 (mod ?v0 ?v1)))
+(let (($x75 (< 0 ?v1)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let (($x74 (= ?v1 0)))
+(let ((?x154 (ite $x74 ?v0 ?x151)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x154))))))))))))
+))
+(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
+(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
+(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
+(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
+(let (($x75 (< 0 ?0)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let ((?x154 (ite $x74 ?1 ?x151)))
+(let (($x157 (= ?x131 ?x154)))
+(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
+(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
+(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
+(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
+(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
+(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
+(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
+(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
+(let (($x266 (or (not $x201) $x260)))
+(let ((?x221 (* (- 1) 2)))
+(let ((?x220 (* (- 1) x$)))
+(let ((?x222 (mod ?x220 ?x221)))
+(let ((?x223 (* (- 1) ?x222)))
+(let (($x219 (<= 2 0)))
+(let ((?x225 (ite $x219 ?x223 ?x224)))
+(let (($x218 (= 2 0)))
+(let ((?x226 (ite $x218 x$ ?x225)))
+(let (($x227 (= ?x29 ?x226)))
+(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
+(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
+(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
+(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
+(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
+(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
+(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
+(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
+(let ((@x336 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
+(let (($x63 (>= ?x29 2)))
+(let ((?x37 (* 2 ?x29)))
+(let (($x56 (>= ?x37 3)))
+(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
+(let (($x49 (not $x46)))
+(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
+(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
+(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
+(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
+(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
+(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
+(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
+((_ th-lemma arith farkas -1 1 1) @x70 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+1880f0ed1cb3d1cfa006dff17f1b5553ce3a5158 236 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x410 (div n$ 2)))
+(let ((?x704 (* (- 1) ?x410)))
+(let ((?x381 (div n$ 4)))
+(let ((?x601 (* (- 2) ?x381)))
+(let ((?x329 (mod n$ 4)))
+(let ((?x363 (* (- 1) ?x329)))
+(let ((?x35 (mod$ n$ 4)))
+(let ((?x705 (+ n$ ?x35 ?x363 ?x601 ?x704)))
+(let (($x706 (>= ?x705 2)))
+(let ((?x39 (mod$ n$ 2)))
+(let (($x515 (>= ?x39 1)))
+(let (($x725 (not $x515)))
+(let (($x514 (<= ?x39 1)))
+(let ((?x519 (mod n$ 2)))
+(let ((?x534 (* (- 1) ?x519)))
+(let ((?x535 (+ ?x39 ?x534)))
+(let (($x408 (<= ?x535 0)))
+(let (($x490 (= ?x535 0)))
+(let (($x191 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x153 (forall ((?v0 Int) (?v1 Int) )(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))))
+))
+(let ((?x108 (mod ?1 ?0)))
+(let ((?x65 (* (- 1) ?0)))
+(let ((?x62 (* (- 1) ?1)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?0 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?0 0)))
+(let ((?x147 (ite $x50 ?1 ?x142)))
+(let ((?x107 (mod$ ?1 ?0)))
+(let (($x150 (= ?x107 ?x147)))
+(let (($x114 (forall ((?v0 Int) (?v1 Int) )(let (($x50 (= ?v1 0)))
+(let ((?x112 (ite $x50 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x112)))))
+))
+(let (($x136 (forall ((?v0 Int) (?v1 Int) )(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let ((?x108 (mod ?v0 ?v1)))
+(let (($x51 (< 0 ?v1)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let (($x50 (= ?v1 0)))
+(let ((?x130 (ite $x50 ?v0 ?x127)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x130))))))))))))
+))
+(let ((@x141 (monotonicity (rewrite (= (< 0 ?0) (not $x83))) (= (ite (< 0 ?0) ?x108 ?x122) (ite (not $x83) ?x108 ?x122)))))
+(let ((@x146 (trans @x141 (rewrite (= (ite (not $x83) ?x108 ?x122) ?x142)) (= (ite (< 0 ?0) ?x108 ?x122) ?x142))))
+(let ((@x149 (monotonicity @x146 (= (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122)) ?x147))))
+(let ((@x152 (monotonicity @x149 (= (= ?x107 (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122))) $x150))))
+(let (($x51 (< 0 ?0)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let ((?x130 (ite $x50 ?1 ?x127)))
+(let (($x133 (= ?x107 ?x130)))
+(let (($x134 (= (= ?x107 (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))))) $x133)))
+(let ((@x118 (monotonicity (rewrite (= (- ?1) ?x62)) (rewrite (= (- ?0) ?x65)) (= (mod (- ?1) (- ?0)) ?x116))))
+(let ((@x126 (trans (monotonicity @x118 (= (- (mod (- ?1) (- ?0))) (- ?x116))) (rewrite (= (- ?x116) ?x122)) (= (- (mod (- ?1) (- ?0))) ?x122))))
+(let ((@x129 (monotonicity @x126 (= (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))) ?x127))))
+(let ((@x132 (monotonicity @x129 (= (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0))))) ?x130))))
+(let ((@x157 (trans (quant-intro (monotonicity @x132 $x134) (= $x114 $x136)) (quant-intro @x152 (= $x136 $x153)) (= $x114 $x153))))
+(let ((@x168 (mp~ (mp (asserted $x114) @x157 $x153) (nnf-pos (refl (~ $x150 $x150)) (~ $x153 $x153)) $x153)))
+(let ((@x196 (mp @x168 (quant-intro (refl (= $x150 $x150)) (= $x153 $x191)) $x191)))
+(let (($x260 (not $x191)))
+(let (($x541 (or $x260 $x490)))
+(let ((?x211 (* (- 1) 2)))
+(let ((?x222 (* (- 1) n$)))
+(let ((?x517 (mod ?x222 ?x211)))
+(let ((?x518 (* (- 1) ?x517)))
+(let (($x209 (<= 2 0)))
+(let ((?x520 (ite $x209 ?x518 ?x519)))
+(let (($x208 (= 2 0)))
+(let ((?x521 (ite $x208 n$ ?x520)))
+(let (($x485 (= ?x39 ?x521)))
+(let ((@x593 (monotonicity (monotonicity (rewrite (= ?x211 (- 2))) (= ?x517 (mod ?x222 (- 2)))) (= ?x518 (* (- 1) (mod ?x222 (- 2)))))))
+(let ((@x221 (rewrite (= $x209 false))))
+(let ((@x596 (monotonicity @x221 @x593 (= ?x520 (ite false (* (- 1) (mod ?x222 (- 2))) ?x519)))))
+(let ((@x599 (trans @x596 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 2))) ?x519) ?x519)) (= ?x520 ?x519))))
+(let ((@x219 (rewrite (= $x208 false))))
+(let ((@x487 (trans (monotonicity @x219 @x599 (= ?x521 (ite false n$ ?x519))) (rewrite (= (ite false n$ ?x519) ?x519)) (= ?x521 ?x519))))
+(let ((@x538 (trans (monotonicity @x487 (= $x485 (= ?x39 ?x519))) (rewrite (= (= ?x39 ?x519) $x490)) (= $x485 $x490))))
+(let ((@x406 (trans (monotonicity @x538 (= (or $x260 $x485) $x541)) (rewrite (= $x541 $x541)) (= (or $x260 $x485) $x541))))
+(let ((@x407 (mp ((_ quant-inst n$ 2) (or $x260 $x485)) @x406 $x541)))
+(let ((@x715 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x408)) (unit-resolution @x407 @x196 $x490) $x408)))
+(let (($x303 (>= ?x519 2)))
+(let (($x304 (not $x303)))
+(let ((@x26 (true-axiom true)))
+(let ((@x722 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x514 $x303 (not $x408))) (unit-resolution ((_ th-lemma arith) (or false $x304)) @x26 $x304) @x715 $x514)))
+(let (($x41 (= ?x39 1)))
+(let (($x169 (not $x41)))
+(let ((?x42 (mod$ m$ 2)))
+(let (($x43 (= ?x42 1)))
+(let ((?x29 (+ n$ m$)))
+(let ((?x214 (mod ?x29 2)))
+(let ((?x253 (* (- 1) ?x214)))
+(let ((?x31 (mod$ ?x29 2)))
+(let ((?x603 (+ n$ m$ ?x31 ?x35 ?x253 (* (- 1) (div ?x29 2)) ?x363 ?x601 (* (- 1) (div m$ 2)))))
+(let (($x604 (>= ?x603 2)))
+(let (($x523 (>= ?x42 1)))
+(let (($x609 (not $x523)))
+(let (($x522 (<= ?x42 1)))
+(let ((?x439 (mod m$ 2)))
+(let ((?x466 (* (- 1) ?x439)))
+(let ((?x467 (+ ?x42 ?x466)))
+(let (($x482 (<= ?x467 0)))
+(let (($x468 (= ?x467 0)))
+(let (($x473 (or $x260 $x468)))
+(let ((?x440 (ite $x209 (* (- 1) (mod (* (- 1) m$) ?x211)) ?x439)))
+(let ((?x441 (ite $x208 m$ ?x440)))
+(let (($x442 (= ?x42 ?x441)))
+(let ((@x453 (rewrite (= (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439) ?x439))))
+(let (($x447 (= (* (- 1) (mod (* (- 1) m$) ?x211)) (* (- 1) (mod (* (- 1) m$) (- 2))))))
+(let ((@x229 (rewrite (= ?x211 (- 2)))))
+(let ((@x445 (monotonicity @x229 (= (mod (* (- 1) m$) ?x211) (mod (* (- 1) m$) (- 2))))))
+(let ((@x451 (monotonicity @x221 (monotonicity @x445 $x447) (= ?x440 (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439)))))
+(let ((@x458 (monotonicity @x219 (trans @x451 @x453 (= ?x440 ?x439)) (= ?x441 (ite false m$ ?x439)))))
+(let ((@x465 (monotonicity (trans @x458 (rewrite (= (ite false m$ ?x439) ?x439)) (= ?x441 ?x439)) (= $x442 (= ?x42 ?x439)))))
+(let ((@x477 (monotonicity (trans @x465 (rewrite (= (= ?x42 ?x439) $x468)) (= $x442 $x468)) (= (or $x260 $x442) $x473))))
+(let ((@x481 (mp ((_ quant-inst m$ 2) (or $x260 $x442)) (trans @x477 (rewrite (= $x473 $x473)) (= (or $x260 $x442) $x473)) $x473)))
+(let ((@x277 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) $x482)) (unit-resolution @x481 @x196 $x468) $x482)))
+(let ((@x386 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x439 2)))) @x26 (not (>= ?x439 2)))))
+(let ((@x384 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x522 (>= ?x439 2) (not $x482))) @x386 @x277 $x522)))
+(let ((@x564 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x43 (not $x522) $x609)) (hypothesis (not $x43)) (or (not $x522) $x609))))
+(let ((?x272 (div ?x29 2)))
+(let ((?x288 (* (- 2) ?x272)))
+(let ((?x289 (+ n$ m$ ?x253 ?x288)))
+(let (($x294 (<= ?x289 0)))
+(let (($x287 (= ?x289 0)))
+(let ((@x617 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x294)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x294)))
+(let (($x433 (<= ?x31 0)))
+(let (($x32 (= ?x31 0)))
+(let ((@x33 (asserted $x32)))
+(let ((?x254 (+ ?x31 ?x253)))
+(let (($x270 (<= ?x254 0)))
+(let (($x255 (= ?x254 0)))
+(let (($x261 (or $x260 $x255)))
+(let ((?x215 (ite $x209 (* (- 1) (mod (* (- 1) ?x29) ?x211)) ?x214)))
+(let ((?x216 (ite $x208 ?x29 ?x215)))
+(let (($x217 (= ?x31 ?x216)))
+(let (($x239 (= (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214) ?x214)))
+(let (($x237 (= ?x215 (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214))))
+(let (($x234 (= (* (- 1) (mod (* (- 1) ?x29) ?x211)) (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x232 (monotonicity (rewrite (= (* (- 1) ?x29) (+ ?x222 (* (- 1) m$)))) @x229 (= (mod (* (- 1) ?x29) ?x211) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x242 (trans (monotonicity @x221 (monotonicity @x232 $x234) $x237) (rewrite $x239) (= ?x215 ?x214))))
+(let ((@x249 (trans (monotonicity @x219 @x242 (= ?x216 (ite false ?x29 ?x214))) (rewrite (= (ite false ?x29 ?x214) ?x214)) (= ?x216 ?x214))))
+(let ((@x259 (trans (monotonicity @x249 (= $x217 (= ?x31 ?x214))) (rewrite (= (= ?x31 ?x214) $x255)) (= $x217 $x255))))
+(let ((@x268 (trans (monotonicity @x259 (= (or $x260 $x217) $x261)) (rewrite (= $x261 $x261)) (= (or $x260 $x217) $x261))))
+(let ((@x269 (mp ((_ quant-inst (+ n$ m$) 2) (or $x260 $x217)) @x268 $x261)))
+(let ((@x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x270)) (unit-resolution @x269 @x196 $x255) $x270)))
+(let ((?x498 (+ m$ ?x466 (* (- 2) (div m$ 2)))))
+(let (($x496 (= ?x498 0)))
+(let ((@x633 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (<= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (<= ?x498 0))))
+(let ((?x397 (* (- 4) ?x381)))
+(let ((?x398 (+ n$ ?x363 ?x397)))
+(let (($x403 (<= ?x398 0)))
+(let (($x396 (= ?x398 0)))
+(let ((@x640 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x403)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x403)))
+(let ((?x364 (+ ?x35 ?x363)))
+(let (($x379 (<= ?x364 0)))
+(let (($x365 (= ?x364 0)))
+(let (($x370 (or $x260 $x365)))
+(let ((?x330 (ite (<= 4 0) (* (- 1) (mod ?x222 (* (- 1) 4))) ?x329)))
+(let ((?x331 (ite (= 4 0) n$ ?x330)))
+(let (($x332 (= ?x35 ?x331)))
+(let ((@x342 (monotonicity (rewrite (= (* (- 1) 4) (- 4))) (= (mod ?x222 (* (- 1) 4)) (mod ?x222 (- 4))))))
+(let ((@x345 (monotonicity @x342 (= (* (- 1) (mod ?x222 (* (- 1) 4))) (* (- 1) (mod ?x222 (- 4)))))))
+(let ((@x348 (monotonicity (rewrite (= (<= 4 0) false)) @x345 (= ?x330 (ite false (* (- 1) (mod ?x222 (- 4))) ?x329)))))
+(let ((@x352 (trans @x348 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 4))) ?x329) ?x329)) (= ?x330 ?x329))))
+(let ((@x355 (monotonicity (rewrite (= (= 4 0) false)) @x352 (= ?x331 (ite false n$ ?x329)))))
+(let ((@x362 (monotonicity (trans @x355 (rewrite (= (ite false n$ ?x329) ?x329)) (= ?x331 ?x329)) (= $x332 (= ?x35 ?x329)))))
+(let ((@x374 (monotonicity (trans @x362 (rewrite (= (= ?x35 ?x329) $x365)) (= $x332 $x365)) (= (or $x260 $x332) $x370))))
+(let ((@x378 (mp ((_ quant-inst n$ 4) (or $x260 $x332)) (trans @x374 (rewrite (= $x370 $x370)) (= (or $x260 $x332) $x370)) $x370)))
+(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x379)) (unit-resolution @x378 @x196 $x365) $x379)))
+(let (($x435 (<= ?x35 3)))
+(let (($x37 (= ?x35 3)))
+(let ((@x38 (asserted $x37)))
+(let ((@x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) (>= ?x467 0))) (unit-resolution @x481 @x196 $x468) (>= ?x467 0))))
+(let ((@x656 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1 1 1 1) @x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x604) @x645 @x640 @x633 @x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x433)) @x33 $x433) @x617 (hypothesis $x609) false)))
+(let ((@x565 (unit-resolution (lemma @x656 (or (not $x604) $x523)) (unit-resolution @x564 @x384 $x609) (not $x604))))
+(let (($x295 (>= ?x289 0)))
+(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x295)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x295)))
+(let (($x434 (>= ?x31 0)))
+(let (($x271 (>= ?x254 0)))
+(let ((@x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x271)) (unit-resolution @x269 @x196 $x255) $x271)))
+(let ((@x537 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (>= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (>= ?x498 0))))
+(let ((@x549 (unit-resolution ((_ th-lemma arith) (or false (>= ?x439 0))) @x26 (>= ?x439 0))))
+(let (($x404 (>= ?x398 0)))
+(let ((@x552 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x404)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x404)))
+(let (($x380 (>= ?x364 0)))
+(let ((@x273 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x380)) (unit-resolution @x378 @x196 $x365) $x380)))
+(let (($x436 (>= ?x35 3)))
+(let ((@x545 ((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x273 @x552 @x549 @x537 @x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x434)) @x33 $x434) @x566 @x565 false)))
+(let (($x171 (or $x169 (not $x43))))
+(let ((@x177 (monotonicity (rewrite (= (and $x41 $x43) (not $x171))) (= (not (and $x41 $x43)) (not (not $x171))))))
+(let ((@x181 (trans @x177 (rewrite (= (not (not $x171)) $x171)) (= (not (and $x41 $x43)) $x171))))
+(let ((@x182 (mp (asserted (not (and $x41 $x43))) @x181 $x171)))
+(let ((@x729 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x41 (not $x514) $x725)) (unit-resolution @x182 (lemma @x545 $x43) $x169) (or (not $x514) $x725))))
+(let ((?x420 (* (- 2) ?x410)))
+(let ((?x421 (+ n$ ?x420 ?x534)))
+(let (($x426 (<= ?x421 0)))
+(let (($x419 (= ?x421 0)))
+(let ((@x737 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x426)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x426)))
+(let (($x409 (>= ?x535 0)))
+(let ((@x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x409)) (unit-resolution @x407 @x196 $x490) $x409)))
+(let ((@x742 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1) @x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x706) @x640 @x737 @x645 (unit-resolution @x729 @x722 $x725) false)))
+(let (($x427 (>= ?x421 0)))
+(let ((@x584 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x427)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x427)))
+(let (($x542 (>= ?x519 0)))
+((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x552 (unit-resolution ((_ th-lemma arith) (or false $x542)) @x26 $x542) @x584 @x273 (lemma @x742 (not $x706)) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+f6a4c40290fd6742c0b08a1fe90b3664e90c2143 336 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x99 (mod$ l$ 2)))
+(let ((?x96 (map$ uu$ xs$)))
+(let ((?x97 (eval_dioph$ ks$ ?x96)))
+(let ((?x98 (mod$ ?x97 2)))
+(let (($x100 (= ?x98 ?x99)))
+(let ((?x93 (eval_dioph$ ks$ xs$)))
+(let (($x95 (= ?x93 l$)))
+(let ((?x110 (* (- 1) ?x97)))
+(let ((?x111 (+ l$ ?x110)))
+(let ((?x114 (divide$ ?x111 2)))
+(let ((?x101 (map$ uua$ xs$)))
+(let ((?x102 (eval_dioph$ ks$ ?x101)))
+(let (($x117 (= ?x102 ?x114)))
+(let (($x282 (not $x117)))
+(let (($x281 (not $x100)))
+(let (($x283 (or $x281 $x282)))
+(let ((?x744 (div ?x93 2)))
+(let ((?x970 (* (- 1) ?x744)))
+(let ((?x699 (mod ?x93 2)))
+(let ((?x726 (* (- 1) ?x699)))
+(let ((?x516 (mod l$ 2)))
+(let ((?x543 (* (- 1) ?x516)))
+(let (($x972 (>= (+ l$ ?x99 ?x543 (* (- 1) (div l$ 2)) ?x726 ?x970) 1)))
+(let ((?x369 (* (- 1) l$)))
+(let ((?x693 (+ ?x93 ?x369)))
+(let (($x695 (>= ?x693 0)))
+(let (($x861 (not $x695)))
+(let (($x694 (<= ?x693 0)))
+(let ((?x686 (+ ?x102 (* (- 1) ?x114))))
+(let (($x687 (<= ?x686 0)))
+(let (($x284 (not $x283)))
+(let ((@x466 (hypothesis $x284)))
+(let ((@x856 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x687)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x687)))
+(let ((?x437 (+ l$ ?x110 (* (- 2) (div ?x111 2)) (* (- 1) (mod (+ l$ ?x97) 2)))))
+(let (($x443 (>= ?x437 0)))
+(let (($x434 (= ?x437 0)))
+(let ((@x26 (true-axiom true)))
+(let ((@x793 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
+(let ((?x501 (* (- 2) ?x102)))
+(let ((?x502 (+ ?x93 ?x110 ?x501)))
+(let (($x509 (<= ?x502 0)))
+(let (($x503 (= ?x502 0)))
+(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
+))
+(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))))
+))
+(let ((?x45 (eval_dioph$ ?1 ?0)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
+(let (($x79 (= ?x83 0)))
+(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
+(= ?x56 ?x45)))))
+))
+(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x66 (+ ?x48 ?x60)))
+(= ?x66 ?x45)))))))
+))
+(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
+(let ((?x66 (+ ?x48 ?x60)))
+(let (($x71 (= ?x66 ?x45)))
+(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
+(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
+(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
+(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
+(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
+(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
+(let (($x507 (or (not $x304) $x503)))
+(let ((@x508 ((_ quant-inst ks$ xs$) $x507)))
+(let ((@x800 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x509)) (unit-resolution @x508 @x309 $x503) $x509)))
+(let ((?x396 (+ ?x114 (* (- 1) (div ?x111 2)))))
+(let (($x413 (<= ?x396 0)))
+(let (($x397 (= ?x396 0)))
+(let (($x311 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) )))
+))
+(let (($x193 (forall ((?v0 Int) (?v1 Int) )(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))))
+))
+(let ((?x145 (div ?1 ?0)))
+(let ((?x157 (* (- 1) ?0)))
+(let ((?x154 (* (- 1) ?1)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?0 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?0 0)))
+(let ((?x141 (divide$ ?1 ?0)))
+(let (($x190 (= ?x141 (ite $x143 0 ?x182))))
+(let (($x152 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x150)))))
+))
+(let (($x172 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let ((?x145 (div ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let (($x143 (= ?v1 0)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x166)))))))))))
+))
+(let (($x144 (< 0 ?0)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
+(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) ?x182)) (= ?x163 ?x182))))
+(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 ?x182))) (= (= ?x141 ?x166) $x190))))
+(let (($x169 (= ?x141 ?x166)))
+(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
+(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
+(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
+(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
+(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
+(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
+(let (($x403 (or (not $x311) $x397)))
+(let ((?x361 (div ?x111 2)))
+(let (($x357 (<= 2 0)))
+(let ((?x362 (ite $x357 (div (* (- 1) ?x111) (* (- 1) 2)) ?x361)))
+(let (($x356 (= 2 0)))
+(let ((?x363 (ite $x356 0 ?x362)))
+(let (($x364 (= ?x114 ?x363)))
+(let ((@x374 (rewrite (= (* (- 1) 2) (- 2)))))
+(let ((@x377 (monotonicity (rewrite (= (* (- 1) ?x111) (+ ?x369 ?x97))) @x374 (= (div (* (- 1) ?x111) (* (- 1) 2)) (div (+ ?x369 ?x97) (- 2))))))
+(let ((@x368 (rewrite (= $x357 false))))
+(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
+(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
+(let ((@x366 (rewrite (= $x356 false))))
+(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
+(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
+(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
+(let ((@x802 (unit-resolution (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403) @x316 $x397)))
+(let ((?x425 (mod (+ l$ ?x97) 2)))
+(let (($x465 (>= ?x425 0)))
+(let ((@x810 ((_ th-lemma arith farkas 1 -2 -2 -1 1 1) (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (hypothesis $x687) @x800 (hypothesis (not $x694)) @x793 false)))
+(let (($x134 (not $x95)))
+(let (($x290 (= $x95 $x283)))
+(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
+(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
+(let (($x120 (and $x100 $x117)))
+(let (($x135 (= $x134 $x120)))
+(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
+(let (($x108 (not $x107)))
+(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
+(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
+(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
+(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
+(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
+(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
+(let ((@x898 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 (not $x694) $x861)) (unit-resolution @x344 @x466 $x134) (or (not $x694) $x861))))
+(let ((@x899 (unit-resolution @x898 (unit-resolution (lemma @x810 (or $x694 (not $x687))) @x856 $x694) $x861)))
+(let ((?x544 (+ ?x99 ?x543)))
+(let (($x561 (>= ?x544 0)))
+(let (($x545 (= ?x544 0)))
+(let (($x318 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x245 (forall ((?v0 Int) (?v1 Int) )(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))))
+))
+(let ((?x200 (mod ?1 ?0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let ((?x239 (ite $x143 ?1 ?x234)))
+(let ((?x199 (mod$ ?1 ?0)))
+(let (($x242 (= ?x199 ?x239)))
+(let (($x206 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x204)))))
+))
+(let (($x228 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x200 (mod ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let (($x143 (= ?v1 0)))
+(let ((?x222 (ite $x143 ?v0 ?x219)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x222))))))))))))
+))
+(let ((@x233 (monotonicity (rewrite (= $x144 (not $x175))) (= (ite $x144 ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
+(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite $x144 ?x200 ?x214) ?x234))))
+(let ((@x244 (monotonicity (monotonicity @x238 (= (ite $x143 ?1 (ite $x144 ?x200 ?x214)) ?x239)) (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 ?x214))) $x242))))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let ((?x222 (ite $x143 ?1 ?x219)))
+(let (($x225 (= ?x199 ?x222)))
+(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
+(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
+(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
+(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
+(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
+(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
+(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
+(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
+(let (($x550 (not $x318)))
+(let (($x551 (or $x550 $x545)))
+(let ((?x359 (* (- 1) 2)))
+(let ((?x511 (mod ?x369 ?x359)))
+(let ((?x512 (* (- 1) ?x511)))
+(let ((?x517 (ite $x357 ?x512 ?x516)))
+(let ((?x518 (ite $x356 l$ ?x517)))
+(let (($x519 (= ?x99 ?x518)))
+(let ((@x525 (monotonicity (monotonicity @x374 (= ?x511 (mod ?x369 (- 2)))) (= ?x512 (* (- 1) (mod ?x369 (- 2)))))))
+(let ((@x528 (monotonicity @x368 @x525 (= ?x517 (ite false (* (- 1) (mod ?x369 (- 2))) ?x516)))))
+(let ((@x532 (trans @x528 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x516) ?x516)) (= ?x517 ?x516))))
+(let ((@x539 (trans (monotonicity @x366 @x532 (= ?x518 (ite false l$ ?x516))) (rewrite (= (ite false l$ ?x516) ?x516)) (= ?x518 ?x516))))
+(let ((@x549 (trans (monotonicity @x539 (= $x519 (= ?x99 ?x516))) (rewrite (= (= ?x99 ?x516) $x545)) (= $x519 $x545))))
+(let ((@x558 (trans (monotonicity @x549 (= (or $x550 $x519) $x551)) (rewrite (= $x551 $x551)) (= (or $x550 $x519) $x551))))
+(let ((@x559 (mp ((_ quant-inst l$ 2) (or $x550 $x519)) @x558 $x551)))
+(let ((@x902 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x561)) (unit-resolution @x559 @x323 $x545) $x561)))
+(let ((?x757 (* (- 2) ?x744)))
+(let ((?x758 (+ ?x93 ?x726 ?x757)))
+(let (($x764 (>= ?x758 0)))
+(let (($x756 (= ?x758 0)))
+(let ((@x872 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x764)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x764)))
+(let ((?x562 (div l$ 2)))
+(let ((?x575 (* (- 2) ?x562)))
+(let ((?x576 (+ l$ ?x543 ?x575)))
+(let (($x582 (>= ?x576 0)))
+(let (($x574 (= ?x576 0)))
+(let ((@x880 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x582)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x582)))
+(let ((?x504 (mod$ ?x93 2)))
+(let ((?x727 (+ ?x504 ?x726)))
+(let (($x728 (= ?x727 0)))
+(let (($x733 (or $x550 $x728)))
+(let ((?x696 (* (- 1) ?x93)))
+(let ((?x697 (mod ?x696 ?x359)))
+(let ((?x698 (* (- 1) ?x697)))
+(let ((?x700 (ite $x357 ?x698 ?x699)))
+(let ((?x701 (ite $x356 ?x93 ?x700)))
+(let (($x702 (= ?x504 ?x701)))
+(let ((@x708 (monotonicity (monotonicity @x374 (= ?x697 (mod ?x696 (- 2)))) (= ?x698 (* (- 1) (mod ?x696 (- 2)))))))
+(let ((@x711 (monotonicity @x368 @x708 (= ?x700 (ite false (* (- 1) (mod ?x696 (- 2))) ?x699)))))
+(let ((@x715 (trans @x711 (rewrite (= (ite false (* (- 1) (mod ?x696 (- 2))) ?x699) ?x699)) (= ?x700 ?x699))))
+(let ((@x722 (trans (monotonicity @x366 @x715 (= ?x701 (ite false ?x93 ?x699))) (rewrite (= (ite false ?x93 ?x699) ?x699)) (= ?x701 ?x699))))
+(let ((@x732 (trans (monotonicity @x722 (= $x702 (= ?x504 ?x699))) (rewrite (= (= ?x504 ?x699) $x728)) (= $x702 $x728))))
+(let ((@x740 (trans (monotonicity @x732 (= (or $x550 $x702) $x733)) (rewrite (= $x733 $x733)) (= (or $x550 $x702) $x733))))
+(let ((@x427 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (>= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (>= ?x727 0))))
+(let ((?x783 (* (- 1) ?x504)))
+(let ((?x784 (+ ?x99 ?x783)))
+(let (($x786 (>= ?x784 0)))
+(let (($x782 (= ?x99 ?x504)))
+(let (($x821 (= ?x98 ?x504)))
+(let (($x505 (= ?x504 ?x98)))
+(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) )))
+))
+(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
+))
+(let (($x50 (= (mod$ ?x45 2) (mod$ ?x48 2))))
+(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
+(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
+(let (($x514 (or (not $x297) $x505)))
+(let ((@x515 ((_ quant-inst ks$ xs$) $x514)))
+(let ((@x824 (symm (unit-resolution (def-axiom (or $x283 $x100)) @x466 $x100) (= ?x99 ?x98))))
+(let ((@x939 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x786)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x786)))
+(let (($x785 (<= ?x784 0)))
+(let ((@x887 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x785)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x785)))
+(let (($x688 (>= ?x686 0)))
+(let ((@x855 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x688)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x688)))
+(let ((@x979 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x425 2)))) @x26 (not (>= ?x425 2)))))
+(let (($x560 (<= ?x544 0)))
+(let ((@x461 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x560)) (unit-resolution @x559 @x323 $x545) $x560)))
+(let (($x763 (<= ?x758 0)))
+(let ((@x658 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x763)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x763)))
+(let (($x581 (<= ?x576 0)))
+(let ((@x986 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x581)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x581)))
+(let ((@x989 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (<= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (<= ?x727 0))))
+(let (($x510 (>= ?x502 0)))
+(let ((@x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x510)) (unit-resolution @x508 @x309 $x503) $x510)))
+(let ((@x998 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) (>= ?x396 0))) @x802 (>= ?x396 0))))
+(let ((@x1001 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) (<= ?x437 0))) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) (<= ?x437 0))))
+(let ((@x1002 ((_ th-lemma arith farkas 1 -2 -2 -1 -2 1 1 1 1 1 1) @x1001 @x998 (hypothesis $x688) @x994 (hypothesis $x972) (hypothesis $x785) @x989 @x986 @x658 @x461 @x979 false)))
+(let ((@x474 (unit-resolution (lemma @x1002 (or (not $x972) (not $x688) (not $x785))) @x855 @x887 (not $x972))))
+(let ((@x941 (unit-resolution @x474 ((_ th-lemma arith) @x939 @x427 @x880 @x872 @x902 @x899 $x972) false)))
+(let ((@x942 (lemma @x941 $x283)))
+(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
+(let ((@x679 (unit-resolution @x340 @x942 $x95)))
+(let ((@x889 (trans (symm (unit-resolution @x515 @x302 $x505) $x821) (monotonicity @x679 (= ?x504 ?x99)) $x100)))
+(let (($x811 (not $x687)))
+(let ((@x845 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x688 (not $x413) (not $x465) (not $x443) (not $x509) $x861))))
+(let ((@x892 (unit-resolution @x845 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x695)) @x679 $x695) @x793 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x800 $x688)))
+(let ((@x935 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x811 (not $x688))) (hypothesis $x282) (or $x811 (not $x688)))))
+(let ((@x955 ((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x935 @x892 $x811) @x998 @x1001 @x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x694)) @x679 $x694) @x979 false)))
+(let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281)))
+(unit-resolution @x472 @x889 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+0f7f4a10f8a84029fd3a6efddc4408fa429b0cda 113 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x228 (mod x$ 2)))
+(let ((?x262 (* (- 1) ?x228)))
+(let ((?x31 (mod$ x$ 2)))
+(let ((?x263 (+ ?x31 ?x262)))
+(let (($x280 (>= ?x263 0)))
+(let (($x264 (= ?x263 0)))
+(let (($x205 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x181 (forall ((?v0 Int) (?v1 Int) )(let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))))
+))
+(let ((?x136 (mod ?1 ?0)))
+(let ((?x93 (* (- 1) ?0)))
+(let ((?x90 (* (- 1) ?1)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?0 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?0 0)))
+(let ((?x175 (ite $x78 ?1 ?x170)))
+(let ((?x135 (mod$ ?1 ?0)))
+(let (($x178 (= ?x135 ?x175)))
+(let (($x142 (forall ((?v0 Int) (?v1 Int) )(let (($x78 (= ?v1 0)))
+(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x140)))))
+))
+(let (($x164 (forall ((?v0 Int) (?v1 Int) )(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let ((?x136 (mod ?v0 ?v1)))
+(let (($x79 (< 0 ?v1)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let (($x78 (= ?v1 0)))
+(let ((?x158 (ite $x78 ?v0 ?x155)))
+(let ((?x135 (mod$ ?v0 ?v1)))
+(= ?x135 ?x158))))))))))))
+))
+(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
+(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
+(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
+(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
+(let (($x79 (< 0 ?0)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let ((?x158 (ite $x78 ?1 ?x155)))
+(let (($x161 (= ?x135 ?x158)))
+(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
+(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
+(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
+(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
+(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
+(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
+(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
+(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
+(let (($x270 (or (not $x205) $x264)))
+(let ((?x225 (* (- 1) 2)))
+(let ((?x224 (* (- 1) x$)))
+(let ((?x226 (mod ?x224 ?x225)))
+(let ((?x227 (* (- 1) ?x226)))
+(let (($x223 (<= 2 0)))
+(let ((?x229 (ite $x223 ?x227 ?x228)))
+(let (($x222 (= 2 0)))
+(let ((?x230 (ite $x222 x$ ?x229)))
+(let (($x231 (= ?x31 ?x230)))
+(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
+(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
+(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
+(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
+(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
+(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
+(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
+(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
+(let ((@x337 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
+(let (($x305 (>= ?x228 0)))
+(let (($x64 (>= ?x31 0)))
+(let (($x67 (not $x64)))
+(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
+(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
+(let ((?x32 (* 2 ?x31)))
+(let ((?x47 (+ 1 x$ ?x32)))
+(let (($x52 (<= (+ 1 x$) ?x47)))
+(let (($x55 (not $x52)))
+(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
+(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
+(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
+(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
+(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
+(let ((@x74 (mp (asserted $x36) @x73 $x67)))
+((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x337 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+fa5abc269019f00f5093218b287856c2a08c0adf 112 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x224 (mod x$ 2)))
+(let (($x318 (>= ?x224 2)))
+(let (($x319 (not $x318)))
+(let ((?x258 (* (- 1) ?x224)))
+(let ((?x29 (mod$ x$ 2)))
+(let ((?x259 (+ ?x29 ?x258)))
+(let (($x275 (<= ?x259 0)))
+(let (($x260 (= ?x259 0)))
+(let (($x201 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x177 (forall ((?v0 Int) (?v1 Int) )(let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))))
+))
+(let ((?x132 (mod ?1 ?0)))
+(let ((?x89 (* (- 1) ?0)))
+(let ((?x86 (* (- 1) ?1)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?0 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?0 0)))
+(let ((?x171 (ite $x74 ?1 ?x166)))
+(let ((?x131 (mod$ ?1 ?0)))
+(let (($x174 (= ?x131 ?x171)))
+(let (($x138 (forall ((?v0 Int) (?v1 Int) )(let (($x74 (= ?v1 0)))
+(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x136)))))
+))
+(let (($x160 (forall ((?v0 Int) (?v1 Int) )(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let ((?x132 (mod ?v0 ?v1)))
+(let (($x75 (< 0 ?v1)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let (($x74 (= ?v1 0)))
+(let ((?x154 (ite $x74 ?v0 ?x151)))
+(let ((?x131 (mod$ ?v0 ?v1)))
+(= ?x131 ?x154))))))))))))
+))
+(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
+(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
+(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
+(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
+(let (($x75 (< 0 ?0)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let ((?x154 (ite $x74 ?1 ?x151)))
+(let (($x157 (= ?x131 ?x154)))
+(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
+(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
+(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
+(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
+(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
+(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
+(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
+(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
+(let (($x266 (or (not $x201) $x260)))
+(let ((?x221 (* (- 1) 2)))
+(let ((?x220 (* (- 1) x$)))
+(let ((?x222 (mod ?x220 ?x221)))
+(let ((?x223 (* (- 1) ?x222)))
+(let (($x219 (<= 2 0)))
+(let ((?x225 (ite $x219 ?x223 ?x224)))
+(let (($x218 (= 2 0)))
+(let ((?x226 (ite $x218 x$ ?x225)))
+(let (($x227 (= ?x29 ?x226)))
+(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
+(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
+(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
+(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
+(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
+(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
+(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
+(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
+(let ((@x336 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
+(let (($x63 (>= ?x29 2)))
+(let ((?x37 (* 2 ?x29)))
+(let (($x56 (>= ?x37 3)))
+(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
+(let (($x49 (not $x46)))
+(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
+(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
+(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
+(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
+(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
+(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
+(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
+((_ th-lemma arith farkas -1 1 1) @x70 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+1880f0ed1cb3d1cfa006dff17f1b5553ce3a5158 236 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x410 (div n$ 2)))
+(let ((?x704 (* (- 1) ?x410)))
+(let ((?x381 (div n$ 4)))
+(let ((?x601 (* (- 2) ?x381)))
+(let ((?x329 (mod n$ 4)))
+(let ((?x363 (* (- 1) ?x329)))
+(let ((?x35 (mod$ n$ 4)))
+(let ((?x705 (+ n$ ?x35 ?x363 ?x601 ?x704)))
+(let (($x706 (>= ?x705 2)))
+(let ((?x39 (mod$ n$ 2)))
+(let (($x515 (>= ?x39 1)))
+(let (($x725 (not $x515)))
+(let (($x514 (<= ?x39 1)))
+(let ((?x519 (mod n$ 2)))
+(let ((?x534 (* (- 1) ?x519)))
+(let ((?x535 (+ ?x39 ?x534)))
+(let (($x408 (<= ?x535 0)))
+(let (($x490 (= ?x535 0)))
+(let (($x191 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x153 (forall ((?v0 Int) (?v1 Int) )(let ((?x108 (mod ?v0 ?v1)))
+(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?v1 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?v1 0)))
+(let ((?x147 (ite $x50 ?v0 ?x142)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x147))))))))))))
+))
+(let ((?x108 (mod ?1 ?0)))
+(let ((?x65 (* (- 1) ?0)))
+(let ((?x62 (* (- 1) ?1)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let (($x83 (<= ?0 0)))
+(let ((?x142 (ite $x83 ?x122 ?x108)))
+(let (($x50 (= ?0 0)))
+(let ((?x147 (ite $x50 ?1 ?x142)))
+(let ((?x107 (mod$ ?1 ?0)))
+(let (($x150 (= ?x107 ?x147)))
+(let (($x114 (forall ((?v0 Int) (?v1 Int) )(let (($x50 (= ?v1 0)))
+(let ((?x112 (ite $x50 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x112)))))
+))
+(let (($x136 (forall ((?v0 Int) (?v1 Int) )(let ((?x65 (* (- 1) ?v1)))
+(let ((?x62 (* (- 1) ?v0)))
+(let ((?x116 (mod ?x62 ?x65)))
+(let ((?x122 (* (- 1) ?x116)))
+(let ((?x108 (mod ?v0 ?v1)))
+(let (($x51 (< 0 ?v1)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let (($x50 (= ?v1 0)))
+(let ((?x130 (ite $x50 ?v0 ?x127)))
+(let ((?x107 (mod$ ?v0 ?v1)))
+(= ?x107 ?x130))))))))))))
+))
+(let ((@x141 (monotonicity (rewrite (= (< 0 ?0) (not $x83))) (= (ite (< 0 ?0) ?x108 ?x122) (ite (not $x83) ?x108 ?x122)))))
+(let ((@x146 (trans @x141 (rewrite (= (ite (not $x83) ?x108 ?x122) ?x142)) (= (ite (< 0 ?0) ?x108 ?x122) ?x142))))
+(let ((@x149 (monotonicity @x146 (= (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122)) ?x147))))
+(let ((@x152 (monotonicity @x149 (= (= ?x107 (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122))) $x150))))
+(let (($x51 (< 0 ?0)))
+(let ((?x127 (ite $x51 ?x108 ?x122)))
+(let ((?x130 (ite $x50 ?1 ?x127)))
+(let (($x133 (= ?x107 ?x130)))
+(let (($x134 (= (= ?x107 (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))))) $x133)))
+(let ((@x118 (monotonicity (rewrite (= (- ?1) ?x62)) (rewrite (= (- ?0) ?x65)) (= (mod (- ?1) (- ?0)) ?x116))))
+(let ((@x126 (trans (monotonicity @x118 (= (- (mod (- ?1) (- ?0))) (- ?x116))) (rewrite (= (- ?x116) ?x122)) (= (- (mod (- ?1) (- ?0))) ?x122))))
+(let ((@x129 (monotonicity @x126 (= (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))) ?x127))))
+(let ((@x132 (monotonicity @x129 (= (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0))))) ?x130))))
+(let ((@x157 (trans (quant-intro (monotonicity @x132 $x134) (= $x114 $x136)) (quant-intro @x152 (= $x136 $x153)) (= $x114 $x153))))
+(let ((@x168 (mp~ (mp (asserted $x114) @x157 $x153) (nnf-pos (refl (~ $x150 $x150)) (~ $x153 $x153)) $x153)))
+(let ((@x196 (mp @x168 (quant-intro (refl (= $x150 $x150)) (= $x153 $x191)) $x191)))
+(let (($x260 (not $x191)))
+(let (($x541 (or $x260 $x490)))
+(let ((?x211 (* (- 1) 2)))
+(let ((?x222 (* (- 1) n$)))
+(let ((?x517 (mod ?x222 ?x211)))
+(let ((?x518 (* (- 1) ?x517)))
+(let (($x209 (<= 2 0)))
+(let ((?x520 (ite $x209 ?x518 ?x519)))
+(let (($x208 (= 2 0)))
+(let ((?x521 (ite $x208 n$ ?x520)))
+(let (($x485 (= ?x39 ?x521)))
+(let ((@x593 (monotonicity (monotonicity (rewrite (= ?x211 (- 2))) (= ?x517 (mod ?x222 (- 2)))) (= ?x518 (* (- 1) (mod ?x222 (- 2)))))))
+(let ((@x221 (rewrite (= $x209 false))))
+(let ((@x596 (monotonicity @x221 @x593 (= ?x520 (ite false (* (- 1) (mod ?x222 (- 2))) ?x519)))))
+(let ((@x599 (trans @x596 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 2))) ?x519) ?x519)) (= ?x520 ?x519))))
+(let ((@x219 (rewrite (= $x208 false))))
+(let ((@x487 (trans (monotonicity @x219 @x599 (= ?x521 (ite false n$ ?x519))) (rewrite (= (ite false n$ ?x519) ?x519)) (= ?x521 ?x519))))
+(let ((@x538 (trans (monotonicity @x487 (= $x485 (= ?x39 ?x519))) (rewrite (= (= ?x39 ?x519) $x490)) (= $x485 $x490))))
+(let ((@x406 (trans (monotonicity @x538 (= (or $x260 $x485) $x541)) (rewrite (= $x541 $x541)) (= (or $x260 $x485) $x541))))
+(let ((@x407 (mp ((_ quant-inst n$ 2) (or $x260 $x485)) @x406 $x541)))
+(let ((@x715 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x408)) (unit-resolution @x407 @x196 $x490) $x408)))
+(let (($x303 (>= ?x519 2)))
+(let (($x304 (not $x303)))
+(let ((@x26 (true-axiom true)))
+(let ((@x722 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x514 $x303 (not $x408))) (unit-resolution ((_ th-lemma arith) (or false $x304)) @x26 $x304) @x715 $x514)))
+(let (($x41 (= ?x39 1)))
+(let (($x169 (not $x41)))
+(let ((?x42 (mod$ m$ 2)))
+(let (($x43 (= ?x42 1)))
+(let ((?x29 (+ n$ m$)))
+(let ((?x214 (mod ?x29 2)))
+(let ((?x253 (* (- 1) ?x214)))
+(let ((?x31 (mod$ ?x29 2)))
+(let ((?x603 (+ n$ m$ ?x31 ?x35 ?x253 (* (- 1) (div ?x29 2)) ?x363 ?x601 (* (- 1) (div m$ 2)))))
+(let (($x604 (>= ?x603 2)))
+(let (($x523 (>= ?x42 1)))
+(let (($x609 (not $x523)))
+(let (($x522 (<= ?x42 1)))
+(let ((?x439 (mod m$ 2)))
+(let ((?x466 (* (- 1) ?x439)))
+(let ((?x467 (+ ?x42 ?x466)))
+(let (($x482 (<= ?x467 0)))
+(let (($x468 (= ?x467 0)))
+(let (($x473 (or $x260 $x468)))
+(let ((?x440 (ite $x209 (* (- 1) (mod (* (- 1) m$) ?x211)) ?x439)))
+(let ((?x441 (ite $x208 m$ ?x440)))
+(let (($x442 (= ?x42 ?x441)))
+(let ((@x453 (rewrite (= (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439) ?x439))))
+(let (($x447 (= (* (- 1) (mod (* (- 1) m$) ?x211)) (* (- 1) (mod (* (- 1) m$) (- 2))))))
+(let ((@x229 (rewrite (= ?x211 (- 2)))))
+(let ((@x445 (monotonicity @x229 (= (mod (* (- 1) m$) ?x211) (mod (* (- 1) m$) (- 2))))))
+(let ((@x451 (monotonicity @x221 (monotonicity @x445 $x447) (= ?x440 (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439)))))
+(let ((@x458 (monotonicity @x219 (trans @x451 @x453 (= ?x440 ?x439)) (= ?x441 (ite false m$ ?x439)))))
+(let ((@x465 (monotonicity (trans @x458 (rewrite (= (ite false m$ ?x439) ?x439)) (= ?x441 ?x439)) (= $x442 (= ?x42 ?x439)))))
+(let ((@x477 (monotonicity (trans @x465 (rewrite (= (= ?x42 ?x439) $x468)) (= $x442 $x468)) (= (or $x260 $x442) $x473))))
+(let ((@x481 (mp ((_ quant-inst m$ 2) (or $x260 $x442)) (trans @x477 (rewrite (= $x473 $x473)) (= (or $x260 $x442) $x473)) $x473)))
+(let ((@x277 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) $x482)) (unit-resolution @x481 @x196 $x468) $x482)))
+(let ((@x386 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x439 2)))) @x26 (not (>= ?x439 2)))))
+(let ((@x384 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x522 (>= ?x439 2) (not $x482))) @x386 @x277 $x522)))
+(let ((@x564 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x43 (not $x522) $x609)) (hypothesis (not $x43)) (or (not $x522) $x609))))
+(let ((?x272 (div ?x29 2)))
+(let ((?x288 (* (- 2) ?x272)))
+(let ((?x289 (+ n$ m$ ?x253 ?x288)))
+(let (($x294 (<= ?x289 0)))
+(let (($x287 (= ?x289 0)))
+(let ((@x617 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x294)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x294)))
+(let (($x433 (<= ?x31 0)))
+(let (($x32 (= ?x31 0)))
+(let ((@x33 (asserted $x32)))
+(let ((?x254 (+ ?x31 ?x253)))
+(let (($x270 (<= ?x254 0)))
+(let (($x255 (= ?x254 0)))
+(let (($x261 (or $x260 $x255)))
+(let ((?x215 (ite $x209 (* (- 1) (mod (* (- 1) ?x29) ?x211)) ?x214)))
+(let ((?x216 (ite $x208 ?x29 ?x215)))
+(let (($x217 (= ?x31 ?x216)))
+(let (($x239 (= (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214) ?x214)))
+(let (($x237 (= ?x215 (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214))))
+(let (($x234 (= (* (- 1) (mod (* (- 1) ?x29) ?x211)) (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x232 (monotonicity (rewrite (= (* (- 1) ?x29) (+ ?x222 (* (- 1) m$)))) @x229 (= (mod (* (- 1) ?x29) ?x211) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
+(let ((@x242 (trans (monotonicity @x221 (monotonicity @x232 $x234) $x237) (rewrite $x239) (= ?x215 ?x214))))
+(let ((@x249 (trans (monotonicity @x219 @x242 (= ?x216 (ite false ?x29 ?x214))) (rewrite (= (ite false ?x29 ?x214) ?x214)) (= ?x216 ?x214))))
+(let ((@x259 (trans (monotonicity @x249 (= $x217 (= ?x31 ?x214))) (rewrite (= (= ?x31 ?x214) $x255)) (= $x217 $x255))))
+(let ((@x268 (trans (monotonicity @x259 (= (or $x260 $x217) $x261)) (rewrite (= $x261 $x261)) (= (or $x260 $x217) $x261))))
+(let ((@x269 (mp ((_ quant-inst (+ n$ m$) 2) (or $x260 $x217)) @x268 $x261)))
+(let ((@x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x270)) (unit-resolution @x269 @x196 $x255) $x270)))
+(let ((?x498 (+ m$ ?x466 (* (- 2) (div m$ 2)))))
+(let (($x496 (= ?x498 0)))
+(let ((@x633 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (<= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (<= ?x498 0))))
+(let ((?x397 (* (- 4) ?x381)))
+(let ((?x398 (+ n$ ?x363 ?x397)))
+(let (($x403 (<= ?x398 0)))
+(let (($x396 (= ?x398 0)))
+(let ((@x640 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x403)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x403)))
+(let ((?x364 (+ ?x35 ?x363)))
+(let (($x379 (<= ?x364 0)))
+(let (($x365 (= ?x364 0)))
+(let (($x370 (or $x260 $x365)))
+(let ((?x330 (ite (<= 4 0) (* (- 1) (mod ?x222 (* (- 1) 4))) ?x329)))
+(let ((?x331 (ite (= 4 0) n$ ?x330)))
+(let (($x332 (= ?x35 ?x331)))
+(let ((@x342 (monotonicity (rewrite (= (* (- 1) 4) (- 4))) (= (mod ?x222 (* (- 1) 4)) (mod ?x222 (- 4))))))
+(let ((@x345 (monotonicity @x342 (= (* (- 1) (mod ?x222 (* (- 1) 4))) (* (- 1) (mod ?x222 (- 4)))))))
+(let ((@x348 (monotonicity (rewrite (= (<= 4 0) false)) @x345 (= ?x330 (ite false (* (- 1) (mod ?x222 (- 4))) ?x329)))))
+(let ((@x352 (trans @x348 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 4))) ?x329) ?x329)) (= ?x330 ?x329))))
+(let ((@x355 (monotonicity (rewrite (= (= 4 0) false)) @x352 (= ?x331 (ite false n$ ?x329)))))
+(let ((@x362 (monotonicity (trans @x355 (rewrite (= (ite false n$ ?x329) ?x329)) (= ?x331 ?x329)) (= $x332 (= ?x35 ?x329)))))
+(let ((@x374 (monotonicity (trans @x362 (rewrite (= (= ?x35 ?x329) $x365)) (= $x332 $x365)) (= (or $x260 $x332) $x370))))
+(let ((@x378 (mp ((_ quant-inst n$ 4) (or $x260 $x332)) (trans @x374 (rewrite (= $x370 $x370)) (= (or $x260 $x332) $x370)) $x370)))
+(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x379)) (unit-resolution @x378 @x196 $x365) $x379)))
+(let (($x435 (<= ?x35 3)))
+(let (($x37 (= ?x35 3)))
+(let ((@x38 (asserted $x37)))
+(let ((@x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) (>= ?x467 0))) (unit-resolution @x481 @x196 $x468) (>= ?x467 0))))
+(let ((@x656 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1 1 1 1) @x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x604) @x645 @x640 @x633 @x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x433)) @x33 $x433) @x617 (hypothesis $x609) false)))
+(let ((@x565 (unit-resolution (lemma @x656 (or (not $x604) $x523)) (unit-resolution @x564 @x384 $x609) (not $x604))))
+(let (($x295 (>= ?x289 0)))
+(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x295)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x295)))
+(let (($x434 (>= ?x31 0)))
+(let (($x271 (>= ?x254 0)))
+(let ((@x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x271)) (unit-resolution @x269 @x196 $x255) $x271)))
+(let ((@x537 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x496) (>= ?x498 0))) (unit-resolution ((_ th-lemma arith) (or false $x496)) @x26 $x496) (>= ?x498 0))))
+(let ((@x549 (unit-resolution ((_ th-lemma arith) (or false (>= ?x439 0))) @x26 (>= ?x439 0))))
+(let (($x404 (>= ?x398 0)))
+(let ((@x552 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x404)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x404)))
+(let (($x380 (>= ?x364 0)))
+(let ((@x273 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x380)) (unit-resolution @x378 @x196 $x365) $x380)))
+(let (($x436 (>= ?x35 3)))
+(let ((@x545 ((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x273 @x552 @x549 @x537 @x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x32) $x434)) @x33 $x434) @x566 @x565 false)))
+(let (($x171 (or $x169 (not $x43))))
+(let ((@x177 (monotonicity (rewrite (= (and $x41 $x43) (not $x171))) (= (not (and $x41 $x43)) (not (not $x171))))))
+(let ((@x181 (trans @x177 (rewrite (= (not (not $x171)) $x171)) (= (not (and $x41 $x43)) $x171))))
+(let ((@x182 (mp (asserted (not (and $x41 $x43))) @x181 $x171)))
+(let ((@x729 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x41 (not $x514) $x725)) (unit-resolution @x182 (lemma @x545 $x43) $x169) (or (not $x514) $x725))))
+(let ((?x420 (* (- 2) ?x410)))
+(let ((?x421 (+ n$ ?x420 ?x534)))
+(let (($x426 (<= ?x421 0)))
+(let (($x419 (= ?x421 0)))
+(let ((@x737 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x426)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x426)))
+(let (($x409 (>= ?x535 0)))
+(let ((@x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x409)) (unit-resolution @x407 @x196 $x490) $x409)))
+(let ((@x742 ((_ th-lemma arith farkas -1 1 -2 1 1 1 1) @x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x435)) @x38 $x435) (hypothesis $x706) @x640 @x737 @x645 (unit-resolution @x729 @x722 $x725) false)))
+(let (($x427 (>= ?x421 0)))
+(let ((@x584 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x427)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x427)))
+(let (($x542 (>= ?x519 0)))
+((_ th-lemma arith farkas -1/2 -1/2 -1/2 -1/2 -1/2 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x37) $x436)) @x38 $x436) @x552 (unit-resolution ((_ th-lemma arith) (or false $x542)) @x26 $x542) @x584 @x273 (lemma @x742 (not $x706)) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+f6a4c40290fd6742c0b08a1fe90b3664e90c2143 336 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x99 (mod$ l$ 2)))
+(let ((?x96 (map$ uu$ xs$)))
+(let ((?x97 (eval_dioph$ ks$ ?x96)))
+(let ((?x98 (mod$ ?x97 2)))
+(let (($x100 (= ?x98 ?x99)))
+(let ((?x93 (eval_dioph$ ks$ xs$)))
+(let (($x95 (= ?x93 l$)))
+(let ((?x110 (* (- 1) ?x97)))
+(let ((?x111 (+ l$ ?x110)))
+(let ((?x114 (divide$ ?x111 2)))
+(let ((?x101 (map$ uua$ xs$)))
+(let ((?x102 (eval_dioph$ ks$ ?x101)))
+(let (($x117 (= ?x102 ?x114)))
+(let (($x282 (not $x117)))
+(let (($x281 (not $x100)))
+(let (($x283 (or $x281 $x282)))
+(let ((?x744 (div ?x93 2)))
+(let ((?x970 (* (- 1) ?x744)))
+(let ((?x699 (mod ?x93 2)))
+(let ((?x726 (* (- 1) ?x699)))
+(let ((?x516 (mod l$ 2)))
+(let ((?x543 (* (- 1) ?x516)))
+(let (($x972 (>= (+ l$ ?x99 ?x543 (* (- 1) (div l$ 2)) ?x726 ?x970) 1)))
+(let ((?x369 (* (- 1) l$)))
+(let ((?x693 (+ ?x93 ?x369)))
+(let (($x695 (>= ?x693 0)))
+(let (($x861 (not $x695)))
+(let (($x694 (<= ?x693 0)))
+(let ((?x686 (+ ?x102 (* (- 1) ?x114))))
+(let (($x687 (<= ?x686 0)))
+(let (($x284 (not $x283)))
+(let ((@x466 (hypothesis $x284)))
+(let ((@x856 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x687)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x687)))
+(let ((?x437 (+ l$ ?x110 (* (- 2) (div ?x111 2)) (* (- 1) (mod (+ l$ ?x97) 2)))))
+(let (($x443 (>= ?x437 0)))
+(let (($x434 (= ?x437 0)))
+(let ((@x26 (true-axiom true)))
+(let ((@x793 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
+(let ((?x501 (* (- 2) ?x102)))
+(let ((?x502 (+ ?x93 ?x110 ?x501)))
+(let (($x509 (<= ?x502 0)))
+(let (($x503 (= ?x502 0)))
+(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
+))
+(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))))
+))
+(let ((?x45 (eval_dioph$ ?1 ?0)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
+(let (($x79 (= ?x83 0)))
+(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
+(= ?x56 ?x45)))))
+))
+(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x66 (+ ?x48 ?x60)))
+(= ?x66 ?x45)))))))
+))
+(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
+(let ((?x66 (+ ?x48 ?x60)))
+(let (($x71 (= ?x66 ?x45)))
+(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
+(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
+(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
+(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
+(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
+(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
+(let (($x507 (or (not $x304) $x503)))
+(let ((@x508 ((_ quant-inst ks$ xs$) $x507)))
+(let ((@x800 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x509)) (unit-resolution @x508 @x309 $x503) $x509)))
+(let ((?x396 (+ ?x114 (* (- 1) (div ?x111 2)))))
+(let (($x413 (<= ?x396 0)))
+(let (($x397 (= ?x396 0)))
+(let (($x311 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) )))
+))
+(let (($x193 (forall ((?v0 Int) (?v1 Int) )(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))))
+))
+(let ((?x145 (div ?1 ?0)))
+(let ((?x157 (* (- 1) ?0)))
+(let ((?x154 (* (- 1) ?1)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?0 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?0 0)))
+(let ((?x141 (divide$ ?1 ?0)))
+(let (($x190 (= ?x141 (ite $x143 0 ?x182))))
+(let (($x152 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x150)))))
+))
+(let (($x172 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let ((?x145 (div ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let (($x143 (= ?v1 0)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x166)))))))))))
+))
+(let (($x144 (< 0 ?0)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
+(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) ?x182)) (= ?x163 ?x182))))
+(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 ?x182))) (= (= ?x141 ?x166) $x190))))
+(let (($x169 (= ?x141 ?x166)))
+(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
+(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
+(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
+(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
+(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
+(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
+(let (($x403 (or (not $x311) $x397)))
+(let ((?x361 (div ?x111 2)))
+(let (($x357 (<= 2 0)))
+(let ((?x362 (ite $x357 (div (* (- 1) ?x111) (* (- 1) 2)) ?x361)))
+(let (($x356 (= 2 0)))
+(let ((?x363 (ite $x356 0 ?x362)))
+(let (($x364 (= ?x114 ?x363)))
+(let ((@x374 (rewrite (= (* (- 1) 2) (- 2)))))
+(let ((@x377 (monotonicity (rewrite (= (* (- 1) ?x111) (+ ?x369 ?x97))) @x374 (= (div (* (- 1) ?x111) (* (- 1) 2)) (div (+ ?x369 ?x97) (- 2))))))
+(let ((@x368 (rewrite (= $x357 false))))
+(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
+(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
+(let ((@x366 (rewrite (= $x356 false))))
+(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
+(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
+(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
+(let ((@x802 (unit-resolution (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403) @x316 $x397)))
+(let ((?x425 (mod (+ l$ ?x97) 2)))
+(let (($x465 (>= ?x425 0)))
+(let ((@x810 ((_ th-lemma arith farkas 1 -2 -2 -1 1 1) (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (hypothesis $x687) @x800 (hypothesis (not $x694)) @x793 false)))
+(let (($x134 (not $x95)))
+(let (($x290 (= $x95 $x283)))
+(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
+(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
+(let (($x120 (and $x100 $x117)))
+(let (($x135 (= $x134 $x120)))
+(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
+(let (($x108 (not $x107)))
+(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
+(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
+(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
+(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
+(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
+(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
+(let ((@x898 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 (not $x694) $x861)) (unit-resolution @x344 @x466 $x134) (or (not $x694) $x861))))
+(let ((@x899 (unit-resolution @x898 (unit-resolution (lemma @x810 (or $x694 (not $x687))) @x856 $x694) $x861)))
+(let ((?x544 (+ ?x99 ?x543)))
+(let (($x561 (>= ?x544 0)))
+(let (($x545 (= ?x544 0)))
+(let (($x318 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+))
+(let (($x245 (forall ((?v0 Int) (?v1 Int) )(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))))
+))
+(let ((?x200 (mod ?1 ?0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let ((?x239 (ite $x143 ?1 ?x234)))
+(let ((?x199 (mod$ ?1 ?0)))
+(let (($x242 (= ?x199 ?x239)))
+(let (($x206 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x204)))))
+))
+(let (($x228 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x200 (mod ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let (($x143 (= ?v1 0)))
+(let ((?x222 (ite $x143 ?v0 ?x219)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x222))))))))))))
+))
+(let ((@x233 (monotonicity (rewrite (= $x144 (not $x175))) (= (ite $x144 ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
+(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite $x144 ?x200 ?x214) ?x234))))
+(let ((@x244 (monotonicity (monotonicity @x238 (= (ite $x143 ?1 (ite $x144 ?x200 ?x214)) ?x239)) (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 ?x214))) $x242))))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let ((?x222 (ite $x143 ?1 ?x219)))
+(let (($x225 (= ?x199 ?x222)))
+(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
+(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
+(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
+(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
+(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
+(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
+(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
+(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
+(let (($x550 (not $x318)))
+(let (($x551 (or $x550 $x545)))
+(let ((?x359 (* (- 1) 2)))
+(let ((?x511 (mod ?x369 ?x359)))
+(let ((?x512 (* (- 1) ?x511)))
+(let ((?x517 (ite $x357 ?x512 ?x516)))
+(let ((?x518 (ite $x356 l$ ?x517)))
+(let (($x519 (= ?x99 ?x518)))
+(let ((@x525 (monotonicity (monotonicity @x374 (= ?x511 (mod ?x369 (- 2)))) (= ?x512 (* (- 1) (mod ?x369 (- 2)))))))
+(let ((@x528 (monotonicity @x368 @x525 (= ?x517 (ite false (* (- 1) (mod ?x369 (- 2))) ?x516)))))
+(let ((@x532 (trans @x528 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x516) ?x516)) (= ?x517 ?x516))))
+(let ((@x539 (trans (monotonicity @x366 @x532 (= ?x518 (ite false l$ ?x516))) (rewrite (= (ite false l$ ?x516) ?x516)) (= ?x518 ?x516))))
+(let ((@x549 (trans (monotonicity @x539 (= $x519 (= ?x99 ?x516))) (rewrite (= (= ?x99 ?x516) $x545)) (= $x519 $x545))))
+(let ((@x558 (trans (monotonicity @x549 (= (or $x550 $x519) $x551)) (rewrite (= $x551 $x551)) (= (or $x550 $x519) $x551))))
+(let ((@x559 (mp ((_ quant-inst l$ 2) (or $x550 $x519)) @x558 $x551)))
+(let ((@x902 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x561)) (unit-resolution @x559 @x323 $x545) $x561)))
+(let ((?x757 (* (- 2) ?x744)))
+(let ((?x758 (+ ?x93 ?x726 ?x757)))
+(let (($x764 (>= ?x758 0)))
+(let (($x756 (= ?x758 0)))
+(let ((@x872 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x764)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x764)))
+(let ((?x562 (div l$ 2)))
+(let ((?x575 (* (- 2) ?x562)))
+(let ((?x576 (+ l$ ?x543 ?x575)))
+(let (($x582 (>= ?x576 0)))
+(let (($x574 (= ?x576 0)))
+(let ((@x880 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x582)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x582)))
+(let ((?x504 (mod$ ?x93 2)))
+(let ((?x727 (+ ?x504 ?x726)))
+(let (($x728 (= ?x727 0)))
+(let (($x733 (or $x550 $x728)))
+(let ((?x696 (* (- 1) ?x93)))
+(let ((?x697 (mod ?x696 ?x359)))
+(let ((?x698 (* (- 1) ?x697)))
+(let ((?x700 (ite $x357 ?x698 ?x699)))
+(let ((?x701 (ite $x356 ?x93 ?x700)))
+(let (($x702 (= ?x504 ?x701)))
+(let ((@x708 (monotonicity (monotonicity @x374 (= ?x697 (mod ?x696 (- 2)))) (= ?x698 (* (- 1) (mod ?x696 (- 2)))))))
+(let ((@x711 (monotonicity @x368 @x708 (= ?x700 (ite false (* (- 1) (mod ?x696 (- 2))) ?x699)))))
+(let ((@x715 (trans @x711 (rewrite (= (ite false (* (- 1) (mod ?x696 (- 2))) ?x699) ?x699)) (= ?x700 ?x699))))
+(let ((@x722 (trans (monotonicity @x366 @x715 (= ?x701 (ite false ?x93 ?x699))) (rewrite (= (ite false ?x93 ?x699) ?x699)) (= ?x701 ?x699))))
+(let ((@x732 (trans (monotonicity @x722 (= $x702 (= ?x504 ?x699))) (rewrite (= (= ?x504 ?x699) $x728)) (= $x702 $x728))))
+(let ((@x740 (trans (monotonicity @x732 (= (or $x550 $x702) $x733)) (rewrite (= $x733 $x733)) (= (or $x550 $x702) $x733))))
+(let ((@x427 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (>= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (>= ?x727 0))))
+(let ((?x783 (* (- 1) ?x504)))
+(let ((?x784 (+ ?x99 ?x783)))
+(let (($x786 (>= ?x784 0)))
+(let (($x782 (= ?x99 ?x504)))
+(let (($x821 (= ?x98 ?x504)))
+(let (($x505 (= ?x504 ?x98)))
+(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) )))
+))
+(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
+))
+(let (($x50 (= (mod$ ?x45 2) (mod$ ?x48 2))))
+(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
+(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
+(let (($x514 (or (not $x297) $x505)))
+(let ((@x515 ((_ quant-inst ks$ xs$) $x514)))
+(let ((@x824 (symm (unit-resolution (def-axiom (or $x283 $x100)) @x466 $x100) (= ?x99 ?x98))))
+(let ((@x939 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x786)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x786)))
+(let (($x785 (<= ?x784 0)))
+(let ((@x887 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x785)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x785)))
+(let (($x688 (>= ?x686 0)))
+(let ((@x855 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x688)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x688)))
+(let ((@x979 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x425 2)))) @x26 (not (>= ?x425 2)))))
+(let (($x560 (<= ?x544 0)))
+(let ((@x461 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x560)) (unit-resolution @x559 @x323 $x545) $x560)))
+(let (($x763 (<= ?x758 0)))
+(let ((@x658 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x763)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x763)))
+(let (($x581 (<= ?x576 0)))
+(let ((@x986 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x581)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x581)))
+(let ((@x989 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (<= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (<= ?x727 0))))
+(let (($x510 (>= ?x502 0)))
+(let ((@x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x510)) (unit-resolution @x508 @x309 $x503) $x510)))
+(let ((@x998 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) (>= ?x396 0))) @x802 (>= ?x396 0))))
+(let ((@x1001 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) (<= ?x437 0))) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) (<= ?x437 0))))
+(let ((@x1002 ((_ th-lemma arith farkas 1 -2 -2 -1 -2 1 1 1 1 1 1) @x1001 @x998 (hypothesis $x688) @x994 (hypothesis $x972) (hypothesis $x785) @x989 @x986 @x658 @x461 @x979 false)))
+(let ((@x474 (unit-resolution (lemma @x1002 (or (not $x972) (not $x688) (not $x785))) @x855 @x887 (not $x972))))
+(let ((@x941 (unit-resolution @x474 ((_ th-lemma arith) @x939 @x427 @x880 @x872 @x902 @x899 $x972) false)))
+(let ((@x942 (lemma @x941 $x283)))
+(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
+(let ((@x679 (unit-resolution @x340 @x942 $x95)))
+(let ((@x889 (trans (symm (unit-resolution @x515 @x302 $x505) $x821) (monotonicity @x679 (= ?x504 ?x99)) $x100)))
+(let (($x811 (not $x687)))
+(let ((@x845 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x688 (not $x413) (not $x465) (not $x443) (not $x509) $x861))))
+(let ((@x892 (unit-resolution @x845 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x695)) @x679 $x695) @x793 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x800 $x688)))
+(let ((@x935 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x811 (not $x688))) (hypothesis $x282) (or $x811 (not $x688)))))
+(let ((@x955 ((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x935 @x892 $x811) @x998 @x1001 @x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x694)) @x679 $x694) @x979 false)))
+(let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281)))
+(unit-resolution @x472 @x889 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
 785615f585a02b3e6ed8608ecc9660ba5c4025e2 2 0
 sat
 (error "line 9 column 10: proof is not available")
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -402,7 +402,7 @@
    ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
    ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
    ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
-   ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
+   ((@{const_name Rings.divide}, nat_T --> nat_T --> nat_T), 0),
    ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
    ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
    ((@{const_name of_nat}, nat_T --> int_T), 0),
@@ -411,7 +411,7 @@
    ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
    ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
    ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
-   ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
+   ((@{const_name Rings.divide}, int_T --> int_T --> int_T), 0),
    ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
    ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
    ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -553,7 +553,7 @@
         | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
           if is_built_in_const x then Cst (Multiply, T, Any)
           else ConstName (s, T, Any)
-        | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
+        | (Const (x as (s as @{const_name Rings.divide}, T)), []) =>
           if is_built_in_const x then Cst (Divide, T, Any)
           else ConstName (s, T, Any)
         | (t0 as Const (x as (@{const_name ord_class.less}, _)),
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -56,7 +56,7 @@
   let
     fun aux (t1 $ t2) = aux t1 orelse aux t2
       | aux (Const (s, T)) =
-        ((s = @{const_name times} orelse s = @{const_name div}) andalso
+        ((s = @{const_name times} orelse s = @{const_name Rings.divide}) andalso
          is_integer_type (body_type T)) orelse
         (String.isPrefix numeral_prefix s andalso
          let val n = the (Int.fromString (unprefix numeral_prefix s)) in
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -756,7 +756,7 @@
  | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r
  | _ => is_number t orelse can HOLogic.dest_nat t
 
  fun ty cts t = 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -34,7 +34,7 @@
     {logic = K "", fp_kinds = [BNF_Util.Least_FP],
      serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
 
-  fun is_div_mod @{const div (int)} = true
+  fun is_div_mod @{const divide (int)} = true
     | is_div_mod @{const mod (int)} = true
     | is_div_mod _ = false
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/SMT/z3_real.ML
--- a/src/HOL/Tools/SMT/z3_real.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_real.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -12,13 +12,13 @@
 
 fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i)
   | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
-      SOME (@{term "inverse_class.divide :: real => _"} $ t1 $ t2)
+      SOME (@{term "Rings.divide :: real => _"} $ t1 $ t2)
   | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t)
   | real_term_parser _ = NONE
 
 fun abstract abs t =
   (case t of
-    (c as @{term "inverse_class.divide :: real => _"}) $ t1 $ t2 =>
+    (c as @{term "Rings.divide :: real => _"}) $ t1 $ t2 =>
       abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
   | (c as @{term "Real.real :: int => _"}) $ t =>
       abs t #>> (fn u => SOME (c $ u))
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -135,8 +135,7 @@
     | Fastforce_Method => Clasimp.fast_force_tac ctxt
     | Force_Method => Clasimp.force_tac ctxt
     | Moura_Method => moura_tac ctxt
-    | Linarith_Method =>
-      let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
+    | Linarith_Method => Lin_Arith.tac ctxt
     | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -21,7 +21,6 @@
   val global_setup: theory -> theory
   val split_limit: int Config.T
   val neq_limit: int Config.T
-  val verbose: bool Config.T
   val trace: bool Config.T
 end;
 
@@ -102,15 +101,13 @@
 
 val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
 val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
-val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true);
 val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false);
 
 
-structure LA_Data =
+structure LA_Data: LIN_ARITH_DATA =
 struct
 
 val neq_limit = neq_limit;
-val verbose = verbose;
 val trace = trace;
 
 
@@ -139,7 +136,9 @@
 
    returns either (SOME term, associated multiplicity) or (NONE, constant)
 *)
-fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
+fun of_field_sort thy U = Sign.of_sort thy (U, @{sort inverse});
+
+fun demult thy (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
 let
   fun demult ((mC as Const (@{const_name Groups.times}, _)) $ s $ t, m) =
       (case s of Const (@{const_name Groups.times}, _) $ s1 $ s2 =>
@@ -153,24 +152,26 @@
               (SOME t', m'') => (SOME (mC $ s' $ t'), m'')
             | (NONE,    m'') => (SOME s', m''))
         | (NONE,    m') => demult (t, m')))
-    | demult ((mC as Const (@{const_name Fields.divide}, _)) $ s $ t, m) =
+    | demult (atom as (mC as Const (@{const_name Rings.divide}, T)) $ s $ t, m) =
       (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
          become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
          if we choose to do so here, the simpset used by arith must be able to
          perform the same simplifications. *)
       (* quotient 's / t', where the denominator t can be NONE *)
       (* Note: will raise Rat.DIVZERO iff m' is Rat.zero *)
-      let val (os',m') = demult (s, m);
+      if of_field_sort thy (domain_type T) then
+        let
+          val (os',m') = demult (s, m);
           val (ot',p) = demult (t, Rat.one)
-      in (case (os',ot') of
+        in (case (os',ot') of
             (SOME s', SOME t') => SOME (mC $ s' $ t')
           | (SOME s', NONE) => SOME s'
           | (NONE, SOME t') =>
-               let val Const(_,T) = mC
-               in SOME (mC $ Const (@{const_name Groups.one}, domain_type T) $ t') end
+               SOME (mC $ Const (@{const_name Groups.one}, domain_type (snd (dest_Const mC))) $ t')
           | (NONE, NONE) => NONE,
           Rat.mult m' (Rat.inv p))
-      end
+        end
+      else (SOME atom, m)
     (* terms that evaluate to numeric constants *)
     | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
     | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
@@ -192,7 +193,7 @@
     | demult (atom, m) = (SOME atom, m)
 in demult end;
 
-fun decomp0 (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) :
+fun decomp0 thy (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) :
             ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
 let
   (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
@@ -215,13 +216,15 @@
     | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
         poly (t, m, (p, Rat.add i m))
     | poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) =
-        (case demult inj_consts (all, m) of
+        (case demult thy inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const (@{const_name Fields.divide}, _) $ _ $ _, m, pi as (p, i)) =
-        (case demult inj_consts (all, m) of
-           (NONE,   m') => (p, Rat.add i m')
-         | (SOME u, m') => add_atom u m' pi)
+    | poly (all as Const (@{const_name Rings.divide}, T) $ _ $ _, m, pi as (p, i)) =
+        if of_field_sort thy (domain_type T) then 
+          (case demult thy inj_consts (all, m) of
+             (NONE,   m') => (p, Rat.add i m')
+           | (SOME u, m') => add_atom u m' pi)
+        else add_atom all m pi
     | poly (all as Const f $ x, m, pi) =
         if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
     | poly (all, m, pi) =
@@ -244,12 +247,12 @@
       else if member (op =) discrete D then (true, true) else (false, false)
   | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
 
-fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
+fun decomp_typecheck thy (discrete, inj_consts) (T : typ, xxx) : decomp option =
   case T of
     Type ("fun", [U, _]) =>
       (case allows_lin_arith thy discrete U of
         (true, d) =>
-          (case decomp0 inj_consts xxx of
+          (case decomp0 thy inj_consts xxx of
             NONE                   => NONE
           | SOME (p, i, rel, q, j) => SOME (p, i, rel, q, j, d))
       | (false, _) =>
@@ -259,20 +262,20 @@
 fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d)
   | negate NONE                        = NONE;
 
-fun decomp_negation data
-  ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
-      decomp_typecheck data (T, (rel, lhs, rhs))
-  | decomp_negation data ((Const (@{const_name Trueprop}, _)) $
-  (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
-      negate (decomp_typecheck data (T, (rel, lhs, rhs)))
-  | decomp_negation data _ =
+fun decomp_negation thy data
+      ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
+      decomp_typecheck thy data (T, (rel, lhs, rhs))
+  | decomp_negation thy data
+      ((Const (@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
+      negate (decomp_typecheck thy data (T, (rel, lhs, rhs)))
+  | decomp_negation thy data _ =
       NONE;
 
 fun decomp ctxt : term -> decomp option =
   let
     val thy = Proof_Context.theory_of ctxt
     val {discrete, inj_consts, ...} = get_arith_data ctxt
-  in decomp_negation (thy, discrete, inj_consts) end;
+  in decomp_negation thy (discrete, inj_consts) end;
 
 fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
   | domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
@@ -299,7 +302,7 @@
           @{const_name Groups.minus},
           "Int.nat" (*DYNAMIC BINDING!*),
           "Divides.div_class.mod" (*DYNAMIC BINDING!*),
-          "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
+          @{const_name Rings.divide}] a
     | _ =>
       (if Context_Position.is_visible ctxt then
         warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
@@ -498,7 +501,7 @@
     (* ?P ((?n::nat) div (numeral ?k)) =
          ((numeral ?k = 0 --> ?P 0) & (~ (numeral ?k = 0) -->
            (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P i))) *)
-    | (Const ("Divides.div_class.div", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
+    | (Const (@{const_name Rings.divide}, Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const (@{const_name Groups.zero}, split_type)
@@ -589,7 +592,7 @@
           (numeral ?k < 0 -->
             (ALL i j.
               numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P i))) *)
-    | (Const ("Divides.div_class.div",
+    | (Const (@{const_name Rings.divide},
         Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -288,8 +288,8 @@
 
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} HOLogic.natT
   val cancel = @{thm nat_mult_div_cancel1} RS trans
   val neg_exchanges = false
 );
@@ -393,8 +393,8 @@
 
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} HOLogic.natT
   fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
 );
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -116,7 +116,7 @@
   Fractions are reduced later by the cancel_numeral_factor simproc.*)
 fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
 
-val mk_divide = HOLogic.mk_binop @{const_name Fields.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
 
 (*Build term (p / q) * t*)
 fun mk_fcoeff ((p, q), t) =
@@ -125,7 +125,7 @@
 
 (*Express t as a product of a fraction with other sorted terms*)
 fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
-  | dest_fcoeff sign (Const (@{const_name Fields.divide}, _) $ t $ u) =
+  | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
     let val (p, t') = dest_coeff sign t
         val (q, u') = dest_coeff 1 u
     in (mk_frac (p, q), mk_divide (t', u')) end
@@ -401,8 +401,8 @@
 (*Version for semiring_div*)
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   val cancel = @{thm div_mult_mult1} RS trans
   val neg_exchanges = false
 )
@@ -410,8 +410,8 @@
 (*Version for fields*)
 structure DivideCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   val neg_exchanges = false
 )
@@ -548,8 +548,8 @@
 (*for semirings with division*)
 structure DivCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
 );
 
@@ -571,8 +571,8 @@
 (*Version for all fields, including unordered ones (type complex).*)
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
 );
 
@@ -620,13 +620,13 @@
     val (l,r) = Thm.dest_binop ct
     val T = Thm.ctyp_of_cterm l
   in (case (Thm.term_of l, Thm.term_of r) of
-      (Const(@{const_name Fields.divide},_)$_$_, _) =>
+      (Const(@{const_name Rings.divide},_)$_$_, _) =>
         let val (x,y) = Thm.dest_binop l val z = r
             val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
             val ynz = prove_nz ctxt T y
         in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
         end
-     | (_, Const (@{const_name Fields.divide},_)$_$_) =>
+     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
         let val (x,y) = Thm.dest_binop r val z = l
             val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
             val ynz = prove_nz ctxt T y
@@ -636,49 +636,49 @@
   end
   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
 
- fun is_number (Const(@{const_name Fields.divide},_)$a$b) = is_number a andalso is_number b
+ fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
    | is_number t = can HOLogic.dest_number t
 
  val is_number = is_number o Thm.term_of
 
  fun proc3 phi ctxt ct =
   (case Thm.term_of ct of
-    Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
+    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = Thm.ctyp_of_cterm c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
+  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = Thm.ctyp_of_cterm c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
+  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = Thm.ctyp_of_cterm c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
+  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = Thm.ctyp_of_cterm c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
+  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = Thm.ctyp_of_cterm c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
+  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -127,12 +127,12 @@
   let
     fun numeral_is_const ct =
       case Thm.term_of ct of
-       Const (@{const_name Fields.divide},_) $ a $ b =>
+       Const (@{const_name Rings.divide},_) $ a $ b =>
          can HOLogic.dest_number a andalso can HOLogic.dest_number b
      | Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t
      | t => can HOLogic.dest_number t
     fun dest_const ct = ((case Thm.term_of ct of
-       Const (@{const_name Fields.divide},_) $ a $ b=>
+       Const (@{const_name Rings.divide},_) $ a $ b=>
         Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
      | Const (@{const_name Fields.inverse},_)$t => 
                    Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Tools/try0.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -105,7 +105,6 @@
    bound exceeded" warnings and the like. *)
 fun silence_methods debug =
   Config.put Metis_Tactic.verbose debug
-  #> Config.put Lin_Arith.verbose debug
   #> not debug ? (fn ctxt =>
       ctxt
       |> Context_Position.set_visible false
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/Word/Word.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -307,7 +307,7 @@
   by (metis bintr_ariths(4))
 
 definition
-  word_div_def: "a div b = word_of_int (uint a div uint b)"
+  word_div_def: "divide a b = word_of_int (uint a div uint b)"
 
 definition
   word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -102,7 +102,7 @@
   preal_inverse_def:
     "inverse R == Abs_preal (inverse_set (Rep_preal R))"
 
-definition "R / S = R * inverse (S\<Colon>preal)"
+definition "divide R S = R * inverse (S\<Colon>preal)"
 
 definition
   preal_one_def:
@@ -1222,7 +1222,7 @@
   real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
 
 definition
-  real_divide_def: "R / (S::real) = R * inverse S"
+  real_divide_def: "divide R (S::real) = R * inverse S"
 
 definition
   real_le_def: "z \<le> (w::real) \<longleftrightarrow>
diff -r ccafd7d193e7 -r 2e1c1968b38e src/HOL/ex/FinFunPred.thy
--- a/src/HOL/ex/FinFunPred.thy	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Wed Jun 03 09:32:49 2015 +0200
@@ -15,7 +15,7 @@
 
 definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)"
 
-definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
+definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> g \<le> f"
 
 instance ..
 
diff -r ccafd7d193e7 -r 2e1c1968b38e src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -207,105 +207,6 @@
    Need to know if it is a lower or upper bound for unambiguous interpretation!
 *)
 
-fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)]
-  | elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)]
-  | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)];
-
-(* PRE: ex[v] must be 0! *)
-fun eval ex v (a, le, cs) =
-  let
-    val rs = map Rat.rat_of_int cs;
-    val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
-  in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (nth rs v)), le) end;
-(* If nth rs v < 0, le should be negated.
-   Instead this swap is taken into account in ratrelmin2.
-*)
-
-fun ratrelmin2 (x as (r, ler), y as (s, les)) =
-  case Rat.ord (r, s)
-   of EQUAL => (r, (not ler) andalso (not les))
-    | LESS => x
-    | GREATER => y;
-
-fun ratrelmax2 (x as (r, ler), y as (s, les)) =
-  case Rat.ord (r, s)
-   of EQUAL => (r, ler andalso les)
-    | LESS => y
-    | GREATER => x;
-
-val ratrelmin = foldr1 ratrelmin2;
-val ratrelmax = foldr1 ratrelmax2;
-
-fun ratexact up (r, exact) =
-  if exact then r else
-  let
-    val (_, q) = Rat.quotient_of_rat r;
-    val nth = Rat.inv (Rat.rat_of_int q);
-  in Rat.add r (if up then nth else Rat.neg nth) end;
-
-fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two);
-
-fun choose2 d ((lb, exactl), (ub, exactu)) =
-  let val ord = Rat.sign lb in
-  if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu)
-    then Rat.zero
-    else if not d then
-      if ord = GREATER
-        then if exactl then lb else ratmiddle (lb, ub)
-        else if exactu then ub else ratmiddle (lb, ub)
-      else (*discrete domain, both bounds must be exact*)
-      if ord = GREATER
-        then let val lb' = Rat.roundup lb in
-          if Rat.le lb' ub then lb' else raise NoEx end
-        else let val ub' = Rat.rounddown ub in
-          if Rat.le lb ub' then ub' else raise NoEx end
-  end;
-
-fun findex1 discr (v, lineqs) ex =
-  let
-    val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs;
-    val ineqs = maps elim_eqns nz;
-    val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs
-    val lb = ratrelmax (map (eval ex v) ge)
-    val ub = ratrelmin (map (eval ex v) le)
-  in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end;
-
-fun elim1 v x =
-  map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le,
-                        nth_map v (K Rat.zero) bs));
-
-fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.sign) cs
- of [x] => x =/ nth cs v
-  | _ => false;
-
-(* The base case:
-   all variables occur only with positive or only with negative coefficients *)
-fun pick_vars discr (ineqs,ex) =
-  let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.sign) cs) ineqs
-  in case nz of [] => ex
-     | (_,_,cs) :: _ =>
-       let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs
-           val d = nth discr v;
-           val pos = not (Rat.sign (nth cs v) = LESS);
-           val sv = filter (single_var v) nz;
-           val minmax =
-             if pos then if d then Rat.roundup o fst o ratrelmax
-                         else ratexact true o ratrelmax
-                    else if d then Rat.rounddown o fst o ratrelmin
-                         else ratexact false o ratrelmin
-           val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (nth bs v)), le)) sv
-           val x = minmax((Rat.zero,if pos then true else false)::bnds)
-           val ineqs' = elim1 v x nz
-           val ex' = nth_map v (K x) ex
-       in pick_vars discr (ineqs',ex') end
-  end;
-
-fun findex0 discr n lineqs =
-  let val ineqs = maps elim_eqns lineqs
-      val rineqs = map (fn (a,le,cs) => (Rat.rat_of_int a, le, map Rat.rat_of_int cs))
-                       ineqs
-  in pick_vars discr (rineqs,replicate n Rat.zero) end;
-
 (* ------------------------------------------------------------------------- *)
 (* End of counterexample finder. The actual decision procedure starts here.  *)
 (* ------------------------------------------------------------------------- *)
@@ -432,7 +333,7 @@
       val nziblows = filter_out (fn (i, _) => i = 0) iblows
   in if null nziblows then Failure((~1,nontriv)::hist)
      else
-     let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows)
+     let val (_,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows)
          val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs
          val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes
      in elim ctxt (no @ map_product (elim_var v) pos neg, (v,nontriv)::hist) end
@@ -458,7 +359,6 @@
   if Config.get ctxt LA_Data.trace then tracing msg else ();
 
 val union_term = union Envir.aeconv;
-val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Envir.aeconv (t, t'));
 
 fun add_atoms (lhs, _, _, rhs, _, _) =
   union_term (map fst lhs) o union_term (map fst rhs);
@@ -607,46 +507,6 @@
 (* Print (counter) example                                                   *)
 (* ------------------------------------------------------------------------- *)
 
-fun print_atom((a,d),r) =
-  let val (p,q) = Rat.quotient_of_rat r
-      val s = if d then string_of_int p else
-              if p = 0 then "0"
-              else string_of_int p ^ "/" ^ string_of_int q
-  in a ^ " = " ^ s end;
-
-fun is_variable (Free _) = true
-  | is_variable (Var _) = true
-  | is_variable (Bound _) = true
-  | is_variable _ = false
-
-fun trace_ex ctxt params atoms discr n (hist: history) =
-  case hist of
-    [] => ()
-  | (v, lineqs) :: hist' =>
-      let
-        val frees = map Free params
-        fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t))
-        val start =
-          if v = ~1 then (hist', findex0 discr n lineqs)
-          else (hist, replicate n Rat.zero)
-        val produce_ex =
-          map print_atom #> commas #>
-          prefix "Counterexample (possibly spurious):\n"
-        val ex = (
-          uncurry (fold (findex1 discr)) start
-          |> map2 pair (atoms ~~ discr)
-          |> filter (fn ((t, _), _) => is_variable t)
-          |> map (apfst (apfst show_term))
-          |> (fn [] => NONE | sdss => SOME (produce_ex sdss)))
-          handle NoEx => NONE
-      in
-        case ex of
-          SOME s =>
-            (warning "Linear arithmetic failed -- see trace for a (potentially spurious) counterexample.";
-              tracing s)
-        | NONE => warning "Linear arithmetic failed"
-      end;
-
 (* ------------------------------------------------------------------------- *)
 
 fun mknat (pTs : typ list) (ixs : int list) (atom : term, i : int) : lineq option =
@@ -731,9 +591,6 @@
   result
 end;
 
-fun add_datoms ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _) (dats : (bool * term) list) =
-  union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats);
-
 fun refutes ctxt :
     (typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option =
   let
diff -r ccafd7d193e7 -r 2e1c1968b38e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/class.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -13,12 +13,12 @@
   val rules: theory -> class -> thm option * thm
   val these_defs: theory -> sort -> thm list
   val these_operations: theory -> sort
-    -> (string * (class * (typ * term))) list
+    -> (string * (class * ((typ * term) * bool))) list
   val print_classes: Proof.context -> unit
   val init: class -> theory -> Proof.context
   val begin: class list -> sort -> Proof.context -> Proof.context
   val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
-  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> term -> term list * term list -> local_theory -> local_theory
+  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
   val class_prefix: string -> string
   val register: class -> class list -> ((string * typ) * (string * typ)) list
@@ -74,7 +74,7 @@
 
   (* dynamic part *)
   defs: thm list,
-  operations: (string * (class * (typ * term))) list
+  operations: (string * (class * ((typ * term) * bool))) list
 
   (* n.b.
     params = logical parameters of class
@@ -216,7 +216,7 @@
     some_axiom some_assm_intro of_class thy =
   let
     val operations = map (fn (v_ty as (_, ty), (c, _)) =>
-      (c, (class, (ty, Free v_ty)))) params;
+      (c, (class, ((ty, Free v_ty), false)))) params;
     val add_class = Graph.new_node (class,
         make_class_data (((map o apply2) fst params, base_sort,
           base_morph, export_morph, some_assm_intro, of_class, some_axiom), ([], operations)))
@@ -230,7 +230,7 @@
         (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
   | NONE => thy);
 
-fun register_operation class (c, t) thy =
+fun register_operation class (c, t) input_only thy =
   let
     val base_sort = base_sort thy class;
     val prep_typ = map_type_tfree
@@ -241,7 +241,7 @@
   in
     thy
     |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apsnd)
-        (cons (c, (class, (ty', t'))))
+        (cons (c, (class, ((ty', t'), input_only))))
   end;
 
 fun register_def class def_thm thy =
@@ -259,8 +259,22 @@
 
 (* class context syntax *)
 
-fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
-  o these_operations thy;
+fun make_rewrite t c_ty =
+  let
+    val (vs, t') = strip_abs t;
+    val vts = map snd vs
+      |> Name.invent_names Name.context Name.uu
+      |> map (fn (v, T) => Var ((v, 0), T));
+  in (betapplys (t, vts), betapplys (Const c_ty, vts)) end;
+
+fun these_unchecks thy =
+  these_operations thy
+  #> map_filter (fn (c, (_, ((ty, t), input_only))) =>
+    if input_only then NONE else SOME (make_rewrite t (c, ty)));
+
+fun these_unchecks_reversed thy =
+  these_operations thy
+  #> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t));
 
 fun redeclare_const thy c =
   let val b = Long_Name.base_name c
@@ -273,9 +287,9 @@
     val operations = these_operations thy sort;
     fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
     val primary_constraints =
-      (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
+      (map o apsnd) (subst_class_typ base_sort o fst o fst o snd) operations;
     val secondary_constraints =
-      (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
+      (map o apsnd) (fn (class, ((ty, _), _)) => subst_class_typ [class] ty) operations;
     fun improve (c, ty) =
       (case AList.lookup (op =) primary_constraints c of
         SOME ty' =>
@@ -289,13 +303,14 @@
               | _ => NONE)
           | NONE => NONE)
       | NONE => NONE);
-    fun subst (c, _) = Option.map snd (AList.lookup (op =) operations c);
+    fun subst (c, _) = Option.map (fst o snd) (AList.lookup (op =) operations c);
     val unchecks = these_unchecks thy sort;
   in
     ctxt
     |> fold (redeclare_const thy o fst) primary_constraints
-    |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
-        (((improve, subst), true), unchecks)), false))
+    |> Overloading.map_improvable_syntax (K {primary_constraints = primary_constraints,
+      secondary_constraints = secondary_constraints, improve = improve, subst = subst,
+      no_subst_in_abbrev_mode = true, unchecks = unchecks})
     |> Overloading.set_primary_constraints
   end;
 
@@ -324,8 +339,6 @@
 
 val class_prefix = Logic.const_of_class o Long_Name.base_name;
 
-local
-
 fun guess_morphism_identity (b, rhs) phi1 phi2 =
   let
     (*FIXME proper concept to identify morphism instead of educated guess*)
@@ -336,15 +349,19 @@
     val rhs2 = Morphism.term phi2 rhs;
   in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;
 
-fun target_const class phi0 prmode ((b, _), rhs) =
+fun target_const class phi0 prmode (b, rhs) lthy =
   let
-    val guess_identity = guess_morphism_identity (b, rhs) Morphism.identity;
-    val guess_canonical = guess_morphism_identity (b, rhs) phi0;
+    val export = Variable.export_morphism lthy (Local_Theory.target_of lthy);
+    val guess_identity = guess_morphism_identity (b, rhs) export;
+    val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0);
   in
-    Generic_Target.locale_target_const class
+    lthy
+    |> Generic_Target.locale_target_const class
       (not o (guess_identity orf guess_canonical)) prmode ((b, NoSyn), rhs)
   end;
 
+local
+
 fun dangling_params_for lthy class (type_params, term_params) =
   let
     val class_param_names =
@@ -374,28 +391,10 @@
     |> snd
     |> global_def (b_def, def_eq)
     |-> (fn def_thm => register_def class def_thm)
-    |> null dangling_params ? register_operation class (c, rhs)
+    |> null dangling_params ? register_operation class (c, rhs) false
     |> Sign.add_const_constraint (c, SOME ty)
   end;
 
-fun canonical_abbrev class phi prmode dangling_term_params ((b, mx), rhs) thy =
-  let
-    val unchecks = these_unchecks thy [class];
-    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
-    val c' = Sign.full_name thy b;
-    val ty' = map Term.fastype_of dangling_term_params ---> Term.fastype_of rhs';
-    val ty'' = Morphism.typ phi ty';
-    val rhs'' = map_types (Morphism.typ phi) (fold lambda dangling_term_params rhs');
-  in
-    thy
-    |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs'')
-    |> snd
-    |> Sign.notation true prmode [(Const (c', ty''), mx)]
-    |> (null dangling_term_params andalso not (#1 prmode = Print_Mode.input))
-      ? register_operation class (c', rhs')
-    |> Sign.add_const_constraint (c', SOME ty')
-  end;
-
 in
 
 fun const class ((b, mx), lhs) params lthy =
@@ -404,7 +403,7 @@
     val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
   in
     lthy
-    |> target_const class phi Syntax.mode_default ((b, mx), lhs)
+    |> target_const class phi Syntax.mode_default (b, lhs)
     |> Local_Theory.raw_theory (canonical_const class phi dangling_params
          ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
     |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
@@ -412,18 +411,57 @@
     |> synchronize_class_syntax_target class
   end;
 
-fun abbrev class prmode ((b, mx), lhs) rhs' params lthy =
+end;
+
+local
+
+fun canonical_abbrev class phi prmode with_syntax ((b, mx), rhs) thy =
   let
-    val phi = morphism (Proof_Context.theory_of lthy) class;
-    val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params));
+    val c = Sign.full_name thy b;
+    val constrain = map_atyps (fn T as TFree (v, _) =>
+      if v = Name.aT then TFree (v, [class]) else T | T => T);
+    val rhs' = map_types constrain rhs;
+  in
+    thy
+    |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs')
+    |> snd
+    |> with_syntax ? Sign.notation true prmode [(Const (c, fastype_of rhs), mx)]
+    |> with_syntax ? register_operation class (c, rhs)
+        (#1 prmode = Print_Mode.input)
+    |> Sign.add_const_constraint (c, SOME (fastype_of rhs'))
+  end;
+
+fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy =
+  let
+    val thy = Proof_Context.theory_of lthy;
+    val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) []));
+    val (global_rhs, (extra_tfrees, (type_params, term_params))) =
+      Generic_Target.export_abbrev lthy preprocess rhs;
+    val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx;
   in
     lthy
-    |> target_const class phi prmode ((b, mx), lhs)
-    |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params
-         ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs'))
-    |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
-         prmode ((b, if null dangling_term_params then NoSyn else mx), lhs)
-    |> synchronize_class_syntax_target class
+    |> Local_Theory.raw_theory (canonical_abbrev class phi prmode (null term_params)
+        ((Morphism.binding phi b, mx'), Logic.unvarify_types_global global_rhs))
+  end;
+
+fun further_abbrev_target class phi prmode (b, mx) rhs params =
+  Generic_Target.background_abbrev (b, rhs) (snd params)
+  #-> (fn (lhs, _) => target_const class phi prmode (b, lhs)
+    #> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), lhs))
+
+in
+
+fun abbrev class prmode ((b, mx), rhs) lthy =
+  let
+    val thy = Proof_Context.theory_of lthy;
+    val phi = morphism thy class;
+    val rhs_generic =
+      perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs;
+  in
+    lthy
+    |> canonical_abbrev_target class phi prmode ((b, mx), rhs)
+    |> Generic_Target.abbrev (further_abbrev_target class phi) prmode ((b, mx), rhs_generic)
+    ||> synchronize_class_syntax_target class
   end;
 
 end;
@@ -545,9 +583,10 @@
       map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   in
     ctxt
-    |> Overloading.map_improvable_syntax
-      (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
-          (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
+    |> Overloading.map_improvable_syntax (fn {primary_constraints, improve, ...} =>
+      {primary_constraints = primary_constraints, secondary_constraints = [],
+        improve = improve, subst = subst, no_subst_in_abbrev_mode = false,
+        unchecks = unchecks})
   end;
 
 fun resort_terms ctxt algebra consts constraints ts =
@@ -578,7 +617,7 @@
     SOME c =>
       if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
       else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
-  | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
+  | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
   let
@@ -635,15 +674,16 @@
     |> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
     |> fold (Variable.declare_typ o TFree) vs
     |> fold (Variable.declare_names o Free o snd) params
-    |> (Overloading.map_improvable_syntax o apfst)
-         (K ((primary_constraints, []), (((improve, K NONE), false), [])))
+    |> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints,
+      secondary_constraints = [], improve = improve, subst = K NONE,
+      no_subst_in_abbrev_mode = false, unchecks = []})
     |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
     |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes Generic_Target.theory_notes,
-        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+        notes = Generic_Target.notes Generic_Target.theory_target_notes,
+        abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         subscription = Generic_Target.theory_registration,
         pretty = pretty,
diff -r ccafd7d193e7 -r 2e1c1968b38e src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -116,7 +116,7 @@
       else fold inter_sort (map (Class.base_sort thy) sups) [];
     val is_param = member (op =) (map fst (Class.these_params thy sups));
     val base_constraints = (map o apsnd)
-      (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
+      (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd)
         (Class.these_operations thy sups);
     fun singleton_fixateT Ts =
       let
diff -r ccafd7d193e7 -r 2e1c1968b38e src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -7,17 +7,22 @@
 
 signature GENERIC_TARGET =
 sig
-  (*consts*)
-  val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
-    local_theory -> local_theory
+  (*auxiliary*)
+  val export_abbrev: Proof.context ->
+      (term -> term) -> term -> term * ((string * sort) list * (term list * term list))
+  val check_mixfix_global: binding * bool -> mixfix -> mixfix
 
-  (*background operations*)
+  (*background primitives*)
   val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
 
-  (*lifting primitives to local theory operations*)
+  (*nested local theories primitives*)
+  val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+    local_theory -> local_theory
+
+  (*lifting target primitives to local theory operations*)
   val define: (((binding * typ) * mixfix) * (binding * term) ->
       term list * term list -> local_theory -> (term * thm) * local_theory) ->
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -27,33 +32,43 @@
       (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
     string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
     (string * thm list) list * local_theory
-  val abbrev: (string * bool -> binding * mixfix -> term ->
+  val abbrev: (Syntax.mode -> binding * mixfix -> term ->
       term list * term list -> local_theory -> local_theory) ->
-    string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
+    Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
 
-  (*theory operations*)
-  val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
-    term list * term list -> local_theory -> (term * thm) * local_theory
-  val theory_notes: string ->
+  (*theory target primitives*)
+  val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+     term list * term list -> local_theory -> (term * thm) * local_theory
+  val theory_target_notes: string ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
+  val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+    local_theory -> local_theory
+
+  (*theory target operations*)
+  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
+    local_theory -> (term * term) * local_theory
   val theory_declaration: declaration -> local_theory -> local_theory
-  val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
-    local_theory -> local_theory
   val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
 
-  (*locale operations*)
-  val locale_notes: string -> string ->
+  (*locale target primitives*)
+  val locale_target_notes: string -> string ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
+  val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+    local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+  val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
+    (binding * mixfix) * term -> local_theory -> local_theory
+
+  (*locale operations*)
+  val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
+    local_theory -> (term * term) * local_theory
   val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
     local_theory -> local_theory
-  val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
-    (binding * mixfix) * term -> local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
   val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
@@ -63,30 +78,23 @@
 structure Generic_Target: GENERIC_TARGET =
 struct
 
-(** notes **)
-
-fun standard_facts lthy ctxt =
-  Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+(** consts **)
 
-fun standard_notes pred kind facts lthy =
-  Local_Theory.map_contexts (fn level => fn ctxt =>
-    if pred (Local_Theory.level lthy, level)
-    then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
-    else ctxt) lthy;
-
+fun export_abbrev lthy preprocess rhs =
+  let
+    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
-
-(** declarations **)
+    val rhs' = rhs
+      |> Assumption.export_term lthy (Local_Theory.target_of lthy)
+      |> preprocess;
+    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
+    val u = fold_rev lambda term_params rhs';
+    val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
-fun standard_declaration pred decl lthy =
-  Local_Theory.map_contexts (fn level => fn ctxt =>
-    if pred (Local_Theory.level lthy, level)
-    then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
-    else ctxt) lthy;
-
-
-
-(** consts **)
+    val extra_tfrees =
+      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
+  in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
 
 fun check_mixfix ctxt (b, extra_tfrees) mx =
   if null extra_tfrees then mx
@@ -139,9 +147,6 @@
     end
   else context;
 
-fun standard_const pred prmode ((b, mx), rhs) =
-  standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
-
 
 
 (** background primitives **)
@@ -174,7 +179,28 @@
 
 
 
-(** lifting primitive to local theory operations **)
+(** nested local theories primitives **)
+
+fun standard_facts lthy ctxt =
+  Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+
+fun standard_notes pred kind facts lthy =
+  Local_Theory.map_contexts (fn level => fn ctxt =>
+    if pred (Local_Theory.level lthy, level)
+    then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
+    else ctxt) lthy;
+
+fun standard_declaration pred decl lthy =
+  Local_Theory.map_contexts (fn level => fn ctxt =>
+    if pred (Local_Theory.level lthy, level)
+    then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
+    else ctxt) lthy;
+
+fun standard_const pred prmode ((b, mx), rhs) =
+  standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
+
+
+(** lifting target primitives to local theory operations **)
 
 (* define *)
 
@@ -264,7 +290,7 @@
 
 in
 
-fun notes notes' kind facts lthy =
+fun notes target_notes kind facts lthy =
   let
     val facts' = facts
       |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
@@ -274,7 +300,7 @@
     val global_facts = Global_Theory.map_facts #2 facts';
   in
     lthy
-    |> notes' kind global_facts (Attrib.partial_evaluation lthy local_facts)
+    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
     |> Attrib.local_notes kind local_facts
   end;
 
@@ -283,43 +309,31 @@
 
 (* abbrev *)
 
-fun abbrev abbrev' prmode ((b, mx), rhs) lthy =
+fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   let
-    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
-
-    val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs;
-    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
-    val u = fold_rev lambda term_params rhs';
-    val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
-
-    val extra_tfrees =
-      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+    val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs;
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
-    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in
     lthy
-    |> abbrev' prmode (b, mx') global_rhs (type_params, term_params)
+    |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
     |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
     |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
   end;
 
 
 
-(** theory operations **)
+(** theory target primitives **)
 
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
-fun theory_notes kind global_facts local_facts =
+fun theory_target_notes kind global_facts local_facts =
   Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
   #> standard_notes (op <>) kind local_facts;
 
-fun theory_declaration decl =
-  background_declaration decl #> standard_declaration (K true) decl;
-
-fun theory_abbrev prmode (b, mx) global_rhs params =
+fun theory_target_abbrev prmode (b, mx) global_rhs params =
   Local_Theory.background_theory_result
     (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
       (fn (lhs, _) =>  (* FIXME type_params!? *)
@@ -327,14 +341,22 @@
   #-> (fn lhs => standard_const (op <>) prmode
           ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
 
+
+(** theory operations **)
+
+val theory_abbrev = abbrev theory_target_abbrev;
+
+fun theory_declaration decl =
+  background_declaration decl #> standard_declaration (K true) decl;
+
 val theory_registration =
   Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
 
 
 
-(** locale operations **)
+(** locale target primitives **)
 
-fun locale_notes locale kind global_facts local_facts =
+fun locale_target_notes locale kind global_facts local_facts =
   Local_Theory.background_theory
     (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
   (fn lthy => lthy |>
@@ -347,14 +369,17 @@
     Locale.add_declaration locale syntax
       (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
 
+fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
+  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+
+
+(** locale operations **)
+
 fun locale_declaration locale {syntax, pervasive} decl =
   pervasive ? background_declaration decl
   #> locale_target_declaration locale syntax decl
   #> standard_declaration (fn (_, other) => other <> 0) decl;
 
-fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
-  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
-
 fun locale_const locale prmode ((b, mx), rhs) =
   locale_target_const locale (K true) prmode ((b, mx), rhs)
   #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
@@ -363,4 +388,13 @@
   (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
   #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
 
+
+(** locale abbreviations **)
+
+fun locale_target_abbrev locale prmode (b, mx) global_rhs params =
+  background_abbrev (b, global_rhs) (snd params)
+  #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs));
+
+fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
+
 end;
diff -r ccafd7d193e7 -r 2e1c1968b38e src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -75,30 +75,22 @@
   #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
     #> pair (lhs, def));
 
-fun foundation ("", _) = Generic_Target.theory_foundation
+fun foundation ("", _) = Generic_Target.theory_target_foundation
   | foundation (locale, false) = locale_foundation locale
   | foundation (class, true) = class_foundation class;
 
 
 (* notes *)
 
-fun notes ("", _) = Generic_Target.theory_notes
-  | notes (locale, _) = Generic_Target.locale_notes locale;
+fun notes ("", _) = Generic_Target.theory_target_notes
+  | notes (locale, _) = Generic_Target.locale_target_notes locale;
 
 
 (* abbrev *)
 
-fun locale_abbrev locale prmode (b, mx) global_rhs params =
-  Generic_Target.background_abbrev (b, global_rhs) (snd params)
-  #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs));
-
-fun class_abbrev class prmode (b, mx) global_rhs params =
-  Generic_Target.background_abbrev (b, global_rhs) (snd params)
-  #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params);
-
 fun abbrev ("", _) = Generic_Target.theory_abbrev
-  | abbrev (locale, false) = locale_abbrev locale
-  | abbrev (class, true) = class_abbrev class;
+  | abbrev (locale, false) = Generic_Target.locale_abbrev locale
+  | abbrev (class, true) = Class.abbrev class;
 
 
 (* declaration *)
@@ -165,7 +157,7 @@
     |> Local_Theory.init background_naming
        {define = Generic_Target.define (foundation name_data),
         notes = Generic_Target.notes (notes name_data),
-        abbrev = Generic_Target.abbrev (abbrev name_data),
+        abbrev = abbrev name_data,
         declaration = declaration name_data,
         subscription = subscription name_data,
         pretty = pretty name_data,
diff -r ccafd7d193e7 -r 2e1c1968b38e src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Tue Jun 02 13:14:36 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -11,6 +11,7 @@
   val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     -> Proof.context -> Proof.context
   val set_primary_constraints: Proof.context -> Proof.context
+  val show_reverted_improvements: bool Config.T;
 
   val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
   val overloading_cmd: (string * string * bool) list -> theory -> local_theory
@@ -21,63 +22,46 @@
 
 (* generic check/uncheck combinators for improvable constants *)
 
-type improvable_syntax = ((((string * typ) list * (string * typ) list) *
-  ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
-    (term * term) list)) * bool);
+type improvable_syntax = {
+  primary_constraints: (string * typ) list,
+  secondary_constraints: (string * typ) list,
+  improve: string * typ -> (typ * typ) option,
+  subst: string * typ -> (typ * term) option,
+  no_subst_in_abbrev_mode: bool,
+  unchecks: (term * term) list
+}
 
 structure Improvable_Syntax = Proof_Data
 (
-  type T = {
-    primary_constraints: (string * typ) list,
-    secondary_constraints: (string * typ) list,
-    improve: string * typ -> (typ * typ) option,
-    subst: string * typ -> (typ * term) option,
-    consider_abbrevs: bool,
-    unchecks: (term * term) list,
-    passed: bool
-  };
-  val empty: T = {
-    primary_constraints = [],
-    secondary_constraints = [],
-    improve = K NONE,
-    subst = K NONE,
-    consider_abbrevs = false,
-    unchecks = [],
-    passed = true
-  };
-  fun init _ = empty;
+  type T = {syntax: improvable_syntax, secondary_pass: bool}
+  fun init _ = {syntax = {
+      primary_constraints = [],
+      secondary_constraints = [],
+      improve = K NONE,
+      subst = K NONE,
+      no_subst_in_abbrev_mode = false,
+      unchecks = []
+    }, secondary_pass = false}: T;
 );
 
-fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints,
-    secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} =>
-  let
-    val (((primary_constraints', secondary_constraints'),
-      (((improve', subst'), consider_abbrevs'), unchecks')), passed')
-        = f (((primary_constraints, secondary_constraints),
-            (((improve, subst), consider_abbrevs), unchecks)), passed)
-  in
-   {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
-    improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
-    unchecks = unchecks', passed = passed'}
-  end);
+fun map_improvable_syntax f =
+  Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = f syntax, secondary_pass = secondary_pass});
 
-val mark_passed = (map_improvable_syntax o apsnd) (K true);
+val mark_passed =
+  Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = syntax, secondary_pass = true});
 
 fun improve_term_check ts ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} =
+    val {syntax = {secondary_constraints, improve, subst, no_subst_in_abbrev_mode, ...}, secondary_pass} =
       Improvable_Syntax.get ctxt;
-    val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
-    val passed_or_abbrev = passed orelse is_abbrev;
+    val no_subst = Proof_Context.abbrev_mode ctxt andalso no_subst_in_abbrev_mode;
     fun accumulate_improvements (Const (c, ty)) =
           (case improve (c, ty) of
             SOME ty_ty' => Sign.typ_match thy ty_ty'
           | _ => I)
       | accumulate_improvements _ = I;
-    val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
-    val ts' = (map o map_types) (Envir.subst_type improvements) ts;
     fun apply_subst t =
       Envir.expand_term
         (fn Const (c, ty) =>
@@ -87,30 +71,40 @@
               then SOME (ty', apply_subst t') else NONE
           | NONE => NONE)
         | _ => NONE) t;
-    val ts'' = if is_abbrev then ts' else map apply_subst ts';
+    val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
+    val ts' =
+      ts
+      |> (map o map_types) (Envir.subst_type improvements)
+      |> not no_subst ? map apply_subst;
   in
-    if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE
-    else if passed_or_abbrev then SOME (ts'', ctxt)
+    if secondary_pass orelse no_subst then
+      if eq_list (op aconv) (ts, ts') then NONE
+      else SOME (ts', ctxt)
     else
-      SOME (ts'', ctxt
+      SOME (ts', ctxt
         |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
         |> mark_passed)
   end;
 
 fun rewrite_liberal thy unchecks t =
-  (case try (Pattern.rewrite_term thy unchecks []) t of
+  (case try (Pattern.rewrite_term_top thy unchecks []) t of
     NONE => NONE
   | SOME t' => if t aconv t' then NONE else SOME t');
 
+val show_reverted_improvements =
+  Attrib.setup_config_bool @{binding "show_reverted_improvements"} (K true);
+
 fun improve_term_uncheck ts ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val {unchecks, ...} = Improvable_Syntax.get ctxt;
+    val {syntax = {unchecks, ...}, ...} = Improvable_Syntax.get ctxt;
+    val revert = Config.get ctxt show_reverted_improvements;
     val ts' = map (rewrite_liberal thy unchecks) ts;
-  in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
+  in if revert andalso exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
 
 fun set_primary_constraints ctxt =
-  let val {primary_constraints, ...} = Improvable_Syntax.get ctxt;
+  let
+    val {syntax = {primary_constraints, ...}, ...} = Improvable_Syntax.get ctxt;
   in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
 
 val activate_improvable_syntax =
@@ -147,7 +141,9 @@
       map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
   in 
     ctxt
-    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
+    |> map_improvable_syntax (K {primary_constraints = [],
+      secondary_constraints = [], improve = K NONE, subst = subst,
+      no_subst_in_abbrev_mode = false, unchecks = unchecks})
   end;
 
 fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
@@ -165,7 +161,7 @@
       if mx <> NoSyn
       then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
       else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
-  | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
+  | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
   let
@@ -205,8 +201,8 @@
     |> synchronize_syntax
     |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes Generic_Target.theory_notes,
-        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+        notes = Generic_Target.notes Generic_Target.theory_target_notes,
+        abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         subscription = Generic_Target.theory_registration,
         pretty = pretty,