|
(real_to_fp
(truncate_zero 0
(truncate_zero-1 nil 3321205307
("" (skosimp*)
(("" (apply-extensionality)
(("" (expand "truncate")
(("" (expand "d_zero")
(("" (assert)
(("" (lemma "div_eq_zero")
(("" (assert)
(("" (rewrite "floor_int")
(("" (rewrite "mod_zero") nil))))))))))))))))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil) (> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(below type-eq-decl nil naturalnumbers nil)
(b formal-const-decl "above(1)" real_to_fp nil)
(d_zero const-decl "digits" IEEE_854_values nil)
(digits type-eq-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(truncate const-decl "[below(p) -> below(b)]" fp_round_aux nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(integer nonempty-type-from-decl nil integers nil)
(div_eq_zero formula-decl nil real_props nil)
(floor_int formula-decl nil floor_ceil nil)
(mod_zero formula-decl nil mod nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(nil application-judgement "below(m)" mod nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil))
nil))
(digits_of_finite 0
(digits_of_finite-1 nil 3321205307
("" (skosimp*)
(("" (rewrite "abs_value_fin")
((""
(case "b ^ (Exp(fin!1)) * Sum(p, value_digit(d(fin!1))) >=0")
(("1" (apply-extensionality)
(("1" (hide 2)
(("1" (rewrite "truncate")
(("1" (assert)
(("1"
(case-replace "(b ^ (x!1 - Exp(fin!1))
*
(b ^ (Exp(fin!1))
* Sum(p, value_digit(d(fin!1))))) =
Sum(p, value_digit(d(fin!1)))*b^x!1")
(("1" (hide -1 -2)
(("1" (lemma "floor_Sum")
(("1" (inst?)
(("1" (replace -1)
(("1" (hide -1)
(("1" (lemma "mod_Sum")
(("1" (inst?) nil)))))))))))))
("2" (hide -1 2)
(("2" (assert)
(("2" (lemma "expt_plus")
(("2" (inst?)
(("2" (inst - "Exp(fin!1)")
(("2" (assert) nil)))))))))))))))))))))
("2" (lemma "expt_pos")
(("2" (inst?)
(("2" (lemma "Sum_nonneg")
(("2" (inst?)
(("2" (rewrite "pos_times_ge")
(("2" (assert) nil))))))))))))))))
nil)
((abs_value_fin formula-decl nil IEEE_854_values nil)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" 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)" real_to_fp nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(expt_pos formula-decl nil exponentiation nil)
(Sum_nonneg formula-decl nil sum_hack nil)
(pos_times_ge formula-decl nil real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(truncate const-decl "[below(p) -> below(b)]" fp_round_aux nil)
(fin!1 skolem-const-decl "(finite?)" real_to_fp nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nil application-judgement "below(m)" mod nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posint_exp application-judgement "posint" exponentiation nil)
(floor_Sum formula-decl nil IEEE_854_values nil)
(mod_Sum formula-decl nil IEEE_854_values nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(expt_plus formula-decl nil exponentiation nil)
(>= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values
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))
nil))
(real_to_fp_TCC1 0
(real_to_fp_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(real_to_fp_TCC2 0
(real_to_fp_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)
(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)
(int_plus_int_is_int application-judgement "int" integers nil)
(minus_int_is_int application-judgement "int" integers nil))
nil))
(real_to_fp_TCC3 0
(real_to_fp_TCC3-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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(real_to_fp_TCC4 0
(real_to_fp_TCC4-1 nil 3321205307
("" (skosimp*)
(("" (lemma "expt_pos") (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil)
((expt_pos formula-decl nil 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(b formal-const-decl "above(1)" real_to_fp 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}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp 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 nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(real_to_fp_TCC5 0
(real_to_fp_TCC5-1 nil 3321205307
("" (skosimp)
(("" (case "abs(r!1)>0")
(("1" (typepred "Exp_of(abs(r!1))")
(("1" (ground)
(("1" (case "b^E_min<= abs(r!1)")
(("1" (lemma "both_sides_expt_gt1_lt")
(("1" (inst - "b" "E_min" "(1 + Exp_of(abs(r!1)))")
(("1" (assert) nil)))))
("2" (assert) nil)))
("2" (case "abs(r!1))
(("1" (lemma "both_sides_expt_gt1_lt")
(("1" (inst - "b" "Exp_of(abs(r!1))" "1+E_max")
(("1" (assert) nil)))))
("2" (assert) nil)))))
("2" (skosimp*) (("2" (assert) nil)))
("3" (skosimp*) (("3" (assert) nil))) ("4" (propax) nil)))
("2" (lemma "expt_pos")
(("2" (inst - "E_min" "b")
(("1" (assert) nil) ("2" (assert) nil))))))))
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)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(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)" real_to_fp nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(Exp_of const-decl "{i: int | b ^ i <= x & x < b ^ (i + 1)}"
fp_round_aux nil)
(expt_pos formula-decl nil exponentiation nil))
nil))
(real_to_fp_zero 0
(real_to_fp_zero-1 nil 3321205307
("" (rewrite "real_to_fp")
(("" (expand "abs")
(("" (lemma "expt_pos")
(("" (inst-cp - "(1+E_max)" "b")
(("" (assert)
(("" (hide -2)
(("" (inst?)
(("" (assert)
(("" (rewrite "truncate_zero")
(("" (expand "sign_of")
(("" (expand "pos_zero")
(("" (propax) nil))))))))))))))))))))))
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)
(numfield nonempty-type-eq-decl nil 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" real_to_fp 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)" real_to_fp nil)
(sign_of const-decl "sign_rep" fp_round_aux nil)
(pos_zero const-decl "{fin | zero?(fin)}" IEEE_854_values nil)
(truncate_zero formula-decl nil real_to_fp nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(expt_pos formula-decl nil exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(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 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)
(real_to_fp const-decl "fp_num" real_to_fp nil))
nil))
(sign_of_value 0
(sign_of_value-1 nil 3321205307
("" (skosimp*)
(("" (expand "sign_of")
(("" (lift-if)
(("" (lemma "value_negative")
(("" (inst?)
(("" (ground)
(("" (expand "neg")
(("" (expand "pos")
(("" (assert)
(("" (typepred "sign(fin!1)")
(("" (assert) nil))))))))))))))))))))
nil)
((sign_of const-decl "sign_rep" fp_round_aux nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(b formal-const-decl "above(1)" real_to_fp 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)
(value_negative formula-decl nil IEEE_854_values nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pos const-decl "sign_rep" enumerated_type_defs nil)
(sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(neg const-decl "sign_rep" enumerated_type_defs nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil))
nil))
(Exp_of_value_normal_TCC1 0
(Exp_of_value_normal_TCC1-1 nil 3321205307
("" (skosimp*)
(("" (expand "abs")
(("" (lift-if)
(("" (ground)
(("" (lemma "finite_disjoint1")
(("" (inst?)
(("" (expand "zero?") (("" (propax) nil))))))))))))))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil)
(zero? const-decl "bool" IEEE_854_values nil)
(finite_disjoint1 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)" real_to_fp nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp
nil))
nil))
(Exp_of_value_normal 0
(Exp_of_value_normal-1 nil 3321205307
("" (skosimp*)
(("" (rewrite "normal_value")
(("" (rewrite "abs_value_fin")
(("" (lemma "value_sig_lt_b")
(("" (lemma "value_sig_ge1")
(("" (expand "normal?")
(("" (assert)
(("" (inst?)
(("" (assert)
(("" (inst?)
(("" (lemma "expt_pos")
(("" (inst?)
((""
(case "(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1)))))>0")
(("1" (assert)
(("1"
(typepred
"Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1)))))")
(("1"
(lemma "div_mult_pos_lt2")
(("1"
(inst
-
"b ^ (Exp(normalize(fin!1)))"
"Sum(p, value_digit(d(normalize(fin!1))))"
"b
^
(1
+
Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))")
(("1"
(replace -1 :dir rl)
(("1"
(hide -1)
(("1"
(lemma "div_mult_pos_le1")
(("1"
(inst
-
"b ^ (Exp(normalize(fin!1)))"
"Sum(p, value_digit(d(normalize(fin!1))))"
"b
^
( Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))")
(("1"
(replace -1 :dir rl)
(("1"
(hide -1)
(("1"
(rewrite "expt_div")
(("1"
(rewrite
"expt_div")
(("1"
(case
"(Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))
> (Exp(normalize(fin!1)))")
(("1"
(lemma
"expt_gt1_pos")
(("1"
(inst
-
"b"
"(Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))
- (Exp(normalize(fin!1)))")
(("1"
(assert)
nil)
("2"
(assert)
nil)))))
("2"
(lemma
"expt_gt1_nonpos")
(("2"
(inst
-
"b"
"-((1
+
Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))
- (Exp(normalize(fin!1))))")
(("1"
(assert)
nil)
("2"
(assert)
nil)))))))))))))))))))))))))))))))
("2" (rewrite "pos_times_gt")
(("2"
(assert)
nil))))))))))))))))))))))))))))
nil)
((normal_value formula-decl nil IEEE_854_values nil)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" 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)" real_to_fp nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(value_sig_lt_b formula-decl nil IEEE_854_values nil)
(normal? const-decl "bool" IEEE_854_values nil)
(d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil)
(digits type-eq-decl nil IEEE_854_values nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values
nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_div formula-decl nil exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(fin!1 skolem-const-decl "(finite?)" real_to_fp nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt_gt1_pos formula-decl nil exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(expt_gt1_nonpos formula-decl nil exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(Exp_of const-decl "{i: int | b ^ i <= x & x < b ^ (i + 1)}"
fp_round_aux nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(Sum def-decl "real" sum_hack nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(expt_pos formula-decl nil exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(value_sig_ge1 formula-decl nil IEEE_854_values nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(normalize def-decl "(finite?)" IEEE_854_values nil)
(abs_value_fin formula-decl nil IEEE_854_values nil))
nil))
(real_to_fp_normal 0
(real_to_fp_normal-1 nil 3321205307
("" (skosimp*)
(("" (rewrite "real_to_fp")
(("" (lift-if)
(("" (lemma "value_normal")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (assert)
(("" (case "max_pos < b^(1+E_max)")
(("1" (assert)
(("1" (hide -1 -2 -3)
(("1" (rewrite "Exp_of_value_normal")
(("1" (lemma "finite_disjoint1")
(("1" (inst?)
(("1"
(assert)
(("1"
(rewrite "normal_value")
(("1"
(rewrite "sign_of_value")
(("1"
(assert)
(("1"
(rewrite "digits_of_finite")
(("1"
(rewrite "fp_num_finite_eta")
nil)))))
("2"
(expand "zero?")
(("2"
(rewrite "normal_value" +)
nil)))))))))))))))))))
("2" (hide 2)
(("2" (hide -1 -2 -3)
(("2" (lemma "max_fp_correct")
(("2" (lemma "expt_pos")
(("2" (inst - "(E_max-(p-1))" "b")
(("2"
(assert)
nil))))))))))))))))))))))))))))
nil)
((real_to_fp const-decl "fp_num" real_to_fp 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)" real_to_fp nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(value const-decl "real" IEEE_854_values nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(value_normal formula-decl nil IEEE_854_values nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max_fp_correct formula-decl nil IEEE_854_values nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(expt_pos formula-decl nil exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Exp_of_value_normal formula-decl nil real_to_fp nil)
(normal_value formula-decl nil IEEE_854_values nil)
(zero? const-decl "bool" IEEE_854_values nil)
(fp_num_finite_eta formula-decl nil IEEE_854_values nil)
(digits_of_finite formula-decl nil real_to_fp nil)
(sign_of_value formula-decl nil real_to_fp nil)
(normalize def-decl "(finite?)" IEEE_854_values nil)
(finite_disjoint1 formula-decl nil IEEE_854_values nil)
(< const-decl "bool" reals 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)
(max_pos const-decl "posreal" IEEE_854_values nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(real_to_fp_subnormal 0
(real_to_fp_subnormal-1 nil 3321205307
("" (skosimp*)
(("" (rewrite "real_to_fp")
(("" (lemma "value_subnormal")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (assert)
(("" (case "b^E_min < b^(1+E_max)")
(("1" (assert)
(("1" (rewrite "normal_value")
(("1" (rewrite "sign_of_value")
(("1" (hide -1)
(("1" (expand "subnormal?")
(("1" (assert)
(("1"
(ground)
(("1"
(lemma "digits_of_finite")
(("1"
(inst?)
(("1"
(lemma "fp_num_finite_eta")
(("1"
(inst?)
(("1"
(replace -5)
(("1"
(replace -2)
(("1"
(propax)
nil)))))))))))))))))))))
("2" (expand "subnormal?")
(("2" (ground)
(("2" (expand "zero?")
(("2"
(assert)
(("2"
(rewrite "normal_value" +)
nil)))))))))))))))
("2" (hide -1 -2 -3 2)
(("2" (rewrite "both_sides_expt_gt1_lt")
nil))))))))))))))))))
nil)
((real_to_fp const-decl "fp_num" real_to_fp 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)" real_to_fp nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(value const-decl "real" IEEE_854_values nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(< const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(normal_value formula-decl nil IEEE_854_values nil)
(zero? const-decl "bool" IEEE_854_values nil)
(digits_of_finite formula-decl nil real_to_fp nil)
(fp_num_finite_eta formula-decl nil IEEE_854_values nil)
(subnormal? const-decl "bool" IEEE_854_values nil)
(sign_of_value formula-decl nil real_to_fp nil)
(normalize def-decl "(finite?)" IEEE_854_values 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(value_subnormal formula-decl nil IEEE_854_values nil))
nil))
(real_to_fp_inverts_value 0
(real_to_fp_inverts_value-1 nil 3321205307
("" (skosimp*)
(("" (lemma "finite_cover")
(("" (inst?)
(("" (ground)
(("1" (rewrite "real_to_fp_normal") nil)
("2" (rewrite "real_to_fp_subnormal") nil))))))))
nil)
((E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(b formal-const-decl "above(1)" real_to_fp 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)
(finite_cover formula-decl nil IEEE_854_values nil)
(real_to_fp_normal formula-decl nil real_to_fp nil)
(real_to_fp_subnormal formula-decl nil real_to_fp nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil))
nil))
(round_exceptions_x_TCC1 0
(round_exceptions_x_TCC1-1 nil 3321205307
("" (skolem-typepred)
(("" (expand "over_under?") (("" (ground) nil)))) nil)
((over_under? const-decl "bool" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(alpha formal-const-decl "integer" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(b formal-const-decl "above(1)" real_to_fp nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(round_exceptions_x_TCC2 0
(round_exceptions_x_TCC2-1 nil 3321205307
("" (skolem-typepred)
(("" (expand "over_under?") (("" (ground) nil)))) nil)
((over_under? const-decl "bool" over_under nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(alpha formal-const-decl "integer" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(b formal-const-decl "above(1)" real_to_fp nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(fp_round_TCC1 0
(fp_round_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal 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}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(b formal-const-decl "above(1)" real_to_fp 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)
(alpha formal-const-decl "integer" real_to_fp nil)
(over_under? const-decl "bool" over_under 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))
(round_value 0
(round_value-1 nil 3321205307
("" (skosimp*)
(("" (expand "fp_round")
(("" (expand "round_scaled")
(("" (assert)
(("" (lift-if)
(("" (assert)
(("" (ground)
(("" (expand "scale")
(("" (rewrite "Exp_of_value_normal")
(("1" (rewrite "round_int")
(("1" (rewrite "expt_inverse")
(("1" (assert) nil)))
("2" (hide 2 3 4)
(("2"
(case "integer?(value(fin!1)*b^(-(1 + Exp(normalize(fin!1)) - p)))")
(("1" (expand "integer?")
(("1" (assert) (("1" (ground) nil)))))
("2" (hide 2)
(("2" (rewrite "normal_value")
(("2"
(expand "value")
(("2"
(case-replace
"(Sum(p, value_digit(d(normalize(fin!1))))
* (-1) ^ sign(normalize(fin!1))
* b ^ Exp(normalize(fin!1))
* b ^ (-(1 + Exp(normalize(fin!1)) - p))) =
(-1) ^ sign(normalize(fin!1))
* Sum(p, value_digit(d(normalize(fin!1))))
* b ^ (p-1)")
(("1"
(hide -1)
(("1"
(case-replace
"((-1) ^ sign(normalize(fin!1))
* Sum(p, value_digit(d(normalize(fin!1))))
* b ^ (p - 1)) = ((-1) ^ sign(normalize(fin!1))
* Sum(p, scale_value_p(d(normalize(fin!1)))))")
(("1"
(hide -1)
(("1"
(case
"FORALL (i,j:int): integer?(i*j)")
(("1"
(inst?)
(("1"
(hide 2)
(("1"
(case
"forall (n:nat),(d:digits): integer?(Sum(n,scale_value_p(d)))")
(("1"
(expand "integer?")
(("1" (inst?) nil)))
("2"
(hide 2)
(("2"
(induct "n")
(("1"
(expand "Sum")
(("1"
(expand
"integer?")
(("1"
(propax)
nil)))))
("2"
(skosimp*)
(("2"
(rewrite "Sum")
(("2"
(inst?)
(("2"
(case
"FORALL (i,j:int): integer?(i+j)")
(("1"
(inst?)
(("1"
(expand
"integer?")
(("1"
(propax)
nil)))))
("2"
(hide
-1
2)
(("2"
(skosimp*)
(("2"
(expand
"integer?")
(("2"
(propax)
nil)))))))))))))))))))))))))
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(expand "integer?")
(("2"
(propax)
nil)))))))))))
("2"
(hide 2)
(("2"
(assert)
(("2"
(lemma "scaled_Sum")
(("2"
(inst?)
(("2"
(assert)
nil)))))))))))))
("2"
(hide 2)
(("2"
(assert)
(("2"
(lemma "expt_plus")
(("2"
(inst
-
"Exp(normalize(fin!1))"
"(-(1+Exp(normalize(fin!1)) - p))"
"b")
(("2"
(assert)
nil)))))))))))))))))))))))
("2" (hide 3)
(("2" (expand "over_under?")
(("2" (lemma "value_subnormal")
(("2" (inst?)
(("2" (ground)
(("2"
(lemma "finite_cover")
(("2"
(inst?)
(("2"
(expand "zero?")
(("2"
(propax)
nil))))))))))))))))))))))))))))))))))
nil)
((fp_round const-decl "real" real_to_fp nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(scale const-decl
"{i: int | b ^ (i + p - 1) <= x & x < b ^ (i + p)}"
fp_round_aux nil)
(value_subnormal formula-decl nil IEEE_854_values nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero? const-decl "bool" IEEE_854_values nil)
(finite_cover formula-decl nil IEEE_854_values nil)
(over_under? const-decl "bool" over_under nil)
(round_int formula-decl nil round nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(Exponent type-eq-decl nil IEEE_854_values nil)
(Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values
nil)
(normalize def-decl "(finite?)" IEEE_854_values nil)
(value const-decl "real" IEEE_854_values nil)
(rounding_mode type-decl nil enumerated_type_defs nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(expt_inverse formula-decl nil exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(integer? const-decl "bool" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(normal_value formula-decl nil IEEE_854_values nil)
(sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
nil)
(sign_rep type-eq-decl nil enumerated_type_defs nil)
(d adt-accessor-decl "[(finite?) -> 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)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil) (Sum def-decl "real" sum_hack nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(scale_value_p const-decl "nat" IEEE_854_values nil)
(j!1 skolem-const-decl "nat" real_to_fp nil)
(d!1 skolem-const-decl "digits[b, p, E_max, E_min]" real_to_fp nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(fin!1 skolem-const-decl "(finite?)" real_to_fp nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(scaled_Sum formula-decl nil IEEE_854_values nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(expt_plus formula-decl nil exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(b formal-const-decl "above(1)" real_to_fp 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)
(Exp_of_value_normal formula-decl nil real_to_fp nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(round_scaled const-decl "real" fp_round_aux nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(round_value2 0
(round_value2-1 nil 3321205307
("" (skosimp*)
(("" (rewrite "round_value")
(("" (expand "fp_round")
(("" (lift-if)
(("" (assert)
(("" (prop)
(("" (expand "round_exceptions")
(("" (expand "round_exceptions_x")
(("" (lemma "value_nonzero")
(("" (inst?)
(("" (assert)
(("" (expand "zero?")
(("" (lift-if)
(("" (prop)
(("1" (assert) nil)
("2"
(expand "over_under?")
(("2"
(assert)
(("2"
(expand "underflow")
(("2"
(lift-if)
(("2"
(assert)
(("2"
(rewrite "round_under_value")
(("2"
(lemma "finite_cover")
(("2"
(inst?)
(("2"
(expand "zero?")
(("2"
(lemma
"value_normal")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))))))))
nil)
((round_value formula-decl nil real_to_fp 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)" real_to_fp nil)
(p formal-const-decl "above(1)" real_to_fp nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" real_to_fp nil)
(E_min formal-const-decl "{i: integer | E_max > i}" real_to_fp nil)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(rounding_mode type-decl nil enumerated_type_defs nil)
(round_exceptions_x const-decl "[real, exception]" real_to_fp nil)
(zero? const-decl "bool" IEEE_854_values nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(alpha formal-const-decl "integer" real_to_fp nil)
(round_under_value formula-decl nil over_under nil)
(value_normal formula-decl nil IEEE_854_values nil)
(finite_cover formula-decl nil 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)
(underflow const-decl "[real, exception]" over_under nil)
(over_under? const-decl "bool" over_under nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(value_nonzero formula-decl nil IEEE_854_values nil)
(round_exceptions const-decl "real" real_to_fp nil)
(fp_round const-decl "real" real_to_fp nil))
nil))
(round_0 0
(round_0-1 nil 3321205307
("" (skosimp*) (("" (expand "fp_round") (("" (propax) nil)))) nil)
((fp_round const-decl "real" real_to_fp nil)) nil))
(round_value3 0
(round_value3-1 nil 3321205307
("" (skosimp*)
(("" (rewrite "round_value2")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.63 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.
|
