separate class for division operator, with particular syntax added in more specific classes
authorhaftmann
Mon Jun 01 18:59:21 2015 +0200 (2015-06-01)
changeset 60352d46de31a50c4
parent 60351 5cdf3903a302
child 60353 838025c6e278
separate class for division operator, with particular syntax added in more specific classes
NEWS
src/Doc/Main/Main_Doc.thy
src/HOL/Code_Numeral.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Fields.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Function_Division.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Library/Old_SMT/old_smt_normalize.ML
src/HOL/Library/Old_SMT/old_z3_interface.ML
src/HOL/Library/Polynomial.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/NSA/StarDef.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/SMT_Examples/SMT_Examples.certs
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_real.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/semiring_normalizer.ML
src/HOL/Word/Word.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/NEWS	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/NEWS	Mon Jun 01 18:59:21 2015 +0200
     1.3 @@ -36,6 +36,14 @@
     1.4  * Nitpick:
     1.5    - Removed "check_potential" and "check_genuine" options.
     1.6  
     1.7 +* Constants Fields.divide (... / ...) and Divides.div (... div ...)
     1.8 +are logically unified to Rings.divide in syntactic type class
     1.9 +Rings.divide, with particular infix syntax added as abbreviations
    1.10 +in classes Fields.inverse and Divides.div respectively.  INCOMPATIBILITY,
    1.11 +instantiatios must refer to Rings.divide rather than the former
    1.12 +separate constants, and infix syntax is usually not available during
    1.13 +instantiation.
    1.14 +
    1.15  
    1.16  New in Isabelle2015 (May 2015)
    1.17  ------------------------------
     2.1 --- a/src/Doc/Main/Main_Doc.thy	Mon Jun 01 18:59:21 2015 +0200
     2.2 +++ b/src/Doc/Main/Main_Doc.thy	Mon Jun 01 18:59:21 2015 +0200
     2.3 @@ -325,7 +325,7 @@
     2.4  @{const abs} & @{typeof abs}\\
     2.5  @{const sgn} & @{typeof sgn}\\
     2.6  @{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
     2.7 -@{const div_class.div} & @{typeof "div_class.div"}\\
     2.8 +@{const Rings.divide} & @{typeof Rings.divide}\\
     2.9  @{const div_class.mod} & @{typeof "div_class.mod"}\\
    2.10  \end{supertabular}
    2.11  
     3.1 --- a/src/HOL/Code_Numeral.thy	Mon Jun 01 18:59:21 2015 +0200
     3.2 +++ b/src/HOL/Code_Numeral.thy	Mon Jun 01 18:59:21 2015 +0200
     3.3 @@ -150,11 +150,11 @@
     3.4  instantiation integer :: "{ring_div, equal, linordered_idom}"
     3.5  begin
     3.6  
     3.7 -lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
     3.8 -  is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
     3.9 +lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    3.10 +  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
    3.11    .
    3.12  
    3.13 -declare div_integer.rep_eq [simp]
    3.14 +declare divide_integer.rep_eq [simp]
    3.15  
    3.16  lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    3.17    is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
    3.18 @@ -709,11 +709,11 @@
    3.19  instantiation natural :: "{semiring_div, equal, linordered_semiring}"
    3.20  begin
    3.21  
    3.22 -lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    3.23 -  is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
    3.24 +lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    3.25 +  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
    3.26    .
    3.27  
    3.28 -declare div_natural.rep_eq [simp]
    3.29 +declare divide_natural.rep_eq [simp]
    3.30  
    3.31  lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    3.32    is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
     4.1 --- a/src/HOL/Complex.thy	Mon Jun 01 18:59:21 2015 +0200
     4.2 +++ b/src/HOL/Complex.thy	Mon Jun 01 18:59:21 2015 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4    "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
     4.5  | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
     4.6  
     4.7 -definition "x / (y\<Colon>complex) = x * inverse y"
     4.8 +definition "divide x (y\<Colon>complex) = x * inverse y"
     4.9  
    4.10  instance
    4.11    by intro_classes
     5.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Jun 01 18:59:21 2015 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Jun 01 18:59:21 2015 +0200
     5.3 @@ -710,7 +710,7 @@
     5.4  
     5.5  fun dest_frac ct =
     5.6    case Thm.term_of ct of
     5.7 -    Const (@{const_name Fields.divide},_) $ a $ b=>
     5.8 +    Const (@{const_name Rings.divide},_) $ a $ b=>
     5.9        Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    5.10    | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
    5.11    | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
     6.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Jun 01 18:59:21 2015 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Jun 01 18:59:21 2015 +0200
     6.3 @@ -4033,7 +4033,7 @@
     6.4        @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
     6.5    | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) =
     6.6        @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
     6.7 -  | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) =
     6.8 +  | num_of_term ps (Const (@{const_name Rings.divide}, _) $ a $ b) =
     6.9        mk_C (dest_num a, dest_num b)
    6.10    | num_of_term ps t =
    6.11        (case try_dest_num t of
    6.12 @@ -4087,7 +4087,7 @@
    6.13          (if d = 1 then HOLogic.mk_number T c
    6.14          else if d = 0 then Const (@{const_name Groups.zero}, T)
    6.15          else
    6.16 -          Const (@{const_name Fields.divide}, binopT T) $
    6.17 +          Const (@{const_name Rings.divide}, binopT T) $
    6.18              HOLogic.mk_number T c $ HOLogic.mk_number T d)
    6.19        end
    6.20    | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
     7.1 --- a/src/HOL/Divides.thy	Mon Jun 01 18:59:21 2015 +0200
     7.2 +++ b/src/HOL/Divides.thy	Mon Jun 01 18:59:21 2015 +0200
     7.3 @@ -11,10 +11,15 @@
     7.4  
     7.5  subsection {* Syntactic division operations *}
     7.6  
     7.7 -class div = dvd +
     7.8 -  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
     7.9 -    and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
    7.10 -
    7.11 +class div = dvd + divide +
    7.12 +  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    7.13 +begin
    7.14 +
    7.15 +abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
    7.16 +where
    7.17 +  "op div \<equiv> divide"
    7.18 +
    7.19 +end
    7.20  
    7.21  subsection {* Abstract division in commutative semirings. *}
    7.22  
    7.23 @@ -951,19 +956,26 @@
    7.24    shows "divmod_nat m n = qr"
    7.25    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
    7.26  
    7.27 +instantiation nat :: "Divides.div"
    7.28 +begin
    7.29 +
    7.30 +definition divide_nat where
    7.31 +  div_nat_def: "divide m n = fst (divmod_nat m n)"
    7.32 +
    7.33 +definition mod_nat where
    7.34 +  "m mod n = snd (divmod_nat m n)"
    7.35 +  
    7.36 +instance ..
    7.37 +
    7.38 +end
    7.39 +
    7.40  instantiation nat :: semiring_div
    7.41  begin
    7.42  
    7.43 -definition div_nat where
    7.44 -  "m div n = fst (divmod_nat m n)"
    7.45 -
    7.46  lemma fst_divmod_nat [simp]:
    7.47    "fst (divmod_nat m n) = m div n"
    7.48    by (simp add: div_nat_def)
    7.49  
    7.50 -definition mod_nat where
    7.51 -  "m mod n = snd (divmod_nat m n)"
    7.52 -
    7.53  lemma snd_divmod_nat [simp]:
    7.54    "snd (divmod_nat m n) = m mod n"
    7.55    by (simp add: mod_nat_def)
    7.56 @@ -1069,7 +1081,7 @@
    7.57  ML {*
    7.58  structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
    7.59  (
    7.60 -  val div_name = @{const_name div};
    7.61 +  val div_name = @{const_name divide};
    7.62    val mod_name = @{const_name mod};
    7.63    val mk_binop = HOLogic.mk_binop;
    7.64    val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    7.65 @@ -1184,18 +1196,23 @@
    7.66    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    7.67  by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
    7.68  
    7.69 -lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
    7.70 -  apply (cut_tac m = q and n = c in mod_less_divisor)
    7.71 -  apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
    7.72 -  apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
    7.73 -  apply (simp add: add_mult_distrib2)
    7.74 -  done
    7.75 -
    7.76  lemma divmod_nat_rel_mult2_eq:
    7.77 -  "divmod_nat_rel a b (q, r)
    7.78 -   \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
    7.79 -by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
    7.80 -
    7.81 +  assumes "divmod_nat_rel a b (q, r)"
    7.82 +  shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
    7.83 +proof -
    7.84 +  { assume "r < b" and "0 < c" 
    7.85 +    then have "b * (q mod c) + r < b * c"
    7.86 +      apply (cut_tac m = q and n = c in mod_less_divisor)
    7.87 +      apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
    7.88 +      apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
    7.89 +      apply (simp add: add_mult_distrib2)
    7.90 +      done
    7.91 +    then have "r + b * (q mod c) < b * c"
    7.92 +      by (simp add: ac_simps)
    7.93 +  } with assms show ?thesis
    7.94 +    by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
    7.95 +qed
    7.96 +    
    7.97  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
    7.98  by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
    7.99  
   7.100 @@ -1583,8 +1600,16 @@
   7.101    using odd_succ_div_two [of n] by simp
   7.102  
   7.103  lemma odd_two_times_div_two_nat [simp]:
   7.104 -  "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
   7.105 -  using odd_two_times_div_two_succ [of n] by simp
   7.106 +  assumes "odd n"
   7.107 +  shows "2 * (n div 2) = n - (1 :: nat)"
   7.108 +proof -
   7.109 +  from assms have "2 * (n div 2) + 1 = n"
   7.110 +    by (rule odd_two_times_div_two_succ)
   7.111 +  then have "Suc (2 * (n div 2)) - 1 = n - 1"
   7.112 +    by simp
   7.113 +  then show ?thesis
   7.114 +    by simp
   7.115 +qed
   7.116  
   7.117  lemma odd_Suc_minus_one [simp]:
   7.118    "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   7.119 @@ -1669,24 +1694,24 @@
   7.120  instantiation int :: Divides.div
   7.121  begin
   7.122  
   7.123 -definition div_int where
   7.124 -  "a div b = fst (divmod_int a b)"
   7.125 +definition divide_int where
   7.126 +  div_int_def: "divide a b = fst (divmod_int a b)"
   7.127 +
   7.128 +definition mod_int where
   7.129 +  "a mod b = snd (divmod_int a b)"
   7.130 +
   7.131 +instance ..
   7.132 +
   7.133 +end
   7.134  
   7.135  lemma fst_divmod_int [simp]:
   7.136    "fst (divmod_int a b) = a div b"
   7.137    by (simp add: div_int_def)
   7.138  
   7.139 -definition mod_int where
   7.140 -  "a mod b = snd (divmod_int a b)"
   7.141 -
   7.142  lemma snd_divmod_int [simp]:
   7.143    "snd (divmod_int a b) = a mod b"
   7.144    by (simp add: mod_int_def)
   7.145  
   7.146 -instance ..
   7.147 -
   7.148 -end
   7.149 -
   7.150  lemma divmod_int_mod_div:
   7.151    "divmod_int p q = (p div q, p mod q)"
   7.152    by (simp add: prod_eq_iff)
   7.153 @@ -1909,7 +1934,7 @@
   7.154  ML {*
   7.155  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   7.156  (
   7.157 -  val div_name = @{const_name div};
   7.158 +  val div_name = @{const_name Rings.divide};
   7.159    val mod_name = @{const_name mod};
   7.160    val mk_binop = HOLogic.mk_binop;
   7.161    val mk_sum = Arith_Data.mk_sum HOLogic.intT;
     8.1 --- a/src/HOL/Enum.thy	Mon Jun 01 18:59:21 2015 +0200
     8.2 +++ b/src/HOL/Enum.thy	Mon Jun 01 18:59:21 2015 +0200
     8.3 @@ -585,12 +585,11 @@
     8.4  definition [simp]: "Groups.one = a\<^sub>1"
     8.5  definition [simp]: "op + = (\<lambda>_ _. a\<^sub>1)"
     8.6  definition [simp]: "op * = (\<lambda>_ _. a\<^sub>1)"
     8.7 -definition [simp]: "op div = (\<lambda>_ _. a\<^sub>1)" 
     8.8  definition [simp]: "op mod = (\<lambda>_ _. a\<^sub>1)" 
     8.9  definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
    8.10  definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
    8.11  definition [simp]: "inverse = (\<lambda>_. a\<^sub>1)"
    8.12 -definition [simp]: "op / = (\<lambda>_ _. a\<^sub>1)"
    8.13 +definition [simp]: "divide = (\<lambda>_ _. a\<^sub>1)"
    8.14  
    8.15  instance by intro_classes(simp_all add: less_finite_1_def)
    8.16  end
    8.17 @@ -691,15 +690,14 @@
    8.18  definition "op - = (op + :: finite_2 \<Rightarrow> _)"
    8.19  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    8.20  definition "inverse = (\<lambda>x :: finite_2. x)"
    8.21 -definition "op / = (op * :: finite_2 \<Rightarrow> _)"
    8.22 +definition "divide = (op * :: finite_2 \<Rightarrow> _)"
    8.23  definition "abs = (\<lambda>x :: finite_2. x)"
    8.24 -definition "op div = (op / :: finite_2 \<Rightarrow> _)"
    8.25  definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    8.26  definition "sgn = (\<lambda>x :: finite_2. x)"
    8.27  instance
    8.28  by intro_classes
    8.29    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    8.30 -       inverse_finite_2_def divide_finite_2_def abs_finite_2_def div_finite_2_def mod_finite_2_def sgn_finite_2_def
    8.31 +       inverse_finite_2_def divide_finite_2_def abs_finite_2_def mod_finite_2_def sgn_finite_2_def
    8.32       split: finite_2.splits)
    8.33  end
    8.34  
    8.35 @@ -819,15 +817,14 @@
    8.36  definition "x - y = x + (- y :: finite_3)"
    8.37  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)"
    8.38  definition "inverse = (\<lambda>x :: finite_3. x)" 
    8.39 -definition "x / y = x * inverse (y :: finite_3)"
    8.40 +definition "divide x y = x * inverse (y :: finite_3)"
    8.41  definition "abs = (\<lambda>x :: finite_3. x)"
    8.42 -definition "op div = (op / :: finite_3 \<Rightarrow> _)"
    8.43  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)"
    8.44  definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
    8.45  instance
    8.46  by intro_classes
    8.47    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    8.48 -       inverse_finite_3_def divide_finite_3_def abs_finite_3_def div_finite_3_def mod_finite_3_def sgn_finite_3_def
    8.49 +       inverse_finite_3_def divide_finite_3_def abs_finite_3_def mod_finite_3_def sgn_finite_3_def
    8.50         less_finite_3_def
    8.51       split: finite_3.splits)
    8.52  end
     9.1 --- a/src/HOL/Fields.thy	Mon Jun 01 18:59:21 2015 +0200
     9.2 +++ b/src/HOL/Fields.thy	Mon Jun 01 18:59:21 2015 +0200
     9.3 @@ -19,35 +19,16 @@
     9.4    A division ring is like a field, but without the commutativity requirement.
     9.5  *}
     9.6  
     9.7 -class inverse =
     9.8 +class inverse = divide +
     9.9    fixes inverse :: "'a \<Rightarrow> 'a"
    9.10 -    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    9.11 -
    9.12 -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    9.13 -
    9.14 -
    9.15 -context semiring
    9.16  begin
    9.17 -
    9.18 -lemma [field_simps]:
    9.19 -  shows distrib_left_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
    9.20 -    and distrib_right_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
    9.21 -  by (rule distrib_left distrib_right)+
    9.22 +  
    9.23 +abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    9.24 +where
    9.25 +  "inverse_divide \<equiv> divide"
    9.26  
    9.27  end
    9.28  
    9.29 -context ring
    9.30 -begin
    9.31 -
    9.32 -lemma [field_simps]:
    9.33 -  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
    9.34 -    and right_diff_distrib_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
    9.35 -  by (rule left_diff_distrib right_diff_distrib)+
    9.36 -
    9.37 -end
    9.38 -
    9.39 -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    9.40 -
    9.41  text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
    9.42  
    9.43  named_theorems divide_simps "rewrite rules to eliminate divisions"
    9.44 @@ -385,6 +366,7 @@
    9.45  
    9.46  lemma diff_frac_eq:
    9.47    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
    9.48 +  thm field_simps
    9.49    by (simp add: field_simps)
    9.50  
    9.51  lemma frac_eq_eq:
    10.1 --- a/src/HOL/Library/Bit.thy	Mon Jun 01 18:59:21 2015 +0200
    10.2 +++ b/src/HOL/Library/Bit.thy	Mon Jun 01 18:59:21 2015 +0200
    10.3 @@ -117,7 +117,7 @@
    10.4    "inverse x = (x :: bit)"
    10.5  
    10.6  definition divide_bit_def [simp]:
    10.7 -  "x / y = (x * y :: bit)"
    10.8 +  "divide x y = (x * y :: bit)"
    10.9  
   10.10  lemmas field_bit_defs =
   10.11    plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   10.12 @@ -201,4 +201,3 @@
   10.13  hide_const (open) set
   10.14  
   10.15  end
   10.16 -
    11.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Jun 01 18:59:21 2015 +0200
    11.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon Jun 01 18:59:21 2015 +0200
    11.3 @@ -1403,7 +1403,7 @@
    11.4    by (auto intro: ereal_cases)
    11.5  termination by (relation "{}") simp
    11.6  
    11.7 -definition "x / y = x * inverse (y :: ereal)"
    11.8 +definition "divide x y = x * inverse (y :: ereal)"
    11.9  
   11.10  instance ..
   11.11  
    12.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Jun 01 18:59:21 2015 +0200
    12.2 +++ b/src/HOL/Library/Fraction_Field.thy	Mon Jun 01 18:59:21 2015 +0200
    12.3 @@ -241,9 +241,9 @@
    12.4      by (simp add: Fract_def inverse_fract_def UN_fractrel)
    12.5  qed
    12.6  
    12.7 -definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
    12.8 +definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
    12.9  
   12.10 -lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   12.11 +lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
   12.12    by (simp add: divide_fract_def)
   12.13  
   12.14  instance
   12.15 @@ -255,7 +255,7 @@
   12.16        (simp_all add: fract_expand eq_fract mult.commute)
   12.17  next
   12.18    fix q r :: "'a fract"
   12.19 -  show "q / r = q * inverse r" by (simp add: divide_fract_def)
   12.20 +  show "divide q r = q * inverse r" by (simp add: divide_fract_def)
   12.21  next
   12.22    show "inverse 0 = (0:: 'a fract)"
   12.23      by (simp add: fract_expand) (simp add: fract_collapse)
    13.1 --- a/src/HOL/Library/Function_Division.thy	Mon Jun 01 18:59:21 2015 +0200
    13.2 +++ b/src/HOL/Library/Function_Division.thy	Mon Jun 01 18:59:21 2015 +0200
    13.3 @@ -15,7 +15,7 @@
    13.4  
    13.5  definition "inverse f = inverse \<circ> f"
    13.6  
    13.7 -definition "(f / g) = (\<lambda>x. f x / g x)"
    13.8 +definition "divide f g = (\<lambda>x. f x / g x)"
    13.9  
   13.10  instance ..
   13.11  
   13.12 @@ -63,4 +63,3 @@
   13.13  *}
   13.14  
   13.15  end
   13.16 -
    14.1 --- a/src/HOL/Library/Nat_Bijection.thy	Mon Jun 01 18:59:21 2015 +0200
    14.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Mon Jun 01 18:59:21 2015 +0200
    14.3 @@ -336,10 +336,19 @@
    14.4  
    14.5  lemma set_decode_plus_power_2:
    14.6    "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
    14.7 - apply (induct n arbitrary: z, simp_all)
    14.8 -  apply (rule set_eqI, induct_tac x, simp, simp)
    14.9 - apply (rule set_eqI, induct_tac x, simp, simp add: add.commute)
   14.10 -done
   14.11 +proof (induct n arbitrary: z)
   14.12 +  case 0 show ?case
   14.13 +  proof (rule set_eqI)
   14.14 +    fix q show "q \<in> set_decode (2 ^ 0 + z) \<longleftrightarrow> q \<in> insert 0 (set_decode z)"
   14.15 +      by (induct q) (insert 0, simp_all)
   14.16 +  qed
   14.17 +next
   14.18 +  case (Suc n) show ?case
   14.19 +  proof (rule set_eqI)
   14.20 +    fix q show "q \<in> set_decode (2 ^ Suc n + z) \<longleftrightarrow> q \<in> insert (Suc n) (set_decode z)"
   14.21 +      by (induct q) (insert Suc, simp_all)
   14.22 +  qed
   14.23 +qed
   14.24  
   14.25  lemma finite_set_decode [simp]: "finite (set_decode n)"
   14.26  apply (induct n rule: nat_less_induct)
   14.27 @@ -389,4 +398,3 @@
   14.28  qed
   14.29  
   14.30  end
   14.31 -
    15.1 --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Mon Jun 01 18:59:21 2015 +0200
    15.2 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Mon Jun 01 18:59:21 2015 +0200
    15.3 @@ -429,7 +429,7 @@
    15.4      @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
    15.5  
    15.6    val mult_nat_ops =
    15.7 -    [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
    15.8 +    [@{const times (nat)}, @{const divide (nat)}, @{const mod (nat)}]
    15.9  
   15.10    val nat_ops = simple_nat_ops @ mult_nat_ops
   15.11  
    16.1 --- a/src/HOL/Library/Old_SMT/old_z3_interface.ML	Mon Jun 01 18:59:21 2015 +0200
    16.2 +++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML	Mon Jun 01 18:59:21 2015 +0200
    16.3 @@ -41,7 +41,7 @@
    16.4          has_datatypes=true}
    16.5      end
    16.6  
    16.7 -  fun is_div_mod @{const div (int)} = true
    16.8 +  fun is_div_mod @{const divide (int)} = true
    16.9      | is_div_mod @{const mod (int)} = true
   16.10      | is_div_mod _ = false
   16.11  
    17.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jun 01 18:59:21 2015 +0200
    17.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jun 01 18:59:21 2015 +0200
    17.3 @@ -1360,14 +1360,14 @@
    17.4  instantiation poly :: (field) ring_div
    17.5  begin
    17.6  
    17.7 -definition div_poly where
    17.8 -  "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
    17.9 +definition divide_poly where
   17.10 +  div_poly_def: "divide x y = (THE q. \<exists>r. pdivmod_rel x y q r)"
   17.11  
   17.12  definition mod_poly where
   17.13    "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
   17.14  
   17.15  lemma div_poly_eq:
   17.16 -  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
   17.17 +  "pdivmod_rel x y q r \<Longrightarrow> divide x y = q"
   17.18  unfolding div_poly_def
   17.19  by (fast elim: pdivmod_rel_unique_div)
   17.20  
   17.21 @@ -1377,7 +1377,7 @@
   17.22  by (fast elim: pdivmod_rel_unique_mod)
   17.23  
   17.24  lemma pdivmod_rel:
   17.25 -  "pdivmod_rel x y (x div y) (x mod y)"
   17.26 +  "pdivmod_rel x y (divide x y) (x mod y)"
   17.27  proof -
   17.28    from pdivmod_rel_exists
   17.29      obtain q r where "pdivmod_rel x y q r" by fast
   17.30 @@ -1387,41 +1387,41 @@
   17.31  
   17.32  instance proof
   17.33    fix x y :: "'a poly"
   17.34 -  show "x div y * y + x mod y = x"
   17.35 +  show "divide x y * y + x mod y = x"
   17.36      using pdivmod_rel [of x y]
   17.37      by (simp add: pdivmod_rel_def)
   17.38  next
   17.39    fix x :: "'a poly"
   17.40    have "pdivmod_rel x 0 0 x"
   17.41      by (rule pdivmod_rel_by_0)
   17.42 -  thus "x div 0 = 0"
   17.43 +  thus "divide x 0 = 0"
   17.44      by (rule div_poly_eq)
   17.45  next
   17.46    fix y :: "'a poly"
   17.47    have "pdivmod_rel 0 y 0 0"
   17.48      by (rule pdivmod_rel_0)
   17.49 -  thus "0 div y = 0"
   17.50 +  thus "divide 0 y = 0"
   17.51      by (rule div_poly_eq)
   17.52  next
   17.53    fix x y z :: "'a poly"
   17.54    assume "y \<noteq> 0"
   17.55 -  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   17.56 +  hence "pdivmod_rel (x + z * y) y (z + divide x y) (x mod y)"
   17.57      using pdivmod_rel [of x y]
   17.58      by (simp add: pdivmod_rel_def distrib_right)
   17.59 -  thus "(x + z * y) div y = z + x div y"
   17.60 +  thus "divide (x + z * y) y = z + divide x y"
   17.61      by (rule div_poly_eq)
   17.62  next
   17.63    fix x y z :: "'a poly"
   17.64    assume "x \<noteq> 0"
   17.65 -  show "(x * y) div (x * z) = y div z"
   17.66 +  show "divide (x * y) (x * z) = divide y z"
   17.67    proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
   17.68      have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
   17.69        by (rule pdivmod_rel_by_0)
   17.70 -    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
   17.71 +    then have [simp]: "\<And>x::'a poly. divide x 0 = 0"
   17.72        by (rule div_poly_eq)
   17.73      have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
   17.74        by (rule pdivmod_rel_0)
   17.75 -    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
   17.76 +    then have [simp]: "\<And>x::'a poly. divide 0 x = 0"
   17.77        by (rule div_poly_eq)
   17.78      case False then show ?thesis by auto
   17.79    next
   17.80 @@ -1430,8 +1430,8 @@
   17.81      have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
   17.82        by (auto simp add: pdivmod_rel_def algebra_simps)
   17.83          (rule classical, simp add: degree_mult_eq)
   17.84 -    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
   17.85 -    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
   17.86 +    moreover from pdivmod_rel have "pdivmod_rel y z (divide y z) (y mod z)" .
   17.87 +    ultimately have "pdivmod_rel (x * y) (x * z) (divide y z) (x * (y mod z))" .
   17.88      then show ?thesis by (simp add: div_poly_eq)
   17.89    qed
   17.90  qed
    18.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Jun 01 18:59:21 2015 +0200
    18.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Jun 01 18:59:21 2015 +0200
    18.3 @@ -53,7 +53,7 @@
    18.4  setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
    18.5  setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
    18.6  
    18.7 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
    18.8 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}] *}
    18.9  
   18.10  section {* Arithmetic operations *}
   18.11  
    19.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jun 01 18:59:21 2015 +0200
    19.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jun 01 18:59:21 2015 +0200
    19.3 @@ -283,14 +283,13 @@
    19.4     (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
    19.5     (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
    19.6     (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
    19.7 -   (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
    19.8 -   (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
    19.9 +      (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
   19.10     (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
   19.11     (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
   19.12     (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
   19.13     (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
   19.14     (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
   19.15 -   (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
   19.16 +   (@{const_name Rings.divide}, @{typ "prop => prop => prop"}),
   19.17     (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
   19.18     (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
   19.19     (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
    20.1 --- a/src/HOL/NSA/StarDef.thy	Mon Jun 01 18:59:21 2015 +0200
    20.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Jun 01 18:59:21 2015 +0200
    20.3 @@ -505,11 +505,18 @@
    20.4  
    20.5  end
    20.6  
    20.7 -instantiation star :: (inverse) inverse
    20.8 +instantiation star :: (divide) divide
    20.9  begin
   20.10  
   20.11  definition
   20.12 -  star_divide_def:  "(op /) \<equiv> *f2* (op /)"
   20.13 +  star_divide_def:  "divide \<equiv> *f2* divide"
   20.14 +
   20.15 +instance ..
   20.16 +
   20.17 +end
   20.18 +
   20.19 +instantiation star :: (inverse) inverse
   20.20 +begin
   20.21  
   20.22  definition
   20.23    star_inverse_def: "inverse \<equiv> *f* inverse"
   20.24 @@ -524,9 +531,6 @@
   20.25  begin
   20.26  
   20.27  definition
   20.28 -  star_div_def:     "(op div) \<equiv> *f2* (op div)"
   20.29 -
   20.30 -definition
   20.31    star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
   20.32  
   20.33  instance ..
   20.34 @@ -551,7 +555,7 @@
   20.35    star_add_def      star_diff_def     star_minus_def
   20.36    star_mult_def     star_divide_def   star_inverse_def
   20.37    star_le_def       star_less_def     star_abs_def       star_sgn_def
   20.38 -  star_div_def      star_mod_def
   20.39 +  star_mod_def
   20.40  
   20.41  text {* Class operations preserve standard elements *}
   20.42  
   20.43 @@ -573,7 +577,7 @@
   20.44  lemma Standard_mult: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
   20.45  by (simp add: star_mult_def)
   20.46  
   20.47 -lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
   20.48 +lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> divide x y \<in> Standard"
   20.49  by (simp add: star_divide_def)
   20.50  
   20.51  lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
   20.52 @@ -582,17 +586,14 @@
   20.53  lemma Standard_abs: "x \<in> Standard \<Longrightarrow> abs x \<in> Standard"
   20.54  by (simp add: star_abs_def)
   20.55  
   20.56 -lemma Standard_div: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x div y \<in> Standard"
   20.57 -by (simp add: star_div_def)
   20.58 -
   20.59  lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
   20.60  by (simp add: star_mod_def)
   20.61  
   20.62  lemmas Standard_simps [simp] =
   20.63    Standard_zero  Standard_one
   20.64 -  Standard_add  Standard_diff  Standard_minus
   20.65 +  Standard_add   Standard_diff    Standard_minus
   20.66    Standard_mult  Standard_divide  Standard_inverse
   20.67 -  Standard_abs  Standard_div  Standard_mod
   20.68 +  Standard_abs   Standard_mod
   20.69  
   20.70  text {* @{term star_of} preserves class operations *}
   20.71  
   20.72 @@ -614,9 +615,6 @@
   20.73  lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
   20.74  by transfer (rule refl)
   20.75  
   20.76 -lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
   20.77 -by transfer (rule refl)
   20.78 -
   20.79  lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
   20.80  by transfer (rule refl)
   20.81  
   20.82 @@ -665,7 +663,7 @@
   20.83  lemmas star_of_simps [simp] =
   20.84    star_of_add     star_of_diff    star_of_minus
   20.85    star_of_mult    star_of_divide  star_of_inverse
   20.86 -  star_of_div     star_of_mod     star_of_abs
   20.87 +  star_of_mod     star_of_abs
   20.88    star_of_zero    star_of_one
   20.89    star_of_less    star_of_le      star_of_eq
   20.90    star_of_0_less  star_of_0_le    star_of_0_eq
    21.1 --- a/src/HOL/Rat.thy	Mon Jun 01 18:59:21 2015 +0200
    21.2 +++ b/src/HOL/Rat.thy	Mon Jun 01 18:59:21 2015 +0200
    21.3 @@ -162,9 +162,9 @@
    21.4    by transfer simp
    21.5  
    21.6  definition
    21.7 -  divide_rat_def: "q / r = q * inverse (r::rat)"
    21.8 +  divide_rat_def: "divide q r = q * inverse (r::rat)"
    21.9  
   21.10 -lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   21.11 +lemma divide_rat [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
   21.12    by (simp add: divide_rat_def)
   21.13  
   21.14  instance proof
   21.15 @@ -191,7 +191,7 @@
   21.16      by transfer simp
   21.17    { assume "q \<noteq> 0" thus "inverse q * q = 1"
   21.18      by transfer simp }
   21.19 -  show "q / r = q * inverse r"
   21.20 +  show "divide q r = q * inverse r"
   21.21      by (fact divide_rat_def)
   21.22    show "inverse 0 = (0::rat)"
   21.23      by transfer simp
   21.24 @@ -1158,8 +1158,8 @@
   21.25          val {mant = i, exp = n} = Lexicon.read_float str;
   21.26          val exp = Syntax.const @{const_syntax Power.power};
   21.27          val ten = Numeral.mk_number_syntax 10;
   21.28 -        val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;;
   21.29 -      in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end;
   21.30 +        val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;
   21.31 +      in Syntax.const @{const_syntax Fields.inverse_divide} $ Numeral.mk_number_syntax i $ exp10 end;
   21.32  
   21.33      fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
   21.34        | float_tr [t as Const (str, _)] = mk_frac str
    22.1 --- a/src/HOL/Real.thy	Mon Jun 01 18:59:21 2015 +0200
    22.2 +++ b/src/HOL/Real.thy	Mon Jun 01 18:59:21 2015 +0200
    22.3 @@ -438,7 +438,7 @@
    22.4    "x - y = (x::real) + - y"
    22.5  
    22.6  definition
    22.7 -  "x / y = (x::real) * inverse y"
    22.8 +  "divide x y = (x::real) * inverse y"
    22.9  
   22.10  lemma add_Real:
   22.11    assumes X: "cauchy X" and Y: "cauchy Y"
   22.12 @@ -501,7 +501,7 @@
   22.13      apply (rule_tac x=k in exI, clarify)
   22.14      apply (drule_tac x=n in spec, simp)
   22.15      done
   22.16 -  show "a / b = a * inverse b"
   22.17 +  show "divide a b = a * inverse b"
   22.18      by (rule divide_real_def)
   22.19    show "inverse (0::real) = 0"
   22.20      by transfer (simp add: realrel_def)
    23.1 --- a/src/HOL/Rings.thy	Mon Jun 01 18:59:21 2015 +0200
    23.2 +++ b/src/HOL/Rings.thy	Mon Jun 01 18:59:21 2015 +0200
    23.3 @@ -415,6 +415,33 @@
    23.4  
    23.5  end
    23.6  
    23.7 +class divide =
    23.8 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    23.9 +
   23.10 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
   23.11 +
   23.12 +context semiring
   23.13 +begin
   23.14 +
   23.15 +lemma [field_simps]:
   23.16 +  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
   23.17 +    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   23.18 +  by (rule distrib_left distrib_right)+
   23.19 +
   23.20 +end
   23.21 +
   23.22 +context ring
   23.23 +begin
   23.24 +
   23.25 +lemma [field_simps]:
   23.26 +  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
   23.27 +    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   23.28 +  by (rule left_diff_distrib right_diff_distrib)+
   23.29 +
   23.30 +end
   23.31 +
   23.32 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
   23.33 +  
   23.34  class semiring_no_zero_divisors = semiring_0 +
   23.35    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   23.36  begin
    24.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Jun 01 18:59:21 2015 +0200
    24.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Jun 01 18:59:21 2015 +0200
    24.3 @@ -4415,6 +4415,1608 @@
    24.4  (let ((@x128 (asserted $x127)))
    24.5  (unit-resolution @x128 @x546 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    24.6  
    24.7 +0f7f4a10f8a84029fd3a6efddc4408fa429b0cda 113 0
    24.8 +unsat
    24.9 +((set-logic <null>)
   24.10 +(proof
   24.11 +(let ((?x228 (mod x$ 2)))
   24.12 +(let ((?x262 (* (- 1) ?x228)))
   24.13 +(let ((?x31 (mod$ x$ 2)))
   24.14 +(let ((?x263 (+ ?x31 ?x262)))
   24.15 +(let (($x280 (>= ?x263 0)))
   24.16 +(let (($x264 (= ?x263 0)))
   24.17 +(let (($x205 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x136 (mod ?v0 ?v1)))
   24.18 +(let ((?x93 (* (- 1) ?v1)))
   24.19 +(let ((?x90 (* (- 1) ?v0)))
   24.20 +(let ((?x144 (mod ?x90 ?x93)))
   24.21 +(let ((?x150 (* (- 1) ?x144)))
   24.22 +(let (($x111 (<= ?v1 0)))
   24.23 +(let ((?x170 (ite $x111 ?x150 ?x136)))
   24.24 +(let (($x78 (= ?v1 0)))
   24.25 +(let ((?x175 (ite $x78 ?v0 ?x170)))
   24.26 +(let ((?x135 (mod$ ?v0 ?v1)))
   24.27 +(= ?x135 ?x175))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
   24.28 +))
   24.29 +(let (($x181 (forall ((?v0 Int) (?v1 Int) )(let ((?x136 (mod ?v0 ?v1)))
   24.30 +(let ((?x93 (* (- 1) ?v1)))
   24.31 +(let ((?x90 (* (- 1) ?v0)))
   24.32 +(let ((?x144 (mod ?x90 ?x93)))
   24.33 +(let ((?x150 (* (- 1) ?x144)))
   24.34 +(let (($x111 (<= ?v1 0)))
   24.35 +(let ((?x170 (ite $x111 ?x150 ?x136)))
   24.36 +(let (($x78 (= ?v1 0)))
   24.37 +(let ((?x175 (ite $x78 ?v0 ?x170)))
   24.38 +(let ((?x135 (mod$ ?v0 ?v1)))
   24.39 +(= ?x135 ?x175))))))))))))
   24.40 +))
   24.41 +(let ((?x136 (mod ?1 ?0)))
   24.42 +(let ((?x93 (* (- 1) ?0)))
   24.43 +(let ((?x90 (* (- 1) ?1)))
   24.44 +(let ((?x144 (mod ?x90 ?x93)))
   24.45 +(let ((?x150 (* (- 1) ?x144)))
   24.46 +(let (($x111 (<= ?0 0)))
   24.47 +(let ((?x170 (ite $x111 ?x150 ?x136)))
   24.48 +(let (($x78 (= ?0 0)))
   24.49 +(let ((?x175 (ite $x78 ?1 ?x170)))
   24.50 +(let ((?x135 (mod$ ?1 ?0)))
   24.51 +(let (($x178 (= ?x135 ?x175)))
   24.52 +(let (($x142 (forall ((?v0 Int) (?v1 Int) )(let (($x78 (= ?v1 0)))
   24.53 +(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
   24.54 +(let ((?x135 (mod$ ?v0 ?v1)))
   24.55 +(= ?x135 ?x140)))))
   24.56 +))
   24.57 +(let (($x164 (forall ((?v0 Int) (?v1 Int) )(let ((?x93 (* (- 1) ?v1)))
   24.58 +(let ((?x90 (* (- 1) ?v0)))
   24.59 +(let ((?x144 (mod ?x90 ?x93)))
   24.60 +(let ((?x150 (* (- 1) ?x144)))
   24.61 +(let ((?x136 (mod ?v0 ?v1)))
   24.62 +(let (($x79 (< 0 ?v1)))
   24.63 +(let ((?x155 (ite $x79 ?x136 ?x150)))
   24.64 +(let (($x78 (= ?v1 0)))
   24.65 +(let ((?x158 (ite $x78 ?v0 ?x155)))
   24.66 +(let ((?x135 (mod$ ?v0 ?v1)))
   24.67 +(= ?x135 ?x158))))))))))))
   24.68 +))
   24.69 +(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
   24.70 +(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
   24.71 +(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
   24.72 +(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
   24.73 +(let (($x79 (< 0 ?0)))
   24.74 +(let ((?x155 (ite $x79 ?x136 ?x150)))
   24.75 +(let ((?x158 (ite $x78 ?1 ?x155)))
   24.76 +(let (($x161 (= ?x135 ?x158)))
   24.77 +(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
   24.78 +(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
   24.79 +(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
   24.80 +(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
   24.81 +(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
   24.82 +(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
   24.83 +(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
   24.84 +(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
   24.85 +(let (($x270 (or (not $x205) $x264)))
   24.86 +(let ((?x225 (* (- 1) 2)))
   24.87 +(let ((?x224 (* (- 1) x$)))
   24.88 +(let ((?x226 (mod ?x224 ?x225)))
   24.89 +(let ((?x227 (* (- 1) ?x226)))
   24.90 +(let (($x223 (<= 2 0)))
   24.91 +(let ((?x229 (ite $x223 ?x227 ?x228)))
   24.92 +(let (($x222 (= 2 0)))
   24.93 +(let ((?x230 (ite $x222 x$ ?x229)))
   24.94 +(let (($x231 (= ?x31 ?x230)))
   24.95 +(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
   24.96 +(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
   24.97 +(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
   24.98 +(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
   24.99 +(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
  24.100 +(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
  24.101 +(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
  24.102 +(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
  24.103 +(let ((@x337 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
  24.104 +(let (($x305 (>= ?x228 0)))
  24.105 +(let (($x64 (>= ?x31 0)))
  24.106 +(let (($x67 (not $x64)))
  24.107 +(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
  24.108 +(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
  24.109 +(let ((?x32 (* 2 ?x31)))
  24.110 +(let ((?x47 (+ 1 x$ ?x32)))
  24.111 +(let (($x52 (<= (+ 1 x$) ?x47)))
  24.112 +(let (($x55 (not $x52)))
  24.113 +(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
  24.114 +(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
  24.115 +(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
  24.116 +(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
  24.117 +(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
  24.118 +(let ((@x74 (mp (asserted $x36) @x73 $x67)))
  24.119 +((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x337 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  24.120 +
  24.121 +fa5abc269019f00f5093218b287856c2a08c0adf 112 0
  24.122 +unsat
  24.123 +((set-logic <null>)
  24.124 +(proof
  24.125 +(let ((?x224 (mod x$ 2)))
  24.126 +(let (($x318 (>= ?x224 2)))
  24.127 +(let (($x319 (not $x318)))
  24.128 +(let ((?x258 (* (- 1) ?x224)))
  24.129 +(let ((?x29 (mod$ x$ 2)))
  24.130 +(let ((?x259 (+ ?x29 ?x258)))
  24.131 +(let (($x275 (<= ?x259 0)))
  24.132 +(let (($x260 (= ?x259 0)))
  24.133 +(let (($x201 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x132 (mod ?v0 ?v1)))
  24.134 +(let ((?x89 (* (- 1) ?v1)))
  24.135 +(let ((?x86 (* (- 1) ?v0)))
  24.136 +(let ((?x140 (mod ?x86 ?x89)))
  24.137 +(let ((?x146 (* (- 1) ?x140)))
  24.138 +(let (($x107 (<= ?v1 0)))
  24.139 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  24.140 +(let (($x74 (= ?v1 0)))
  24.141 +(let ((?x171 (ite $x74 ?v0 ?x166)))
  24.142 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.143 +(= ?x131 ?x171))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
  24.144 +))
  24.145 +(let (($x177 (forall ((?v0 Int) (?v1 Int) )(let ((?x132 (mod ?v0 ?v1)))
  24.146 +(let ((?x89 (* (- 1) ?v1)))
  24.147 +(let ((?x86 (* (- 1) ?v0)))
  24.148 +(let ((?x140 (mod ?x86 ?x89)))
  24.149 +(let ((?x146 (* (- 1) ?x140)))
  24.150 +(let (($x107 (<= ?v1 0)))
  24.151 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  24.152 +(let (($x74 (= ?v1 0)))
  24.153 +(let ((?x171 (ite $x74 ?v0 ?x166)))
  24.154 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.155 +(= ?x131 ?x171))))))))))))
  24.156 +))
  24.157 +(let ((?x132 (mod ?1 ?0)))
  24.158 +(let ((?x89 (* (- 1) ?0)))
  24.159 +(let ((?x86 (* (- 1) ?1)))
  24.160 +(let ((?x140 (mod ?x86 ?x89)))
  24.161 +(let ((?x146 (* (- 1) ?x140)))
  24.162 +(let (($x107 (<= ?0 0)))
  24.163 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  24.164 +(let (($x74 (= ?0 0)))
  24.165 +(let ((?x171 (ite $x74 ?1 ?x166)))
  24.166 +(let ((?x131 (mod$ ?1 ?0)))
  24.167 +(let (($x174 (= ?x131 ?x171)))
  24.168 +(let (($x138 (forall ((?v0 Int) (?v1 Int) )(let (($x74 (= ?v1 0)))
  24.169 +(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
  24.170 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.171 +(= ?x131 ?x136)))))
  24.172 +))
  24.173 +(let (($x160 (forall ((?v0 Int) (?v1 Int) )(let ((?x89 (* (- 1) ?v1)))
  24.174 +(let ((?x86 (* (- 1) ?v0)))
  24.175 +(let ((?x140 (mod ?x86 ?x89)))
  24.176 +(let ((?x146 (* (- 1) ?x140)))
  24.177 +(let ((?x132 (mod ?v0 ?v1)))
  24.178 +(let (($x75 (< 0 ?v1)))
  24.179 +(let ((?x151 (ite $x75 ?x132 ?x146)))
  24.180 +(let (($x74 (= ?v1 0)))
  24.181 +(let ((?x154 (ite $x74 ?v0 ?x151)))
  24.182 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.183 +(= ?x131 ?x154))))))))))))
  24.184 +))
  24.185 +(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
  24.186 +(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
  24.187 +(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
  24.188 +(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
  24.189 +(let (($x75 (< 0 ?0)))
  24.190 +(let ((?x151 (ite $x75 ?x132 ?x146)))
  24.191 +(let ((?x154 (ite $x74 ?1 ?x151)))
  24.192 +(let (($x157 (= ?x131 ?x154)))
  24.193 +(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
  24.194 +(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
  24.195 +(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
  24.196 +(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
  24.197 +(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
  24.198 +(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
  24.199 +(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
  24.200 +(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
  24.201 +(let (($x266 (or (not $x201) $x260)))
  24.202 +(let ((?x221 (* (- 1) 2)))
  24.203 +(let ((?x220 (* (- 1) x$)))
  24.204 +(let ((?x222 (mod ?x220 ?x221)))
  24.205 +(let ((?x223 (* (- 1) ?x222)))
  24.206 +(let (($x219 (<= 2 0)))
  24.207 +(let ((?x225 (ite $x219 ?x223 ?x224)))
  24.208 +(let (($x218 (= 2 0)))
  24.209 +(let ((?x226 (ite $x218 x$ ?x225)))
  24.210 +(let (($x227 (= ?x29 ?x226)))
  24.211 +(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
  24.212 +(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
  24.213 +(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
  24.214 +(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
  24.215 +(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
  24.216 +(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
  24.217 +(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
  24.218 +(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
  24.219 +(let ((@x336 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
  24.220 +(let (($x63 (>= ?x29 2)))
  24.221 +(let ((?x37 (* 2 ?x29)))
  24.222 +(let (($x56 (>= ?x37 3)))
  24.223 +(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
  24.224 +(let (($x49 (not $x46)))
  24.225 +(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
  24.226 +(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
  24.227 +(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
  24.228 +(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
  24.229 +(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
  24.230 +(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
  24.231 +(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
  24.232 +((_ th-lemma arith farkas -1 1 1) @x70 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  24.233 +
  24.234 +1880f0ed1cb3d1cfa006dff17f1b5553ce3a5158 236 0
  24.235 +unsat
  24.236 +((set-logic <null>)
  24.237 +(proof
  24.238 +(let ((?x410 (div n$ 2)))
  24.239 +(let ((?x704 (* (- 1) ?x410)))
  24.240 +(let ((?x381 (div n$ 4)))
  24.241 +(let ((?x601 (* (- 2) ?x381)))
  24.242 +(let ((?x329 (mod n$ 4)))
  24.243 +(let ((?x363 (* (- 1) ?x329)))
  24.244 +(let ((?x35 (mod$ n$ 4)))
  24.245 +(let ((?x705 (+ n$ ?x35 ?x363 ?x601 ?x704)))
  24.246 +(let (($x706 (>= ?x705 2)))
  24.247 +(let ((?x39 (mod$ n$ 2)))
  24.248 +(let (($x515 (>= ?x39 1)))
  24.249 +(let (($x725 (not $x515)))
  24.250 +(let (($x514 (<= ?x39 1)))
  24.251 +(let ((?x519 (mod n$ 2)))
  24.252 +(let ((?x534 (* (- 1) ?x519)))
  24.253 +(let ((?x535 (+ ?x39 ?x534)))
  24.254 +(let (($x408 (<= ?x535 0)))
  24.255 +(let (($x490 (= ?x535 0)))
  24.256 +(let (($x191 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x108 (mod ?v0 ?v1)))
  24.257 +(let ((?x65 (* (- 1) ?v1)))
  24.258 +(let ((?x62 (* (- 1) ?v0)))
  24.259 +(let ((?x116 (mod ?x62 ?x65)))
  24.260 +(let ((?x122 (* (- 1) ?x116)))
  24.261 +(let (($x83 (<= ?v1 0)))
  24.262 +(let ((?x142 (ite $x83 ?x122 ?x108)))
  24.263 +(let (($x50 (= ?v1 0)))
  24.264 +(let ((?x147 (ite $x50 ?v0 ?x142)))
  24.265 +(let ((?x107 (mod$ ?v0 ?v1)))
  24.266 +(= ?x107 ?x147))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
  24.267 +))
  24.268 +(let (($x153 (forall ((?v0 Int) (?v1 Int) )(let ((?x108 (mod ?v0 ?v1)))
  24.269 +(let ((?x65 (* (- 1) ?v1)))
  24.270 +(let ((?x62 (* (- 1) ?v0)))
  24.271 +(let ((?x116 (mod ?x62 ?x65)))
  24.272 +(let ((?x122 (* (- 1) ?x116)))
  24.273 +(let (($x83 (<= ?v1 0)))
  24.274 +(let ((?x142 (ite $x83 ?x122 ?x108)))
  24.275 +(let (($x50 (= ?v1 0)))
  24.276 +(let ((?x147 (ite $x50 ?v0 ?x142)))
  24.277 +(let ((?x107 (mod$ ?v0 ?v1)))
  24.278 +(= ?x107 ?x147))))))))))))
  24.279 +))
  24.280 +(let ((?x108 (mod ?1 ?0)))
  24.281 +(let ((?x65 (* (- 1) ?0)))
  24.282 +(let ((?x62 (* (- 1) ?1)))
  24.283 +(let ((?x116 (mod ?x62 ?x65)))
  24.284 +(let ((?x122 (* (- 1) ?x116)))
  24.285 +(let (($x83 (<= ?0 0)))
  24.286 +(let ((?x142 (ite $x83 ?x122 ?x108)))
  24.287 +(let (($x50 (= ?0 0)))
  24.288 +(let ((?x147 (ite $x50 ?1 ?x142)))
  24.289 +(let ((?x107 (mod$ ?1 ?0)))
  24.290 +(let (($x150 (= ?x107 ?x147)))
  24.291 +(let (($x114 (forall ((?v0 Int) (?v1 Int) )(let (($x50 (= ?v1 0)))
  24.292 +(let ((?x112 (ite $x50 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
  24.293 +(let ((?x107 (mod$ ?v0 ?v1)))
  24.294 +(= ?x107 ?x112)))))
  24.295 +))
  24.296 +(let (($x136 (forall ((?v0 Int) (?v1 Int) )(let ((?x65 (* (- 1) ?v1)))
  24.297 +(let ((?x62 (* (- 1) ?v0)))
  24.298 +(let ((?x116 (mod ?x62 ?x65)))
  24.299 +(let ((?x122 (* (- 1) ?x116)))
  24.300 +(let ((?x108 (mod ?v0 ?v1)))
  24.301 +(let (($x51 (< 0 ?v1)))
  24.302 +(let ((?x127 (ite $x51 ?x108 ?x122)))
  24.303 +(let (($x50 (= ?v1 0)))
  24.304 +(let ((?x130 (ite $x50 ?v0 ?x127)))
  24.305 +(let ((?x107 (mod$ ?v0 ?v1)))
  24.306 +(= ?x107 ?x130))))))))))))
  24.307 +))
  24.308 +(let ((@x141 (monotonicity (rewrite (= (< 0 ?0) (not $x83))) (= (ite (< 0 ?0) ?x108 ?x122) (ite (not $x83) ?x108 ?x122)))))
  24.309 +(let ((@x146 (trans @x141 (rewrite (= (ite (not $x83) ?x108 ?x122) ?x142)) (= (ite (< 0 ?0) ?x108 ?x122) ?x142))))
  24.310 +(let ((@x149 (monotonicity @x146 (= (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122)) ?x147))))
  24.311 +(let ((@x152 (monotonicity @x149 (= (= ?x107 (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122))) $x150))))
  24.312 +(let (($x51 (< 0 ?0)))
  24.313 +(let ((?x127 (ite $x51 ?x108 ?x122)))
  24.314 +(let ((?x130 (ite $x50 ?1 ?x127)))
  24.315 +(let (($x133 (= ?x107 ?x130)))
  24.316 +(let (($x134 (= (= ?x107 (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))))) $x133)))
  24.317 +(let ((@x118 (monotonicity (rewrite (= (- ?1) ?x62)) (rewrite (= (- ?0) ?x65)) (= (mod (- ?1) (- ?0)) ?x116))))
  24.318 +(let ((@x126 (trans (monotonicity @x118 (= (- (mod (- ?1) (- ?0))) (- ?x116))) (rewrite (= (- ?x116) ?x122)) (= (- (mod (- ?1) (- ?0))) ?x122))))
  24.319 +(let ((@x129 (monotonicity @x126 (= (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))) ?x127))))
  24.320 +(let ((@x132 (monotonicity @x129 (= (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0))))) ?x130))))
  24.321 +(let ((@x157 (trans (quant-intro (monotonicity @x132 $x134) (= $x114 $x136)) (quant-intro @x152 (= $x136 $x153)) (= $x114 $x153))))
  24.322 +(let ((@x168 (mp~ (mp (asserted $x114) @x157 $x153) (nnf-pos (refl (~ $x150 $x150)) (~ $x153 $x153)) $x153)))
  24.323 +(let ((@x196 (mp @x168 (quant-intro (refl (= $x150 $x150)) (= $x153 $x191)) $x191)))
  24.324 +(let (($x260 (not $x191)))
  24.325 +(let (($x541 (or $x260 $x490)))
  24.326 +(let ((?x211 (* (- 1) 2)))
  24.327 +(let ((?x222 (* (- 1) n$)))
  24.328 +(let ((?x517 (mod ?x222 ?x211)))
  24.329 +(let ((?x518 (* (- 1) ?x517)))
  24.330 +(let (($x209 (<= 2 0)))
  24.331 +(let ((?x520 (ite $x209 ?x518 ?x519)))
  24.332 +(let (($x208 (= 2 0)))
  24.333 +(let ((?x521 (ite $x208 n$ ?x520)))
  24.334 +(let (($x485 (= ?x39 ?x521)))
  24.335 +(let ((@x593 (monotonicity (monotonicity (rewrite (= ?x211 (- 2))) (= ?x517 (mod ?x222 (- 2)))) (= ?x518 (* (- 1) (mod ?x222 (- 2)))))))
  24.336 +(let ((@x221 (rewrite (= $x209 false))))
  24.337 +(let ((@x596 (monotonicity @x221 @x593 (= ?x520 (ite false (* (- 1) (mod ?x222 (- 2))) ?x519)))))
  24.338 +(let ((@x599 (trans @x596 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 2))) ?x519) ?x519)) (= ?x520 ?x519))))
  24.339 +(let ((@x219 (rewrite (= $x208 false))))
  24.340 +(let ((@x487 (trans (monotonicity @x219 @x599 (= ?x521 (ite false n$ ?x519))) (rewrite (= (ite false n$ ?x519) ?x519)) (= ?x521 ?x519))))
  24.341 +(let ((@x538 (trans (monotonicity @x487 (= $x485 (= ?x39 ?x519))) (rewrite (= (= ?x39 ?x519) $x490)) (= $x485 $x490))))
  24.342 +(let ((@x406 (trans (monotonicity @x538 (= (or $x260 $x485) $x541)) (rewrite (= $x541 $x541)) (= (or $x260 $x485) $x541))))
  24.343 +(let ((@x407 (mp ((_ quant-inst n$ 2) (or $x260 $x485)) @x406 $x541)))
  24.344 +(let ((@x715 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x408)) (unit-resolution @x407 @x196 $x490) $x408)))
  24.345 +(let (($x303 (>= ?x519 2)))
  24.346 +(let (($x304 (not $x303)))
  24.347 +(let ((@x26 (true-axiom true)))
  24.348 +(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)))
  24.349 +(let (($x41 (= ?x39 1)))
  24.350 +(let (($x169 (not $x41)))
  24.351 +(let ((?x42 (mod$ m$ 2)))
  24.352 +(let (($x43 (= ?x42 1)))
  24.353 +(let ((?x29 (+ n$ m$)))
  24.354 +(let ((?x214 (mod ?x29 2)))
  24.355 +(let ((?x253 (* (- 1) ?x214)))
  24.356 +(let ((?x31 (mod$ ?x29 2)))
  24.357 +(let ((?x603 (+ n$ m$ ?x31 ?x35 ?x253 (* (- 1) (div ?x29 2)) ?x363 ?x601 (* (- 1) (div m$ 2)))))
  24.358 +(let (($x604 (>= ?x603 2)))
  24.359 +(let (($x523 (>= ?x42 1)))
  24.360 +(let (($x609 (not $x523)))
  24.361 +(let (($x522 (<= ?x42 1)))
  24.362 +(let ((?x439 (mod m$ 2)))
  24.363 +(let ((?x466 (* (- 1) ?x439)))
  24.364 +(let ((?x467 (+ ?x42 ?x466)))
  24.365 +(let (($x482 (<= ?x467 0)))
  24.366 +(let (($x468 (= ?x467 0)))
  24.367 +(let (($x473 (or $x260 $x468)))
  24.368 +(let ((?x440 (ite $x209 (* (- 1) (mod (* (- 1) m$) ?x211)) ?x439)))
  24.369 +(let ((?x441 (ite $x208 m$ ?x440)))
  24.370 +(let (($x442 (= ?x42 ?x441)))
  24.371 +(let ((@x453 (rewrite (= (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439) ?x439))))
  24.372 +(let (($x447 (= (* (- 1) (mod (* (- 1) m$) ?x211)) (* (- 1) (mod (* (- 1) m$) (- 2))))))
  24.373 +(let ((@x229 (rewrite (= ?x211 (- 2)))))
  24.374 +(let ((@x445 (monotonicity @x229 (= (mod (* (- 1) m$) ?x211) (mod (* (- 1) m$) (- 2))))))
  24.375 +(let ((@x451 (monotonicity @x221 (monotonicity @x445 $x447) (= ?x440 (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439)))))
  24.376 +(let ((@x458 (monotonicity @x219 (trans @x451 @x453 (= ?x440 ?x439)) (= ?x441 (ite false m$ ?x439)))))
  24.377 +(let ((@x465 (monotonicity (trans @x458 (rewrite (= (ite false m$ ?x439) ?x439)) (= ?x441 ?x439)) (= $x442 (= ?x42 ?x439)))))
  24.378 +(let ((@x477 (monotonicity (trans @x465 (rewrite (= (= ?x42 ?x439) $x468)) (= $x442 $x468)) (= (or $x260 $x442) $x473))))
  24.379 +(let ((@x481 (mp ((_ quant-inst m$ 2) (or $x260 $x442)) (trans @x477 (rewrite (= $x473 $x473)) (= (or $x260 $x442) $x473)) $x473)))
  24.380 +(let ((@x277 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) $x482)) (unit-resolution @x481 @x196 $x468) $x482)))
  24.381 +(let ((@x386 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x439 2)))) @x26 (not (>= ?x439 2)))))
  24.382 +(let ((@x384 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x522 (>= ?x439 2) (not $x482))) @x386 @x277 $x522)))
  24.383 +(let ((@x564 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x43 (not $x522) $x609)) (hypothesis (not $x43)) (or (not $x522) $x609))))
  24.384 +(let ((?x272 (div ?x29 2)))
  24.385 +(let ((?x288 (* (- 2) ?x272)))
  24.386 +(let ((?x289 (+ n$ m$ ?x253 ?x288)))
  24.387 +(let (($x294 (<= ?x289 0)))
  24.388 +(let (($x287 (= ?x289 0)))
  24.389 +(let ((@x617 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x294)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x294)))
  24.390 +(let (($x433 (<= ?x31 0)))
  24.391 +(let (($x32 (= ?x31 0)))
  24.392 +(let ((@x33 (asserted $x32)))
  24.393 +(let ((?x254 (+ ?x31 ?x253)))
  24.394 +(let (($x270 (<= ?x254 0)))
  24.395 +(let (($x255 (= ?x254 0)))
  24.396 +(let (($x261 (or $x260 $x255)))
  24.397 +(let ((?x215 (ite $x209 (* (- 1) (mod (* (- 1) ?x29) ?x211)) ?x214)))
  24.398 +(let ((?x216 (ite $x208 ?x29 ?x215)))
  24.399 +(let (($x217 (= ?x31 ?x216)))
  24.400 +(let (($x239 (= (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214) ?x214)))
  24.401 +(let (($x237 (= ?x215 (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214))))
  24.402 +(let (($x234 (= (* (- 1) (mod (* (- 1) ?x29) ?x211)) (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
  24.403 +(let ((@x232 (monotonicity (rewrite (= (* (- 1) ?x29) (+ ?x222 (* (- 1) m$)))) @x229 (= (mod (* (- 1) ?x29) ?x211) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
  24.404 +(let ((@x242 (trans (monotonicity @x221 (monotonicity @x232 $x234) $x237) (rewrite $x239) (= ?x215 ?x214))))
  24.405 +(let ((@x249 (trans (monotonicity @x219 @x242 (= ?x216 (ite false ?x29 ?x214))) (rewrite (= (ite false ?x29 ?x214) ?x214)) (= ?x216 ?x214))))
  24.406 +(let ((@x259 (trans (monotonicity @x249 (= $x217 (= ?x31 ?x214))) (rewrite (= (= ?x31 ?x214) $x255)) (= $x217 $x255))))
  24.407 +(let ((@x268 (trans (monotonicity @x259 (= (or $x260 $x217) $x261)) (rewrite (= $x261 $x261)) (= (or $x260 $x217) $x261))))
  24.408 +(let ((@x269 (mp ((_ quant-inst (+ n$ m$) 2) (or $x260 $x217)) @x268 $x261)))
  24.409 +(let ((@x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x270)) (unit-resolution @x269 @x196 $x255) $x270)))
  24.410 +(let ((?x498 (+ m$ ?x466 (* (- 2) (div m$ 2)))))
  24.411 +(let (($x496 (= ?x498 0)))
  24.412 +(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))))
  24.413 +(let ((?x397 (* (- 4) ?x381)))
  24.414 +(let ((?x398 (+ n$ ?x363 ?x397)))
  24.415 +(let (($x403 (<= ?x398 0)))
  24.416 +(let (($x396 (= ?x398 0)))
  24.417 +(let ((@x640 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x403)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x403)))
  24.418 +(let ((?x364 (+ ?x35 ?x363)))
  24.419 +(let (($x379 (<= ?x364 0)))
  24.420 +(let (($x365 (= ?x364 0)))
  24.421 +(let (($x370 (or $x260 $x365)))
  24.422 +(let ((?x330 (ite (<= 4 0) (* (- 1) (mod ?x222 (* (- 1) 4))) ?x329)))
  24.423 +(let ((?x331 (ite (= 4 0) n$ ?x330)))
  24.424 +(let (($x332 (= ?x35 ?x331)))
  24.425 +(let ((@x342 (monotonicity (rewrite (= (* (- 1) 4) (- 4))) (= (mod ?x222 (* (- 1) 4)) (mod ?x222 (- 4))))))
  24.426 +(let ((@x345 (monotonicity @x342 (= (* (- 1) (mod ?x222 (* (- 1) 4))) (* (- 1) (mod ?x222 (- 4)))))))
  24.427 +(let ((@x348 (monotonicity (rewrite (= (<= 4 0) false)) @x345 (= ?x330 (ite false (* (- 1) (mod ?x222 (- 4))) ?x329)))))
  24.428 +(let ((@x352 (trans @x348 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 4))) ?x329) ?x329)) (= ?x330 ?x329))))
  24.429 +(let ((@x355 (monotonicity (rewrite (= (= 4 0) false)) @x352 (= ?x331 (ite false n$ ?x329)))))
  24.430 +(let ((@x362 (monotonicity (trans @x355 (rewrite (= (ite false n$ ?x329) ?x329)) (= ?x331 ?x329)) (= $x332 (= ?x35 ?x329)))))
  24.431 +(let ((@x374 (monotonicity (trans @x362 (rewrite (= (= ?x35 ?x329) $x365)) (= $x332 $x365)) (= (or $x260 $x332) $x370))))
  24.432 +(let ((@x378 (mp ((_ quant-inst n$ 4) (or $x260 $x332)) (trans @x374 (rewrite (= $x370 $x370)) (= (or $x260 $x332) $x370)) $x370)))
  24.433 +(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x379)) (unit-resolution @x378 @x196 $x365) $x379)))
  24.434 +(let (($x435 (<= ?x35 3)))
  24.435 +(let (($x37 (= ?x35 3)))
  24.436 +(let ((@x38 (asserted $x37)))
  24.437 +(let ((@x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) (>= ?x467 0))) (unit-resolution @x481 @x196 $x468) (>= ?x467 0))))
  24.438 +(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)))
  24.439 +(let ((@x565 (unit-resolution (lemma @x656 (or (not $x604) $x523)) (unit-resolution @x564 @x384 $x609) (not $x604))))
  24.440 +(let (($x295 (>= ?x289 0)))
  24.441 +(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x295)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x295)))
  24.442 +(let (($x434 (>= ?x31 0)))
  24.443 +(let (($x271 (>= ?x254 0)))
  24.444 +(let ((@x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x271)) (unit-resolution @x269 @x196 $x255) $x271)))
  24.445 +(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))))
  24.446 +(let ((@x549 (unit-resolution ((_ th-lemma arith) (or false (>= ?x439 0))) @x26 (>= ?x439 0))))
  24.447 +(let (($x404 (>= ?x398 0)))
  24.448 +(let ((@x552 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x404)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x404)))
  24.449 +(let (($x380 (>= ?x364 0)))
  24.450 +(let ((@x273 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x380)) (unit-resolution @x378 @x196 $x365) $x380)))
  24.451 +(let (($x436 (>= ?x35 3)))
  24.452 +(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)))
  24.453 +(let (($x171 (or $x169 (not $x43))))
  24.454 +(let ((@x177 (monotonicity (rewrite (= (and $x41 $x43) (not $x171))) (= (not (and $x41 $x43)) (not (not $x171))))))
  24.455 +(let ((@x181 (trans @x177 (rewrite (= (not (not $x171)) $x171)) (= (not (and $x41 $x43)) $x171))))
  24.456 +(let ((@x182 (mp (asserted (not (and $x41 $x43))) @x181 $x171)))
  24.457 +(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))))
  24.458 +(let ((?x420 (* (- 2) ?x410)))
  24.459 +(let ((?x421 (+ n$ ?x420 ?x534)))
  24.460 +(let (($x426 (<= ?x421 0)))
  24.461 +(let (($x419 (= ?x421 0)))
  24.462 +(let ((@x737 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x426)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x426)))
  24.463 +(let (($x409 (>= ?x535 0)))
  24.464 +(let ((@x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x409)) (unit-resolution @x407 @x196 $x490) $x409)))
  24.465 +(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)))
  24.466 +(let (($x427 (>= ?x421 0)))
  24.467 +(let ((@x584 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x427)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x427)))
  24.468 +(let (($x542 (>= ?x519 0)))
  24.469 +((_ 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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  24.470 +
  24.471 +f6a4c40290fd6742c0b08a1fe90b3664e90c2143 336 0
  24.472 +unsat
  24.473 +((set-logic <null>)
  24.474 +(proof
  24.475 +(let ((?x99 (mod$ l$ 2)))
  24.476 +(let ((?x96 (map$ uu$ xs$)))
  24.477 +(let ((?x97 (eval_dioph$ ks$ ?x96)))
  24.478 +(let ((?x98 (mod$ ?x97 2)))
  24.479 +(let (($x100 (= ?x98 ?x99)))
  24.480 +(let ((?x93 (eval_dioph$ ks$ xs$)))
  24.481 +(let (($x95 (= ?x93 l$)))
  24.482 +(let ((?x110 (* (- 1) ?x97)))
  24.483 +(let ((?x111 (+ l$ ?x110)))
  24.484 +(let ((?x114 (divide$ ?x111 2)))
  24.485 +(let ((?x101 (map$ uua$ xs$)))
  24.486 +(let ((?x102 (eval_dioph$ ks$ ?x101)))
  24.487 +(let (($x117 (= ?x102 ?x114)))
  24.488 +(let (($x282 (not $x117)))
  24.489 +(let (($x281 (not $x100)))
  24.490 +(let (($x283 (or $x281 $x282)))
  24.491 +(let ((?x744 (div ?x93 2)))
  24.492 +(let ((?x970 (* (- 1) ?x744)))
  24.493 +(let ((?x699 (mod ?x93 2)))
  24.494 +(let ((?x726 (* (- 1) ?x699)))
  24.495 +(let ((?x516 (mod l$ 2)))
  24.496 +(let ((?x543 (* (- 1) ?x516)))
  24.497 +(let (($x972 (>= (+ l$ ?x99 ?x543 (* (- 1) (div l$ 2)) ?x726 ?x970) 1)))
  24.498 +(let ((?x369 (* (- 1) l$)))
  24.499 +(let ((?x693 (+ ?x93 ?x369)))
  24.500 +(let (($x695 (>= ?x693 0)))
  24.501 +(let (($x861 (not $x695)))
  24.502 +(let (($x694 (<= ?x693 0)))
  24.503 +(let ((?x686 (+ ?x102 (* (- 1) ?x114))))
  24.504 +(let (($x687 (<= ?x686 0)))
  24.505 +(let (($x284 (not $x283)))
  24.506 +(let ((@x466 (hypothesis $x284)))
  24.507 +(let ((@x856 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x687)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x687)))
  24.508 +(let ((?x437 (+ l$ ?x110 (* (- 2) (div ?x111 2)) (* (- 1) (mod (+ l$ ?x97) 2)))))
  24.509 +(let (($x443 (>= ?x437 0)))
  24.510 +(let (($x434 (= ?x437 0)))
  24.511 +(let ((@x26 (true-axiom true)))
  24.512 +(let ((@x793 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
  24.513 +(let ((?x501 (* (- 2) ?x102)))
  24.514 +(let ((?x502 (+ ?x93 ?x110 ?x501)))
  24.515 +(let (($x509 (<= ?x502 0)))
  24.516 +(let (($x503 (= ?x502 0)))
  24.517 +(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(let ((?x45 (eval_dioph$ ?v0 ?v1)))
  24.518 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
  24.519 +(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
  24.520 +))
  24.521 +(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
  24.522 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
  24.523 +(= ?x83 0))))
  24.524 +))
  24.525 +(let ((?x45 (eval_dioph$ ?1 ?0)))
  24.526 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
  24.527 +(let (($x79 (= ?x83 0)))
  24.528 +(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
  24.529 +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
  24.530 +(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
  24.531 +(= ?x56 ?x45)))))
  24.532 +))
  24.533 +(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
  24.534 +(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
  24.535 +(let ((?x60 (* 2 ?x54)))
  24.536 +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
  24.537 +(let ((?x66 (+ ?x48 ?x60)))
  24.538 +(= ?x66 ?x45)))))))
  24.539 +))
  24.540 +(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
  24.541 +(let ((?x60 (* 2 ?x54)))
  24.542 +(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
  24.543 +(let ((?x66 (+ ?x48 ?x60)))
  24.544 +(let (($x71 (= ?x66 ?x45)))
  24.545 +(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
  24.546 +(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
  24.547 +(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
  24.548 +(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
  24.549 +(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
  24.550 +(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
  24.551 +(let (($x507 (or (not $x304) $x503)))
  24.552 +(let ((@x508 ((_ quant-inst ks$ xs$) $x507)))
  24.553 +(let ((@x800 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x509)) (unit-resolution @x508 @x309 $x503) $x509)))
  24.554 +(let ((?x396 (+ ?x114 (* (- 1) (div ?x111 2)))))
  24.555 +(let (($x413 (<= ?x396 0)))
  24.556 +(let (($x397 (= ?x396 0)))
  24.557 +(let (($x311 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x145 (div ?v0 ?v1)))
  24.558 +(let ((?x157 (* (- 1) ?v1)))
  24.559 +(let ((?x154 (* (- 1) ?v0)))
  24.560 +(let ((?x160 (div ?x154 ?x157)))
  24.561 +(let (($x175 (<= ?v1 0)))
  24.562 +(let ((?x182 (ite $x175 ?x160 ?x145)))
  24.563 +(let (($x143 (= ?v1 0)))
  24.564 +(let ((?x141 (divide$ ?v0 ?v1)))
  24.565 +(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) )))
  24.566 +))
  24.567 +(let (($x193 (forall ((?v0 Int) (?v1 Int) )(let ((?x145 (div ?v0 ?v1)))
  24.568 +(let ((?x157 (* (- 1) ?v1)))
  24.569 +(let ((?x154 (* (- 1) ?v0)))
  24.570 +(let ((?x160 (div ?x154 ?x157)))
  24.571 +(let (($x175 (<= ?v1 0)))
  24.572 +(let ((?x182 (ite $x175 ?x160 ?x145)))
  24.573 +(let (($x143 (= ?v1 0)))
  24.574 +(let ((?x141 (divide$ ?v0 ?v1)))
  24.575 +(= ?x141 (ite $x143 0 ?x182)))))))))))
  24.576 +))
  24.577 +(let ((?x145 (div ?1 ?0)))
  24.578 +(let ((?x157 (* (- 1) ?0)))
  24.579 +(let ((?x154 (* (- 1) ?1)))
  24.580 +(let ((?x160 (div ?x154 ?x157)))
  24.581 +(let (($x175 (<= ?0 0)))
  24.582 +(let ((?x182 (ite $x175 ?x160 ?x145)))
  24.583 +(let (($x143 (= ?0 0)))
  24.584 +(let ((?x141 (divide$ ?1 ?0)))
  24.585 +(let (($x190 (= ?x141 (ite $x143 0 ?x182))))
  24.586 +(let (($x152 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
  24.587 +(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
  24.588 +(let ((?x141 (divide$ ?v0 ?v1)))
  24.589 +(= ?x141 ?x150)))))
  24.590 +))
  24.591 +(let (($x172 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
  24.592 +(let ((?x154 (* (- 1) ?v0)))
  24.593 +(let ((?x160 (div ?x154 ?x157)))
  24.594 +(let ((?x145 (div ?v0 ?v1)))
  24.595 +(let (($x144 (< 0 ?v1)))
  24.596 +(let ((?x163 (ite $x144 ?x145 ?x160)))
  24.597 +(let (($x143 (= ?v1 0)))
  24.598 +(let ((?x166 (ite $x143 0 ?x163)))
  24.599 +(let ((?x141 (divide$ ?v0 ?v1)))
  24.600 +(= ?x141 ?x166)))))))))))
  24.601 +))
  24.602 +(let (($x144 (< 0 ?0)))
  24.603 +(let ((?x163 (ite $x144 ?x145 ?x160)))
  24.604 +(let ((?x166 (ite $x143 0 ?x163)))
  24.605 +(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
  24.606 +(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) ?x182)) (= ?x163 ?x182))))
  24.607 +(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 ?x182))) (= (= ?x141 ?x166) $x190))))
  24.608 +(let (($x169 (= ?x141 ?x166)))
  24.609 +(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
  24.610 +(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
  24.611 +(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
  24.612 +(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
  24.613 +(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
  24.614 +(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
  24.615 +(let (($x403 (or (not $x311) $x397)))
  24.616 +(let ((?x361 (div ?x111 2)))
  24.617 +(let (($x357 (<= 2 0)))
  24.618 +(let ((?x362 (ite $x357 (div (* (- 1) ?x111) (* (- 1) 2)) ?x361)))
  24.619 +(let (($x356 (= 2 0)))
  24.620 +(let ((?x363 (ite $x356 0 ?x362)))
  24.621 +(let (($x364 (= ?x114 ?x363)))
  24.622 +(let ((@x374 (rewrite (= (* (- 1) 2) (- 2)))))
  24.623 +(let ((@x377 (monotonicity (rewrite (= (* (- 1) ?x111) (+ ?x369 ?x97))) @x374 (= (div (* (- 1) ?x111) (* (- 1) 2)) (div (+ ?x369 ?x97) (- 2))))))
  24.624 +(let ((@x368 (rewrite (= $x357 false))))
  24.625 +(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
  24.626 +(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
  24.627 +(let ((@x366 (rewrite (= $x356 false))))
  24.628 +(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
  24.629 +(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
  24.630 +(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
  24.631 +(let ((@x802 (unit-resolution (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403) @x316 $x397)))
  24.632 +(let ((?x425 (mod (+ l$ ?x97) 2)))
  24.633 +(let (($x465 (>= ?x425 0)))
  24.634 +(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)))
  24.635 +(let (($x134 (not $x95)))
  24.636 +(let (($x290 (= $x95 $x283)))
  24.637 +(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
  24.638 +(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
  24.639 +(let (($x120 (and $x100 $x117)))
  24.640 +(let (($x135 (= $x134 $x120)))
  24.641 +(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
  24.642 +(let (($x108 (not $x107)))
  24.643 +(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
  24.644 +(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
  24.645 +(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
  24.646 +(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
  24.647 +(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
  24.648 +(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
  24.649 +(let ((@x898 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 (not $x694) $x861)) (unit-resolution @x344 @x466 $x134) (or (not $x694) $x861))))
  24.650 +(let ((@x899 (unit-resolution @x898 (unit-resolution (lemma @x810 (or $x694 (not $x687))) @x856 $x694) $x861)))
  24.651 +(let ((?x544 (+ ?x99 ?x543)))
  24.652 +(let (($x561 (>= ?x544 0)))
  24.653 +(let (($x545 (= ?x544 0)))
  24.654 +(let (($x318 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x200 (mod ?v0 ?v1)))
  24.655 +(let ((?x157 (* (- 1) ?v1)))
  24.656 +(let ((?x154 (* (- 1) ?v0)))
  24.657 +(let ((?x208 (mod ?x154 ?x157)))
  24.658 +(let ((?x214 (* (- 1) ?x208)))
  24.659 +(let (($x175 (<= ?v1 0)))
  24.660 +(let ((?x234 (ite $x175 ?x214 ?x200)))
  24.661 +(let (($x143 (= ?v1 0)))
  24.662 +(let ((?x239 (ite $x143 ?v0 ?x234)))
  24.663 +(let ((?x199 (mod$ ?v0 ?v1)))
  24.664 +(= ?x199 ?x239))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
  24.665 +))
  24.666 +(let (($x245 (forall ((?v0 Int) (?v1 Int) )(let ((?x200 (mod ?v0 ?v1)))
  24.667 +(let ((?x157 (* (- 1) ?v1)))
  24.668 +(let ((?x154 (* (- 1) ?v0)))
  24.669 +(let ((?x208 (mod ?x154 ?x157)))
  24.670 +(let ((?x214 (* (- 1) ?x208)))
  24.671 +(let (($x175 (<= ?v1 0)))
  24.672 +(let ((?x234 (ite $x175 ?x214 ?x200)))
  24.673 +(let (($x143 (= ?v1 0)))
  24.674 +(let ((?x239 (ite $x143 ?v0 ?x234)))
  24.675 +(let ((?x199 (mod$ ?v0 ?v1)))
  24.676 +(= ?x199 ?x239))))))))))))
  24.677 +))
  24.678 +(let ((?x200 (mod ?1 ?0)))
  24.679 +(let ((?x208 (mod ?x154 ?x157)))
  24.680 +(let ((?x214 (* (- 1) ?x208)))
  24.681 +(let ((?x234 (ite $x175 ?x214 ?x200)))
  24.682 +(let ((?x239 (ite $x143 ?1 ?x234)))
  24.683 +(let ((?x199 (mod$ ?1 ?0)))
  24.684 +(let (($x242 (= ?x199 ?x239)))
  24.685 +(let (($x206 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
  24.686 +(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
  24.687 +(let ((?x199 (mod$ ?v0 ?v1)))
  24.688 +(= ?x199 ?x204)))))
  24.689 +))
  24.690 +(let (($x228 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
  24.691 +(let ((?x154 (* (- 1) ?v0)))
  24.692 +(let ((?x208 (mod ?x154 ?x157)))
  24.693 +(let ((?x214 (* (- 1) ?x208)))
  24.694 +(let ((?x200 (mod ?v0 ?v1)))
  24.695 +(let (($x144 (< 0 ?v1)))
  24.696 +(let ((?x219 (ite $x144 ?x200 ?x214)))
  24.697 +(let (($x143 (= ?v1 0)))
  24.698 +(let ((?x222 (ite $x143 ?v0 ?x219)))
  24.699 +(let ((?x199 (mod$ ?v0 ?v1)))
  24.700 +(= ?x199 ?x222))))))))))))
  24.701 +))
  24.702 +(let ((@x233 (monotonicity (rewrite (= $x144 (not $x175))) (= (ite $x144 ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
  24.703 +(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite $x144 ?x200 ?x214) ?x234))))
  24.704 +(let ((@x244 (monotonicity (monotonicity @x238 (= (ite $x143 ?1 (ite $x144 ?x200 ?x214)) ?x239)) (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 ?x214))) $x242))))
  24.705 +(let ((?x219 (ite $x144 ?x200 ?x214)))
  24.706 +(let ((?x222 (ite $x143 ?1 ?x219)))
  24.707 +(let (($x225 (= ?x199 ?x222)))
  24.708 +(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
  24.709 +(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
  24.710 +(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
  24.711 +(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
  24.712 +(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
  24.713 +(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
  24.714 +(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
  24.715 +(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
  24.716 +(let (($x550 (not $x318)))
  24.717 +(let (($x551 (or $x550 $x545)))
  24.718 +(let ((?x359 (* (- 1) 2)))
  24.719 +(let ((?x511 (mod ?x369 ?x359)))
  24.720 +(let ((?x512 (* (- 1) ?x511)))
  24.721 +(let ((?x517 (ite $x357 ?x512 ?x516)))
  24.722 +(let ((?x518 (ite $x356 l$ ?x517)))
  24.723 +(let (($x519 (= ?x99 ?x518)))
  24.724 +(let ((@x525 (monotonicity (monotonicity @x374 (= ?x511 (mod ?x369 (- 2)))) (= ?x512 (* (- 1) (mod ?x369 (- 2)))))))
  24.725 +(let ((@x528 (monotonicity @x368 @x525 (= ?x517 (ite false (* (- 1) (mod ?x369 (- 2))) ?x516)))))
  24.726 +(let ((@x532 (trans @x528 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x516) ?x516)) (= ?x517 ?x516))))
  24.727 +(let ((@x539 (trans (monotonicity @x366 @x532 (= ?x518 (ite false l$ ?x516))) (rewrite (= (ite false l$ ?x516) ?x516)) (= ?x518 ?x516))))
  24.728 +(let ((@x549 (trans (monotonicity @x539 (= $x519 (= ?x99 ?x516))) (rewrite (= (= ?x99 ?x516) $x545)) (= $x519 $x545))))
  24.729 +(let ((@x558 (trans (monotonicity @x549 (= (or $x550 $x519) $x551)) (rewrite (= $x551 $x551)) (= (or $x550 $x519) $x551))))
  24.730 +(let ((@x559 (mp ((_ quant-inst l$ 2) (or $x550 $x519)) @x558 $x551)))
  24.731 +(let ((@x902 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x561)) (unit-resolution @x559 @x323 $x545) $x561)))
  24.732 +(let ((?x757 (* (- 2) ?x744)))
  24.733 +(let ((?x758 (+ ?x93 ?x726 ?x757)))
  24.734 +(let (($x764 (>= ?x758 0)))
  24.735 +(let (($x756 (= ?x758 0)))
  24.736 +(let ((@x872 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x764)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x764)))
  24.737 +(let ((?x562 (div l$ 2)))
  24.738 +(let ((?x575 (* (- 2) ?x562)))
  24.739 +(let ((?x576 (+ l$ ?x543 ?x575)))
  24.740 +(let (($x582 (>= ?x576 0)))
  24.741 +(let (($x574 (= ?x576 0)))
  24.742 +(let ((@x880 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x582)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x582)))
  24.743 +(let ((?x504 (mod$ ?x93 2)))
  24.744 +(let ((?x727 (+ ?x504 ?x726)))
  24.745 +(let (($x728 (= ?x727 0)))
  24.746 +(let (($x733 (or $x550 $x728)))
  24.747 +(let ((?x696 (* (- 1) ?x93)))
  24.748 +(let ((?x697 (mod ?x696 ?x359)))
  24.749 +(let ((?x698 (* (- 1) ?x697)))
  24.750 +(let ((?x700 (ite $x357 ?x698 ?x699)))
  24.751 +(let ((?x701 (ite $x356 ?x93 ?x700)))
  24.752 +(let (($x702 (= ?x504 ?x701)))
  24.753 +(let ((@x708 (monotonicity (monotonicity @x374 (= ?x697 (mod ?x696 (- 2)))) (= ?x698 (* (- 1) (mod ?x696 (- 2)))))))
  24.754 +(let ((@x711 (monotonicity @x368 @x708 (= ?x700 (ite false (* (- 1) (mod ?x696 (- 2))) ?x699)))))
  24.755 +(let ((@x715 (trans @x711 (rewrite (= (ite false (* (- 1) (mod ?x696 (- 2))) ?x699) ?x699)) (= ?x700 ?x699))))
  24.756 +(let ((@x722 (trans (monotonicity @x366 @x715 (= ?x701 (ite false ?x93 ?x699))) (rewrite (= (ite false ?x93 ?x699) ?x699)) (= ?x701 ?x699))))
  24.757 +(let ((@x732 (trans (monotonicity @x722 (= $x702 (= ?x504 ?x699))) (rewrite (= (= ?x504 ?x699) $x728)) (= $x702 $x728))))
  24.758 +(let ((@x740 (trans (monotonicity @x732 (= (or $x550 $x702) $x733)) (rewrite (= $x733 $x733)) (= (or $x550 $x702) $x733))))
  24.759 +(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))))
  24.760 +(let ((?x783 (* (- 1) ?x504)))
  24.761 +(let ((?x784 (+ ?x99 ?x783)))
  24.762 +(let (($x786 (>= ?x784 0)))
  24.763 +(let (($x782 (= ?x99 ?x504)))
  24.764 +(let (($x821 (= ?x98 ?x504)))
  24.765 +(let (($x505 (= ?x504 ?x98)))
  24.766 +(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)) )))
  24.767 +))
  24.768 +(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
  24.769 +))
  24.770 +(let (($x50 (= (mod$ ?x45 2) (mod$ ?x48 2))))
  24.771 +(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
  24.772 +(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
  24.773 +(let (($x514 (or (not $x297) $x505)))
  24.774 +(let ((@x515 ((_ quant-inst ks$ xs$) $x514)))
  24.775 +(let ((@x824 (symm (unit-resolution (def-axiom (or $x283 $x100)) @x466 $x100) (= ?x99 ?x98))))
  24.776 +(let ((@x939 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x786)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x786)))
  24.777 +(let (($x785 (<= ?x784 0)))
  24.778 +(let ((@x887 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x785)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x785)))
  24.779 +(let (($x688 (>= ?x686 0)))
  24.780 +(let ((@x855 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x688)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x688)))
  24.781 +(let ((@x979 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x425 2)))) @x26 (not (>= ?x425 2)))))
  24.782 +(let (($x560 (<= ?x544 0)))
  24.783 +(let ((@x461 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x560)) (unit-resolution @x559 @x323 $x545) $x560)))
  24.784 +(let (($x763 (<= ?x758 0)))
  24.785 +(let ((@x658 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x763)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x763)))
  24.786 +(let (($x581 (<= ?x576 0)))
  24.787 +(let ((@x986 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x581)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x581)))
  24.788 +(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))))
  24.789 +(let (($x510 (>= ?x502 0)))
  24.790 +(let ((@x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x510)) (unit-resolution @x508 @x309 $x503) $x510)))
  24.791 +(let ((@x998 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) (>= ?x396 0))) @x802 (>= ?x396 0))))
  24.792 +(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))))
  24.793 +(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)))
  24.794 +(let ((@x474 (unit-resolution (lemma @x1002 (or (not $x972) (not $x688) (not $x785))) @x855 @x887 (not $x972))))
  24.795 +(let ((@x941 (unit-resolution @x474 ((_ th-lemma arith) @x939 @x427 @x880 @x872 @x902 @x899 $x972) false)))
  24.796 +(let ((@x942 (lemma @x941 $x283)))
  24.797 +(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
  24.798 +(let ((@x679 (unit-resolution @x340 @x942 $x95)))
  24.799 +(let ((@x889 (trans (symm (unit-resolution @x515 @x302 $x505) $x821) (monotonicity @x679 (= ?x504 ?x99)) $x100)))
  24.800 +(let (($x811 (not $x687)))
  24.801 +(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))))
  24.802 +(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)))
  24.803 +(let ((@x935 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x811 (not $x688))) (hypothesis $x282) (or $x811 (not $x688)))))
  24.804 +(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)))
  24.805 +(let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281)))
  24.806 +(unit-resolution @x472 @x889 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  24.807 +
  24.808 +0f7f4a10f8a84029fd3a6efddc4408fa429b0cda 113 0
  24.809 +unsat
  24.810 +((set-logic <null>)
  24.811 +(proof
  24.812 +(let ((?x228 (mod x$ 2)))
  24.813 +(let ((?x262 (* (- 1) ?x228)))
  24.814 +(let ((?x31 (mod$ x$ 2)))
  24.815 +(let ((?x263 (+ ?x31 ?x262)))
  24.816 +(let (($x280 (>= ?x263 0)))
  24.817 +(let (($x264 (= ?x263 0)))
  24.818 +(let (($x205 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x136 (mod ?v0 ?v1)))
  24.819 +(let ((?x93 (* (- 1) ?v1)))
  24.820 +(let ((?x90 (* (- 1) ?v0)))
  24.821 +(let ((?x144 (mod ?x90 ?x93)))
  24.822 +(let ((?x150 (* (- 1) ?x144)))
  24.823 +(let (($x111 (<= ?v1 0)))
  24.824 +(let ((?x170 (ite $x111 ?x150 ?x136)))
  24.825 +(let (($x78 (= ?v1 0)))
  24.826 +(let ((?x175 (ite $x78 ?v0 ?x170)))
  24.827 +(let ((?x135 (mod$ ?v0 ?v1)))
  24.828 +(= ?x135 ?x175))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
  24.829 +))
  24.830 +(let (($x181 (forall ((?v0 Int) (?v1 Int) )(let ((?x136 (mod ?v0 ?v1)))
  24.831 +(let ((?x93 (* (- 1) ?v1)))
  24.832 +(let ((?x90 (* (- 1) ?v0)))
  24.833 +(let ((?x144 (mod ?x90 ?x93)))
  24.834 +(let ((?x150 (* (- 1) ?x144)))
  24.835 +(let (($x111 (<= ?v1 0)))
  24.836 +(let ((?x170 (ite $x111 ?x150 ?x136)))
  24.837 +(let (($x78 (= ?v1 0)))
  24.838 +(let ((?x175 (ite $x78 ?v0 ?x170)))
  24.839 +(let ((?x135 (mod$ ?v0 ?v1)))
  24.840 +(= ?x135 ?x175))))))))))))
  24.841 +))
  24.842 +(let ((?x136 (mod ?1 ?0)))
  24.843 +(let ((?x93 (* (- 1) ?0)))
  24.844 +(let ((?x90 (* (- 1) ?1)))
  24.845 +(let ((?x144 (mod ?x90 ?x93)))
  24.846 +(let ((?x150 (* (- 1) ?x144)))
  24.847 +(let (($x111 (<= ?0 0)))
  24.848 +(let ((?x170 (ite $x111 ?x150 ?x136)))
  24.849 +(let (($x78 (= ?0 0)))
  24.850 +(let ((?x175 (ite $x78 ?1 ?x170)))
  24.851 +(let ((?x135 (mod$ ?1 ?0)))
  24.852 +(let (($x178 (= ?x135 ?x175)))
  24.853 +(let (($x142 (forall ((?v0 Int) (?v1 Int) )(let (($x78 (= ?v1 0)))
  24.854 +(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
  24.855 +(let ((?x135 (mod$ ?v0 ?v1)))
  24.856 +(= ?x135 ?x140)))))
  24.857 +))
  24.858 +(let (($x164 (forall ((?v0 Int) (?v1 Int) )(let ((?x93 (* (- 1) ?v1)))
  24.859 +(let ((?x90 (* (- 1) ?v0)))
  24.860 +(let ((?x144 (mod ?x90 ?x93)))
  24.861 +(let ((?x150 (* (- 1) ?x144)))
  24.862 +(let ((?x136 (mod ?v0 ?v1)))
  24.863 +(let (($x79 (< 0 ?v1)))
  24.864 +(let ((?x155 (ite $x79 ?x136 ?x150)))
  24.865 +(let (($x78 (= ?v1 0)))
  24.866 +(let ((?x158 (ite $x78 ?v0 ?x155)))
  24.867 +(let ((?x135 (mod$ ?v0 ?v1)))
  24.868 +(= ?x135 ?x158))))))))))))
  24.869 +))
  24.870 +(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
  24.871 +(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
  24.872 +(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
  24.873 +(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
  24.874 +(let (($x79 (< 0 ?0)))
  24.875 +(let ((?x155 (ite $x79 ?x136 ?x150)))
  24.876 +(let ((?x158 (ite $x78 ?1 ?x155)))
  24.877 +(let (($x161 (= ?x135 ?x158)))
  24.878 +(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
  24.879 +(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
  24.880 +(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
  24.881 +(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
  24.882 +(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
  24.883 +(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
  24.884 +(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
  24.885 +(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
  24.886 +(let (($x270 (or (not $x205) $x264)))
  24.887 +(let ((?x225 (* (- 1) 2)))
  24.888 +(let ((?x224 (* (- 1) x$)))
  24.889 +(let ((?x226 (mod ?x224 ?x225)))
  24.890 +(let ((?x227 (* (- 1) ?x226)))
  24.891 +(let (($x223 (<= 2 0)))
  24.892 +(let ((?x229 (ite $x223 ?x227 ?x228)))
  24.893 +(let (($x222 (= 2 0)))
  24.894 +(let ((?x230 (ite $x222 x$ ?x229)))
  24.895 +(let (($x231 (= ?x31 ?x230)))
  24.896 +(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
  24.897 +(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
  24.898 +(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
  24.899 +(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
  24.900 +(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
  24.901 +(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
  24.902 +(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
  24.903 +(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
  24.904 +(let ((@x337 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
  24.905 +(let (($x305 (>= ?x228 0)))
  24.906 +(let (($x64 (>= ?x31 0)))
  24.907 +(let (($x67 (not $x64)))
  24.908 +(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
  24.909 +(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
  24.910 +(let ((?x32 (* 2 ?x31)))
  24.911 +(let ((?x47 (+ 1 x$ ?x32)))
  24.912 +(let (($x52 (<= (+ 1 x$) ?x47)))
  24.913 +(let (($x55 (not $x52)))
  24.914 +(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
  24.915 +(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
  24.916 +(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
  24.917 +(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
  24.918 +(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
  24.919 +(let ((@x74 (mp (asserted $x36) @x73 $x67)))
  24.920 +((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x337 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  24.921 +
  24.922 +fa5abc269019f00f5093218b287856c2a08c0adf 112 0
  24.923 +unsat
  24.924 +((set-logic <null>)
  24.925 +(proof
  24.926 +(let ((?x224 (mod x$ 2)))
  24.927 +(let (($x318 (>= ?x224 2)))
  24.928 +(let (($x319 (not $x318)))
  24.929 +(let ((?x258 (* (- 1) ?x224)))
  24.930 +(let ((?x29 (mod$ x$ 2)))
  24.931 +(let ((?x259 (+ ?x29 ?x258)))
  24.932 +(let (($x275 (<= ?x259 0)))
  24.933 +(let (($x260 (= ?x259 0)))
  24.934 +(let (($x201 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x132 (mod ?v0 ?v1)))
  24.935 +(let ((?x89 (* (- 1) ?v1)))
  24.936 +(let ((?x86 (* (- 1) ?v0)))
  24.937 +(let ((?x140 (mod ?x86 ?x89)))
  24.938 +(let ((?x146 (* (- 1) ?x140)))
  24.939 +(let (($x107 (<= ?v1 0)))
  24.940 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  24.941 +(let (($x74 (= ?v1 0)))
  24.942 +(let ((?x171 (ite $x74 ?v0 ?x166)))
  24.943 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.944 +(= ?x131 ?x171))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
  24.945 +))
  24.946 +(let (($x177 (forall ((?v0 Int) (?v1 Int) )(let ((?x132 (mod ?v0 ?v1)))
  24.947 +(let ((?x89 (* (- 1) ?v1)))
  24.948 +(let ((?x86 (* (- 1) ?v0)))
  24.949 +(let ((?x140 (mod ?x86 ?x89)))
  24.950 +(let ((?x146 (* (- 1) ?x140)))
  24.951 +(let (($x107 (<= ?v1 0)))
  24.952 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  24.953 +(let (($x74 (= ?v1 0)))
  24.954 +(let ((?x171 (ite $x74 ?v0 ?x166)))
  24.955 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.956 +(= ?x131 ?x171))))))))))))
  24.957 +))
  24.958 +(let ((?x132 (mod ?1 ?0)))
  24.959 +(let ((?x89 (* (- 1) ?0)))
  24.960 +(let ((?x86 (* (- 1) ?1)))
  24.961 +(let ((?x140 (mod ?x86 ?x89)))
  24.962 +(let ((?x146 (* (- 1) ?x140)))
  24.963 +(let (($x107 (<= ?0 0)))
  24.964 +(let ((?x166 (ite $x107 ?x146 ?x132)))
  24.965 +(let (($x74 (= ?0 0)))
  24.966 +(let ((?x171 (ite $x74 ?1 ?x166)))
  24.967 +(let ((?x131 (mod$ ?1 ?0)))
  24.968 +(let (($x174 (= ?x131 ?x171)))
  24.969 +(let (($x138 (forall ((?v0 Int) (?v1 Int) )(let (($x74 (= ?v1 0)))
  24.970 +(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
  24.971 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.972 +(= ?x131 ?x136)))))
  24.973 +))
  24.974 +(let (($x160 (forall ((?v0 Int) (?v1 Int) )(let ((?x89 (* (- 1) ?v1)))
  24.975 +(let ((?x86 (* (- 1) ?v0)))
  24.976 +(let ((?x140 (mod ?x86 ?x89)))
  24.977 +(let ((?x146 (* (- 1) ?x140)))
  24.978 +(let ((?x132 (mod ?v0 ?v1)))
  24.979 +(let (($x75 (< 0 ?v1)))
  24.980 +(let ((?x151 (ite $x75 ?x132 ?x146)))
  24.981 +(let (($x74 (= ?v1 0)))
  24.982 +(let ((?x154 (ite $x74 ?v0 ?x151)))
  24.983 +(let ((?x131 (mod$ ?v0 ?v1)))
  24.984 +(= ?x131 ?x154))))))))))))
  24.985 +))
  24.986 +(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
  24.987 +(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
  24.988 +(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
  24.989 +(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
  24.990 +(let (($x75 (< 0 ?0)))
  24.991 +(let ((?x151 (ite $x75 ?x132 ?x146)))
  24.992 +(let ((?x154 (ite $x74 ?1 ?x151)))
  24.993 +(let (($x157 (= ?x131 ?x154)))
  24.994 +(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
  24.995 +(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
  24.996 +(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
  24.997 +(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
  24.998 +(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
  24.999 +(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
 24.1000 +(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
 24.1001 +(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
 24.1002 +(let (($x266 (or (not $x201) $x260)))
 24.1003 +(let ((?x221 (* (- 1) 2)))
 24.1004 +(let ((?x220 (* (- 1) x$)))
 24.1005 +(let ((?x222 (mod ?x220 ?x221)))
 24.1006 +(let ((?x223 (* (- 1) ?x222)))
 24.1007 +(let (($x219 (<= 2 0)))
 24.1008 +(let ((?x225 (ite $x219 ?x223 ?x224)))
 24.1009 +(let (($x218 (= 2 0)))
 24.1010 +(let ((?x226 (ite $x218 x$ ?x225)))
 24.1011 +(let (($x227 (= ?x29 ?x226)))
 24.1012 +(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
 24.1013 +(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
 24.1014 +(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
 24.1015 +(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
 24.1016 +(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
 24.1017 +(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
 24.1018 +(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
 24.1019 +(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
 24.1020 +(let ((@x336 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
 24.1021 +(let (($x63 (>= ?x29 2)))
 24.1022 +(let ((?x37 (* 2 ?x29)))
 24.1023 +(let (($x56 (>= ?x37 3)))
 24.1024 +(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
 24.1025 +(let (($x49 (not $x46)))
 24.1026 +(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
 24.1027 +(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
 24.1028 +(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
 24.1029 +(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
 24.1030 +(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
 24.1031 +(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
 24.1032 +(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
 24.1033 +((_ th-lemma arith farkas -1 1 1) @x70 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 24.1034 +
 24.1035 +1880f0ed1cb3d1cfa006dff17f1b5553ce3a5158 236 0
 24.1036 +unsat
 24.1037 +((set-logic <null>)
 24.1038 +(proof
 24.1039 +(let ((?x410 (div n$ 2)))
 24.1040 +(let ((?x704 (* (- 1) ?x410)))
 24.1041 +(let ((?x381 (div n$ 4)))
 24.1042 +(let ((?x601 (* (- 2) ?x381)))
 24.1043 +(let ((?x329 (mod n$ 4)))
 24.1044 +(let ((?x363 (* (- 1) ?x329)))
 24.1045 +(let ((?x35 (mod$ n$ 4)))
 24.1046 +(let ((?x705 (+ n$ ?x35 ?x363 ?x601 ?x704)))
 24.1047 +(let (($x706 (>= ?x705 2)))
 24.1048 +(let ((?x39 (mod$ n$ 2)))
 24.1049 +(let (($x515 (>= ?x39 1)))
 24.1050 +(let (($x725 (not $x515)))
 24.1051 +(let (($x514 (<= ?x39 1)))
 24.1052 +(let ((?x519 (mod n$ 2)))
 24.1053 +(let ((?x534 (* (- 1) ?x519)))
 24.1054 +(let ((?x535 (+ ?x39 ?x534)))
 24.1055 +(let (($x408 (<= ?x535 0)))
 24.1056 +(let (($x490 (= ?x535 0)))
 24.1057 +(let (($x191 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x108 (mod ?v0 ?v1)))
 24.1058 +(let ((?x65 (* (- 1) ?v1)))
 24.1059 +(let ((?x62 (* (- 1) ?v0)))
 24.1060 +(let ((?x116 (mod ?x62 ?x65)))
 24.1061 +(let ((?x122 (* (- 1) ?x116)))
 24.1062 +(let (($x83 (<= ?v1 0)))
 24.1063 +(let ((?x142 (ite $x83 ?x122 ?x108)))
 24.1064 +(let (($x50 (= ?v1 0)))
 24.1065 +(let ((?x147 (ite $x50 ?v0 ?x142)))
 24.1066 +(let ((?x107 (mod$ ?v0 ?v1)))
 24.1067 +(= ?x107 ?x147))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
 24.1068 +))
 24.1069 +(let (($x153 (forall ((?v0 Int) (?v1 Int) )(let ((?x108 (mod ?v0 ?v1)))
 24.1070 +(let ((?x65 (* (- 1) ?v1)))
 24.1071 +(let ((?x62 (* (- 1) ?v0)))
 24.1072 +(let ((?x116 (mod ?x62 ?x65)))
 24.1073 +(let ((?x122 (* (- 1) ?x116)))
 24.1074 +(let (($x83 (<= ?v1 0)))
 24.1075 +(let ((?x142 (ite $x83 ?x122 ?x108)))
 24.1076 +(let (($x50 (= ?v1 0)))
 24.1077 +(let ((?x147 (ite $x50 ?v0 ?x142)))
 24.1078 +(let ((?x107 (mod$ ?v0 ?v1)))
 24.1079 +(= ?x107 ?x147))))))))))))
 24.1080 +))
 24.1081 +(let ((?x108 (mod ?1 ?0)))
 24.1082 +(let ((?x65 (* (- 1) ?0)))
 24.1083 +(let ((?x62 (* (- 1) ?1)))
 24.1084 +(let ((?x116 (mod ?x62 ?x65)))
 24.1085 +(let ((?x122 (* (- 1) ?x116)))
 24.1086 +(let (($x83 (<= ?0 0)))
 24.1087 +(let ((?x142 (ite $x83 ?x122 ?x108)))
 24.1088 +(let (($x50 (= ?0 0)))
 24.1089 +(let ((?x147 (ite $x50 ?1 ?x142)))
 24.1090 +(let ((?x107 (mod$ ?1 ?0)))
 24.1091 +(let (($x150 (= ?x107 ?x147)))
 24.1092 +(let (($x114 (forall ((?v0 Int) (?v1 Int) )(let (($x50 (= ?v1 0)))
 24.1093 +(let ((?x112 (ite $x50 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
 24.1094 +(let ((?x107 (mod$ ?v0 ?v1)))
 24.1095 +(= ?x107 ?x112)))))
 24.1096 +))
 24.1097 +(let (($x136 (forall ((?v0 Int) (?v1 Int) )(let ((?x65 (* (- 1) ?v1)))
 24.1098 +(let ((?x62 (* (- 1) ?v0)))
 24.1099 +(let ((?x116 (mod ?x62 ?x65)))
 24.1100 +(let ((?x122 (* (- 1) ?x116)))
 24.1101 +(let ((?x108 (mod ?v0 ?v1)))
 24.1102 +(let (($x51 (< 0 ?v1)))
 24.1103 +(let ((?x127 (ite $x51 ?x108 ?x122)))
 24.1104 +(let (($x50 (= ?v1 0)))
 24.1105 +(let ((?x130 (ite $x50 ?v0 ?x127)))
 24.1106 +(let ((?x107 (mod$ ?v0 ?v1)))
 24.1107 +(= ?x107 ?x130))))))))))))
 24.1108 +))
 24.1109 +(let ((@x141 (monotonicity (rewrite (= (< 0 ?0) (not $x83))) (= (ite (< 0 ?0) ?x108 ?x122) (ite (not $x83) ?x108 ?x122)))))
 24.1110 +(let ((@x146 (trans @x141 (rewrite (= (ite (not $x83) ?x108 ?x122) ?x142)) (= (ite (< 0 ?0) ?x108 ?x122) ?x142))))
 24.1111 +(let ((@x149 (monotonicity @x146 (= (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122)) ?x147))))
 24.1112 +(let ((@x152 (monotonicity @x149 (= (= ?x107 (ite $x50 ?1 (ite (< 0 ?0) ?x108 ?x122))) $x150))))
 24.1113 +(let (($x51 (< 0 ?0)))
 24.1114 +(let ((?x127 (ite $x51 ?x108 ?x122)))
 24.1115 +(let ((?x130 (ite $x50 ?1 ?x127)))
 24.1116 +(let (($x133 (= ?x107 ?x130)))
 24.1117 +(let (($x134 (= (= ?x107 (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))))) $x133)))
 24.1118 +(let ((@x118 (monotonicity (rewrite (= (- ?1) ?x62)) (rewrite (= (- ?0) ?x65)) (= (mod (- ?1) (- ?0)) ?x116))))
 24.1119 +(let ((@x126 (trans (monotonicity @x118 (= (- (mod (- ?1) (- ?0))) (- ?x116))) (rewrite (= (- ?x116) ?x122)) (= (- (mod (- ?1) (- ?0))) ?x122))))
 24.1120 +(let ((@x129 (monotonicity @x126 (= (ite $x51 ?x108 (- (mod (- ?1) (- ?0)))) ?x127))))
 24.1121 +(let ((@x132 (monotonicity @x129 (= (ite $x50 ?1 (ite $x51 ?x108 (- (mod (- ?1) (- ?0))))) ?x130))))
 24.1122 +(let ((@x157 (trans (quant-intro (monotonicity @x132 $x134) (= $x114 $x136)) (quant-intro @x152 (= $x136 $x153)) (= $x114 $x153))))
 24.1123 +(let ((@x168 (mp~ (mp (asserted $x114) @x157 $x153) (nnf-pos (refl (~ $x150 $x150)) (~ $x153 $x153)) $x153)))
 24.1124 +(let ((@x196 (mp @x168 (quant-intro (refl (= $x150 $x150)) (= $x153 $x191)) $x191)))
 24.1125 +(let (($x260 (not $x191)))
 24.1126 +(let (($x541 (or $x260 $x490)))
 24.1127 +(let ((?x211 (* (- 1) 2)))
 24.1128 +(let ((?x222 (* (- 1) n$)))
 24.1129 +(let ((?x517 (mod ?x222 ?x211)))
 24.1130 +(let ((?x518 (* (- 1) ?x517)))
 24.1131 +(let (($x209 (<= 2 0)))
 24.1132 +(let ((?x520 (ite $x209 ?x518 ?x519)))
 24.1133 +(let (($x208 (= 2 0)))
 24.1134 +(let ((?x521 (ite $x208 n$ ?x520)))
 24.1135 +(let (($x485 (= ?x39 ?x521)))
 24.1136 +(let ((@x593 (monotonicity (monotonicity (rewrite (= ?x211 (- 2))) (= ?x517 (mod ?x222 (- 2)))) (= ?x518 (* (- 1) (mod ?x222 (- 2)))))))
 24.1137 +(let ((@x221 (rewrite (= $x209 false))))
 24.1138 +(let ((@x596 (monotonicity @x221 @x593 (= ?x520 (ite false (* (- 1) (mod ?x222 (- 2))) ?x519)))))
 24.1139 +(let ((@x599 (trans @x596 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 2))) ?x519) ?x519)) (= ?x520 ?x519))))
 24.1140 +(let ((@x219 (rewrite (= $x208 false))))
 24.1141 +(let ((@x487 (trans (monotonicity @x219 @x599 (= ?x521 (ite false n$ ?x519))) (rewrite (= (ite false n$ ?x519) ?x519)) (= ?x521 ?x519))))
 24.1142 +(let ((@x538 (trans (monotonicity @x487 (= $x485 (= ?x39 ?x519))) (rewrite (= (= ?x39 ?x519) $x490)) (= $x485 $x490))))
 24.1143 +(let ((@x406 (trans (monotonicity @x538 (= (or $x260 $x485) $x541)) (rewrite (= $x541 $x541)) (= (or $x260 $x485) $x541))))
 24.1144 +(let ((@x407 (mp ((_ quant-inst n$ 2) (or $x260 $x485)) @x406 $x541)))
 24.1145 +(let ((@x715 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x408)) (unit-resolution @x407 @x196 $x490) $x408)))
 24.1146 +(let (($x303 (>= ?x519 2)))
 24.1147 +(let (($x304 (not $x303)))
 24.1148 +(let ((@x26 (true-axiom true)))
 24.1149 +(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)))
 24.1150 +(let (($x41 (= ?x39 1)))
 24.1151 +(let (($x169 (not $x41)))
 24.1152 +(let ((?x42 (mod$ m$ 2)))
 24.1153 +(let (($x43 (= ?x42 1)))
 24.1154 +(let ((?x29 (+ n$ m$)))
 24.1155 +(let ((?x214 (mod ?x29 2)))
 24.1156 +(let ((?x253 (* (- 1) ?x214)))
 24.1157 +(let ((?x31 (mod$ ?x29 2)))
 24.1158 +(let ((?x603 (+ n$ m$ ?x31 ?x35 ?x253 (* (- 1) (div ?x29 2)) ?x363 ?x601 (* (- 1) (div m$ 2)))))
 24.1159 +(let (($x604 (>= ?x603 2)))
 24.1160 +(let (($x523 (>= ?x42 1)))
 24.1161 +(let (($x609 (not $x523)))
 24.1162 +(let (($x522 (<= ?x42 1)))
 24.1163 +(let ((?x439 (mod m$ 2)))
 24.1164 +(let ((?x466 (* (- 1) ?x439)))
 24.1165 +(let ((?x467 (+ ?x42 ?x466)))
 24.1166 +(let (($x482 (<= ?x467 0)))
 24.1167 +(let (($x468 (= ?x467 0)))
 24.1168 +(let (($x473 (or $x260 $x468)))
 24.1169 +(let ((?x440 (ite $x209 (* (- 1) (mod (* (- 1) m$) ?x211)) ?x439)))
 24.1170 +(let ((?x441 (ite $x208 m$ ?x440)))
 24.1171 +(let (($x442 (= ?x42 ?x441)))
 24.1172 +(let ((@x453 (rewrite (= (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439) ?x439))))
 24.1173 +(let (($x447 (= (* (- 1) (mod (* (- 1) m$) ?x211)) (* (- 1) (mod (* (- 1) m$) (- 2))))))
 24.1174 +(let ((@x229 (rewrite (= ?x211 (- 2)))))
 24.1175 +(let ((@x445 (monotonicity @x229 (= (mod (* (- 1) m$) ?x211) (mod (* (- 1) m$) (- 2))))))
 24.1176 +(let ((@x451 (monotonicity @x221 (monotonicity @x445 $x447) (= ?x440 (ite false (* (- 1) (mod (* (- 1) m$) (- 2))) ?x439)))))
 24.1177 +(let ((@x458 (monotonicity @x219 (trans @x451 @x453 (= ?x440 ?x439)) (= ?x441 (ite false m$ ?x439)))))
 24.1178 +(let ((@x465 (monotonicity (trans @x458 (rewrite (= (ite false m$ ?x439) ?x439)) (= ?x441 ?x439)) (= $x442 (= ?x42 ?x439)))))
 24.1179 +(let ((@x477 (monotonicity (trans @x465 (rewrite (= (= ?x42 ?x439) $x468)) (= $x442 $x468)) (= (or $x260 $x442) $x473))))
 24.1180 +(let ((@x481 (mp ((_ quant-inst m$ 2) (or $x260 $x442)) (trans @x477 (rewrite (= $x473 $x473)) (= (or $x260 $x442) $x473)) $x473)))
 24.1181 +(let ((@x277 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) $x482)) (unit-resolution @x481 @x196 $x468) $x482)))
 24.1182 +(let ((@x386 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x439 2)))) @x26 (not (>= ?x439 2)))))
 24.1183 +(let ((@x384 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x522 (>= ?x439 2) (not $x482))) @x386 @x277 $x522)))
 24.1184 +(let ((@x564 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x43 (not $x522) $x609)) (hypothesis (not $x43)) (or (not $x522) $x609))))
 24.1185 +(let ((?x272 (div ?x29 2)))
 24.1186 +(let ((?x288 (* (- 2) ?x272)))
 24.1187 +(let ((?x289 (+ n$ m$ ?x253 ?x288)))
 24.1188 +(let (($x294 (<= ?x289 0)))
 24.1189 +(let (($x287 (= ?x289 0)))
 24.1190 +(let ((@x617 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x294)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x294)))
 24.1191 +(let (($x433 (<= ?x31 0)))
 24.1192 +(let (($x32 (= ?x31 0)))
 24.1193 +(let ((@x33 (asserted $x32)))
 24.1194 +(let ((?x254 (+ ?x31 ?x253)))
 24.1195 +(let (($x270 (<= ?x254 0)))
 24.1196 +(let (($x255 (= ?x254 0)))
 24.1197 +(let (($x261 (or $x260 $x255)))
 24.1198 +(let ((?x215 (ite $x209 (* (- 1) (mod (* (- 1) ?x29) ?x211)) ?x214)))
 24.1199 +(let ((?x216 (ite $x208 ?x29 ?x215)))
 24.1200 +(let (($x217 (= ?x31 ?x216)))
 24.1201 +(let (($x239 (= (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214) ?x214)))
 24.1202 +(let (($x237 (= ?x215 (ite false (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))) ?x214))))
 24.1203 +(let (($x234 (= (* (- 1) (mod (* (- 1) ?x29) ?x211)) (* (- 1) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
 24.1204 +(let ((@x232 (monotonicity (rewrite (= (* (- 1) ?x29) (+ ?x222 (* (- 1) m$)))) @x229 (= (mod (* (- 1) ?x29) ?x211) (mod (+ ?x222 (* (- 1) m$)) (- 2))))))
 24.1205 +(let ((@x242 (trans (monotonicity @x221 (monotonicity @x232 $x234) $x237) (rewrite $x239) (= ?x215 ?x214))))
 24.1206 +(let ((@x249 (trans (monotonicity @x219 @x242 (= ?x216 (ite false ?x29 ?x214))) (rewrite (= (ite false ?x29 ?x214) ?x214)) (= ?x216 ?x214))))
 24.1207 +(let ((@x259 (trans (monotonicity @x249 (= $x217 (= ?x31 ?x214))) (rewrite (= (= ?x31 ?x214) $x255)) (= $x217 $x255))))
 24.1208 +(let ((@x268 (trans (monotonicity @x259 (= (or $x260 $x217) $x261)) (rewrite (= $x261 $x261)) (= (or $x260 $x217) $x261))))
 24.1209 +(let ((@x269 (mp ((_ quant-inst (+ n$ m$) 2) (or $x260 $x217)) @x268 $x261)))
 24.1210 +(let ((@x626 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x270)) (unit-resolution @x269 @x196 $x255) $x270)))
 24.1211 +(let ((?x498 (+ m$ ?x466 (* (- 2) (div m$ 2)))))
 24.1212 +(let (($x496 (= ?x498 0)))
 24.1213 +(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))))
 24.1214 +(let ((?x397 (* (- 4) ?x381)))
 24.1215 +(let ((?x398 (+ n$ ?x363 ?x397)))
 24.1216 +(let (($x403 (<= ?x398 0)))
 24.1217 +(let (($x396 (= ?x398 0)))
 24.1218 +(let ((@x640 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x403)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x403)))
 24.1219 +(let ((?x364 (+ ?x35 ?x363)))
 24.1220 +(let (($x379 (<= ?x364 0)))
 24.1221 +(let (($x365 (= ?x364 0)))
 24.1222 +(let (($x370 (or $x260 $x365)))
 24.1223 +(let ((?x330 (ite (<= 4 0) (* (- 1) (mod ?x222 (* (- 1) 4))) ?x329)))
 24.1224 +(let ((?x331 (ite (= 4 0) n$ ?x330)))
 24.1225 +(let (($x332 (= ?x35 ?x331)))
 24.1226 +(let ((@x342 (monotonicity (rewrite (= (* (- 1) 4) (- 4))) (= (mod ?x222 (* (- 1) 4)) (mod ?x222 (- 4))))))
 24.1227 +(let ((@x345 (monotonicity @x342 (= (* (- 1) (mod ?x222 (* (- 1) 4))) (* (- 1) (mod ?x222 (- 4)))))))
 24.1228 +(let ((@x348 (monotonicity (rewrite (= (<= 4 0) false)) @x345 (= ?x330 (ite false (* (- 1) (mod ?x222 (- 4))) ?x329)))))
 24.1229 +(let ((@x352 (trans @x348 (rewrite (= (ite false (* (- 1) (mod ?x222 (- 4))) ?x329) ?x329)) (= ?x330 ?x329))))
 24.1230 +(let ((@x355 (monotonicity (rewrite (= (= 4 0) false)) @x352 (= ?x331 (ite false n$ ?x329)))))
 24.1231 +(let ((@x362 (monotonicity (trans @x355 (rewrite (= (ite false n$ ?x329) ?x329)) (= ?x331 ?x329)) (= $x332 (= ?x35 ?x329)))))
 24.1232 +(let ((@x374 (monotonicity (trans @x362 (rewrite (= (= ?x35 ?x329) $x365)) (= $x332 $x365)) (= (or $x260 $x332) $x370))))
 24.1233 +(let ((@x378 (mp ((_ quant-inst n$ 4) (or $x260 $x332)) (trans @x374 (rewrite (= $x370 $x370)) (= (or $x260 $x332) $x370)) $x370)))
 24.1234 +(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x379)) (unit-resolution @x378 @x196 $x365) $x379)))
 24.1235 +(let (($x435 (<= ?x35 3)))
 24.1236 +(let (($x37 (= ?x35 3)))
 24.1237 +(let ((@x38 (asserted $x37)))
 24.1238 +(let ((@x655 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x468) (>= ?x467 0))) (unit-resolution @x481 @x196 $x468) (>= ?x467 0))))
 24.1239 +(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)))
 24.1240 +(let ((@x565 (unit-resolution (lemma @x656 (or (not $x604) $x523)) (unit-resolution @x564 @x384 $x609) (not $x604))))
 24.1241 +(let (($x295 (>= ?x289 0)))
 24.1242 +(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x287) $x295)) (unit-resolution ((_ th-lemma arith) (or false $x287)) @x26 $x287) $x295)))
 24.1243 +(let (($x434 (>= ?x31 0)))
 24.1244 +(let (($x271 (>= ?x254 0)))
 24.1245 +(let ((@x531 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x255) $x271)) (unit-resolution @x269 @x196 $x255) $x271)))
 24.1246 +(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))))
 24.1247 +(let ((@x549 (unit-resolution ((_ th-lemma arith) (or false (>= ?x439 0))) @x26 (>= ?x439 0))))
 24.1248 +(let (($x404 (>= ?x398 0)))
 24.1249 +(let ((@x552 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x396) $x404)) (unit-resolution ((_ th-lemma arith) (or false $x396)) @x26 $x396) $x404)))
 24.1250 +(let (($x380 (>= ?x364 0)))
 24.1251 +(let ((@x273 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x365) $x380)) (unit-resolution @x378 @x196 $x365) $x380)))
 24.1252 +(let (($x436 (>= ?x35 3)))
 24.1253 +(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)))
 24.1254 +(let (($x171 (or $x169 (not $x43))))
 24.1255 +(let ((@x177 (monotonicity (rewrite (= (and $x41 $x43) (not $x171))) (= (not (and $x41 $x43)) (not (not $x171))))))
 24.1256 +(let ((@x181 (trans @x177 (rewrite (= (not (not $x171)) $x171)) (= (not (and $x41 $x43)) $x171))))
 24.1257 +(let ((@x182 (mp (asserted (not (and $x41 $x43))) @x181 $x171)))
 24.1258 +(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))))
 24.1259 +(let ((?x420 (* (- 2) ?x410)))
 24.1260 +(let ((?x421 (+ n$ ?x420 ?x534)))
 24.1261 +(let (($x426 (<= ?x421 0)))
 24.1262 +(let (($x419 (= ?x421 0)))
 24.1263 +(let ((@x737 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x426)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x426)))
 24.1264 +(let (($x409 (>= ?x535 0)))
 24.1265 +(let ((@x741 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x490) $x409)) (unit-resolution @x407 @x196 $x490) $x409)))
 24.1266 +(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)))
 24.1267 +(let (($x427 (>= ?x421 0)))
 24.1268 +(let ((@x584 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x419) $x427)) (unit-resolution ((_ th-lemma arith) (or false $x419)) @x26 $x419) $x427)))
 24.1269 +(let (($x542 (>= ?x519 0)))
 24.1270 +((_ 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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 24.1271 +
 24.1272 +f6a4c40290fd6742c0b08a1fe90b3664e90c2143 336 0
 24.1273 +unsat
 24.1274 +((set-logic <null>)
 24.1275 +(proof
 24.1276 +(let ((?x99 (mod$ l$ 2)))
 24.1277 +(let ((?x96 (map$ uu$ xs$)))
 24.1278 +(let ((?x97 (eval_dioph$ ks$ ?x96)))
 24.1279 +(let ((?x98 (mod$ ?x97 2)))
 24.1280 +(let (($x100 (= ?x98 ?x99)))
 24.1281 +(let ((?x93 (eval_dioph$ ks$ xs$)))
 24.1282 +(let (($x95 (= ?x93 l$)))
 24.1283 +(let ((?x110 (* (- 1) ?x97)))
 24.1284 +(let ((?x111 (+ l$ ?x110)))
 24.1285 +(let ((?x114 (divide$ ?x111 2)))
 24.1286 +(let ((?x101 (map$ uua$ xs$)))
 24.1287 +(let ((?x102 (eval_dioph$ ks$ ?x101)))
 24.1288 +(let (($x117 (= ?x102 ?x114)))
 24.1289 +(let (($x282 (not $x117)))
 24.1290 +(let (($x281 (not $x100)))
 24.1291 +(let (($x283 (or $x281 $x282)))
 24.1292 +(let ((?x744 (div ?x93 2)))
 24.1293 +(let ((?x970 (* (- 1) ?x744)))
 24.1294 +(let ((?x699 (mod ?x93 2)))
 24.1295 +(let ((?x726 (* (- 1) ?x699)))
 24.1296 +(let ((?x516 (mod l$ 2)))
 24.1297 +(let ((?x543 (* (- 1) ?x516)))
 24.1298 +(let (($x972 (>= (+ l$ ?x99 ?x543 (* (- 1) (div l$ 2)) ?x726 ?x970) 1)))
 24.1299 +(let ((?x369 (* (- 1) l$)))
 24.1300 +(let ((?x693 (+ ?x93 ?x369)))
 24.1301 +(let (($x695 (>= ?x693 0)))
 24.1302 +(let (($x861 (not $x695)))
 24.1303 +(let (($x694 (<= ?x693 0)))
 24.1304 +(let ((?x686 (+ ?x102 (* (- 1) ?x114))))
 24.1305 +(let (($x687 (<= ?x686 0)))
 24.1306 +(let (($x284 (not $x283)))
 24.1307 +(let ((@x466 (hypothesis $x284)))
 24.1308 +(let ((@x856 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x687)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x687)))
 24.1309 +(let ((?x437 (+ l$ ?x110 (* (- 2) (div ?x111 2)) (* (- 1) (mod (+ l$ ?x97) 2)))))
 24.1310 +(let (($x443 (>= ?x437 0)))
 24.1311 +(let (($x434 (= ?x437 0)))
 24.1312 +(let ((@x26 (true-axiom true)))
 24.1313 +(let ((@x793 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
 24.1314 +(let ((?x501 (* (- 2) ?x102)))
 24.1315 +(let ((?x502 (+ ?x93 ?x110 ?x501)))
 24.1316 +(let (($x509 (<= ?x502 0)))
 24.1317 +(let (($x503 (= ?x502 0)))
 24.1318 +(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(let ((?x45 (eval_dioph$ ?v0 ?v1)))
 24.1319 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
 24.1320 +(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
 24.1321 +))
 24.1322 +(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
 24.1323 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
 24.1324 +(= ?x83 0))))
 24.1325 +))
 24.1326 +(let ((?x45 (eval_dioph$ ?1 ?0)))
 24.1327 +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
 24.1328 +(let (($x79 (= ?x83 0)))
 24.1329 +(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
 24.1330 +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
 24.1331 +(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
 24.1332 +(= ?x56 ?x45)))))
 24.1333 +))
 24.1334 +(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
 24.1335 +(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
 24.1336 +(let ((?x60 (* 2 ?x54)))
 24.1337 +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
 24.1338 +(let ((?x66 (+ ?x48 ?x60)))
 24.1339 +(= ?x66 ?x45)))))))
 24.1340 +))
 24.1341 +(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
 24.1342 +(let ((?x60 (* 2 ?x54)))
 24.1343 +(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
 24.1344 +(let ((?x66 (+ ?x48 ?x60)))
 24.1345 +(let (($x71 (= ?x66 ?x45)))
 24.1346 +(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
 24.1347 +(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
 24.1348 +(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
 24.1349 +(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
 24.1350 +(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
 24.1351 +(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
 24.1352 +(let (($x507 (or (not $x304) $x503)))
 24.1353 +(let ((@x508 ((_ quant-inst ks$ xs$) $x507)))
 24.1354 +(let ((@x800 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x509)) (unit-resolution @x508 @x309 $x503) $x509)))
 24.1355 +(let ((?x396 (+ ?x114 (* (- 1) (div ?x111 2)))))
 24.1356 +(let (($x413 (<= ?x396 0)))
 24.1357 +(let (($x397 (= ?x396 0)))
 24.1358 +(let (($x311 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x145 (div ?v0 ?v1)))
 24.1359 +(let ((?x157 (* (- 1) ?v1)))
 24.1360 +(let ((?x154 (* (- 1) ?v0)))
 24.1361 +(let ((?x160 (div ?x154 ?x157)))
 24.1362 +(let (($x175 (<= ?v1 0)))
 24.1363 +(let ((?x182 (ite $x175 ?x160 ?x145)))
 24.1364 +(let (($x143 (= ?v1 0)))
 24.1365 +(let ((?x141 (divide$ ?v0 ?v1)))
 24.1366 +(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) )))
 24.1367 +))
 24.1368 +(let (($x193 (forall ((?v0 Int) (?v1 Int) )(let ((?x145 (div ?v0 ?v1)))
 24.1369 +(let ((?x157 (* (- 1) ?v1)))
 24.1370 +(let ((?x154 (* (- 1) ?v0)))
 24.1371 +(let ((?x160 (div ?x154 ?x157)))
 24.1372 +(let (($x175 (<= ?v1 0)))
 24.1373 +(let ((?x182 (ite $x175 ?x160 ?x145)))
 24.1374 +(let (($x143 (= ?v1 0)))
 24.1375 +(let ((?x141 (divide$ ?v0 ?v1)))
 24.1376 +(= ?x141 (ite $x143 0 ?x182)))))))))))
 24.1377 +))
 24.1378 +(let ((?x145 (div ?1 ?0)))
 24.1379 +(let ((?x157 (* (- 1) ?0)))
 24.1380 +(let ((?x154 (* (- 1) ?1)))
 24.1381 +(let ((?x160 (div ?x154 ?x157)))
 24.1382 +(let (($x175 (<= ?0 0)))
 24.1383 +(let ((?x182 (ite $x175 ?x160 ?x145)))
 24.1384 +(let (($x143 (= ?0 0)))
 24.1385 +(let ((?x141 (divide$ ?1 ?0)))
 24.1386 +(let (($x190 (= ?x141 (ite $x143 0 ?x182))))
 24.1387 +(let (($x152 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
 24.1388 +(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
 24.1389 +(let ((?x141 (divide$ ?v0 ?v1)))
 24.1390 +(= ?x141 ?x150)))))
 24.1391 +))
 24.1392 +(let (($x172 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
 24.1393 +(let ((?x154 (* (- 1) ?v0)))
 24.1394 +(let ((?x160 (div ?x154 ?x157)))
 24.1395 +(let ((?x145 (div ?v0 ?v1)))
 24.1396 +(let (($x144 (< 0 ?v1)))
 24.1397 +(let ((?x163 (ite $x144 ?x145 ?x160)))
 24.1398 +(let (($x143 (= ?v1 0)))
 24.1399 +(let ((?x166 (ite $x143 0 ?x163)))
 24.1400 +(let ((?x141 (divide$ ?v0 ?v1)))
 24.1401 +(= ?x141 ?x166)))))))))))
 24.1402 +))
 24.1403 +(let (($x144 (< 0 ?0)))
 24.1404 +(let ((?x163 (ite $x144 ?x145 ?x160)))
 24.1405 +(let ((?x166 (ite $x143 0 ?x163)))
 24.1406 +(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
 24.1407 +(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) ?x182)) (= ?x163 ?x182))))
 24.1408 +(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 ?x182))) (= (= ?x141 ?x166) $x190))))
 24.1409 +(let (($x169 (= ?x141 ?x166)))
 24.1410 +(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
 24.1411 +(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
 24.1412 +(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
 24.1413 +(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
 24.1414 +(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
 24.1415 +(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
 24.1416 +(let (($x403 (or (not $x311) $x397)))
 24.1417 +(let ((?x361 (div ?x111 2)))
 24.1418 +(let (($x357 (<= 2 0)))
 24.1419 +(let ((?x362 (ite $x357 (div (* (- 1) ?x111) (* (- 1) 2)) ?x361)))
 24.1420 +(let (($x356 (= 2 0)))
 24.1421 +(let ((?x363 (ite $x356 0 ?x362)))
 24.1422 +(let (($x364 (= ?x114 ?x363)))
 24.1423 +(let ((@x374 (rewrite (= (* (- 1) 2) (- 2)))))
 24.1424 +(let ((@x377 (monotonicity (rewrite (= (* (- 1) ?x111) (+ ?x369 ?x97))) @x374 (= (div (* (- 1) ?x111) (* (- 1) 2)) (div (+ ?x369 ?x97) (- 2))))))
 24.1425 +(let ((@x368 (rewrite (= $x357 false))))
 24.1426 +(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
 24.1427 +(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
 24.1428 +(let ((@x366 (rewrite (= $x356 false))))
 24.1429 +(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
 24.1430 +(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
 24.1431 +(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
 24.1432 +(let ((@x802 (unit-resolution (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403) @x316 $x397)))
 24.1433 +(let ((?x425 (mod (+ l$ ?x97) 2)))
 24.1434 +(let (($x465 (>= ?x425 0)))
 24.1435 +(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)))
 24.1436 +(let (($x134 (not $x95)))
 24.1437 +(let (($x290 (= $x95 $x283)))
 24.1438 +(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
 24.1439 +(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
 24.1440 +(let (($x120 (and $x100 $x117)))
 24.1441 +(let (($x135 (= $x134 $x120)))
 24.1442 +(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
 24.1443 +(let (($x108 (not $x107)))
 24.1444 +(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
 24.1445 +(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
 24.1446 +(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
 24.1447 +(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
 24.1448 +(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
 24.1449 +(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
 24.1450 +(let ((@x898 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 (not $x694) $x861)) (unit-resolution @x344 @x466 $x134) (or (not $x694) $x861))))
 24.1451 +(let ((@x899 (unit-resolution @x898 (unit-resolution (lemma @x810 (or $x694 (not $x687))) @x856 $x694) $x861)))
 24.1452 +(let ((?x544 (+ ?x99 ?x543)))
 24.1453 +(let (($x561 (>= ?x544 0)))
 24.1454 +(let (($x545 (= ?x544 0)))
 24.1455 +(let (($x318 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x200 (mod ?v0 ?v1)))
 24.1456 +(let ((?x157 (* (- 1) ?v1)))
 24.1457 +(let ((?x154 (* (- 1) ?v0)))
 24.1458 +(let ((?x208 (mod ?x154 ?x157)))
 24.1459 +(let ((?x214 (* (- 1) ?x208)))
 24.1460 +(let (($x175 (<= ?v1 0)))
 24.1461 +(let ((?x234 (ite $x175 ?x214 ?x200)))
 24.1462 +(let (($x143 (= ?v1 0)))
 24.1463 +(let ((?x239 (ite $x143 ?v0 ?x234)))
 24.1464 +(let ((?x199 (mod$ ?v0 ?v1)))
 24.1465 +(= ?x199 ?x239))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
 24.1466 +))
 24.1467 +(let (($x245 (forall ((?v0 Int) (?v1 Int) )(let ((?x200 (mod ?v0 ?v1)))
 24.1468 +(let ((?x157 (* (- 1) ?v1)))
 24.1469 +(let ((?x154 (* (- 1) ?v0)))
 24.1470 +(let ((?x208 (mod ?x154 ?x157)))
 24.1471 +(let ((?x214 (* (- 1) ?x208)))
 24.1472 +(let (($x175 (<= ?v1 0)))
 24.1473 +(let ((?x234 (ite $x175 ?x214 ?x200)))
 24.1474 +(let (($x143 (= ?v1 0)))
 24.1475 +(let ((?x239 (ite $x143 ?v0 ?x234)))
 24.1476 +(let ((?x199 (mod$ ?v0 ?v1)))
 24.1477 +(= ?x199 ?x239))))))))))))
 24.1478 +))
 24.1479 +(let ((?x200 (mod ?1 ?0)))
 24.1480 +(let ((?x208 (mod ?x154 ?x157)))
 24.1481 +(let ((?x214 (* (- 1) ?x208)))
 24.1482 +(let ((?x234 (ite $x175 ?x214 ?x200)))
 24.1483 +(let ((?x239 (ite $x143 ?1 ?x234)))
 24.1484 +(let ((?x199 (mod$ ?1 ?0)))
 24.1485 +(let (($x242 (= ?x199 ?x239)))
 24.1486 +(let (($x206 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
 24.1487 +(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
 24.1488 +(let ((?x199 (mod$ ?v0 ?v1)))
 24.1489 +(= ?x199 ?x204)))))
 24.1490 +))
 24.1491 +(let (($x228 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
 24.1492 +(let ((?x154 (* (- 1) ?v0)))
 24.1493 +(let ((?x208 (mod ?x154 ?x157)))
 24.1494 +(let ((?x214 (* (- 1) ?x208)))
 24.1495 +(let ((?x200 (mod ?v0 ?v1)))
 24.1496 +(let (($x144 (< 0 ?v1)))
 24.1497 +(let ((?x219 (ite $x144 ?x200 ?x214)))
 24.1498 +(let (($x143 (= ?v1 0)))
 24.1499 +(let ((?x222 (ite $x143 ?v0 ?x219)))
 24.1500 +(let ((?x199 (mod$ ?v0 ?v1)))
 24.1501 +(= ?x199 ?x222))))))))))))
 24.1502 +))
 24.1503 +(let ((@x233 (monotonicity (rewrite (= $x144 (not $x175))) (= (ite $x144 ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
 24.1504 +(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite $x144 ?x200 ?x214) ?x234))))
 24.1505 +(let ((@x244 (monotonicity (monotonicity @x238 (= (ite $x143 ?1 (ite $x144 ?x200 ?x214)) ?x239)) (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 ?x214))) $x242))))
 24.1506 +(let ((?x219 (ite $x144 ?x200 ?x214)))
 24.1507 +(let ((?x222 (ite $x143 ?1 ?x219)))
 24.1508 +(let (($x225 (= ?x199 ?x222)))
 24.1509 +(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
 24.1510 +(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
 24.1511 +(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
 24.1512 +(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
 24.1513 +(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
 24.1514 +(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
 24.1515 +(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
 24.1516 +(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
 24.1517 +(let (($x550 (not $x318)))
 24.1518 +(let (($x551 (or $x550 $x545)))
 24.1519 +(let ((?x359 (* (- 1) 2)))
 24.1520 +(let ((?x511 (mod ?x369 ?x359)))
 24.1521 +(let ((?x512 (* (- 1) ?x511)))
 24.1522 +(let ((?x517 (ite $x357 ?x512 ?x516)))
 24.1523 +(let ((?x518 (ite $x356 l$ ?x517)))
 24.1524 +(let (($x519 (= ?x99 ?x518)))
 24.1525 +(let ((@x525 (monotonicity (monotonicity @x374 (= ?x511 (mod ?x369 (- 2)))) (= ?x512 (* (- 1) (mod ?x369 (- 2)))))))
 24.1526 +(let ((@x528 (monotonicity @x368 @x525 (= ?x517 (ite false (* (- 1) (mod ?x369 (- 2))) ?x516)))))
 24.1527 +(let ((@x532 (trans @x528 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x516) ?x516)) (= ?x517 ?x516))))
 24.1528 +(let ((@x539 (trans (monotonicity @x366 @x532 (= ?x518 (ite false l$ ?x516))) (rewrite (= (ite false l$ ?x516) ?x516)) (= ?x518 ?x516))))
 24.1529 +(let ((@x549 (trans (monotonicity @x539 (= $x519 (= ?x99 ?x516))) (rewrite (= (= ?x99 ?x516) $x545)) (= $x519 $x545))))
 24.1530 +(let ((@x558 (trans (monotonicity @x549 (= (or $x550 $x519) $x551)) (rewrite (= $x551 $x551)) (= (or $x550 $x519) $x551))))
 24.1531 +(let ((@x559 (mp ((_ quant-inst l$ 2) (or $x550 $x519)) @x558 $x551)))
 24.1532 +(let ((@x902 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x561)) (unit-resolution @x559 @x323 $x545) $x561)))
 24.1533 +(let ((?x757 (* (- 2) ?x744)))
 24.1534 +(let ((?x758 (+ ?x93 ?x726 ?x757)))
 24.1535 +(let (($x764 (>= ?x758 0)))
 24.1536 +(let (($x756 (= ?x758 0)))
 24.1537 +(let ((@x872 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x764)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x764)))
 24.1538 +(let ((?x562 (div l$ 2)))
 24.1539 +(let ((?x575 (* (- 2) ?x562)))
 24.1540 +(let ((?x576 (+ l$ ?x543 ?x575)))
 24.1541 +(let (($x582 (>= ?x576 0)))
 24.1542 +(let (($x574 (= ?x576 0)))
 24.1543 +(let ((@x880 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x582)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x582)))
 24.1544 +(let ((?x504 (mod$ ?x93 2)))
 24.1545 +(let ((?x727 (+ ?x504 ?x726)))
 24.1546 +(let (($x728 (= ?x727 0)))
 24.1547 +(let (($x733 (or $x550 $x728)))
 24.1548 +(let ((?x696 (* (- 1) ?x93)))
 24.1549 +(let ((?x697 (mod ?x696 ?x359)))
 24.1550 +(let ((?x698 (* (- 1) ?x697)))
 24.1551 +(let ((?x700 (ite $x357 ?x698 ?x699)))
 24.1552 +(let ((?x701 (ite $x356 ?x93 ?x700)))
 24.1553 +(let (($x702 (= ?x504 ?x701)))
 24.1554 +(let ((@x708 (monotonicity (monotonicity @x374 (= ?x697 (mod ?x696 (- 2)))) (= ?x698 (* (- 1) (mod ?x696 (- 2)))))))
 24.1555 +(let ((@x711 (monotonicity @x368 @x708 (= ?x700 (ite false (* (- 1) (mod ?x696 (- 2))) ?x699)))))
 24.1556 +(let ((@x715 (trans @x711 (rewrite (= (ite false (* (- 1) (mod ?x696 (- 2))) ?x699) ?x699)) (= ?x700 ?x699))))
 24.1557 +(let ((@x722 (trans (monotonicity @x366 @x715 (= ?x701 (ite false ?x93 ?x699))) (rewrite (= (ite false ?x93 ?x699) ?x699)) (= ?x701 ?x699))))
 24.1558 +(let ((@x732 (trans (monotonicity @x722 (= $x702 (= ?x504 ?x699))) (rewrite (= (= ?x504 ?x699) $x728)) (= $x702 $x728))))
 24.1559 +(let ((@x740 (trans (monotonicity @x732 (= (or $x550 $x702) $x733)) (rewrite (= $x733 $x733)) (= (or $x550 $x702) $x733))))
 24.1560 +(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))))
 24.1561 +(let ((?x783 (* (- 1) ?x504)))
 24.1562 +(let ((?x784 (+ ?x99 ?x783)))
 24.1563 +(let (($x786 (>= ?x784 0)))
 24.1564 +(let (($x782 (= ?x99 ?x504)))
 24.1565 +(let (($x821 (= ?x98 ?x504)))
 24.1566 +(let (($x505 (= ?x504 ?x98)))
 24.1567 +(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)) )))
 24.1568 +))
 24.1569 +(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
 24.1570 +))
 24.1571 +(let (($x50 (= (mod$ ?x45 2) (mod$ ?x48 2))))
 24.1572 +(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
 24.1573 +(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
 24.1574 +(let (($x514 (or (not $x297) $x505)))
 24.1575 +(let ((@x515 ((_ quant-inst ks$ xs$) $x514)))
 24.1576 +(let ((@x824 (symm (unit-resolution (def-axiom (or $x283 $x100)) @x466 $x100) (= ?x99 ?x98))))
 24.1577 +(let ((@x939 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x786)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x786)))
 24.1578 +(let (($x785 (<= ?x784 0)))
 24.1579 +(let ((@x887 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x785)) (trans @x824 (symm (unit-resolution @x515 @x302 $x505) $x821) $x782) $x785)))
 24.1580 +(let (($x688 (>= ?x686 0)))
 24.1581 +(let ((@x855 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x688)) (unit-resolution (def-axiom (or $x283 $x117)) @x466 $x117) $x688)))
 24.1582 +(let ((@x979 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x425 2)))) @x26 (not (>= ?x425 2)))))
 24.1583 +(let (($x560 (<= ?x544 0)))
 24.1584 +(let ((@x461 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x560)) (unit-resolution @x559 @x323 $x545) $x560)))
 24.1585 +(let (($x763 (<= ?x758 0)))
 24.1586 +(let ((@x658 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x763)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x763)))
 24.1587 +(let (($x581 (<= ?x576 0)))
 24.1588 +(let ((@x986 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x581)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x581)))
 24.1589 +(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))))
 24.1590 +(let (($x510 (>= ?x502 0)))
 24.1591 +(let ((@x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x510)) (unit-resolution @x508 @x309 $x503) $x510)))
 24.1592 +(let ((@x998 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) (>= ?x396 0))) @x802 (>= ?x396 0))))
 24.1593 +(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))))
 24.1594 +(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)))
 24.1595 +(let ((@x474 (unit-resolution (lemma @x1002 (or (not $x972) (not $x688) (not $x785))) @x855 @x887 (not $x972))))
 24.1596 +(let ((@x941 (unit-resolution @x474 ((_ th-lemma arith) @x939 @x427 @x880 @x872 @x902 @x899 $x972) false)))
 24.1597 +(let ((@x942 (lemma @x941 $x283)))
 24.1598 +(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
 24.1599 +(let ((@x679 (unit-resolution @x340 @x942 $x95)))
 24.1600 +(let ((@x889 (trans (symm (unit-resolution @x515 @x302 $x505) $x821) (monotonicity @x679 (= ?x504 ?x99)) $x100)))
 24.1601 +(let (($x811 (not $x687)))
 24.1602 +(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))))
 24.1603 +(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)))
 24.1604 +(let ((@x935 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x811 (not $x688))) (hypothesis $x282) (or $x811 (not $x688)))))
 24.1605 +(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)))
 24.1606 +(let ((@x472 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x942 $x283) (lemma @x955 $x117) $x281)))
 24.1607 +(unit-resolution @x472 @x889 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 24.1608 +
 24.1609  785615f585a02b3e6ed8608ecc9660ba5c4025e2 2 0
 24.1610  sat
 24.1611  (error "line 9 column 10: proof is not available")
    25.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 01 18:59:21 2015 +0200
    25.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 01 18:59:21 2015 +0200
    25.3 @@ -402,7 +402,7 @@
    25.4     ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
    25.5     ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
    25.6     ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
    25.7 -   ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
    25.8 +   ((@{const_name Rings.divide}, nat_T --> nat_T --> nat_T), 0),
    25.9     ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
   25.10     ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
   25.11     ((@{const_name of_nat}, nat_T --> int_T), 0),
   25.12 @@ -411,7 +411,7 @@
   25.13     ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
   25.14     ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
   25.15     ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
   25.16 -   ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
   25.17 +   ((@{const_name Rings.divide}, int_T --> int_T --> int_T), 0),
   25.18     ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
   25.19     ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
   25.20     ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
    26.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Jun 01 18:59:21 2015 +0200
    26.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Jun 01 18:59:21 2015 +0200
    26.3 @@ -553,7 +553,7 @@
    26.4          | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
    26.5            if is_built_in_const x then Cst (Multiply, T, Any)
    26.6            else ConstName (s, T, Any)
    26.7 -        | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
    26.8 +        | (Const (x as (s as @{const_name Rings.divide}, T)), []) =>
    26.9            if is_built_in_const x then Cst (Divide, T, Any)
   26.10            else ConstName (s, T, Any)
   26.11          | (t0 as Const (x as (@{const_name ord_class.less}, _)),
    27.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Jun 01 18:59:21 2015 +0200
    27.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Jun 01 18:59:21 2015 +0200
    27.3 @@ -56,7 +56,7 @@
    27.4    let
    27.5      fun aux (t1 $ t2) = aux t1 orelse aux t2
    27.6        | aux (Const (s, T)) =
    27.7 -        ((s = @{const_name times} orelse s = @{const_name div}) andalso
    27.8 +        ((s = @{const_name times} orelse s = @{const_name Rings.divide}) andalso
    27.9           is_integer_type (body_type T)) orelse
   27.10          (String.isPrefix numeral_prefix s andalso
   27.11           let val n = the (Int.fromString (unprefix numeral_prefix s)) in
    28.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 01 18:59:21 2015 +0200
    28.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 01 18:59:21 2015 +0200
    28.3 @@ -756,7 +756,7 @@
    28.4   | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
    28.5   | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
    28.6   | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
    28.7 - | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
    28.8 + | Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r
    28.9   | _ => is_number t orelse can HOLogic.dest_nat t
   28.10  
   28.11   fun ty cts t = 
    29.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Jun 01 18:59:21 2015 +0200
    29.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Jun 01 18:59:21 2015 +0200
    29.3 @@ -34,7 +34,7 @@
    29.4      {logic = K "", fp_kinds = [BNF_Util.Least_FP],
    29.5       serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
    29.6  
    29.7 -  fun is_div_mod @{const div (int)} = true
    29.8 +  fun is_div_mod @{const divide (int)} = true
    29.9      | is_div_mod @{const mod (int)} = true
   29.10      | is_div_mod _ = false
   29.11  
    30.1 --- a/src/HOL/Tools/SMT/z3_real.ML	Mon Jun 01 18:59:21 2015 +0200
    30.2 +++ b/src/HOL/Tools/SMT/z3_real.ML	Mon Jun 01 18:59:21 2015 +0200
    30.3 @@ -12,13 +12,13 @@
    30.4  
    30.5  fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i)
    30.6    | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
    30.7 -      SOME (@{term "inverse_class.divide :: real => _"} $ t1 $ t2)
    30.8 +      SOME (@{term "Rings.divide :: real => _"} $ t1 $ t2)
    30.9    | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t)
   30.10    | real_term_parser _ = NONE
   30.11  
   30.12  fun abstract abs t =
   30.13    (case t of
   30.14 -    (c as @{term "inverse_class.divide :: real => _"}) $ t1 $ t2 =>
   30.15 +    (c as @{term "Rings.divide :: real => _"}) $ t1 $ t2 =>
   30.16        abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
   30.17    | (c as @{term "Real.real :: int => _"}) $ t =>
   30.18        abs t #>> (fn u => SOME (c $ u))
    31.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Jun 01 18:59:21 2015 +0200
    31.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Jun 01 18:59:21 2015 +0200
    31.3 @@ -152,7 +152,7 @@
    31.4                (SOME t', m'') => (SOME (mC $ s' $ t'), m'')
    31.5              | (NONE,    m'') => (SOME s', m''))
    31.6          | (NONE,    m') => demult (t, m')))
    31.7 -    | demult (atom as (mC as Const (@{const_name Fields.divide}, T)) $ s $ t, m) =
    31.8 +    | demult (atom as (mC as Const (@{const_name Rings.divide}, T)) $ s $ t, m) =
    31.9        (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
   31.10           become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
   31.11           if we choose to do so here, the simpset used by arith must be able to
   31.12 @@ -219,7 +219,7 @@
   31.13          (case demult thy inj_consts (all, m) of
   31.14             (NONE,   m') => (p, Rat.add i m')
   31.15           | (SOME u, m') => add_atom u m' pi)
   31.16 -    | poly (all as Const (@{const_name Fields.divide}, T) $ _ $ _, m, pi as (p, i)) =
   31.17 +    | poly (all as Const (@{const_name Rings.divide}, T) $ _ $ _, m, pi as (p, i)) =
   31.18          if of_field_sort thy (domain_type T) then 
   31.19            (case demult thy inj_consts (all, m) of
   31.20               (NONE,   m') => (p, Rat.add i m')
   31.21 @@ -302,7 +302,7 @@
   31.22            @{const_name Groups.minus},
   31.23            "Int.nat" (*DYNAMIC BINDING!*),
   31.24            "Divides.div_class.mod" (*DYNAMIC BINDING!*),
   31.25 -          "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
   31.26 +          @{const_name Rings.divide}] a
   31.27      | _ =>
   31.28        (if Context_Position.is_visible ctxt then
   31.29          warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
   31.30 @@ -501,7 +501,7 @@
   31.31      (* ?P ((?n::nat) div (numeral ?k)) =
   31.32           ((numeral ?k = 0 --> ?P 0) & (~ (numeral ?k = 0) -->
   31.33             (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P i))) *)
   31.34 -    | (Const ("Divides.div_class.div", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
   31.35 +    | (Const (@{const_name Rings.divide}, Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
   31.36        let
   31.37          val rev_terms               = rev terms
   31.38          val zero                    = Const (@{const_name Groups.zero}, split_type)
   31.39 @@ -592,7 +592,7 @@
   31.40            (numeral ?k < 0 -->
   31.41              (ALL i j.
   31.42                numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P i))) *)
   31.43 -    | (Const ("Divides.div_class.div",
   31.44 +    | (Const (@{const_name Rings.divide},
   31.45          Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
   31.46        let
   31.47          val rev_terms               = rev terms
    32.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Jun 01 18:59:21 2015 +0200
    32.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Mon Jun 01 18:59:21 2015 +0200
    32.3 @@ -288,8 +288,8 @@
    32.4  
    32.5  structure DivCancelNumeralFactor = CancelNumeralFactorFun
    32.6   (open CancelNumeralFactorCommon
    32.7 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
    32.8 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
    32.9 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   32.10 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} HOLogic.natT
   32.11    val cancel = @{thm nat_mult_div_cancel1} RS trans
   32.12    val neg_exchanges = false
   32.13  );
   32.14 @@ -393,8 +393,8 @@
   32.15  
   32.16  structure DivideCancelFactor = ExtractCommonTermFun
   32.17   (open CancelFactorCommon
   32.18 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   32.19 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   32.20 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   32.21 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} HOLogic.natT
   32.22    fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
   32.23  );
   32.24  
    33.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Jun 01 18:59:21 2015 +0200
    33.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Jun 01 18:59:21 2015 +0200
    33.3 @@ -116,7 +116,7 @@
    33.4    Fractions are reduced later by the cancel_numeral_factor simproc.*)
    33.5  fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
    33.6  
    33.7 -val mk_divide = HOLogic.mk_binop @{const_name Fields.divide};
    33.8 +val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
    33.9  
   33.10  (*Build term (p / q) * t*)
   33.11  fun mk_fcoeff ((p, q), t) =
   33.12 @@ -125,7 +125,7 @@
   33.13  
   33.14  (*Express t as a product of a fraction with other sorted terms*)
   33.15  fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
   33.16 -  | dest_fcoeff sign (Const (@{const_name Fields.divide}, _) $ t $ u) =
   33.17 +  | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
   33.18      let val (p, t') = dest_coeff sign t
   33.19          val (q, u') = dest_coeff 1 u
   33.20      in (mk_frac (p, q), mk_divide (t', u')) end
   33.21 @@ -401,8 +401,8 @@
   33.22  (*Version for semiring_div*)
   33.23  structure DivCancelNumeralFactor = CancelNumeralFactorFun
   33.24   (open CancelNumeralFactorCommon
   33.25 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   33.26 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
   33.27 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   33.28 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   33.29    val cancel = @{thm div_mult_mult1} RS trans
   33.30    val neg_exchanges = false
   33.31  )
   33.32 @@ -410,8 +410,8 @@
   33.33  (*Version for fields*)
   33.34  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   33.35   (open CancelNumeralFactorCommon
   33.36 -  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
   33.37 -  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
   33.38 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   33.39 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   33.40    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   33.41    val neg_exchanges = false
   33.42  )
   33.43 @@ -548,8 +548,8 @@
   33.44  (*for semirings with division*)
   33.45  structure DivCancelFactor = ExtractCommonTermFun
   33.46   (open CancelFactorCommon
   33.47 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   33.48 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
   33.49 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   33.50 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   33.51    fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
   33.52  );
   33.53  
   33.54 @@ -571,8 +571,8 @@
   33.55  (*Version for all fields, including unordered ones (type complex).*)
   33.56  structure DivideCancelFactor = ExtractCommonTermFun
   33.57   (open CancelFactorCommon
   33.58 -  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
   33.59 -  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
   33.60 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
   33.61 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
   33.62    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
   33.63  );
   33.64  
   33.65 @@ -620,13 +620,13 @@
   33.66      val (l,r) = Thm.dest_binop ct
   33.67      val T = Thm.ctyp_of_cterm l
   33.68    in (case (Thm.term_of l, Thm.term_of r) of
   33.69 -      (Const(@{const_name Fields.divide},_)$_$_, _) =>
   33.70 +      (Const(@{const_name Rings.divide},_)$_$_, _) =>
   33.71          let val (x,y) = Thm.dest_binop l val z = r
   33.72              val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   33.73              val ynz = prove_nz ctxt T y
   33.74          in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   33.75          end
   33.76 -     | (_, Const (@{const_name Fields.divide},_)$_$_) =>
   33.77 +     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
   33.78          let val (x,y) = Thm.dest_binop r val z = l
   33.79              val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   33.80              val ynz = prove_nz ctxt T y
   33.81 @@ -636,49 +636,49 @@
   33.82    end
   33.83    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   33.84  
   33.85 - fun is_number (Const(@{const_name Fields.divide},_)$a$b) = is_number a andalso is_number b
   33.86 + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
   33.87     | is_number t = can HOLogic.dest_number t
   33.88  
   33.89   val is_number = is_number o Thm.term_of
   33.90  
   33.91   fun proc3 phi ctxt ct =
   33.92    (case Thm.term_of ct of
   33.93 -    Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
   33.94 +    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   33.95        let
   33.96          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   33.97          val _ = map is_number [a,b,c]
   33.98          val T = Thm.ctyp_of_cterm c
   33.99          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
  33.100        in SOME (mk_meta_eq th) end
  33.101 -  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
  33.102 +  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
  33.103        let
  33.104          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
  33.105          val _ = map is_number [a,b,c]
  33.106          val T = Thm.ctyp_of_cterm c
  33.107          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
  33.108        in SOME (mk_meta_eq th) end
  33.109 -  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
  33.110 +  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
  33.111        let
  33.112          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
  33.113          val _ = map is_number [a,b,c]
  33.114          val T = Thm.ctyp_of_cterm c
  33.115          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
  33.116        in SOME (mk_meta_eq th) end
  33.117 -  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
  33.118 +  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
  33.119      let
  33.120        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
  33.121          val _ = map is_number [a,b,c]
  33.122          val T = Thm.ctyp_of_cterm c
  33.123          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
  33.124        in SOME (mk_meta_eq th) end
  33.125 -  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
  33.126 +  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
  33.127      let
  33.128        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
  33.129          val _ = map is_number [a,b,c]
  33.130          val T = Thm.ctyp_of_cterm c
  33.131          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
  33.132        in SOME (mk_meta_eq th) end
  33.133 -  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
  33.134 +  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
  33.135      let
  33.136        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
  33.137          val _ = map is_number [a,b,c]
    34.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Jun 01 18:59:21 2015 +0200
    34.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Jun 01 18:59:21 2015 +0200
    34.3 @@ -127,12 +127,12 @@
    34.4    let
    34.5      fun numeral_is_const ct =
    34.6        case Thm.term_of ct of
    34.7 -       Const (@{const_name Fields.divide},_) $ a $ b =>
    34.8 +       Const (@{const_name Rings.divide},_) $ a $ b =>
    34.9           can HOLogic.dest_number a andalso can HOLogic.dest_number b
   34.10       | Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t
   34.11       | t => can HOLogic.dest_number t
   34.12      fun dest_const ct = ((case Thm.term_of ct of
   34.13 -       Const (@{const_name Fields.divide},_) $ a $ b=>
   34.14 +       Const (@{const_name Rings.divide},_) $ a $ b=>
   34.15          Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   34.16       | Const (@{const_name Fields.inverse},_)$t => 
   34.17                     Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
    35.1 --- a/src/HOL/Word/Word.thy	Mon Jun 01 18:59:21 2015 +0200
    35.2 +++ b/src/HOL/Word/Word.thy	Mon Jun 01 18:59:21 2015 +0200
    35.3 @@ -307,7 +307,7 @@
    35.4    by (metis bintr_ariths(4))
    35.5  
    35.6  definition
    35.7 -  word_div_def: "a div b = word_of_int (uint a div uint b)"
    35.8 +  word_div_def: "divide a b = word_of_int (uint a div uint b)"
    35.9  
   35.10  definition
   35.11    word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
    36.1 --- a/src/HOL/ex/Dedekind_Real.thy	Mon Jun 01 18:59:21 2015 +0200
    36.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Mon Jun 01 18:59:21 2015 +0200
    36.3 @@ -102,7 +102,7 @@
    36.4    preal_inverse_def:
    36.5      "inverse R == Abs_preal (inverse_set (Rep_preal R))"
    36.6  
    36.7 -definition "R / S = R * inverse (S\<Colon>preal)"
    36.8 +definition "divide R S = R * inverse (S\<Colon>preal)"
    36.9  
   36.10  definition
   36.11    preal_one_def:
   36.12 @@ -1222,7 +1222,7 @@
   36.13    real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
   36.14  
   36.15  definition
   36.16 -  real_divide_def: "R / (S::real) = R * inverse S"
   36.17 +  real_divide_def: "divide R (S::real) = R * inverse S"
   36.18  
   36.19  definition
   36.20    real_le_def: "z \<le> (w::real) \<longleftrightarrow>