|
(tdiv
(tdiv_TCC1 0
(tdiv_TCC1-1 nil 3407849557
("" (skosimp*)
(("" (assert)
(("" (expand "tdiv")
(("" (lemma "pos_div_ge") (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pos_div_ge formula-decl nil real_props nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(tdiv_TCC2 0
(tdiv_TCC2-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lemma "pos_div_ge") (("" (ground) nil nil)) nil)) nil))
nil)
((tdiv const-decl "integer" tdiv nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nprat_div_posrat_is_nprat application-judgement "nprat" rationals
nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pos_div_ge formula-decl nil real_props nil))
nil))
(tdiv_TCC3 0
(tdiv_TCC3-1 nil 3407849557
("" (skosimp*)
(("" (assert)
(("" (expand "tdiv")
(("" (typepred "negi!1")
(("" (typepred "ngi2!1")
(("" (hide -1 -3) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(negint nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nonpos_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)
(<= 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)
(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)
(negrat_div_negrat_is_posrat application-judgement "posrat"
rationals nil)
(tdiv const-decl "integer" tdiv nil))
nil))
(tdiv_TCC4 0
(tdiv_TCC4-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lemma "pos_div_ge")
(("" (inst?) (("" (flatten) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv 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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-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)
(nonpos_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(negint 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_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(nnrrat_div_negrat_is_nprat application-judgement "nprat" rationals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pos_div_ge formula-decl nil real_props nil))
nil))
(tdiv_nat 0
(tdiv_nat-1 nil 3407849557
("" (skosimp*)
(("" (lift-if)
(("" (expand "tdiv")
(("" (split 1)
(("1" (flatten)
(("1" (case "(n!1 - m!1) / m!1 = n!1/m!1 - 1")
(("1" (lemma "floor_plus_int")
(("1" (inst -1 "-1" "n!1/m!1") (("1" (ground) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "floor_small")
(("2" (inst?)
(("2" (expand "abs") (("2" (assert) nil nil)) nil))
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)
(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)
(- 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)
(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)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(integer nonempty-type-from-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(floor_plus_int formula-decl nil floor_ceil nil)
(floor_small formula-decl nil floor_ceil 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)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(tdiv const-decl "integer" tdiv nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(tdiv_neg_d 0
(tdiv_neg_d-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lift-if)
(("" (lemma "floor_neg")
(("" (inst -1 "i!1/j!1")
(("" (lift-if)
(("" (expand "integer?") (("" (ground) nil 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)
(tdiv const-decl "integer" tdiv nil)
(floor_neg formula-decl nil floor_ceil nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(integer? const-decl "bool" integers nil)
(minus_int_is_int application-judgement "int" integers 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)
(/ 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)
(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))
(tdiv_neg 0
(tdiv_neg-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lift-if)
(("" (lemma "floor_neg")
(("" (inst -1 "i!1/j!1")
(("" (lift-if)
(("" (expand "integer?") (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(tdiv const-decl "integer" tdiv nil)
(floor_neg formula-decl nil floor_ceil nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(integer? const-decl "bool" integers 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)
(/ 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)
(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))
(tdiv_def 0
(tdiv_def-1 nil 3407849557
("" (skosimp*)
(("" (lift-if)
(("" (split 1)
(("1" (flatten)
(("1" (lemma "tdiv_nat")
(("1" (inst?)
(("1" (lift-if) (("1" (assert) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split 2)
(("1" (flatten)
(("1" (lemma "tdiv_nat")
(("1" (inst?)
(("1" (lift-if) (("1" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (split 2)
(("1" (flatten)
(("1" (lemma "tdiv_neg")
(("1" (inst?)
(("1" (lift-if) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "tdiv_neg")
(("2" (inst?)
(("2" (lift-if) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(tdiv_neg formula-decl nil tdiv nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(i!1 skolem-const-decl "int" tdiv 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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(tdiv_nat formula-decl nil tdiv nil))
nil))
(tdiv_sgn 0
(tdiv_sgn-1 nil 3407849557
("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
nil)
((minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(tdiv const-decl "integer" tdiv nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
nil))
(tdiv_value 0
(tdiv_value-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lemma "floor_val")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((tdiv const-decl "integer" tdiv 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)
(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)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(floor_val formula-decl nil floor_ceil nil))
nil))
(tdiv_zero 0
(tdiv_zero-1 nil 3407849557
("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
nil)
((tdiv const-decl "integer" tdiv nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
nil))
(tdiv_one 0
(tdiv_one-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lemma "floor_small")
(("" (inst -1 "1" "j!1")
(("" (expand "abs" -1 1)
(("" (assert)
(("" (lemma "pos_div_ge")
(("" (inst -1 "j!1" "1")
(("" (flatten)
(("" (assert)
(("" (lift-if)
(("" (lemma "div_eq_zero")
(("" (inst -1 "j!1" "1")
(("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv 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)
(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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_eq_zero formula-decl nil real_props nil)
(pos_div_ge formula-decl nil real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(floor_small formula-decl nil floor_ceil nil))
nil))
(tdiv_eq_arg 0
(tdiv_eq_arg-1 nil 3407849557
("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
nil)
((tdiv const-decl "integer" tdiv nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil))
nil))
(tdiv_by_one 0
(tdiv_by_one-1 nil 3407849557
("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
nil)
((tdiv const-decl "integer" tdiv nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
nil))
(tdiv_eq_0 0
(tdiv_eq_0-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lemma "floor_eq_0")
(("" (inst -1 "i!1/j!1")
(("" (lemma "pos_div_ge")
(("" (inst?)
(("" (lemma "div_eq_zero")
(("" (inst?)
(("" (flatten)
(("" (expand "sgn")
(("" (expand "abs")
(("" (lift-if)
(("" (lift-if)
(("" (assert)
((""
(ground)
(("1"
(hide 1 3)
(("1"
(lemma "both_sides_times_pos_lt1")
(("1"
(inst -1 "-j!1" "1" "i!1/j!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma "both_sides_times_pos_lt1")
(("2"
(inst -1 "j!1" "1" "i!1/j!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv 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)
(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)
(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)
(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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(sgn const-decl "int" tdiv 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)
(- const-decl "[numfield -> numfield]" number_fields 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)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_int_is_int application-judgement "int" 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(div_eq_zero formula-decl nil real_props nil)
(pos_div_ge formula-decl nil real_props nil)
(floor_eq_0 formula-decl nil floor_ceil nil))
nil))
(tdiv_lt 0
(tdiv_lt-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lemma "floor_small")
(("" (inst?)
(("" (assert)
((""
(case "(i!1 = 0 OR sgn(i!1) = sgn(j!1)) = (i!1 / j!1 >= 0)")
(("1" (lift-if)
(("1" (expand "sgn") (("1" (ground) nil nil)) nil))
nil)
("2" (hide -1 -2 2)
(("2" (iff 1)
(("2" (split 1)
(("1" (flatten)
(("1" (expand "sgn")
(("1" (ground)
(("1" (lemma "pos_div_ge")
(("1" (inst -1 "j!1" "i!1")
(("1"
(assert)
(("1"
(lift-if)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "sgn")
(("2" (lift-if)
(("2" (lift-if)
(("2" (lemma "pos_div_ge")
(("2"
(inst -1 "j!1" "i!1")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv 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)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers 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)
(>= const-decl "bool" reals nil) (sgn const-decl "int" tdiv nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(floor_small formula-decl nil floor_ceil nil))
nil))
(tdiv_parity 0
(tdiv_parity-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (expand "sgn")
(("" (lift-if)
(("" (lemma "pos_div_ge")
(("" (inst?)
(("" (flatten)
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv 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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pos_div_ge formula-decl nil real_props nil)
(sgn const-decl "int" tdiv nil))
nil))
(tdiv_parity_neg 0
(tdiv_parity_neg-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (expand "sgn")
(("" (lift-if)
(("" (lemma "pos_div_ge")
(("" (inst?)
(("" (flatten)
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv 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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pos_div_ge formula-decl nil real_props nil)
(sgn const-decl "int" tdiv nil))
nil))
(tdiv_smaller 0
(tdiv_smaller-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (assert)
(("" (typepred "floor(n!1 / m!1)")
(("" (lemma "both_sides_times_pos_lt1")
(("" (inst -1 "m!1" "floor(n!1 / m!1)" "n!1 / m!1")
(("" (flatten)
(("" (ground)
(("" (case "floor(n!1 / m!1) = n!1 / m!1")
(("1" (ground)
(("1" (replace -1)
(("1" (auto-rewrite-theory "real_props")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tdiv const-decl "integer" tdiv nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(<= 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_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)
(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)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil))
nil))
(tdiv_abs 0
(tdiv_abs-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (expand "abs")
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (lemma "floor_neg")
(("" (inst?)
(("" (lift-if)
(("" (expand "sgn")
(("" (lift-if)
(("" (assert)
(("" (lemma "pos_div_ge")
(("" (expand "integer?")
((""
(inst?)
((""
(split +)
(("1"
(flatten)
(("1" (ground) nil nil))
nil)
("2"
(flatten)
(("2"
(ground)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(tdiv const-decl "integer" tdiv nil)
(minus_int_is_int application-judgement "int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers 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)
(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)
(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)
(sgn const-decl "int" tdiv nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(integer? const-decl "bool" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" 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)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(pos_div_ge formula-decl nil real_props nil)
(floor_neg formula-decl nil floor_ceil nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil))
nil))
(tdiv_max 0
(tdiv_max-1 nil 3407849557
("" (skosimp*)
(("" (lemma "tdiv_smaller")
(("" (inst -1 "abs(j!1)" "abs(i!1)")
(("" (lemma "tdiv_abs")
(("" (inst?)
(("" (replace -1)
(("" (hide -1)
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tdiv_smaller formula-decl nil tdiv nil)
(tdiv_abs formula-decl nil tdiv nil)
(nil application-judgement "nat" tdiv nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal 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)
(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)
(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))
nil))
(tdiv_multiple 0
(tdiv_multiple-1 nil 3407849557
("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(tdiv const-decl "integer" tdiv nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
nil))
(tdiv_sum 0
(tdiv_sum-1 nil 3407849557
("" (skosimp*)
(("" (expand "tdiv")
(("" (lemma "floor_plus_int")
(("" (inst -1 "k!1*j!1/j!1" "i!1/j!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(tdiv const-decl "integer" tdiv 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)
(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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int nonempty-type-eq-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(floor_plus_int formula-decl nil floor_ceil nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.43Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
