|
(over_under
(over_under?_TCC1 0
(over_under?_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(pos const-decl "sign_rep" enumerated_type_defs nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(E_max formal-const-decl "integer" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" over_under nil)
(b formal-const-decl "above(1)" over_under nil)
(above 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)
(max_fp_pos const-decl "fp_num" IEEE_854_values nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(value const-decl "real" IEEE_854_values nil)
(max_pos const-decl "posreal" IEEE_854_values nil)
(/= const-decl "boolean" notequal nil)
(minus_int_is_int application-judgement "int" integers nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(infinity_TCC1 0
(infinity_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(trap_over_TCC1 0
(trap_over_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(overflow_TCC1 0
(overflow_TCC1-1 nil 3321205307 ("" (tcc :defs !) 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(posreal nonempty-type-eq-decl nil real_types 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)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(p formal-const-decl "above(1)" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(max_pos const-decl "posreal" IEEE_854_values nil)
(pos const-decl "sign_rep" enumerated_type_defs nil)
(max_fp_pos const-decl "fp_num" IEEE_854_values nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(value const-decl "real" IEEE_854_values nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(int_expt application-judgement "int" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(exact_underflow_TCC1 0
(exact_underflow_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(exact_underflow_TCC2 0
(exact_underflow_TCC2-1 nil 3321205307
("" (skolem-typepred) (("" (assert) nil nil)) nil)
((posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(E_max formal-const-decl "integer" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" 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)
(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)
(nzreal nonempty-type-eq-decl nil 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)
(/= const-decl "boolean" notequal 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))
nil))
(round_under_TCC1 0
(round_under_TCC1-1 nil 3321205307 ("" (tcc :defs !) 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nat_exp application-judgement "nat" exponentiation nil)
(nat_expt application-judgement "nat" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(expt def-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(round_under_TCC2 0
(round_under_TCC2-1 nil 3321205307 ("" (tcc :defs !) 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nat_exp application-judgement "nat" exponentiation nil)
(nat_expt application-judgement "nat" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(expt def-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(round_under_correct_TCC1 0
(round_under_correct_TCC1-1 nil 3321205307
("" (assert)
(("" (expand "min_pos")
(("" (lemma "min_fp_correct")
(("" (replace -1)
(("" (hide -1)
(("" (lemma "expt_pos")
(("" (inst?)
(("" (assert)
(("" (expand "abs")
(("" (lemma "expt_plus")
(("" (inst - "E_min" "1-p" "b")
(("" (replace -1)
(("" (hide -1)
(("" (lemma "both_sides_times_pos_lt2")
((""
(inst - "b^E_min" "b^(1-p)" "1")
(("1"
(lemma "expt_gt1_neg")
(("1"
(inst - "b" "p-1")
(("1" (ground) nil)))))
("2"
(lemma "expt_pos")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))
nil)
((min_pos const-decl "posreal" IEEE_854_values nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(expt_pos formula-decl nil exponentiation nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(expt_plus formula-decl nil exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(both_sides_times_pos_lt2 formula-decl nil real_props nil)
(expt_gt1_neg formula-decl nil exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(min_fp_correct formula-decl nil IEEE_854_values 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)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(p formal-const-decl "above(1)" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil))
nil))
(round_under_correct 0
(round_under_correct-1 nil 3321205307
("" (skosimp*)
(("" (expand "round_under")
(("" (rewrite "round_int")
(("1" (lemma "expt_plus")
(("1" (inst - "(1 + E_min - p)" "(-(1 + E_min - p))" "b")
(("1" (rewrite "expt_x0")
(("1" (rewrite "associative_mult")
(("1" (assert) nil)))))))))
("2" (hide 2)
(("2" (expand "min_pos")
(("2" (lemma "min_fp_correct")
(("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "expt_plus" :dir rl)
(("2" (rewrite "expt_x0")
(("2" (assert) nil))))))))))))))))))))
nil)
((round_under const-decl "real" over_under nil)
(min_fp_correct formula-decl nil IEEE_854_values nil)
(real_times_real_is_real application-judgement "real" reals nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(associative_mult formula-decl nil number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(rounding_mode type-decl nil enumerated_type_defs nil)
(min_pos const-decl "posreal" IEEE_854_values nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(p formal-const-decl "above(1)" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(E_max formal-const-decl "integer" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(b formal-const-decl "above(1)" over_under nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(>= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil 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)
(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)
(round_int formula-decl nil round nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(round_under_value_TCC1 0
(round_under_value_TCC1-1 nil 3321205307
("" (skosimp*)
(("" (prop)
(("1" (expand "subnormal?")
(("1" (expand "zero?") (("1" (ground) nil)))))
("2" (lemma "value_subnormal")
(("2" (inst?) (("2" (assert) nil))))))))
nil)
((zero? const-decl "bool" IEEE_854_values nil)
(subnormal? const-decl "bool" IEEE_854_values nil)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(value_subnormal formula-decl nil IEEE_854_values 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)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(p formal-const-decl "above(1)" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under
nil))
nil))
(round_under_value 0
(round_under_value-1 nil 3321205307
("" (skosimp*)
(("" (expand "round_under")
(("" (rewrite "round_int")
(("1" (lemma "expt_plus")
(("1" (inst - "(1 + E_min - p)" "(-(1 + E_min - p))" "b")
(("1" (rewrite "expt_x0")
(("1" (ground)
(("1" (rewrite "associative_mult")
(("1" (assert)
(("1" (rewrite "associative_mult" :dir rl)
(("1" (assert) nil)))))))))))))))
("2" (hide 2)
(("2"
(case "integer?(b ^ (-(1 + E_min - p))
* value(fin!1))")
(("1" (expand "integer?") (("1" (propax) nil)))
("2" (hide 2)
(("2" (expand "subnormal?")
(("2" (rewrite "normal_value")
(("2" (expand "value")
(("2" (prop)
(("2" (replace -1)
(("2" (assert)
(("2"
(case-replace "b ^ (-(1 + E_min - p))
*
(Sum(p, value_digit(d(normalize(fin!1))))
* (-1) ^ sign(normalize(fin!1))
* b ^ E_min) =
(-1)^sign(normalize(fin!1)) *(Sum(p,scale_value_p(d(normalize(fin!1)))))")
(("1" (hide -1)
(("1"
(assert)
(("1"
(case-replace
"scale_value_p(d(normalize(fin!1))) = scale_value(d(normalize(fin!1)),p-1)")
(("1"
(hide -1)
(("1"
(lemma "scaled_Sum_int")
(("1"
(inst?)
(("1"
(case
"FORALL (i,j:int): integer?(i*j)")
(("1"
(inst?)
(("1"
(expand "integer?")
(("1" (propax) nil)))))
("2"
(hide -1 -2 -3 2 3)
(("2"
(expand "integer?")
(("2"
(propax)
nil)))))))))))))
("2"
(hide -1 -2 2 3)
(("2"
(apply-extensionality)
(("1"
(expand "scale_value_p")
(("1" (propax) nil)))
("2"
(expand "scale_value")
(("2"
(expand "value_digit")
(("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(lift-if)
(("2"
(assert)
(("2"
(rewrite
"associative_mult"
:dir
rl)
(("2"
(rewrite
"expt_plus"
:dir
rl)
(("2"
(ground)
(("1"
(rewrite
"closed_times")
(("1"
(rewrite
"closed_times")
(("1"
(case
"forall (n:nat): integer_pred(b^n)")
(("1"
(inst?)
nil)
("2"
(skosimp*)
(("2"
(assert)
nil)))))))))
("2"
(rewrite
"pos_times_ge")
(("2"
(lemma
"expt_pos")
(("2"
(inst?)
(("2"
(assert)
nil)))))))))))))))))))))))))))))))))))
("2" (hide -1 -2 2 3)
(("2"
(assert)
(("2"
(lemma "scaled_Sum")
(("2"
(inst?)
(("2"
(replace -1 :dir rl)
(("2"
(hide -1)
(("2"
(lemma "expt_plus")
(("2"
(inst
-
"E_min"
"(-(1 + E_min - p))"
"b")
(("2"
(replace -1)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
((round_under const-decl "real" over_under nil)
(normal_value formula-decl nil IEEE_854_values nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(scaled_Sum formula-decl nil IEEE_854_values nil)
(scale_value const-decl "nonneg_real" IEEE_854_values nil)
(scaled_Sum_int formula-decl nil IEEE_854_values nil)
(fin!1 skolem-const-decl "(finite?)" over_under nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(<= const-decl "bool" reals nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(closed_times formula-decl nil integers nil)
(posint_exp application-judgement "posint" exponentiation nil)
(associative_mult formula-decl nil number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Sum def-decl "real" sum_hack nil) (< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(digits type-eq-decl nil IEEE_854_values nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil)
(normalize def-decl "(finite?)" IEEE_854_values nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
nil)
(scale_value_p const-decl "nat" IEEE_854_values nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil)
(subnormal? const-decl "bool" IEEE_854_values nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(integer? const-decl "bool" integers nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(rounding_mode type-decl nil enumerated_type_defs nil)
(value const-decl "real" IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil)
(p formal-const-decl "above(1)" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(E_max formal-const-decl "integer" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(b formal-const-decl "above(1)" over_under nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(>= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil 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)
(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)
(round_int formula-decl nil round nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(round_under_error_TCC1 0
(round_under_error_TCC1-1 nil 3321205307 ("" (tcc :defs !) 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(round_under_error 0
(round_under_error-1 nil 3321205307
("" (skosimp*)
(("" (expand "round_under")
((""
(case-replace "abs(r!1
- b ^ (1 + E_min - p)
* round(b ^ (-(1 + E_min - p)) * r!1, mode!1)) =
abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, mode!1))")
(("1" (hide -1 -2)
(("1" (rewrite "abs")
(("1" (lemma "expt_pos")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "both_sides_times_pos_lt2")
(("1" (inst - "b^(1+E_min-p)" "_" "1")
(("1" (inst?)
(("1" (lemma "round1")
(("1" (inst?)
(("1" (assert) nil)))))))))))))))))))))
("2" (hide -1 2)
(("2" (rewrite "abs_mult" :dir rl)
(("2" (rewrite "expt_plus" :dir rl)
(("2" (rewrite "expt_x0") (("2" (assert) nil)))))))))
("3" (assert) nil) ("4" (assert) nil))))))
nil)
((int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(round_under const-decl "real" over_under nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(abs_mult formula-decl nil real_props nil)
(expt_pos formula-decl nil exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(round1 formula-decl nil round nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(both_sides_times_pos_lt2 formula-decl nil real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(round const-decl "integer" round nil)
(rounding_mode type-decl nil enumerated_type_defs nil)
(p formal-const-decl "above(1)" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(E_max formal-const-decl "integer" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(b formal-const-decl "above(1)" over_under nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(round_under_near 0
(round_under_near-1 nil 3321205307
("" (skosimp*)
(("" (expand "round_under")
(("" (hide -1)
((""
(case-replace "abs(r!1
- b ^ (1 + E_min - p)
* round(b ^ (-(1 + E_min - p)) * r!1, to_nearest)) =
abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, to_nearest))")
(("1" (hide -1)
(("1" (expand "abs" + 1)
(("1" (lemma "expt_pos")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "both_sides_times_pos_lt2")
(("1" (inst - "b^(1+E_min-p)" "_" "1/2")
(("1" (expand "round")
(("1" (inst?)
(("1" (rewrite "times_div1")
(("1"
(lemma "round_to_even1")
(("1"
(inst?)
(("1" (assert) nil)))))))))))))))))
("2" (assert)
(("2" (split)
(("1" (assert) nil)
("2" (assert) nil)))))))))))))
("2" (hide 2)
(("2" (rewrite "abs_mult" :dir rl)
(("2" (rewrite "expt_plus" :dir rl)
(("2" (rewrite "expt_x0") (("2" (assert) nil)))))))))
("3" (assert) nil) ("4" (assert) nil))))))))
nil)
((int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(round_under const-decl "real" over_under nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_int_is_int application-judgement "int" integers 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(* const-decl "[numfield, numfield -> 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(p formal-const-decl "above(1)" over_under nil)
(rounding_mode type-decl nil enumerated_type_defs nil)
(round const-decl "integer" round nil)
(to_nearest? adt-recognizer-decl "[rounding_mode -> boolean]"
enumerated_type_defs nil)
(to_nearest adt-constructor-decl "(to_nearest?)"
enumerated_type_defs nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(both_sides_times_pos_lt2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div1 formula-decl nil real_props nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(round_to_even1 formula-decl nil round nil)
(round_to_even const-decl "integer" round nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(expt_pos formula-decl nil exponentiation nil)
(abs_mult formula-decl nil real_props nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(expt_x0 formula-decl nil exponentiation nil)
(expt_plus formula-decl nil exponentiation nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(round_under_pos 0
(round_under_pos-1 nil 3321205307
("" (skosimp*)
(("" (expand "round_under")
(("" (hide -1)
(("" (expand "round")
(("" (lemma "both_sides_times_pos_ge2")
(("" (lemma "expt_pos")
(("" (inst - "(-(1 + E_min - p))" "b")
(("1"
(inst - "b ^ (-(1 + E_min - p))"
"b ^ (1 + E_min - p) * ceiling(b ^ (-(1 + E_min - p)) * r!1)"
"r!1")
(("1" (replace -2 :dir rl)
(("1" (hide -2)
(("1" (rewrite "associative_mult")
(("1" (rewrite "associative_mult" :dir rl)
(("1" (rewrite "expt_plus" :dir rl)
(("1" (rewrite "expt_x0")
(("1" (assert) nil)))))))))))))
("2" (assert) nil) ("3" (assert) nil)
("4" (assert) nil)))
("2" (assert) nil))))))))))))))
nil)
((round_under const-decl "real" over_under nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(round const-decl "integer" round nil)
(expt_pos formula-decl nil exponentiation nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(expt_x0 formula-decl nil exponentiation 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)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(expt_plus formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(associative_mult formula-decl nil number_fields nil)
(b formal-const-decl "above(1)" over_under nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(p formal-const-decl "above(1)" over_under nil)
(above nonempty-type-eq-decl nil integers nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(E_max formal-const-decl "integer" over_under nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil 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)
(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)
(minus_int_is_int application-judgement "int" integers nil)
(both_sides_times_pos_ge2 formula-decl nil real_props nil))
nil))
(round_under_neg 0
(round_under_neg-1 nil 3321205307
("" (skosimp*)
(("" (hide -1)
(("" (expand "round_under")
(("" (expand "round")
(("" (lemma "both_sides_times_pos_le2")
((""
(inst - "b ^ (-(1 + E_min - p))"
"b ^ (1 + E_min - p) * floor(b ^ (-(1 + E_min - p)) * r!1)"
"r!1")
(("1" (replace -1 :dir rl)
(("1" (hide -1)
(("1" (rewrite "associative_mult")
(("1" (rewrite "associative_mult" :dir rl)
(("1" (rewrite "expt_plus" :dir rl)
(("1" (rewrite "expt_x0")
(("1" (assert) nil)))))))))))))
("2" (assert) nil)
("3" (lemma "expt_pos")
(("3" (inst?)
(("1" (assert) nil) ("2" (assert) nil)))))
("4" (assert) nil))))))))))))
nil)
((int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(round const-decl "integer" round nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(minus_int_is_int application-judgement "int" 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" over_under nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(p formal-const-decl "above(1)" over_under nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_x0 formula-decl nil exponentiation nil)
(real_le_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)
(expt_plus formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(associative_mult formula-decl nil number_fields nil)
(both_sides_times_pos_le2 formula-decl nil real_props nil)
(round_under const-decl "real" over_under nil))
nil))
(round_under_zero 0
(round_under_zero-1 nil 3321205307
("" (skosimp*)
(("" (expand "round_under")
(("" (rewrite "abs_mult")
(("" (expand "round")
(("" (case "forall (r1,r2:real): abs(sgn(r1)*r2) = abs(r2)")
(("1" (inst?)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(case "forall (r:real): abs(floor(abs(r)))=floor(abs(r))")
(("1" (inst?)
(("1" (replace -1)
(("1" (hide -1)
(("1" (lemma "both_sides_times_pos_le2")
(("1"
(inst - "abs(b ^ (-(1 + E_min - p)))"
"abs(b ^ (1 + E_min - p)) * floor(abs(b ^ (-(1 + E_min - p)) * r!1))"
"abs(r!1)")
(("1"
(replace -1 :dir rl)
(("1"
(hide -1)
(("1"
(hide -1)
(("1"
(rewrite "abs_mult" :dir rl)
(("1"
(rewrite "associative_mult")
(("1"
(rewrite
"associative_mult"
:dir
rl)
(("1"
(rewrite
"abs_mult"
:dir
rl)
(("1"
(rewrite
"expt_plus"
:dir
rl)
(("1"
(rewrite "expt_x0")
(("1"
(expand "abs" + 2)
(("1"
(assert)
nil)))))))))))))))))))))
("2"
(hide -1 2)
(("2"
(lemma "expt_pos")
(("2"
(inst?)
(("2"
(expand "abs")
(("2"
(assert)
nil)))))))))))))))))))
("2" (hide -1 2) (("2" (grind) nil)))))))))))
("2" (hide -1 2) (("2" (tcc) nil))))))))))))
nil)
((int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(round_under const-decl "real" over_under 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(expt_plus formula-decl nil exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt_x0 formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(associative_mult formula-decl nil number_fields nil)
(both_sides_times_pos_le2 formula-decl nil real_props nil)
(sgn const-decl "int" real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals 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)
(to_zero adt-constructor-decl "(to_zero?)" enumerated_type_defs
nil)
(to_zero? adt-recognizer-decl "[rounding_mode -> boolean]"
enumerated_type_defs nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(round const-decl "integer" round nil)
(rounding_mode type-decl nil enumerated_type_defs nil)
(p formal-const-decl "above(1)" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)
(E_max formal-const-decl "integer" over_under nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(b formal-const-decl "above(1)" over_under nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(>= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(abs_mult formula-decl nil real_props nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_int_is_int application-judgement "int" integers nil))
nil)))
¤ Dauer der Verarbeitung: 0.83 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.
|
