# HG changeset patch # User haftmann # Date 1474869414 -7200 # Node ID cdc1e59aa51378fbf210999cf7d546fe89faeac2 # Parent e7e41db7221ba16cb801fdbea2117630f19fa235 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div diff -r e7e41db7221b -r cdc1e59aa513 NEWS --- a/NEWS Mon Sep 26 07:56:54 2016 +0200 +++ b/NEWS Mon Sep 26 07:56:54 2016 +0200 @@ -240,6 +240,11 @@ *** HOL *** +* Type class "div" with operation "mod" renamed to type class "modulo" with +operation "modulo", analogously to type class "divide". This eliminates the +need to qualify any of those names in the presence of infix "mod" syntax. +INCOMPATIBILITY. + * The unique existence quantifier no longer provides 'binder' syntax, but uses syntax translations (as for bounded unique existence). Thus iterated quantification \!x y. P x y with its slightly confusing diff -r e7e41db7221b -r cdc1e59aa513 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/Doc/Main/Main_Doc.thy Mon Sep 26 07:56:54 2016 +0200 @@ -325,9 +325,9 @@ @{const divide} & @{typeof divide}\\ @{const abs} & @{typeof abs}\\ @{const sgn} & @{typeof sgn}\\ -@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\ -@{const Rings.divide} & @{typeof Rings.divide}\\ -@{const div_class.mod} & @{typeof "div_class.mod"}\\ +@{const Rings.dvd} & @{typeof Rings.dvd}\\ +@{const divide} & @{typeof divide}\\ +@{const modulo} & @{typeof modulo}\\ \end{supertabular} \subsubsection*{Syntax} diff -r e7e41db7221b -r cdc1e59aa513 src/Doc/Tutorial/Misc/appendix.thy --- a/src/Doc/Tutorial/Misc/appendix.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/Doc/Tutorial/Misc/appendix.thy Mon Sep 26 07:56:54 2016 +0200 @@ -16,7 +16,7 @@ @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\ @{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\ @{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\ -@{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\ +@{term [source] modulo} & @{typeof [show_sorts] "modulo"} & (infixl $mod$ 70) \\ @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\ @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\ @{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\ diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Code_Numeral.thy Mon Sep 26 07:56:54 2016 +0200 @@ -175,11 +175,11 @@ declare divide_integer.rep_eq [simp] -lift_definition mod_integer :: "integer \ integer \ integer" - is "Divides.mod :: int \ int \ int" +lift_definition modulo_integer :: "integer \ integer \ integer" + is "modulo :: int \ int \ int" . -declare mod_integer.rep_eq [simp] +declare modulo_integer.rep_eq [simp] lift_definition abs_integer :: "integer \ integer" is "abs :: int \ int" @@ -534,7 +534,7 @@ moreover have "2 * (j div 2) = j - j mod 2" by (simp add: zmult_div_cancel mult.commute) ultimately show ?thesis - by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le + by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1) (auto simp add: mult_2 [symmetric]) qed @@ -761,11 +761,11 @@ declare divide_natural.rep_eq [simp] -lift_definition mod_natural :: "natural \ natural \ natural" - is "Divides.mod :: nat \ nat \ nat" +lift_definition modulo_natural :: "natural \ natural \ natural" + is "modulo :: nat \ nat \ nat" . -declare mod_natural.rep_eq [simp] +declare modulo_natural.rep_eq [simp] lift_definition less_eq_natural :: "natural \ natural \ bool" is "less_eq :: nat \ nat \ bool" @@ -973,7 +973,7 @@ functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural" "plus :: natural \ _" "minus :: natural \ _" "times :: natural \ _" "divide :: natural \ _" - "Divides.mod :: natural \ _" + "modulo :: natural \ _" integer_of_natural natural_of_integer end diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Divides.thy Mon Sep 26 07:56:54 2016 +0200 @@ -11,13 +11,10 @@ subsection \Abstract division in commutative semirings.\ -class div = dvd + divide + - fixes mod :: "'a \ 'a \ 'a" (infixl "mod" 70) - -class semiring_div = semidom + div + +class semiring_div = semidom + modulo + assumes mod_div_equality: "a div b * b + a mod b = a" - and div_by_0 [simp]: "a div 0 = 0" - and div_0 [simp]: "0 div a = 0" + and div_by_0: "a div 0 = 0" + and div_0: "0 div a = 0" and div_mult_self1 [simp]: "b \ 0 \ (a + c * b) div b = c + a div b" and div_mult_mult1 [simp]: "c \ 0 \ (c * a) div (c * b) = a div b" begin @@ -27,8 +24,8 @@ fix b a assume "b \ 0" then show "a * b div b = a" - using div_mult_self1 [of b 0 a] by (simp add: ac_simps) -qed simp + using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0) +qed (simp add: div_by_0) lemma div_by_1: "a div 1 = a" @@ -42,7 +39,7 @@ "b \ 0 \ a * b div b = a" by (fact nonzero_mult_divide_cancel_right) -text \@{const divide} and @{const mod}\ +text \@{const divide} and @{const modulo}\ lemma mod_div_equality2: "b * (a div b) + a mod b = a" unfolding mult.commute [of b] @@ -836,7 +833,7 @@ begin text \ - We define @{const divide} and @{const mod} on @{typ nat} by means + We define @{const divide} and @{const modulo} on @{typ nat} by means of a characteristic relation with two input arguments @{term "m::nat"}, @{term "n::nat"} and two output arguments @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder). @@ -953,8 +950,8 @@ definition divide_nat where div_nat_def: "m div n = fst (Divides.divmod_nat m n)" -definition mod_nat where - "m mod n = snd (Divides.divmod_nat m n)" +definition modulo_nat where + mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)" lemma fst_divmod_nat [simp]: "fst (Divides.divmod_nat m n) = m div n" @@ -981,7 +978,7 @@ lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)" using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod) -text \The ''recursion'' equations for @{const divide} and @{const mod}\ +text \The ''recursion'' equations for @{const divide} and @{const modulo}\ lemma div_less [simp]: fixes m n :: nat @@ -1059,7 +1056,7 @@ let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))" by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq) -text \Simproc for cancelling @{const divide} and @{const mod}\ +text \Simproc for cancelling @{const divide} and @{const modulo}\ ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" @@ -1067,7 +1064,7 @@ structure Cancel_Div_Mod_Nat = Cancel_Div_Mod ( val div_name = @{const_name divide}; - val mod_name = @{const_name mod}; + val mod_name = @{const_name modulo}; val mk_binop = HOLogic.mk_binop; val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; @@ -1732,7 +1729,7 @@ apply (blast intro: unique_quotient) done -instantiation int :: Divides.div +instantiation int :: modulo begin definition divide_int @@ -1743,7 +1740,7 @@ if l dvd k then - int (nat \k\ div nat \l\) else - int (Suc (nat \k\ div nat \l\)))" -definition mod_int +definition modulo_int where "k mod l = (if l = 0 then k else if l dvd k then 0 else if k > 0 \ l > 0 \ k < 0 \ l < 0 then sgn l * int (nat \k\ mod nat \l\) @@ -1755,7 +1752,7 @@ lemma divmod_int_rel: "divmod_int_rel k l (k div l, k mod l)" - unfolding divmod_int_rel_def divide_int_def mod_int_def + unfolding divmod_int_rel_def divide_int_def modulo_int_def apply (cases k rule: int_cases3) apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps) apply (cases l rule: int_cases3) @@ -1849,15 +1846,15 @@ by (simp add: divide_int_def) lemma zmod_int: "int (a mod b) = int a mod int b" - by (simp add: mod_int_def int_dvd_iff) + by (simp add: modulo_int_def int_dvd_iff) text \Tool setup\ ML \ structure Cancel_Div_Mod_Int = Cancel_Div_Mod ( - val div_name = @{const_name Rings.divide}; - val mod_name = @{const_name mod}; + val div_name = @{const_name divide}; + val mod_name = @{const_name modulo}; val mk_binop = HOLogic.mk_binop; val mk_sum = Arith_Data.mk_sum HOLogic.intT; val dest_sum = Arith_Data.dest_sum; @@ -2223,7 +2220,7 @@ split_neg_lemma [of concl: "%x y. P y"]) done -text \Enable (lin)arith to deal with @{const divide} and @{const mod} +text \Enable (lin)arith to deal with @{const divide} and @{const modulo} when these are applied to some constant that is of the form @{term "numeral k"}:\ declare split_zdiv [of _ _ "numeral k", arith_split] for k @@ -2327,7 +2324,7 @@ by (simp add: divide_int_def) lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" -by (simp add: mod_int_def) +by (simp add: modulo_int_def) lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0" apply (subgoal_tac "a div b \ -1", force) @@ -2445,9 +2442,9 @@ "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)" proof - have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \ (0::int)" - using that by (simp only: snd_divmod mod_int_def) auto + using that by (simp only: snd_divmod modulo_int_def) auto then show ?thesis - by (auto simp add: split_def Let_def adjust_div_def divides_aux_def mod_int_def) + by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def) qed lemma numeral_div_minus_numeral [simp]: @@ -2463,9 +2460,9 @@ "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)" proof - have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \ (0::int)" - using that by (simp only: snd_divmod mod_int_def) auto + using that by (simp only: snd_divmod modulo_int_def) auto then show ?thesis - by (auto simp add: split_def Let_def adjust_div_def divides_aux_def mod_int_def) + by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def) qed lemma minus_one_div_numeral [simp]: diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Enum.thy Mon Sep 26 07:56:54 2016 +0200 @@ -580,7 +580,7 @@ instantiation finite_1 :: "{linordered_ring_strict, linordered_comm_semiring_strict, ordered_comm_ring, ordered_cancel_comm_monoid_diff, comm_monoid_mult, ordered_ring_abs, - one, Divides.div, sgn_if, inverse}" + one, modulo, sgn_if, inverse}" begin definition [simp]: "Groups.zero = a\<^sub>1" definition [simp]: "Groups.one = a\<^sub>1" @@ -698,7 +698,7 @@ instance by intro_classes (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def - inverse_finite_2_def divide_finite_2_def abs_finite_2_def mod_finite_2_def sgn_finite_2_def + inverse_finite_2_def divide_finite_2_def abs_finite_2_def modulo_finite_2_def sgn_finite_2_def split: finite_2.splits) end @@ -825,7 +825,7 @@ instance by intro_classes (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def - inverse_finite_3_def divide_finite_3_def abs_finite_3_def mod_finite_3_def sgn_finite_3_def + inverse_finite_3_def divide_finite_3_def abs_finite_3_def modulo_finite_3_def sgn_finite_3_def less_finite_3_def split: finite_3.splits) end diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Import/HOL_Light_Maps.thy --- a/src/HOL/Import/HOL_Light_Maps.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Import/HOL_Light_Maps.thy Mon Sep 26 07:56:54 2016 +0200 @@ -197,7 +197,7 @@ "fact (id 0) = id (bit1 0) \ (\n. fact (Suc n) = Suc n * fact n)" by simp -import_const_map MOD : mod +import_const_map MOD : modulo import_const_map DIV : divide lemma DIVISION_0: diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Library/Old_SMT/old_smt_normalize.ML --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Mon Sep 26 07:56:54 2016 +0200 @@ -430,7 +430,7 @@ @{const Suc}, @{const plus (nat)}, @{const minus (nat)}] val mult_nat_ops = - [@{const times (nat)}, @{const divide (nat)}, @{const mod (nat)}] + [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}] val nat_ops = simple_nat_ops @ mult_nat_ops diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Library/Old_SMT/old_z3_interface.ML --- a/src/HOL/Library/Old_SMT/old_z3_interface.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML Mon Sep 26 07:56:54 2016 +0200 @@ -42,7 +42,7 @@ end fun is_div_mod @{const divide (int)} = true - | is_div_mod @{const mod (int)} = true + | is_div_mod @{const modulo (int)} = true | is_div_mod _ = false val div_by_z3div = @{lemma diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Library/Polynomial.thy Mon Sep 26 07:56:54 2016 +0200 @@ -1894,8 +1894,8 @@ instantiation poly :: (field) ring_div begin -definition mod_poly where - "f mod g \ +definition modulo_poly where + mod_poly_def: "f mod g \ if g = 0 then f else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g" diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Mon Sep 26 07:56:54 2016 +0200 @@ -67,7 +67,7 @@ definition [simp]: "normalize_real = (normalize_field :: real \ _)" definition [simp]: "unit_factor_real = (unit_factor_field :: real \ _)" definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \ _)" -definition [simp]: "mod_real = (mod_field :: real \ _)" +definition [simp]: "modulo_real = (mod_field :: real \ _)" instance by standard (simp_all add: dvd_field_iff divide_simps) end @@ -94,7 +94,7 @@ definition [simp]: "normalize_rat = (normalize_field :: rat \ _)" definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \ _)" definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \ _)" -definition [simp]: "mod_rat = (mod_field :: rat \ _)" +definition [simp]: "modulo_rat = (mod_field :: rat \ _)" instance by standard (simp_all add: dvd_field_iff divide_simps) end @@ -121,7 +121,7 @@ definition [simp]: "normalize_complex = (normalize_field :: complex \ _)" definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \ _)" definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \ _)" -definition [simp]: "mod_complex = (mod_field :: complex \ _)" +definition [simp]: "modulo_complex = (mod_field :: complex \ _)" instance by standard (simp_all add: dvd_field_iff divide_simps) end diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Sep 26 07:56:54 2016 +0200 @@ -59,7 +59,7 @@ setup \Predicate_Compile_Data.ignore_consts [@{const_name Char}]\ setup \Predicate_Compile_Data.keep_functions [@{const_name Char}]\ -setup \Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}]\ +setup \Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name modulo}, @{const_name times}]\ section \Arithmetic operations\ diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 26 07:56:54 2016 +0200 @@ -283,12 +283,12 @@ (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}), (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}), (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}), - (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}), + (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}), (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}), (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}), (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}), (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}), - (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}), + (@{const_name "Rings.modulo"}, @{typ "prop => prop => prop"}), (@{const_name Rings.divide}, @{typ "prop => prop => prop"}), (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}), (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}), diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Nonstandard_Analysis/StarDef.thy --- a/src/HOL/Nonstandard_Analysis/StarDef.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Mon Sep 26 07:56:54 2016 +0200 @@ -527,7 +527,7 @@ instance star :: (Rings.dvd) Rings.dvd .. -instantiation star :: (Divides.div) Divides.div +instantiation star :: (modulo) modulo begin definition diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Rings.thy Mon Sep 26 07:56:54 2016 +0200 @@ -542,6 +542,8 @@ \<^item> \<^emph>\Algebra I\ by van der Waerden, Springer \ +text \Syntactic division operator\ + class divide = fixes divide :: "'a \ 'a \ 'a" (infixl "div" 70) @@ -569,6 +571,13 @@ setup \Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \ 'a \ 'a"})\ +text \Syntactic division remainder operator\ + +class modulo = dvd + divide + + fixes modulo :: "'a \ 'a \ 'a" (infixl "mod" 70) + +text \Algebraic classes with division\ + class semidom_divide = semidom + divide + assumes nonzero_mult_divide_cancel_right [simp]: "b \ 0 \ (a * b) div b = a" assumes divide_zero [simp]: "a div 0 = 0" diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/SMT_Examples/SMT_Examples.certs --- a/src/HOL/SMT_Examples/SMT_Examples.certs Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs Mon Sep 26 07:56:54 2016 +0200 @@ -6057,3 +6057,579 @@ (let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false)))) (mp (asserted $x32) @x42 false)))))))) +0b997744cf42fde45b98a34c933b0698332e657f 113 0 +unsat +((set-logic ) +(proof +(let ((?x228 (mod x$ 2))) +(let ((?x262 (* (- 1) ?x228))) +(let ((?x31 (modulo$ x$ 2))) +(let ((?x263 (+ ?x31 ?x262))) +(let (($x280 (>= ?x263 0))) +(let (($x264 (= ?x263 0))) +(let (($x205 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x136 (mod ?v0 ?v1))) +(let ((?x93 (* (- 1) ?v1))) +(let ((?x90 (* (- 1) ?v0))) +(let ((?x144 (mod ?x90 ?x93))) +(let ((?x150 (* (- 1) ?x144))) +(let (($x111 (<= ?v1 0))) +(let ((?x170 (ite $x111 ?x150 ?x136))) +(let (($x78 (= ?v1 0))) +(let ((?x175 (ite $x78 ?v0 ?x170))) +(let ((?x135 (modulo$ ?v0 ?v1))) +(= ?x135 ?x175))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!9)) +)) +(let (($x181 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x136 (mod ?v0 ?v1))) +(let ((?x93 (* (- 1) ?v1))) +(let ((?x90 (* (- 1) ?v0))) +(let ((?x144 (mod ?x90 ?x93))) +(let ((?x150 (* (- 1) ?x144))) +(let (($x111 (<= ?v1 0))) +(let ((?x170 (ite $x111 ?x150 ?x136))) +(let (($x78 (= ?v1 0))) +(let ((?x175 (ite $x78 ?v0 ?x170))) +(let ((?x135 (modulo$ ?v0 ?v1))) +(= ?x135 ?x175))))))))))) :qid k!9)) +)) +(let ((?x136 (mod ?1 ?0))) +(let ((?x93 (* (- 1) ?0))) +(let ((?x90 (* (- 1) ?1))) +(let ((?x144 (mod ?x90 ?x93))) +(let ((?x150 (* (- 1) ?x144))) +(let (($x111 (<= ?0 0))) +(let ((?x170 (ite $x111 ?x150 ?x136))) +(let (($x78 (= ?0 0))) +(let ((?x175 (ite $x78 ?1 ?x170))) +(let ((?x135 (modulo$ ?1 ?0))) +(let (($x178 (= ?x135 ?x175))) +(let (($x142 (forall ((?v0 Int) (?v1 Int) )(! (let (($x78 (= ?v1 0))) +(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1))))))) +(let ((?x135 (modulo$ ?v0 ?v1))) +(= ?x135 ?x140)))) :qid k!9)) +)) +(let (($x164 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x93 (* (- 1) ?v1))) +(let ((?x90 (* (- 1) ?v0))) +(let ((?x144 (mod ?x90 ?x93))) +(let ((?x150 (* (- 1) ?x144))) +(let ((?x136 (mod ?v0 ?v1))) +(let (($x79 (< 0 ?v1))) +(let ((?x155 (ite $x79 ?x136 ?x150))) +(let (($x78 (= ?v1 0))) +(let ((?x158 (ite $x78 ?v0 ?x155))) +(let ((?x135 (modulo$ ?v0 ?v1))) +(= ?x135 ?x158))))))))))) :qid k!9)) +)) +(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150))))) +(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170)))) +(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175)))) +(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178)))) +(let (($x79 (< 0 ?0))) +(let ((?x155 (ite $x79 ?x136 ?x150))) +(let ((?x158 (ite $x78 ?1 ?x155))) +(let (($x161 (= ?x135 ?x158))) +(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161))) +(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144)))) +(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150)))) +(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155)))) +(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158)))) +(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181)))) +(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181))) +(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205))) +(let (($x270 (or (not $x205) $x264))) +(let ((?x225 (* (- 1) 2))) +(let ((?x224 (* (- 1) x$))) +(let ((?x226 (mod ?x224 ?x225))) +(let ((?x227 (* (- 1) ?x226))) +(let (($x223 (<= 2 0))) +(let ((?x229 (ite $x223 ?x227 ?x228))) +(let (($x222 (= 2 0))) +(let ((?x230 (ite $x222 x$ ?x229))) +(let (($x231 (= ?x31 ?x230))) +(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2))))))) +(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228))))) +(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228)))) +(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228))))) +(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228))))) +(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270)))) +(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270)))) +(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270))) +(let ((@x332 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280))) +(let (($x305 (>= ?x228 0))) +(let (($x64 (>= ?x31 0))) +(let (($x67 (not $x64))) +(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1)))))) +(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67)))) +(let ((?x32 (* 2 ?x31))) +(let ((?x47 (+ 1 x$ ?x32))) +(let (($x52 (<= (+ 1 x$) ?x47))) +(let (($x55 (not $x52))) +(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0)))))) +(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32)))))) +(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47)))) +(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52)))) +(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67)))) +(let ((@x74 (mp (asserted $x36) @x73 $x67))) +((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x332 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +2e67f9e254b2a35a9d35027c6e63de01bc5086bd 112 0 +unsat +((set-logic ) +(proof +(let ((?x224 (mod x$ 2))) +(let (($x318 (>= ?x224 2))) +(let (($x319 (not $x318))) +(let ((?x258 (* (- 1) ?x224))) +(let ((?x29 (modulo$ x$ 2))) +(let ((?x259 (+ ?x29 ?x258))) +(let (($x275 (<= ?x259 0))) +(let (($x260 (= ?x259 0))) +(let (($x201 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x132 (mod ?v0 ?v1))) +(let ((?x89 (* (- 1) ?v1))) +(let ((?x86 (* (- 1) ?v0))) +(let ((?x140 (mod ?x86 ?x89))) +(let ((?x146 (* (- 1) ?x140))) +(let (($x107 (<= ?v1 0))) +(let ((?x166 (ite $x107 ?x146 ?x132))) +(let (($x74 (= ?v1 0))) +(let ((?x171 (ite $x74 ?v0 ?x166))) +(let ((?x131 (modulo$ ?v0 ?v1))) +(= ?x131 ?x171))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!9)) +)) +(let (($x177 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x132 (mod ?v0 ?v1))) +(let ((?x89 (* (- 1) ?v1))) +(let ((?x86 (* (- 1) ?v0))) +(let ((?x140 (mod ?x86 ?x89))) +(let ((?x146 (* (- 1) ?x140))) +(let (($x107 (<= ?v1 0))) +(let ((?x166 (ite $x107 ?x146 ?x132))) +(let (($x74 (= ?v1 0))) +(let ((?x171 (ite $x74 ?v0 ?x166))) +(let ((?x131 (modulo$ ?v0 ?v1))) +(= ?x131 ?x171))))))))))) :qid k!9)) +)) +(let ((?x132 (mod ?1 ?0))) +(let ((?x89 (* (- 1) ?0))) +(let ((?x86 (* (- 1) ?1))) +(let ((?x140 (mod ?x86 ?x89))) +(let ((?x146 (* (- 1) ?x140))) +(let (($x107 (<= ?0 0))) +(let ((?x166 (ite $x107 ?x146 ?x132))) +(let (($x74 (= ?0 0))) +(let ((?x171 (ite $x74 ?1 ?x166))) +(let ((?x131 (modulo$ ?1 ?0))) +(let (($x174 (= ?x131 ?x171))) +(let (($x138 (forall ((?v0 Int) (?v1 Int) )(! (let (($x74 (= ?v1 0))) +(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1))))))) +(let ((?x131 (modulo$ ?v0 ?v1))) +(= ?x131 ?x136)))) :qid k!9)) +)) +(let (($x160 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x89 (* (- 1) ?v1))) +(let ((?x86 (* (- 1) ?v0))) +(let ((?x140 (mod ?x86 ?x89))) +(let ((?x146 (* (- 1) ?x140))) +(let ((?x132 (mod ?v0 ?v1))) +(let (($x75 (< 0 ?v1))) +(let ((?x151 (ite $x75 ?x132 ?x146))) +(let (($x74 (= ?v1 0))) +(let ((?x154 (ite $x74 ?v0 ?x151))) +(let ((?x131 (modulo$ ?v0 ?v1))) +(= ?x131 ?x154))))))))))) :qid k!9)) +)) +(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146))))) +(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166)))) +(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171)))) +(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174)))) +(let (($x75 (< 0 ?0))) +(let ((?x151 (ite $x75 ?x132 ?x146))) +(let ((?x154 (ite $x74 ?1 ?x151))) +(let (($x157 (= ?x131 ?x154))) +(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157))) +(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140)))) +(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146)))) +(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151)))) +(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154)))) +(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177)))) +(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177))) +(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201))) +(let (($x266 (or (not $x201) $x260))) +(let ((?x221 (* (- 1) 2))) +(let ((?x220 (* (- 1) x$))) +(let ((?x222 (mod ?x220 ?x221))) +(let ((?x223 (* (- 1) ?x222))) +(let (($x219 (<= 2 0))) +(let ((?x225 (ite $x219 ?x223 ?x224))) +(let (($x218 (= 2 0))) +(let ((?x226 (ite $x218 x$ ?x225))) +(let (($x227 (= ?x29 ?x226))) +(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2))))))) +(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224))))) +(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224)))) +(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224))))) +(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224))))) +(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266)))) +(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266)))) +(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266))) +(let ((@x331 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275))) +(let (($x63 (>= ?x29 2))) +(let ((?x37 (* 2 ?x29))) +(let (($x56 (>= ?x37 3))) +(let (($x46 (< (+ x$ ?x37) (+ 3 x$)))) +(let (($x49 (not $x46))) +(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56)))))) +(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63)))) +(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37))))) +(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46)))) +(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49)))) +(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63)))) +(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63))) +((_ th-lemma arith farkas -1 1 1) @x70 @x331 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +b6d44e20599d4862894eecfa4c98fcb043a6336d 348 0 +unsat +((set-logic ) +(proof +(let ((?x96 (map$ uu$ xs$))) +(let ((?x97 (eval_dioph$ ks$ ?x96))) +(let ((?x424 (+ l$ ?x97))) +(let ((?x425 (mod ?x424 2))) +(let (($x482 (>= ?x425 2))) +(let (($x564 (not $x482))) +(let ((@x26 (true-axiom true))) +(let ((?x369 (* (- 1) l$))) +(let ((?x93 (eval_dioph$ ks$ xs$))) +(let ((?x678 (+ ?x93 ?x369))) +(let (($x679 (<= ?x678 0))) +(let (($x95 (= ?x93 l$))) +(let ((?x110 (* (- 1) ?x97))) +(let ((?x111 (+ l$ ?x110))) +(let ((?x114 (divide$ ?x111 2))) +(let ((?x101 (map$ uua$ xs$))) +(let ((?x102 (eval_dioph$ ks$ ?x101))) +(let (($x117 (= ?x102 ?x114))) +(let (($x282 (not $x117))) +(let ((?x99 (modulo$ l$ 2))) +(let ((?x98 (modulo$ ?x97 2))) +(let (($x100 (= ?x98 ?x99))) +(let (($x281 (not $x100))) +(let (($x283 (or $x281 $x282))) +(let (($x465 (>= ?x425 0))) +(let ((?x496 (* (- 2) ?x102))) +(let ((?x497 (+ ?x93 ?x110 ?x496))) +(let (($x504 (<= ?x497 0))) +(let (($x498 (= ?x497 0))) +(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1))) +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1)))))) +(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) ) :qid k!19)) +)) +(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1))) +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1)))))) +(= ?x83 0))) :qid k!19)) +)) +(let ((?x45 (eval_dioph$ ?1 ?0))) +(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0)))))) +(let (($x79 (= ?x83 0))) +(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1))) +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1)))) +(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48))) +(= ?x56 ?x45)))) :qid k!19)) +)) +(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1))) +(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1)))) +(let ((?x60 (* 2 ?x54))) +(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1)))) +(let ((?x66 (+ ?x48 ?x60))) +(= ?x66 ?x45)))))) :qid k!19)) +)) +(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0)))) +(let ((?x60 (* 2 ?x54))) +(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0)))) +(let ((?x66 (+ ?x48 ?x60))) +(let (($x71 (= ?x66 ?x45))) +(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48))))) +(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66)))) +(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74)))) +(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85)))) +(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85))) +(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304))) +(let (($x502 (or (not $x304) $x498))) +(let ((@x503 ((_ quant-inst ks$ xs$) $x502))) +(let ((@x795 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x498) $x504)) (unit-resolution @x503 @x309 $x498) $x504))) +(let (($x815 (not $x679))) +(let (($x680 (>= ?x678 0))) +(let ((?x592 (mod ?x97 2))) +(let ((?x619 (* (- 1) ?x592))) +(let ((?x511 (mod l$ 2))) +(let ((?x538 (* (- 1) ?x511))) +(let ((?x776 (* (- 1) ?x102))) +(let ((?x759 (+ l$ ?x98 ?x776 ?x538 (* (- 1) (div l$ 2)) ?x619 (* (- 1) (div ?x97 2))))) +(let (($x760 (>= ?x759 1))) +(let (($x747 (not $x760))) +(let ((?x674 (* (- 1) ?x99))) +(let ((?x675 (+ ?x98 ?x674))) +(let (($x676 (<= ?x675 0))) +(let (($x284 (not $x283))) +(let ((@x493 (hypothesis $x284))) +(let ((@x781 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x281 $x676)) (unit-resolution (def-axiom (or $x283 $x100)) @x493 $x100) $x676))) +(let ((?x670 (* (- 1) ?x114))) +(let ((?x671 (+ ?x102 ?x670))) +(let (($x673 (>= ?x671 0))) +(let ((@x787 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x673)) (unit-resolution (def-axiom (or $x283 $x117)) @x493 $x117) $x673))) +(let ((?x557 (div l$ 2))) +(let ((?x570 (* (- 2) ?x557))) +(let ((?x571 (+ l$ ?x538 ?x570))) +(let (($x576 (<= ?x571 0))) +(let (($x569 (= ?x571 0))) +(let ((@x568 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x569) $x576)) (unit-resolution ((_ th-lemma arith) (or false $x569)) @x26 $x569) $x576))) +(let ((?x620 (+ ?x98 ?x619))) +(let (($x635 (<= ?x620 0))) +(let (($x621 (= ?x620 0))) +(let (($x318 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x200 (mod ?v0 ?v1))) +(let ((?x157 (* (- 1) ?v1))) +(let ((?x154 (* (- 1) ?v0))) +(let ((?x208 (mod ?x154 ?x157))) +(let ((?x214 (* (- 1) ?x208))) +(let (($x175 (<= ?v1 0))) +(let ((?x234 (ite $x175 ?x214 ?x200))) +(let (($x143 (= ?v1 0))) +(let ((?x239 (ite $x143 ?v0 ?x234))) +(let ((?x199 (modulo$ ?v0 ?v1))) +(= ?x199 ?x239))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!22)) +)) +(let (($x245 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x200 (mod ?v0 ?v1))) +(let ((?x157 (* (- 1) ?v1))) +(let ((?x154 (* (- 1) ?v0))) +(let ((?x208 (mod ?x154 ?x157))) +(let ((?x214 (* (- 1) ?x208))) +(let (($x175 (<= ?v1 0))) +(let ((?x234 (ite $x175 ?x214 ?x200))) +(let (($x143 (= ?v1 0))) +(let ((?x239 (ite $x143 ?v0 ?x234))) +(let ((?x199 (modulo$ ?v0 ?v1))) +(= ?x199 ?x239))))))))))) :qid k!22)) +)) +(let ((?x200 (mod ?1 ?0))) +(let ((?x157 (* (- 1) ?0))) +(let ((?x154 (* (- 1) ?1))) +(let ((?x208 (mod ?x154 ?x157))) +(let ((?x214 (* (- 1) ?x208))) +(let (($x175 (<= ?0 0))) +(let ((?x234 (ite $x175 ?x214 ?x200))) +(let (($x143 (= ?0 0))) +(let ((?x239 (ite $x143 ?1 ?x234))) +(let ((?x199 (modulo$ ?1 ?0))) +(let (($x242 (= ?x199 ?x239))) +(let (($x206 (forall ((?v0 Int) (?v1 Int) )(! (let (($x143 (= ?v1 0))) +(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1))))))) +(let ((?x199 (modulo$ ?v0 ?v1))) +(= ?x199 ?x204)))) :qid k!22)) +)) +(let (($x228 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x157 (* (- 1) ?v1))) +(let ((?x154 (* (- 1) ?v0))) +(let ((?x208 (mod ?x154 ?x157))) +(let ((?x214 (* (- 1) ?x208))) +(let ((?x200 (mod ?v0 ?v1))) +(let (($x144 (< 0 ?v1))) +(let ((?x219 (ite $x144 ?x200 ?x214))) +(let (($x143 (= ?v1 0))) +(let ((?x222 (ite $x143 ?v0 ?x219))) +(let ((?x199 (modulo$ ?v0 ?v1))) +(= ?x199 ?x222))))))))))) :qid k!22)) +)) +(let ((@x233 (monotonicity (rewrite (= (< 0 ?0) (not $x175))) (= (ite (< 0 ?0) ?x200 ?x214) (ite (not $x175) ?x200 ?x214))))) +(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite (< 0 ?0) ?x200 ?x214) ?x234)))) +(let ((@x241 (monotonicity @x238 (= (ite $x143 ?1 (ite (< 0 ?0) ?x200 ?x214)) ?x239)))) +(let ((@x244 (monotonicity @x241 (= (= ?x199 (ite $x143 ?1 (ite (< 0 ?0) ?x200 ?x214))) $x242)))) +(let (($x144 (< 0 ?0))) +(let ((?x219 (ite $x144 ?x200 ?x214))) +(let ((?x222 (ite $x143 ?1 ?x219))) +(let (($x225 (= ?x199 ?x222))) +(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225))) +(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208)))) +(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214)))) +(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219)))) +(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222)))) +(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245)))) +(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245))) +(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318))) +(let (($x545 (not $x318))) +(let (($x626 (or $x545 $x621))) +(let ((?x359 (* (- 1) 2))) +(let ((?x590 (mod ?x110 ?x359))) +(let ((?x591 (* (- 1) ?x590))) +(let (($x357 (<= 2 0))) +(let ((?x593 (ite $x357 ?x591 ?x592))) +(let (($x356 (= 2 0))) +(let ((?x594 (ite $x356 ?x97 ?x593))) +(let (($x595 (= ?x98 ?x594))) +(let ((@x601 (monotonicity (monotonicity (rewrite (= ?x359 (- 2))) (= ?x590 (mod ?x110 (- 2)))) (= ?x591 (* (- 1) (mod ?x110 (- 2))))))) +(let ((@x368 (rewrite (= $x357 false)))) +(let ((@x604 (monotonicity @x368 @x601 (= ?x593 (ite false (* (- 1) (mod ?x110 (- 2))) ?x592))))) +(let ((@x608 (trans @x604 (rewrite (= (ite false (* (- 1) (mod ?x110 (- 2))) ?x592) ?x592)) (= ?x593 ?x592)))) +(let ((@x366 (rewrite (= $x356 false)))) +(let ((@x615 (trans (monotonicity @x366 @x608 (= ?x594 (ite false ?x97 ?x592))) (rewrite (= (ite false ?x97 ?x592) ?x592)) (= ?x594 ?x592)))) +(let ((@x625 (trans (monotonicity @x615 (= $x595 (= ?x98 ?x592))) (rewrite (= (= ?x98 ?x592) $x621)) (= $x595 $x621)))) +(let ((@x633 (trans (monotonicity @x625 (= (or $x545 $x595) $x626)) (rewrite (= $x626 $x626)) (= (or $x545 $x595) $x626)))) +(let ((@x634 (mp ((_ quant-inst (eval_dioph$ ks$ ?x96) 2) (or $x545 $x595)) @x633 $x626))) +(let ((@x431 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x621) $x635)) (unit-resolution @x634 @x323 $x621) $x635))) +(let ((?x637 (div ?x97 2))) +(let ((?x650 (* (- 2) ?x637))) +(let ((?x651 (+ ?x97 ?x619 ?x650))) +(let (($x656 (<= ?x651 0))) +(let (($x649 (= ?x651 0))) +(let ((@x661 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x649) $x656)) (unit-resolution ((_ th-lemma arith) (or false $x649)) @x26 $x649) $x656))) +(let ((?x539 (+ ?x99 ?x538))) +(let (($x555 (<= ?x539 0))) +(let (($x540 (= ?x539 0))) +(let (($x546 (or $x545 $x540))) +(let ((?x506 (mod ?x369 ?x359))) +(let ((?x507 (* (- 1) ?x506))) +(let ((?x512 (ite $x357 ?x507 ?x511))) +(let ((?x513 (ite $x356 l$ ?x512))) +(let (($x514 (= ?x99 ?x513))) +(let ((@x520 (monotonicity (monotonicity (rewrite (= ?x359 (- 2))) (= ?x506 (mod ?x369 (- 2)))) (= ?x507 (* (- 1) (mod ?x369 (- 2))))))) +(let ((@x523 (monotonicity @x368 @x520 (= ?x512 (ite false (* (- 1) (mod ?x369 (- 2))) ?x511))))) +(let ((@x527 (trans @x523 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x511) ?x511)) (= ?x512 ?x511)))) +(let ((@x534 (trans (monotonicity @x366 @x527 (= ?x513 (ite false l$ ?x511))) (rewrite (= (ite false l$ ?x511) ?x511)) (= ?x513 ?x511)))) +(let ((@x544 (trans (monotonicity @x534 (= $x514 (= ?x99 ?x511))) (rewrite (= (= ?x99 ?x511) $x540)) (= $x514 $x540)))) +(let ((@x553 (trans (monotonicity @x544 (= (or $x545 $x514) $x546)) (rewrite (= $x546 $x546)) (= (or $x545 $x514) $x546)))) +(let ((@x554 (mp ((_ quant-inst l$ 2) (or $x545 $x514)) @x553 $x546))) +(let ((@x668 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x540) $x555)) (unit-resolution @x554 @x323 $x540) $x555))) +(let ((?x361 (div ?x111 2))) +(let ((?x395 (* (- 1) ?x361))) +(let ((?x396 (+ ?x114 ?x395))) +(let (($x414 (>= ?x396 0))) +(let (($x397 (= ?x396 0))) +(let (($x311 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x145 (div ?v0 ?v1))) +(let ((?x157 (* (- 1) ?v1))) +(let ((?x154 (* (- 1) ?v0))) +(let ((?x160 (div ?x154 ?x157))) +(let (($x175 (<= ?v1 0))) +(let ((?x182 (ite $x175 ?x160 ?x145))) +(let (($x143 (= ?v1 0))) +(let ((?x141 (divide$ ?v0 ?v1))) +(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) ) :qid k!21)) +)) +(let (($x193 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x145 (div ?v0 ?v1))) +(let ((?x157 (* (- 1) ?v1))) +(let ((?x154 (* (- 1) ?v0))) +(let ((?x160 (div ?x154 ?x157))) +(let (($x175 (<= ?v1 0))) +(let ((?x182 (ite $x175 ?x160 ?x145))) +(let (($x143 (= ?v1 0))) +(let ((?x141 (divide$ ?v0 ?v1))) +(= ?x141 (ite $x143 0 ?x182)))))))))) :qid k!21)) +)) +(let ((?x141 (divide$ ?1 ?0))) +(let (($x190 (= ?x141 (ite $x143 0 (ite $x175 (div ?x154 ?x157) (div ?1 ?0)))))) +(let (($x152 (forall ((?v0 Int) (?v1 Int) )(! (let (($x143 (= ?v1 0))) +(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1)))))) +(let ((?x141 (divide$ ?v0 ?v1))) +(= ?x141 ?x150)))) :qid k!21)) +)) +(let (($x172 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x157 (* (- 1) ?v1))) +(let ((?x154 (* (- 1) ?v0))) +(let ((?x160 (div ?x154 ?x157))) +(let ((?x145 (div ?v0 ?v1))) +(let (($x144 (< 0 ?v1))) +(let ((?x163 (ite $x144 ?x145 ?x160))) +(let (($x143 (= ?v1 0))) +(let ((?x166 (ite $x143 0 ?x163))) +(let ((?x141 (divide$ ?v0 ?v1))) +(= ?x141 ?x166)))))))))) :qid k!21)) +)) +(let ((?x160 (div ?x154 ?x157))) +(let ((?x145 (div ?1 ?0))) +(let ((?x163 (ite $x144 ?x145 ?x160))) +(let ((?x166 (ite $x143 0 ?x163))) +(let (($x169 (= ?x141 ?x166))) +(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160))))) +(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) (ite $x175 ?x160 ?x145))) (= ?x163 (ite $x175 ?x160 ?x145))))) +(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 (ite $x175 ?x160 ?x145)))) (= $x169 $x190)))) +(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169))) +(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160)))) +(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166)))) +(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193)))) +(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193))) +(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311))) +(let (($x403 (or (not $x311) $x397))) +(let ((?x358 (* (- 1) ?x111))) +(let ((?x360 (div ?x358 ?x359))) +(let ((?x362 (ite $x357 ?x360 ?x361))) +(let ((?x363 (ite $x356 0 ?x362))) +(let (($x364 (= ?x114 ?x363))) +(let ((@x374 (rewrite (= ?x359 (- 2))))) +(let ((@x377 (monotonicity (rewrite (= ?x358 (+ ?x369 ?x97))) @x374 (= ?x360 (div (+ ?x369 ?x97) (- 2)))))) +(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361))))) +(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361)))) +(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361)))) +(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397)))) +(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403)))) +(let ((@x411 (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403))) +(let ((@x485 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x414)) (unit-resolution @x411 @x316 $x397) $x414))) +(let ((?x436 (* (- 1) ?x425))) +(let ((?x435 (* (- 2) ?x361))) +(let ((?x437 (+ l$ ?x110 ?x435 ?x436))) +(let (($x442 (<= ?x437 0))) +(let (($x434 (= ?x437 0))) +(let ((@x745 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x442)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x442))) +(let ((@x746 ((_ th-lemma arith farkas 1 -2 -2 -2 1 1 1 1 1 1) @x745 @x485 (hypothesis $x673) (hypothesis $x760) (hypothesis $x676) @x668 @x661 @x431 @x568 (unit-resolution ((_ th-lemma arith) (or false $x564)) @x26 $x564) false))) +(let ((@x788 (unit-resolution (lemma @x746 (or $x747 (not $x673) (not $x676))) @x787 @x781 $x747))) +(let (($x677 (>= ?x675 0))) +(let ((@x812 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x281 $x677)) (unit-resolution (def-axiom (or $x283 $x100)) @x493 $x100) $x677))) +(let (($x577 (>= ?x571 0))) +(let ((@x778 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x569) $x577)) (unit-resolution ((_ th-lemma arith) (or false $x569)) @x26 $x569) $x577))) +(let (($x556 (>= ?x539 0))) +(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x540) $x556)) (unit-resolution @x554 @x323 $x540) $x556))) +(let (($x636 (>= ?x620 0))) +(let ((@x652 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x621) $x636)) (unit-resolution @x634 @x323 $x621) $x636))) +(let (($x505 (>= ?x497 0))) +(let ((@x488 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x498) $x505)) (unit-resolution @x503 @x309 $x498) $x505))) +(let (($x657 (>= ?x651 0))) +(let ((@x581 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x649) $x657)) (unit-resolution ((_ th-lemma arith) (or false $x649)) @x26 $x649) $x657))) +(let ((@x582 ((_ th-lemma arith farkas -1/2 -1/2 -1/2 1/2 -1/2 -1/2 -1/2 1) @x581 (hypothesis $x677) @x488 (hypothesis (not $x680)) @x652 @x645 @x778 (hypothesis $x747) false))) +(let ((@x813 (unit-resolution (lemma @x582 (or $x680 (not $x677) $x760)) @x812 @x788 $x680))) +(let (($x134 (not $x95))) +(let (($x290 (= $x95 $x283))) +(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284))))) +(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290)))) +(let (($x120 (and $x100 $x117))) +(let (($x135 (= $x134 $x120))) +(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2)))))) +(let (($x108 (not $x107))) +(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114)))) +(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120)))) +(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120))))) +(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135)))) +(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290))) +(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283)))) +(let ((@x819 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 $x815 (not $x680))) (unit-resolution @x344 @x493 $x134) (or $x815 (not $x680))))) +(let (($x672 (<= ?x671 0))) +(let ((@x823 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x672)) (unit-resolution (def-axiom (or $x283 $x117)) @x493 $x117) $x672))) +(let (($x413 (<= ?x396 0))) +(let ((@x802 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) (unit-resolution @x411 @x316 $x397) $x413))) +(let (($x443 (>= ?x437 0))) +(let ((@x826 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443))) +(let ((@x827 ((_ th-lemma arith farkas 1 -2 -2 1 -1 1) @x826 @x802 @x823 (unit-resolution @x819 @x813 $x815) @x795 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) false))) +(let ((@x828 (lemma @x827 $x283))) +(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284)))) +(let ((@x584 (unit-resolution @x340 @x828 $x95))) +(let (($x807 (not $x672))) +(let ((@x888 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x673 (not $x413) (not $x465) (not $x443) (not $x504) (not $x680))))) +(let ((@x889 (unit-resolution @x888 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x680)) @x584 $x680) @x802 @x826 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x795 $x673))) +(let ((@x728 (monotonicity (symm @x584 (= l$ ?x93)) (= ?x99 (modulo$ ?x93 2))))) +(let ((?x499 (modulo$ ?x93 2))) +(let (($x500 (= ?x499 ?x98))) +(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (= (modulo$ (eval_dioph$ ?v0 ?v1) 2) (modulo$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :qid k!18)) +)) +(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (= (modulo$ (eval_dioph$ ?v0 ?v1) 2) (modulo$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :qid k!18)) +)) +(let (($x50 (= (modulo$ ?x45 2) (modulo$ ?x48 2)))) +(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51))) +(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297))) +(let (($x464 (or (not $x297) $x500))) +(let ((@x578 ((_ quant-inst ks$ xs$) $x464))) +(let ((@x748 (trans (symm (unit-resolution @x578 @x302 $x500) (= ?x98 ?x499)) (symm @x728 (= ?x499 ?x99)) $x100))) +(let ((@x891 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x828 $x283) (lemma (unit-resolution (hypothesis $x281) @x748 false) $x100) $x282))) +(let ((@x895 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x807 (not $x673))) @x891 (or $x807 (not $x673))))) +((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x895 @x889 $x807) @x485 @x745 @x488 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x679)) @x584 $x679) (unit-resolution ((_ th-lemma arith) (or false $x564)) @x26 $x564) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 26 07:56:54 2016 +0200 @@ -441,7 +441,7 @@ | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv} (fst (tm_of vs e), fst (tm_of vs e')), integerN) - | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod} + | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name modulo} (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("-", [e])) = diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/String.thy --- a/src/HOL/String.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/String.thy Mon Sep 26 07:56:54 2016 +0200 @@ -147,7 +147,7 @@ lemma integer_of_char_Char [simp]: "integer_of_char (Char k) = numeral k mod 256" by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def - id_apply zmod_int mod_integer.abs_eq [symmetric]) simp + id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp lemma less_256_integer_of_char_Char: assumes "numeral k < (256 :: integer)" diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Mon Sep 26 07:56:54 2016 +0200 @@ -757,7 +757,7 @@ | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r - | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r + | Const(@{const_name Rings.modulo},_)$l$r => isnum l andalso isnum r | Const(@{const_name Rings.divide},_)$l$r => isnum l andalso isnum r | _ => is_number t orelse can HOLogic.dest_nat t diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Tools/SMT/z3_interface.ML --- a/src/HOL/Tools/SMT/z3_interface.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Tools/SMT/z3_interface.ML Mon Sep 26 07:56:54 2016 +0200 @@ -35,7 +35,7 @@ serialize = #serialize (SMTLIB_Interface.translate_config ctxt)} fun is_div_mod @{const divide (int)} = true - | is_div_mod @{const mod (int)} = true + | is_div_mod @{const modulo (int)} = true | is_div_mod _ = false val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of) diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Tools/lin_arith.ML Mon Sep 26 07:56:54 2016 +0200 @@ -299,7 +299,7 @@ @{const_name Groups.abs}, @{const_name Groups.minus}, "Int.nat" (*DYNAMIC BINDING!*), - "Divides.div_class.mod" (*DYNAMIC BINDING!*), + @{const_name Rings.modulo}, @{const_name Rings.divide}] a | _ => (if Context_Position.is_visible ctxt then @@ -467,7 +467,7 @@ (* ?P ((?n::nat) mod (numeral ?k)) = ((numeral ?k = 0 --> ?P ?n) & (~ (numeral ?k = 0) --> (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P j))) *) - | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), (*DYNAMIC BINDING!*) [t1, t2]) => + | (Const (@{const_name Rings.modulo}, Type ("fun", [@{typ nat}, _])), [t1, t2]) => let val rev_terms = rev terms val zero = Const (@{const_name Groups.zero}, split_type) @@ -536,7 +536,7 @@ (numeral ?k < 0 --> (ALL i j. numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P j))) *) - | (Const ("Divides.div_class.mod", + | (Const (@{const_name Rings.modulo}, Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) => let val rev_terms = rev terms diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Mon Sep 26 07:56:54 2016 +0200 @@ -551,8 +551,8 @@ structure ModCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} - val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} dummyT + val mk_bal = HOLogic.mk_binop @{const_name modulo} + val dest_bal = HOLogic.dest_bin @{const_name modulo} dummyT fun simp_conv _ _ = SOME @{thm mod_mult_mult1} ); diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Word/Word.thy Mon Sep 26 07:56:54 2016 +0200 @@ -287,7 +287,7 @@ lift_definition word_pred :: "'a::len0 word \ 'a word" is "\x. x - 1" by (metis bintr_ariths(7)) -instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}" +instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}" begin lift_definition zero_word :: "'a word" is "0" . diff -r e7e41db7221b -r cdc1e59aa513 src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/ex/Arith_Examples.thy Mon Sep 26 07:56:54 2016 +0200 @@ -30,7 +30,7 @@ subsection \Splitting of Operators: @{term max}, @{term min}, @{term abs}, - @{term minus}, @{term nat}, @{term Divides.mod}, + @{term minus}, @{term nat}, @{term modulo}, @{term divide}\ lemma "(i::nat) <= max i j"