separate class for division operator, with particular syntax added in more specific classes
--- a/NEWS Mon Jun 01 18:59:21 2015 +0200
+++ b/NEWS Mon Jun 01 18:59:21 2015 +0200
@@ -36,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)
------------------------------
--- a/src/Doc/Main/Main_Doc.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/Doc/Main/Main_Doc.thy Mon Jun 01 18:59:21 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}
--- a/src/HOL/Code_Numeral.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Code_Numeral.thy Mon Jun 01 18:59:21 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"
--- a/src/HOL/Complex.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Complex.thy Mon Jun 01 18:59:21 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
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Jun 01 18:59:21 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))
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Jun 01 18:59:21 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)
--- a/src/HOL/Divides.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Divides.thy Mon Jun 01 18:59:21 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. *}
@@ -951,19 +956,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 +1081,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 +1196,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 +1600,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 +1694,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 +1934,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;
--- a/src/HOL/Enum.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Enum.thy Mon Jun 01 18:59:21 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
--- a/src/HOL/Fields.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Fields.thy Mon Jun 01 18:59:21 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"
@@ -385,6 +366,7 @@
lemma diff_frac_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
+ thm field_simps
by (simp add: field_simps)
lemma frac_eq_eq:
--- a/src/HOL/Library/Bit.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Bit.thy Mon Jun 01 18:59:21 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
-
--- a/src/HOL/Library/Extended_Real.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Jun 01 18:59:21 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 ..
--- a/src/HOL/Library/Fraction_Field.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Mon Jun 01 18:59:21 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)
--- a/src/HOL/Library/Function_Division.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Function_Division.thy Mon Jun 01 18:59:21 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
-
--- a/src/HOL/Library/Nat_Bijection.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy Mon Jun 01 18:59:21 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
-
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Mon Jun 01 18:59:21 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
--- a/src/HOL/Library/Old_SMT/old_z3_interface.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML Mon Jun 01 18:59:21 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
--- a/src/HOL/Library/Polynomial.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Jun 01 18:59:21 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
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Jun 01 18:59:21 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 *}
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jun 01 18:59:21 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"}),
--- a/src/HOL/NSA/StarDef.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Jun 01 18:59:21 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
--- a/src/HOL/Rat.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Rat.thy Mon Jun 01 18:59:21 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
--- a/src/HOL/Real.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Real.thy Mon Jun 01 18:59:21 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)
--- a/src/HOL/Rings.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Rings.thy Mon Jun 01 18:59:21 2015 +0200
@@ -415,6 +415,33 @@
end
+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 semiring_no_zero_divisors = semiring_0 +
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
begin
--- a/src/HOL/SMT_Examples/SMT_Examples.certs Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Mon Jun 01 18:59:21 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")
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 01 18:59:21 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)]
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 01 18:59:21 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}, _)),
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Jun 01 18:59:21 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
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Jun 01 18:59:21 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 =
--- a/src/HOL/Tools/SMT/z3_interface.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Mon Jun 01 18:59:21 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
--- a/src/HOL/Tools/SMT/z3_real.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_real.ML Mon Jun 01 18:59:21 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))
--- a/src/HOL/Tools/lin_arith.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon Jun 01 18:59:21 2015 +0200
@@ -152,7 +152,7 @@
(SOME t', m'') => (SOME (mC $ s' $ t'), m'')
| (NONE, m'') => (SOME s', m''))
| (NONE, m') => demult (t, m')))
- | demult (atom as (mC as Const (@{const_name Fields.divide}, T)) $ 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
@@ -219,7 +219,7 @@
(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}, T) $ _ $ _, m, pi as (p, i)) =
+ | 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')
@@ -302,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)
@@ -501,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)
@@ -592,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
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Mon Jun 01 18:59:21 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}
);
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Jun 01 18:59:21 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]
--- a/src/HOL/Tools/semiring_normalizer.ML Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Mon Jun 01 18:59:21 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)))
--- a/src/HOL/Word/Word.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Word/Word.thy Mon Jun 01 18:59:21 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)"
--- a/src/HOL/ex/Dedekind_Real.thy Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Mon Jun 01 18:59:21 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>