|
(tmod
(ml3 0
(ml3-1 nil 3406631585
("" (skosimp*)
(("" (expand "abs")
(("" (lift-if)
(("" (case-replace "floor(i!1 / m!1) = i!1/m!1")
(("1" (auto-rewrite-theory "real_props")
(("1" (ground) nil nil)) nil)
("2" (ground)
(("1" (lemma "both_sides_times_pos_lt1")
(("1" (inst -1 "m!1" "floor(i!1 / m!1)" "i!1 / m!1")
(("1" (flatten) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (typepred "floor(i!1 / m!1)")
(("2" (lemma "both_sides_times_pos_lt1")
(("2"
(inst -1 "m!1" "i!1 / m!1" " 1 + floor(i!1 / m!1)")
(("2" (flatten)
(("2" (hide -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(integer nonempty-type-from-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(zero_not_lt_zero formula-decl nil real_props nil)
(div_cancel1 formula-decl nil real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(minus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil))
nil))
(ml4 0
(ml4-1 nil 3406631585
("" (skosimp*)
(("" (expand "abs")
(("" (lift-if)
(("" (ground)
(("1" (typepred "floor(-i!1 / m!1)")
(("1" (lemma "both_sides_times_pos_lt1")
(("1"
(inst -1 "m!1" "-i!1 / m!1" "1 + floor(-i!1 / m!1)")
(("1" (flatten)
(("1" (hide -1) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (lemma "both_sides_times_pos_lt1")
(("2" (inst -1 "m!1" "floor(-i!1 / m!1)" "-i!1 / m!1")
(("2" (assert)
(("2" (case-replace "floor(-i!1 / m!1) = -i!1/m!1")
(("1" (assert)
(("1" (auto-rewrite-theory "real_props")
(("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(<= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(integer nonempty-type-from-decl nil integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(minus_int_is_int application-judgement "int" integers nil))
nil))
(mod_TCC1 0
(mod_TCC1-1 nil 3406631585
("" (skosimp*)
(("" (expand "tdiv")
(("" (case "j!1 >= 0")
(("1" (lemma "ml3")
(("1" (inst?)
(("1" (expand "abs")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
("2" (assert) nil nil))
nil))
nil)
("2" (lemma "ml4")
(("2" (inst -1 "i!1" "-j!1")
(("1" (expand "abs")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv nil)
(ml4 formula-decl nil tmod nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(ml3 formula-decl nil tmod nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(minus_int_is_int application-judgement "int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(j!1 skolem-const-decl "nonzero_integer" tmod nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil))
nil))
(mod_even 0
(mod_even-1 nil 3406631585
("" (skosimp*)
(("" (expand "mod")
(("" (expand "tdiv")
(("" (rewrite "floor_int")
(("1" (assert) nil nil)
("2" (expand "integer?") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(floor_int formula-decl nil floor_ceil nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(integer nonempty-type-from-decl nil integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(int nonempty-type-eq-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(integer? const-decl "bool" integers nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(mod_neg 0
(mod_neg-1 nil 3406631585
("" (auto-rewrite-theory "integers")
(("" (skosimp*)
(("" (lift-if)
(("" (expand "mod")
(("" (expand "tdiv")
(("" (case "-i!1/j!1 = -(i!1/j!1)")
(("1" (replace -1)
(("1" (hide -1)
(("1" (ground)
(("1" (rewrite "floor_int")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(minus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(closed_neg formula-decl nil integers nil)
(integer nonempty-type-from-decl nil integers nil)
(floor_int formula-decl nil floor_ceil nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(integer? const-decl "bool" integers nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(mod_neg_d 0
(mod_neg_d-1 nil 3406631585
("" (auto-rewrite-theory "integers")
(("" (skosimp*)
(("" (lift-if)
(("" (expand "mod")
(("" (expand "tdiv")
(("" (case "i!1/-j!1=-(i!1/j!1)")
(("1" (replace -1)
(("1" (hide -1)
(("1" (rewrite "floor_neg")
(("1" (lift-if)
(("1" (ground)
(("1" (rewrite "floor_int")
(("1" (assert) nil nil)) nil)
("2" (case "integer_pred(--(i!1/j!1))")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("3" (lift-if)
(("3" (ground)
(("3" (hide 1)
(("3"
(lemma "integers.closed_neg")
(("3"
(inst - "-(i!1/j!1)")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_nzint_is_nzint application-judgement "nzint" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(integer nonempty-type-from-decl nil integers nil)
(floor_int formula-decl nil floor_ceil nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(closed_neg formula-decl nil integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(integer? const-decl "bool" integers nil)
(floor_neg formula-decl nil floor_ceil nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(mod_eq_arg 0
(mod_eq_arg-1 nil 3406631585 ("" (tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(tdiv const-decl "integer" tdiv nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(mod_lt 0
(mod_lt-1 nil 3406631585
("" (skosimp*)
(("" (lift-if)
(("" (expand "mod")
(("" (expand "abs")
(("" (expand "sgn")
(("" (grind)
(("1" (rewrite "floor_small")
(("1" (lift-if)
(("1" (ground) (("1" (rewrite "pos_div_ge") nil nil))
nil))
nil))
nil)
("2" (rewrite "floor_small")
(("2" (lift-if)
(("2" (ground) (("2" (rewrite "pos_div_ge") nil nil))
nil))
nil))
nil)
("3" (rewrite "floor_small")
(("3" (lift-if)
(("3" (ground) (("3" (rewrite "pos_div_ge") nil nil))
nil))
nil))
nil)
("4" (rewrite "floor_small")
(("4" (lift-if)
(("4" (ground) (("4" (rewrite "pos_div_ge") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(tdiv const-decl "integer" tdiv nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(pos_div_ge formula-decl nil real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(floor_small formula-decl nil floor_ceil nil)
(sgn const-decl "int" tdiv nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil))
nil))
(mod_lt_nat 0
(mod_lt_nat-1 nil 3406631585
("" (skosimp*)
(("" (rewrite "mod_lt")
(("1" (expand "sgn") (("1" (propax) nil nil)) nil)
("2" (expand "abs") (("2" (propax) nil nil)) nil))
nil))
nil)
((mod_lt formula-decl nil tmod nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sgn const-decl "int" tdiv nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil))
nil))
(mod_sum_pos 0
(mod_sum_pos-1 nil 3406631585
("" (skosimp*)
(("" (expand "mod")
(("" (expand "tdiv")
(("" (lemma "floor_plus_int")
(("" (inst - "k!1*m!1/m!1" "i!1/m!1")
(("" (replace -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(floor_plus_int formula-decl nil floor_ceil nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(tdiv const-decl "integer" tdiv nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(mod_sum 0
(mod_sum-1 nil 3406631585
("" (skosimp*)
(("" (expand "mod")
(("" (expand "tdiv")
(("" (lemma "floor_plus_int")
(("" (inst - "k!1*j!1/j!1" "i!1/j!1")
(("" (replace -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(floor_plus_int formula-decl nil floor_ceil nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(tdiv const-decl "integer" tdiv nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(mod_it_is 0
(mod_it_is-1 nil 3406631585
("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (lemma "mod_sum")
(("" (inst - "b!1" "m!1" "c!1")
(("" (replace -1)
(("" (hide -1)
(("" (rewrite "mod_lt")
(("1" (lift-if)
(("1" (expand "sgn") (("1" (propax) nil nil)) nil))
nil)
("2" (expand "abs") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((mod_sum formula-decl nil tmod nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mod_lt formula-decl nil tmod nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sgn const-decl "int" tdiv nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(mod_zero 0
(mod_zero-1 nil 3406631585 ("" (tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(tdiv const-decl "integer" tdiv nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(mod_0 0
(mod_0-1 nil 3406631761
("" (skosimp*) (("" (rewrite "mod_zero") nil nil)) nil)
((mod_zero formula-decl nil tmod nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil))
shostak))
(mod_one 0
(mod_one-1 nil 3406631585
("" (grind)
(("1" (rewrite "floor_small")
(("1" (lift-if)
(("1" (ground) (("1" (rewrite "pos_div_ge") nil nil)) nil))
nil))
nil)
("2" (rewrite "floor_small")
(("2" (lift-if)
(("2" (ground) (("2" (rewrite "pos_div_ge") nil nil)) nil))
nil))
nil))
nil)
((integer nonempty-type-from-decl nil integers nil)
(floor_small formula-decl nil floor_ceil nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(pos_div_ge formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(mod_of_mod 0
(mod_of_mod-1 nil 3406631585
("" (skosimp*)
(("" (rewrite "mod")
(("" (expand "tdiv")
(("" (lemma "mod_sum")
(("" (inst - "i!1+k!1" "m!1" "-floor(k!1/m!1)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mod_sum formula-decl nil tmod nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(integer nonempty-type-from-decl nil integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(minus_int_is_int application-judgement "int" integers nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(mod_pos 0
(mod_pos-1 nil 3406631585
("" (skosimp*)
(("" (typepred "mod(i!1,m!1)")
(("" (tcc)
(("" (lemma "both_sides_times_pos_le1")
(("" (inst -1 "m!1" "floor(i!1 / m!1)" "i!1/m!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(integer nonempty-type-from-decl nil integers nil)
(<= const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(minus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(mod_TCC2 0
(mod_TCC2-1 nil 3406631585
("" (skosimp*)
(("" (assert) (("" (rewrite "mod_pos") nil nil)) nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(mod_pos formula-decl nil tmod nil))
nil))
(mod_to_rem 0
(mod_to_rem-1 nil 3406631585
("" (skosimp*)
(("" (assert)
(("" (expand "mod")
(("" (lemma "rem_def2")
(("" (inst?)
(("" (inst -1 "i!1 - m!1 * floor(i!1 / m!1)")
(("1" (expand "tdiv")
(("1" (assert)
(("1" (hide 2)
(("1" (expand "divides") (("1" (inst?) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (assert)
(("2" (lemma "mod_pos")
(("2" (expand "mod")
(("2" (inst?)
(("2" (expand "tdiv") (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nil application-judgement "below(m)" tmod nil)
(rem_def2 formula-decl nil modulo_arithmetic nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(integer nonempty-type-from-decl nil integers nil)
(m!1 skolem-const-decl "posnat" tmod nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(i!1 skolem-const-decl "int" tmod nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(mod nonempty-type-eq-decl nil euclidean_division nil)
(divides const-decl "bool" divides nil)
(tdiv const-decl "integer" tdiv nil)
(mod_pos formula-decl nil tmod nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil))
nil))
(mod_0_divides 0
(mod_0_divides-1 nil 3406631585
("" (skosimp*)
(("" (prop)
(("1" (expand "mod")
(("1" (expand "divides")
(("1" (inst + "tdiv(i!1,j!1)") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "divides")
(("2" (skosimp*)
(("2" (replace -1) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((divides const-decl "bool" divides nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(tdiv const-decl "integer" tdiv nil)
(integer nonempty-type-from-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
nil)))
¤ Dauer der Verarbeitung: 0.41 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
