|
(IEEE_854_values
(value_digit_TCC1 0
(value_digit_TCC1-1 nil 3321199176 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(/= const-decl "boolean" notequal nil))
nil))
(value_TCC1 0
(value_TCC1-1 nil 3321199176 ("" (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)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(/= const-decl "boolean" notequal nil))
nil))
(shift_left_TCC1 0
(shift_left_TCC1-1 nil 3321199176 ("" (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)
(< 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 "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(shift_left_TCC2 0
(shift_left_TCC2-1 nil 3321199176 ("" (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)
(< 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 "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(normalize_TCC1 0
(normalize_TCC1-1 nil 3321199176 ("" (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)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(normalize_TCC2 0
(normalize_TCC2-1 nil 3321199176 ("" (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)
(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))
nil))
(normalize_TCC3 0
(normalize_TCC3-1 nil 3321199176 ("" (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)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(normalize_TCC4 0
(normalize_TCC4-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(normalize_idempotent 0
(normalize_idempotent-1 nil 3321199176
("" (skosimp*)
(("" (case-replace "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
(("1" (hide -1)
(("1"
(case "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
normalize(normalize(finite(s,n+E_min,d)))=normalize(finite(s,n+E_min,d))")
(("1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (induct "n" 1 "upto_induction[E_max-E_min]")
(("1" (skosimp*)
(("1" (expand "normalize") (("1" (propax) nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "normalize" +)
(("2" (lift-if)
(("2" (ground)
(("1" (rewrite "normalize") nil nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) (("2" (rewrite "fp_num_finite_eta") nil nil))
nil))
nil))
nil)
((fp_num type-decl nil IEEE_854_values nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(integer nonempty-type-from-decl nil integers nil)
(> const-decl "bool" reals nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(< const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(b formal-const-decl "above(1)" IEEE_854_values nil)
(finite adt-constructor-decl
"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil)
(sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
nil)
(Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values
nil)
(d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(normalize def-decl "(finite?)" IEEE_854_values nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(digits type-eq-decl nil IEEE_854_values nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(fin!1 skolem-const-decl "(finite?)" IEEE_854_values nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pred type-eq-decl nil defined_types nil)
(upto_induction formula-decl nil bounded_nat_inductions 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)
(shift_left const-decl "digits" IEEE_854_values nil)
(fp_num_finite_eta formula-decl nil IEEE_854_values nil))
nil))
(subnormal?_TCC1 0
(subnormal?_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil 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)
(zero? const-decl "bool" IEEE_854_values nil)
(value const-decl "real" IEEE_854_values nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_expt application-judgement "int" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil))
nil))
(normal?_TCC1 0
(normal?_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(max_significand_TCC1 0
(max_significand_TCC1-1 nil 3321199176 ("" (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)
(< 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 "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(min_significand_TCC1 0
(min_significand_TCC1-1 nil 3321199176 ("" (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)
(< 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 "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(min_significand_TCC2 0
(min_significand_TCC2-1 nil 3321199176 ("" (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)
(< 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 "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(d_zero_TCC1 0
(d_zero_TCC1-1 nil 3321199176 ("" (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)
(< 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 "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Sum_value0 0
(Sum_value0-1 nil 3321199176
("" (induct-and-simplify "n") (("" (grind) nil)) nil)
((minus_int_is_int application-judgement "int" integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(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)
(real_plus_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Sum def-decl "real" sum_hack nil) (< const-decl "bool" reals nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(b formal-const-decl "above(1)" IEEE_854_values 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_zero const-decl "digits" IEEE_854_values nil)
(nat_induction formula-decl nil naturalnumbers nil))
nil))
(zero_finite_d_zero 0
(zero_finite_d_zero-1 nil 3321199176
("" (grind :rewrites "Sum_value0") nil nil)
((minus_int_is_int application-judgement "int" integers nil)
(zero? const-decl "bool" IEEE_854_values nil)
(value const-decl "real" IEEE_854_values nil)
(Sum_value0 formula-decl nil IEEE_854_values nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil))
nil))
(max_fp_pos_TCC1 0
(max_fp_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(min_fp_pos_TCC1 0
(min_fp_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(pos_zero_TCC1 0
(pos_zero_TCC1-1 nil 3321199176
("" (rewrite "zero_finite_d_zero") nil nil)
((pos const-decl "sign_rep" enumerated_type_defs nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(> const-decl "bool" reals nil)
(integer nonempty-type-from-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND 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)
(zero_finite_d_zero formula-decl nil IEEE_854_values nil))
nil))
(neg_zero_TCC1 0
(neg_zero_TCC1-1 nil 3321199176
("" (rewrite "zero_finite_d_zero") nil nil)
((neg const-decl "sign_rep" enumerated_type_defs nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(> const-decl "bool" reals nil)
(integer nonempty-type-from-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND 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)
(zero_finite_d_zero formula-decl nil IEEE_854_values nil))
nil))
(max_pos_TCC1 0
(max_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((pos const-decl "sign_rep" enumerated_type_defs nil)
(max_fp_pos const-decl "fp_num" IEEE_854_values nil))
nil))
(max_pos_TCC2 0
(max_pos_TCC2-1 nil 3321199176
("" (expand "value")
(("" (expand "max_fp_pos")
(("" (expand "pos")
(("" (rewrite "expt_x0")
(("" (lemma "pos_times_gt")
(("" (assert)
(("" (inst?)
(("" (assert)
(("" (lemma "expt_pos")
(("" (inst?)
(("" (assert)
((""
(case "Sum(p, value_digit(max_significand)) > 0")
(("1" (ground) nil)
("2" (hide -1 -2 2)
(("2" (expand "Sum")
(("2"
(assert)
(("2"
(lemma "Sum_nonneg")
(("2"
(inst?)
(("2"
(rewrite "value_digit")
(("2"
(rewrite "max_significand")
(("2"
(lemma "expt_pos")
(("2"
(inst?)
(("2"
(lemma "pos_times_gt")
(("2"
(inst?)
(("2"
(ground)
nil))))))))))))))))))))))))))))))))))))))))))))))
nil)
((max_fp_pos const-decl "fp_num" IEEE_854_values nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_x0 formula-decl nil exponentiation 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 "[numfield -> numfield]" number_fields 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals 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)
(minus_int_is_int application-judgement "int" integers nil)
(Sum_nonneg formula-decl nil sum_hack nil)
(expt_pos formula-decl nil exponentiation nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(integer nonempty-type-from-decl nil integers nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(max_significand const-decl "digits" IEEE_854_values nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(digits type-eq-decl nil IEEE_854_values nil)
(b formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil) (Sum def-decl "real" sum_hack 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)
(pos_times_gt formula-decl nil real_props nil)
(pos const-decl "sign_rep" enumerated_type_defs nil)
(value const-decl "real" IEEE_854_values nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil))
nil))
(min_pos_TCC1 0
(min_pos_TCC1-1 nil 3321199176 ("" (tcc) nil nil)
((pos const-decl "sign_rep" enumerated_type_defs nil)
(min_fp_pos const-decl "fp_num" IEEE_854_values nil))
nil))
(min_pos_TCC2 0
(min_pos_TCC2-1 nil 3321199176
("" (expand "min_fp_pos")
(("" (expand "value")
(("" (expand "pos")
(("" (rewrite "expt_x0")
(("" (lemma "expt_pos")
(("" (inst?)
(("1" (assert)
(("1" (lemma "pos_times_gt")
(("1" (inst?)
(("1" (assert)
(("1"
(case "Sum(p, value_digit(min_significand)) > 0")
(("1" (assert) (("1" (assert) nil)))
("2" (hide -1 -2 2)
(("2" (expand "Sum")
(("2" (lemma "Sum_nonneg")
(("2"
(inst?)
(("2"
(rewrite "value_digit")
(("2"
(rewrite "min_significand")
(("2"
(lemma "expt_pos")
(("2"
(inst?)
(("2"
(assert)
nil)))))))))))))))))))))))))))
("2" (assert)
(("2" (split)
(("1" (assert) nil) ("2" (assert) nil))))))))))))))))
nil)
((int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(value const-decl "real" IEEE_854_values nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_x0 formula-decl nil exponentiation 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 "[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)
(integer nonempty-type-from-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
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)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" IEEE_854_values nil)
(pos_times_gt formula-decl nil real_props nil)
(Sum_nonneg formula-decl nil sum_hack 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)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Sum def-decl "real" sum_hack nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(digits type-eq-decl nil IEEE_854_values nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(min_significand const-decl "digits" IEEE_854_values nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" 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)
(expt_pos formula-decl nil exponentiation nil)
(pos const-decl "sign_rep" enumerated_type_defs nil)
(min_fp_pos const-decl "fp_num" IEEE_854_values nil))
nil))
(max_neg_TCC1 0
(max_neg_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((neg const-decl "sign_rep" enumerated_type_defs nil)
(max_fp_neg const-decl "fp_num" IEEE_854_values nil))
nil))
(max_neg_TCC2 0
(max_neg_TCC2-1 nil 3321199176
("" (expand "max_fp_neg")
(("" (expand "value")
(("" (expand "neg")
(("" (rewrite "expt_x1")
(("" (lemma "expt_pos")
(("" (inst?)
(("" (lemma "Sum_pos")
(("" (inst?)
(("" (assert)
(("" (lemma "pos_times_gt")
(("" (inst?)
(("" (ground)
(("1" (inst + "0")
(("1" (rewrite "value_digit")
(("1"
(rewrite "expt_x0")
(("1"
(rewrite "max_significand")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (inst + "0")
(("2" (rewrite "value_digit")
(("2"
(rewrite "expt_x0")
(("2"
(rewrite "max_significand")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (inst + "0")
(("3" (rewrite "value_digit")
(("3"
(rewrite "max_significand")
(("3"
(rewrite "expt_x0")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(value const-decl "real" IEEE_854_values nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_x1 formula-decl nil exponentiation 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 "[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)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" IEEE_854_values 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)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" IEEE_854_values nil)
(max_significand const-decl "digits" IEEE_854_values nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(digits type-eq-decl nil IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pos_times_gt formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(expt_x0 formula-decl nil exponentiation nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(Sum def-decl "real" sum_hack nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation 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)
(Sum_pos formula-decl nil sum_hack nil)
(expt_pos formula-decl nil exponentiation nil)
(neg const-decl "sign_rep" enumerated_type_defs nil)
(max_fp_neg const-decl "fp_num" IEEE_854_values nil))
nil))
(min_neg_TCC1 0
(min_neg_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((neg const-decl "sign_rep" enumerated_type_defs nil)
(min_fp_neg const-decl "fp_num" IEEE_854_values nil))
nil))
(min_neg_TCC2 0
(min_neg_TCC2-1 nil 3321199176
("" (expand "min_fp_neg")
(("" (expand "value")
(("" (expand "neg")
(("" (rewrite "expt_x1")
(("" (assert)
(("" (lemma "expt_pos")
(("" (inst?)
(("" (lemma "Sum_pos")
(("" (inst?)
(("" (lemma "pos_times_gt")
(("" (inst?)
(("" (ground)
(("1" (inst + "p-1")
(("1" (rewrite "value_digit")
(("1"
(rewrite "min_significand")
(("1"
(hide 1 3 4 5 6)
(("1"
(hide -1)
(("1"
(lemma "expt_pos")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 1 3 4 5 6)
(("2" (inst + "p-1")
(("2"
(expand "value_digit")
(("2"
(expand "min_significand")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (hide -1 1 3 4 5 6)
(("3" (inst + "p-1")
(("3"
(expand "value_digit")
(("3"
(expand "min_significand")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(value const-decl "real" IEEE_854_values nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_x1 formula-decl nil exponentiation 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 "[numfield -> numfield]" number_fields nil)
(expt_pos formula-decl nil exponentiation nil)
(Sum_pos formula-decl nil sum_hack nil)
(pos_times_gt formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Sum def-decl "real" sum_hack nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(digits type-eq-decl nil IEEE_854_values nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(min_significand const-decl "digits" IEEE_854_values nil)
(b formal-const-decl "above(1)" IEEE_854_values nil)
(above nonempty-type-eq-decl nil integers 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)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(integer nonempty-type-from-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(neg const-decl "sign_rep" enumerated_type_defs nil)
(min_fp_neg const-decl "fp_num" IEEE_854_values nil))
nil))
(max_fp_correct_TCC1 0
(max_fp_correct_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(max_fp_correct_TCC2 0
(max_fp_correct_TCC2-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(max_fp_correct 0
(max_fp_correct-1 nil 3321199176
("" (rewrite "max_pos")
(("" (rewrite "max_fp_pos")
(("" (rewrite "value")
(("" (rewrite "pos")
(("" (rewrite "expt_x0")
(("" (assert)
((""
(case "forall (i:upto(p)):Sum(i,
(LAMBDA (n: nat):
IF n < p THEN max_significand(n) * (b ^ (-n)) ELSE 0 ENDIF))
* b ^ E_max
= b ^ (1 + E_max) - b ^ (1 + E_max - i)")
(("1" (inst?)
(("1" (expand "value_digit") (("1" (propax) nil)))))
("2" (hide 2)
(("2" (induct "i" 1 "upto_induction[p]")
(("1" (rewrite "Sum") (("1" (assert) nil)))
("2" (skosimp*)
(("2" (expand "Sum" +)
(("2" (replace -2)
(("2" (hide -2)
(("2" (assert)
(("2"
(rewrite "max_significand")
(("2"
(lemma "expt_plus")
(("2"
(inst-cp - "1" "E_max - jt!1" "b")
(("2"
(inst - "E_max" "-jt!1" "b")
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(rewrite "expt_x1")
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))))
nil)
((max_fp_pos const-decl "fp_num" IEEE_854_values nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x1 formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint_exp application-judgement "posint" exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(upto_induction formula-decl nil bounded_nat_inductions nil)
(pred type-eq-decl nil defined_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(Sum def-decl "real" sum_hack nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(expt_x0 formula-decl nil exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(max_significand const-decl "digits" IEEE_854_values nil)
(digits type-eq-decl nil IEEE_854_values nil)
(pos const-decl "sign_rep" enumerated_type_defs nil)
(finite adt-constructor-decl
"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil)
(b formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(above nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(> const-decl "bool" reals nil)
(integer nonempty-type-from-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(boolean nonempty-type-decl nil booleans nil)
(fp_num type-decl nil IEEE_854_values nil)
(value const-decl "real" IEEE_854_values nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(max_pos const-decl "posreal" IEEE_854_values nil))
nil))
(min_fp_correct_TCC1 0
(min_fp_correct_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(min_fp_correct 0
(min_fp_correct-1 nil 3321199176
("" (expand "min_fp_pos")
(("" (expand "value")
(("" (expand "pos")
(("" (rewrite "expt_x0")
(("" (assert)
((""
(case-replace
"Sum(p,value_digit(min_significand))= b^(1-p)")
(("1" (hide -1)
(("1" (lemma "expt_plus")
(("1" (inst - "(1 - p)" "E_min" "b")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "Sum")
(("2" (expand "value_digit")
(("2" (expand "min_significand")
(("2"
(case "forall (i:below(p)):Sum(i,
LAMBDA (n: nat):
IF n < p THEN IF n < p - 1 THEN 0 ELSE 1 ENDIF * b ^ (-n)
ELSE 0
ENDIF)
= 0")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (induct-and-rewrite "i" 1 "Sum") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((value const-decl "real" IEEE_854_values nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_x0 formula-decl nil exponentiation 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 "[numfield -> numfield]" number_fields nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Sum def-decl "real" sum_hack nil) (> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(b formal-const-decl "above(1)" IEEE_854_values 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)
(min_significand const-decl "digits" IEEE_854_values nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(expt_plus formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(pred type-eq-decl nil defined_types nil)
(below_induction formula-decl nil bounded_nat_inductions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(real_plus_real_is_real application-judgement "real" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(pos const-decl "sign_rep" enumerated_type_defs nil)
(min_fp_pos const-decl "fp_num" IEEE_854_values nil))
nil))
(value0 0
(value0-1 nil 3321199176
("" (skosimp*)
(("" (expand "value")
(("" (rewrite "zero_times3")
(("1" (rewrite "zero_times3")
(("1" (lemma "expt_nonzero")
(("1" (inst? :copy? t)
(("1" (assert)
(("1" (hide -2)
(("1" (inst?)
(("1" (assert)
(("1" (hide -1)
(("1" (rewrite "Sum_zero")
(("1" (prop)
(("1" (expand "d_zero")
(("1"
(apply-extensionality)
(("1"
(expand "value_digit")
(("1"
(inst?)
(("1"
(rewrite "zero_times3")
(("1"
(lemma "expt_nonzero")
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))))))
("2" (replace -1)
(("2"
(expand "d_zero")
(("2"
(expand "value_digit")
(("2"
(propax)
nil)))))))))))))))))))))))))))
("2" (assert) nil))))))
nil)
((int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(value const-decl "real" IEEE_854_values nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Sum_zero formula-decl nil sum_hack nil)
(d_zero const-decl "digits" IEEE_854_values nil)
(minus_int_is_int application-judgement "int" integers nil)
(expt_nonzero formula-decl nil exponentiation nil)
(Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values
nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
nil)
(E_max formal-const-decl "integer" IEEE_854_values nil)
(integer nonempty-type-from-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(digits type-eq-decl nil IEEE_854_values nil)
(b formal-const-decl "above(1)" IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(p formal-const-decl "above(1)" IEEE_854_values nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil) (Sum def-decl "real" sum_hack 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(zero_times3 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(value_of_zero 0
(value_of_zero-1 nil 3321199176
("" (rewrite "value0")
(("" (expand "pos_zero") (("" (propax) nil)))) nil)
((pos_zero const-decl "{fin | zero?(fin)}" IEEE_854_values nil)
(zero? const-decl "bool" IEEE_854_values nil)
(bool nonempty-type-eq-decl nil booleans nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(boolean nonempty-type-decl nil booleans nil)
(fp_num type-decl nil IEEE_854_values nil)
(value0 formula-decl nil IEEE_854_values nil))
nil))
(normal_value 0
(normal_value-1 nil 3321199176
("" (skosimp*)
(("" (case-replace "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
(("1" (hide -1)
(("1"
(case "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
value(finite(s,n+E_min,d))=value(normalize(finite(s,n+E_min,d)))")
(("1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (induct "n" 1 "upto_induction[E_max-E_min]")
(("1" (skosimp*)
(("1" (expand "normalize") (("1" (propax) nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "normalize")
(("2" (lift-if)
(("2" (ground)
(("2" (inst?)
(("2" (replace -3 :dir rl)
(("2" (hide -3)
(("2" (expand "value")
(("2"
(expand "value_digit")
(("2"
(case-replace
"Sum(p,(LAMBDA (n: nat):
IF n < p THEN shift_left(d!1)(n) * (b ^ (-n))
ELSE 0
ENDIF))=b*Sum(p,(LAMBDA (n: nat): IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))")
(("1"
(hide -1)
(("1"
(lemma "expt_plus")
(("1"
(inst - "1" "E_min+jt!1" "b")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(rewrite "expt_x1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
--> --------------------
--> maximum size reached
--> --------------------
[ Verzeichnis aufwärts0.95unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
