|
(rem (ml1 0
(ml1-1 nil 3249307029
("" (skolem!)
(("" (expand "div")
(("" (expand "sgn")
(("" (expand "abs")
(("" (assert)
(("" (lemma "both_sides_times_pos_lt1")
(("" (inst - "m!1" "n!1/m!1" "floor(n!1/m!1)+1")
(("" (flatten)
(("" (ground)
(("" (typepred "floor(n!1 / m!1)")
(("" (propax) nil))))))))))))))))))))
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)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(div const-decl "integer" div nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(posint_times_posint_is_posint application-judgement "posint"
integers 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 -> numfield]" number_fields
nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(sgn const-decl "int" real_defs nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
nil))
(ml3 0
(ml3-1 nil 3249307029
("" (skosimp*)
(("" (case "i!1 >= 0")
(("1" (expand "abs")
(("1" (lift-if)
(("1" (split 1)
(("1" (flatten)
(("1" (lemma "div_smaller")
(("1" (inst?) (("1" (assert) nil)))))))
("2" (flatten)
(("2" (lemma "ml1") (("2" (inst?) nil)))))))))))
("2" (expand "abs")
(("2" (lift-if)
(("2" (lemma "div_neg")
(("2" (inst?)
(("2" (split 2)
(("1" (flatten)
(("1" (lemma "ml1")
(("1" (inst -1 "m!1" "-i!1")
(("1" (assert) nil) ("2" (assert) nil)))))))
("2" (flatten)
(("2" (lemma "div_smaller")
(("2" (inst -1 "m!1" "-i!1")
(("1" (assert) nil)
("2" (assert) nil))))))))))))))))))))
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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(ml1 formula-decl nil rem nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(i!1 skolem-const-decl "int" rem nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_smaller formula-decl nil div nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil)
(div_nat formula-decl nil div nil)
(div_neg formula-decl nil div 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))
(rem_TCC1 0
(rem_TCC1-1 nil 3249307029
("" (skosimp*)
(("" (lemma "ml3")
(("" (case "j!1 >= 0")
(("1" (inst?)
(("1" (expand "abs" 1 2) (("1" (assert) nil)))
("2" (assert) nil)))
("2" (inst -1 "i!1" "-j!1")
(("1" (lemma "div_neg_d")
(("1" (inst?)
(("1" (replace -1)
(("1" (expand "abs" 2 2)
(("1" (assert) nil)))))))))
("2" (assert) nil))))))))
nil)
((ml3 formula-decl nil rem nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(minus_int_is_int application-judgement "int" integers nil)
(div_neg_d formula-decl nil div nil)
(real_gt_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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(j!1 skolem-const-decl "nonzero_integer" rem nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(minus_nzint_is_nzint application-judgement "nzint" 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(abs_nat_rew formula-decl nil abs_rews 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))
(rem_neg 0
(rem_neg-1 nil 3249307029
("" (skosimp*)
(("" (expand "rem")
(("" (rewrite "div_neg") (("" (assert) nil))))))
nil)
((mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(minus_int_is_int application-judgement "int" integers 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" 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)
(div_neg formula-decl nil div nil))
nil))
(rem_neg_d 0
(rem_neg_d-1 nil 3249307029
("" (skosimp*)
(("" (expand "rem")
(("" (rewrite "div_neg_d") (("" (assert) nil))))))
nil)
((mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(minus_int_is_int application-judgement "int" integers 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(div_neg_d formula-decl nil div nil)
(minus_nzint_is_nzint application-judgement "nzint" integers
nil))
nil))
(rem_even 0
(rem_even-1 nil 3249307029
("" (skosimp*)
(("" (expand "rem") (("" (rewrite "div_even") nil)))) nil)
((mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(rem const-decl "{k | abs(k) < abs(j)}" rem 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)
(div_even formula-decl nil div nil))
nil))
(rem_eq_arg 0
(rem_eq_arg-1 nil 3249307029
("" (skolem!)
(("" (expand "rem")
(("" (rewrite "div_eq_arg") (("" (assert) nil))))))
nil)
((mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(nzint_times_nzint_is_nzint application-judgement "nzint"
integers nil)
(int_minus_int_is_int application-judgement "int" 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)
(div_eq_arg formula-decl nil div nil))
nil))
(rem_zero 0
(rem_zero-1 nil 3249307029
("" (skosimp*)
(("" (expand "rem")
(("" (rewrite "div_zero") (("" (assert) nil))))))
nil)
((rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(int_times_even_is_even application-judgement "even_int"
integers nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
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)
(div_zero formula-decl nil div nil))
nil))
(rem_lt 0
(rem_lt-1 nil 3249307029
("" (skosimp*)
(("" (expand "rem")
(("" (rewrite "div_lt") (("" (assert) nil))))))
nil)
((mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(int_times_even_is_even application-judgement "even_int"
integers nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(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)
(div_lt formula-decl nil div nil))
nil))
(rem_it_is 0
(rem_it_is-1 nil 3249307029
("" (skosimp*)
(("" (expand "rem")
(("" (case "div(a!1,m!1) = c!1")
(("1" (assert) nil)
("2" (hide 2)
(("2" (expand "div")
(("2" (expand "sgn")
(("2" (expand "abs")
(("2" (replace -1)
(("2" (hide -1)
(("2" (lemma "floor_plus_int")
(("2"
(case "(b!1 + m!1 * c!1) / m!1 = b!1 / m!1 + c!1")
(("1" (replace -1)
(("1"
(hide -1)
(("1"
(inst -1 "c!1" "b!1/m!1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma "floor_small")
(("1"
(inst?)
(("1"
(expand "abs")
(("1"
(assert)
nil)))))))))))))))))
("2" (hide -1 -2 2)
(("2"
(assert)
nil))))))))))))))))))))))))
nil)
((nil application-judgement "nat" div 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)
(rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(sgn const-decl "int" real_defs nil)
(floor_plus_int formula-decl nil floor_ceil nil)
(floor_small formula-decl nil floor_ceil nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnrat_plus_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs 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)
(div_nat formula-decl nil div nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil
nil)
(real_lt_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)
(= 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)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(integer nonempty-type-from-decl nil integers nil)
(div const-decl "integer" div nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil))
nil))
(rem_eq_0 0
(rem_eq_0-1 nil 3249307029 ("" (subtype-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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(div const-decl "integer" div 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)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil))
nil))
(rem_one 0
(rem_one-1 nil 3249307029
("" (skosimp*)
(("" (lift-if)
(("" (split 1)
(("1" (flatten)
(("1" (expand "abs")
(("1" (lift-if)
(("1" (split -1)
(("1" (flatten)
(("1" (lemma "rem_eq_arg")
(("1" (inst -1 "1")
(("1" (lemma "rem_neg_d")
(("1" (inst -1 "1" "1")
(("1" (assert) nil)))))))))))
("2" (flatten)
(("2" (lemma "rem_eq_arg")
(("2" (inst?) (("2" (assert) nil)))))))))))))))
("2" (flatten)
(("2" (lemma "rem_lt")
(("2" (inst?)
(("2" (expand "abs")
(("2" (lift-if) (("2" (ground) nil))))))))))))))))
nil)
((rem_lt formula-decl nil rem 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_nzint_is_nzint application-judgement "nzint" integers
nil)
(rem_neg_d formula-decl nil rem nil)
(rem_eq_arg formula-decl nil rem nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil))
nil))
(rem_TCC2 0
(rem_TCC2-1 nil 3249307029
("" (skosimp*)
(("" (expand "rem")
(("" (lemma "div_smaller")
(("" (inst?)
(("" (assert)
(("" (lemma "ml1")
(("" (inst - "m!1" "n!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nil application-judgement "nat" div 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)
(rem const-decl "{k | abs(k) < abs(j)}" rem 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(ml1 formula-decl nil rem nil)
(div_nat formula-decl nil div nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil
nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(div_smaller formula-decl nil div nil))
nil)))
¤ Dauer der Verarbeitung: 0.31 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.
|
