|
(IEEE_link
(Significand_size_TCC1 0
(Significand_size_TCC1-1 nil 3321372494 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(IMP_IEEE_854_TCC1 0
(IMP_IEEE_854_TCC1-1 nil 3321372494
("" (assuming-tcc)
(("" (lemma "Base_values") (("" (assert) nil nil)) nil)) nil)
((Base_values formula-decl nil IEEE_link nil)) nil))
(IMP_IEEE_854_TCC2 0
(IMP_IEEE_854_TCC2-1 nil 3321372494
("" (assuming-tcc)
(("" (lemma "Exponent_range") (("" (propax) nil nil)) nil)) nil)
((Exponent_range formula-decl nil IEEE_link nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(IMP_IEEE_854_TCC3 0
(IMP_IEEE_854_TCC3-1 nil 3321372494
("" (lemma "Significand_size") (("" (propax) nil nil)) nil)
((Significand_size formula-decl nil IEEE_link nil)) nil))
(IMP_IEEE_854_TCC4 0
(IMP_IEEE_854_TCC4-1 nil 3321372494
("" (lemma "E_balance") (("" (propax) nil nil)) nil)
((E_balance formula-decl nil IEEE_link nil)) nil))
(IMP_IEEE_854_TCC5 0
(IMP_IEEE_854_TCC5-1 nil 3321372494
("" (lemma "Exponent_Adjustment") (("" (propax) nil nil)) nil)
((Exponent_Adjustment formula-decl nil IEEE_link nil)) nil))
(b_TCC1 0
(b_TCC1-1 nil 3321373471
("" (lemma "E_min_neg") (("" (assert) nil nil)) nil)
((minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(E_min_neg formula-decl nil IEEE_854 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)
(radix formal-const-decl "above(1)" IEEE_link nil)
(p formal-const-decl "above(1)" IEEE_link nil)
(integer nonempty-type-from-decl nil integers nil)
(alpha formal-const-decl "integer" IEEE_link nil)
(E_max formal-const-decl "integer" IEEE_link nil)
(E_min formal-const-decl "integer" IEEE_link nil))
nil))
(IEEE_to_float_TCC1 0
(IEEE_to_float_TCC1-1 nil 3321373471
("" (skeep)
(("" (lemma "E_max_gt_E_min") (("" (propax) nil nil)) nil)) nil)
((E_min formal-const-decl "integer" IEEE_link nil)
(E_max formal-const-decl "integer" IEEE_link nil)
(alpha formal-const-decl "integer" IEEE_link nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_link nil)
(radix formal-const-decl "above(1)" IEEE_link 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)
(E_max_gt_E_min formula-decl nil IEEE_854 nil))
nil))
(IEEE_to_float_TCC2 0
(IEEE_to_float_TCC2-1 nil 3321373471
("" (skeep) (("" (assert) nil nil)) nil) nil nil))
(IEEE_to_float_TCC3 0
(IEEE_to_float_TCC3-1 nil 3321614391
("" (skeep)
(("" (lemma "E_max_gt_E_min") (("" (propax) nil nil)) nil)) nil)
((E_min formal-const-decl "integer" IEEE_link nil)
(E_max formal-const-decl "integer" IEEE_link nil)
(alpha formal-const-decl "integer" IEEE_link nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_link nil)
(radix formal-const-decl "above(1)" IEEE_link 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)
(E_max_gt_E_min formula-decl nil IEEE_854 nil))
nil))
(IEEE_to_float_TCC4 0
(IEEE_to_float_TCC4-1 nil 3321373471
("" (skeep)
(("" (case "FORALL (i,j:int): integer?(i*j)")
(("1"
(inst -1 "(-1) ^ sign[radix, p, E_max, E_min](ieee)"
"radix ^ (p - 1)
*
Sum(p,
value_digit[radix, p, E_max, E_min]
(d[radix, p, E_max, E_min](ieee)))")
(("1" (expand "integer?")
(("1" (flatten) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2"
(case "FORALL (d:digits),(n:upto(p)): rational_pred(radix ^ (p - 1) *
Sum(n,
value_digit[radix, p, E_max, E_min]
(d)))
AND
integer_pred(radix ^ (p - 1) *
Sum(n,
value_digit[radix, p, E_max, E_min]
(d)))")
(("1" (inst -1 "d[radix, p, E_max, E_min](ieee)" "p") nil
nil)
("2" (hide 2)
(("2" (induct "n" 1 "upto_induction[p]")
(("1" (expand "Sum") (("1" (propax) nil nil)) nil)
("2" (skosimp*)
(("2" (inst -2 "d!1")
(("2" (flatten)
(("2" (rewrite "Sum" 1)
(("2" (assert)
(("2"
(case " rational_pred(value_digit[radix, p, E_max, E_min](d!1)(jt!1) *
radix ^ (p - 1)) AND
integer_pred(value_digit[radix, p, E_max, E_min](d!1)(jt!1) *
radix ^ (p - 1))")
(("1"
(case "FORALL (i,j:int): integer?(i+j)")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "integer?")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skosimp*)
(("2"
(expand "integer?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide -2 -3 2)
(("2"
(split)
(("1"
(expand "value_digit")
(("1" (propax) nil nil))
nil)
("2"
(expand "value_digit")
(("2"
(case-replace
"d!1(jt!1) * radix ^ (p - 1) * radix ^ (-jt!1)=
d!1(jt!1) *(radix ^ (p - 1) * radix ^ (-jt!1))")
(("1"
(rewrite "expt_plus" :dir rl)
(("1"
(hide -1)
(("1"
(case
"FORALL (i,j:int): integer?(i*j)")
(("1"
(inst?)
(("1"
(expand "integer?")
(("1" (propax) nil nil))
nil)
("2"
(grind-reals)
(("2"
(case
"0 <= (-jt!1) - 1 + p ")
(("1"
(assert)
(("1"
(expand "^")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(skeep)
(("2"
(expand "integer?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)
("4" (hide 2)
(("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)
("4" (hide 2)
(("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil))
nil))
nil)
("3" (hide 2) (("3" (grind-reals) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (expand "integer?") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(integer? const-decl "bool" integers 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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_plus formula-decl nil exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(jt!1 skolem-const-decl "upto(p)" IEEE_link nil)
(d!1 skolem-const-decl "digits[radix, p, E_max, E_min]" IEEE_link
nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(upto_induction formula-decl nil bounded_nat_inductions nil)
(pred type-eq-decl nil defined_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
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)
(alpha formal-const-decl "integer" IEEE_link nil)
(E_max_gt_E_min formula-decl nil IEEE_854 nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation 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)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" IEEE_link nil)
(E_min formal-const-decl "integer" IEEE_link 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)
(fp_num type-decl nil IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil)
(ieee skolem-const-decl "(finite?[radix, p, E_max, E_min])"
IEEE_link nil)
(p formal-const-decl "above(1)" IEEE_link nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(radix formal-const-decl "above(1)" IEEE_link nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation 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))
nil))
(IEEE_to_float_TCC5 0
(IEEE_to_float_TCC5-1 nil 3321373471
("" (skeep)
((""
(case "value[radix, p, E_max, E_min](ieee) =
FtoR[radix]
((# Fnum
:= (-1) ^ sign[radix, p, E_max, E_min](ieee) *
radix ^ (p - 1)
*
Sum(p,
value_digit[radix, p, E_max, E_min]
(d[radix, p, E_max, E_min](ieee))),
Fexp := Exp[radix, p, E_max, E_min](ieee) + 1 - p #))")
(("1" (split)
(("1" (hide -1)
(("1" (expand "Fbounded?")
(("1" (split)
(("1" (expand "vNum")
(("1" (expand "b")
(("1" (rewrite "abs_mult")
(("1" (rewrite "abs_mult")
(("1" (lemma "Sum_nonneg")
(("1" (inst?)
(("1" (expand "abs" 1 1)
(("1" (grind-reals)
(("1"
(case-replace
"abs((-1) ^ sign[radix, p, E_max, E_min](ieee))=1")
(("1"
(expand "abs" 1 1)
(("1"
(lemma "value_sig_lt_b")
(("1"
(inst?)
(("1"
(case-replace
" radix ^ p=radix*radix^ (p - 1)")
(("1"
(div-by 1 "radix ^ (p - 1)")
nil
nil)
("2"
(lemma "expt_plus")
(("2"
(inst -1 "1" "p-1" "radix")
(("2"
(rewrite "expt_x1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(typepred
"sign[radix, p, E_max, E_min](ieee)")
(("2"
(split)
(("1"
(rewrite -1)
(("1"
(expand* "^" "expt" "abs")
nil
nil))
nil)
("2"
(replace -1)
(("2"
(expand* "^" "expt" "abs")
(("2"
(expand "expt")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "b") (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (replace -1 :dir rl)
(("3" (hide -1)
(("3" (lemma "finite_cover")
(("3" (inst?)
(("3" (split)
(("1" (expand "zero?")
(("1" (replace -1)
(("1" (expand "abs") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "value_normal")
(("2" (inst?)
(("2" (split)
(("1" (flatten)
(("1" (trans-ineq 1 " max_pos" :strict 2)
(("1" (rewrite "max_fp_correct")
(("1" (grind-reals) nil nil)) nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("3" (lemma "value_subnormal")
(("3" (inst?)
(("3" (split)
(("1" (flatten)
(("1"
(trans-ineq 1 "radix ^ E_min" :strict 1)
(("1" (rewrite "Exp_increq_1")
(("1"
(lemma "E_max_gt_E_min")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "FtoR")
(("2" (expand "value")
(("2"
(case "Sum(p, value_digit(d(ieee))) * (-1) ^ sign(ieee) * radix ^ Exp(ieee)
=
Sum(p,
value_digit[radix, p, E_max, E_min]
(d[radix, p, E_max, E_min](ieee)))
* (-1) ^ sign[radix, p, E_max, E_min](ieee)
* (radix ^ (p - 1)
* radix ^ (1+Exp[radix, p, E_max, E_min](ieee) - p))")
(("1" (rewrite -1) nil nil)
("2" (hide 2)
(("2" (rewrite "expt_plus" :dir rl) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "IEEE_to_float_TCC4")
(("3" (inst?) (("3" (flatten) (("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("4" (hide 2) (("4" (flatten) (("4" (assert) nil nil)) nil))
nil))
nil))
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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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 "[numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(>= const-decl "bool" reals 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)
(FtoR const-decl "real" float nil)
(float type-eq-decl nil float nil)
(value const-decl "real" IEEE_854_values nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil)
(E_min formal-const-decl "integer" IEEE_link nil)
(E_max formal-const-decl "integer" IEEE_link nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_link nil)
(radix formal-const-decl "above(1)" IEEE_link 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
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)
(finite_cover formula-decl nil IEEE_854_values nil)
(zero? const-decl "bool" IEEE_854_values nil)
(max_fp_correct formula-decl nil IEEE_854_values nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(max_pos const-decl "posreal" IEEE_854_values nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(value_normal formula-decl nil IEEE_854_values nil)
(Exp_increq_1 formula-decl nil float nil)
(value_subnormal formula-decl nil IEEE_854_values nil)
(b const-decl "Format" IEEE_link nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(alpha formal-const-decl "integer" IEEE_link nil)
(E_max_gt_E_min formula-decl nil IEEE_854 nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint_exp application-judgement "posint" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x1 formula-decl nil exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(times_div_cancel2 formula-decl nil extra_real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(value_sig_lt_b formula-decl nil IEEE_854_values nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(Sum_nonneg formula-decl nil sum_hack nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(abs_mult formula-decl nil real_props nil)
(vNum const-decl "posnat" float nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Fbounded? const-decl "bool" float nil)
(IEEE_to_float_TCC4 subtype-tcc nil IEEE_link 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))
nil))
(float_to_IEEE_TCC1 0
(float_to_IEEE_TCC1-1 nil 3321378670
("" (skeep) (("" (assert) nil nil)) nil) nil nil))
(float_to_IEEE_TCC2 0
(float_to_IEEE_TCC2-1 nil 3321378670
("" (skosimp*)
(("" (typepred "f!1")
(("" (split)
(("1" (case "Fbounded?(b)(f!1)")
(("1" (expand* "Fbounded?" "b")
(("1" (flatten) (("1" (assert) nil nil)) nil)) nil)
("2" (rewrite "FcanonicBounded") nil nil))
nil)
("2" (expand "Fcanonic?")
(("2" (split)
(("1" (expand "Fnormal?")
(("1" (flatten)
(("1" (case " Fexp(f!1) + p - 1 < E_max + 1")
(("1" (assert) nil nil)
("2" (rewrite "Exp_incr_2")
(("2" (hide 2 3)
(("2" (trans-ineq 1 "abs(FtoR(f!1))" :strict 2)
(("2" (rewrite "expt_plus")
(("2" (rewrite "expt_div" :dir rl)
(("2" (expand "FtoR")
(("2"
(rewrite "abs_mult")
(("2"
(expand "abs" 1 2)
(("2"
(rewrite "abs_mult")
(("2"
(expand "abs" -2 1)
(("2"
(case-replace
"vNum(b)=radix ^ p")
(("1"
(div-by
1
"radix ^ Fexp(f!1)")
(("1" (field 1) nil nil))
nil)
("2"
(expand "b")
(("2"
(expand "vNum")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "Fsubnormal?" "b")
(("2" (flatten)
(("2" (rewrite -2)
(("2" (lemma "E_max_gt_E_min")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((E_max formal-const-decl "integer" IEEE_link nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(FtoR const-decl "real" float 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)
(b const-decl "Format" IEEE_link nil)
(Fcanonic? const-decl "bool" float nil)
(float type-eq-decl nil float nil)
(Format type-eq-decl nil float nil)
(radix formal-const-decl "above(1)" IEEE_link 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)
(above nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Fsubnormal? const-decl "bool" float nil)
(E_min formal-const-decl "integer" IEEE_link nil)
(alpha formal-const-decl "integer" IEEE_link nil)
(E_max_gt_E_min formula-decl nil IEEE_854 nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(Fnormal? const-decl "bool" float nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(p formal-const-decl "above(1)" IEEE_link nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_plus formula-decl nil exponentiation nil)
(posint_exp application-judgement "posint" exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(times_div_cancel2 formula-decl nil extra_real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(div_cancel2 formula-decl nil real_props nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(vNum const-decl "posnat" float nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(abs_mult formula-decl nil real_props nil)
(expt_x1 formula-decl nil exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(expt_div formula-decl nil exponentiation nil)
(<= const-decl "bool" reals nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(Exp_incr_2 formula-decl nil float nil)
(Fbounded? const-decl "bool" float nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(FcanonicBounded formula-decl nil float nil))
nil))
(float_to_IEEE_TCC3 0
(float_to_IEEE_TCC3-1 nil 3321378670
("" (skosimp*)
(("" (typepred "f!1") (("" (grind-reals) nil nil)) nil)) nil)
((E_max formal-const-decl "integer" IEEE_link nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(FtoR const-decl "real" float 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)
(b const-decl "Format" IEEE_link nil)
(Fcanonic? const-decl "bool" float nil)
(float type-eq-decl nil float nil)
(Format type-eq-decl nil float nil)
(radix formal-const-decl "above(1)" IEEE_link 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)
(above nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(float_to_IEEE_TCC4 0
(float_to_IEEE_TCC4-1 nil 3321381545
("" (skeep)
(("" (lemma "E_max_gt_E_min") (("" (propax) nil nil)) nil)) nil)
((E_min formal-const-decl "integer" IEEE_link nil)
(E_max formal-const-decl "integer" IEEE_link nil)
(alpha formal-const-decl "integer" IEEE_link nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" IEEE_link nil)
(radix formal-const-decl "above(1)" IEEE_link 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)
(E_max_gt_E_min formula-decl nil IEEE_854 nil))
nil))
(float_to_IEEE_TCC5 0
(float_to_IEEE_TCC5-1 nil 3321381545
("" (skosimp*)
(("" (typepred "f!1")
(("" (expand* "FtoR" "value")
((""
(case-replace
"radix ^ (Fexp(f!1) - 1 + p)=radix ^ (Fexp(f!1))*radix^(p-1)")
(("1" (div-by 1 "radix ^ (Fexp(f!1))")
(("1" (field 1)
(("1"
(case " Sum(p,
value_digit(LAMBDA (i: below(p)):
mod(floor((radix ^ (1+i-p)) * abs(Fnum(f!1))), radix)))*(radix ^ (p - 1))=abs(Fnum(f!1))")
(("1"
(case "Fnum(f!1) =((-1) ^ sign_of[radix, p](Fnum(f!1)))* abs(Fnum(f!1))")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (expand* "sign_of" "pos" "neg" "abs")
(("2" (grind-reals)
(("1" (rewrite "expt_x1")
(("1" (assert) nil nil)) nil)
("2" (rewrite "expt_x0")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2 -1)
(("2"
(case "FORALL (j:upto(p)): Sum(j, value_digit(LAMBDA (i: below(p)):
mod(floor((radix ^ (1+i-p)) * abs(Fnum(f!1))), radix)))
* (radix ^ (j-1))
= floor(abs(Fnum(f!1))*radix^(j-p))")
(("1" (inst?)
(("1" (copy -2)
(("1" (rewrite -2)
(("1" (rewrite "expt_x0")
(("1" (assert)
(("1"
(lemma "floor_int")
(("1" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "j" 1 "upto_induction[p]")
(("1" (rewrite "Sum")
(("1" (lemma "floor_0")
(("1" (inst?)
(("1"
(flatten)
(("1"
(split -2)
(("1" (assert) nil nil)
("2" (grind-reals) nil nil)
("3"
(hide 2)
(("3"
(case-replace "0-p=-p")
(("1"
(rewrite "expt_inverse")
(("1"
(mult-by 1 "radix ^ p")
(("1"
(field 1)
(("1"
(case
"radix ^ p=vNum(b)")
(("1"
(expand*
"Fcanonic?"
"Fsubnormal?"
"Fnormal?"
"Fbounded?")
(("1"
(assert)
nil
nil))
nil)
("2"
(expand "b" 1)
(("2"
(expand "vNum")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "Sum" 1)
(("2" (assert)
(("2"
(case-replace
"Sum(jt!1,
value_digit(LAMBDA (i: below(p)):
mod(floor((radix ^ (1 + i - p)) * abs(Fnum(f!1))),
radix)))
* (radix ^ jt!1)=radix*floor(abs(Fnum(f!1)) * radix ^ (jt!1 - p))")
(("1"
(expand "value_digit")
(("1"
(hide -1 -3)
(("1"
(case-replace
"mod(floor((radix ^ (1 - p + jt!1)) * abs(Fnum(f!1))), radix) *
radix ^ (-jt!1)
* (radix ^ jt!1) = mod(floor((radix ^ (1 - p + jt!1)) * abs(Fnum(f!1))), radix) *
( radix ^ (-jt!1)* (radix ^ jt!1))")
(("1"
(rewrite "expt_plus" :dir rl)
(("1"
(assert)
(("1"
(case-replace
" mod(floor((radix ^ (1 - p + jt!1)) * abs(Fnum(f!1))), radix)
* radix ^ ((-jt!1) + jt!1)=mod(floor((radix ^ (1 - p + jt!1)) * abs(Fnum(f!1))), radix)")
(("1"
(case
"FORALL (n,j:int): mod(floor(radix^j*n),radix)+
radix*floor(radix^(j-1)*n)=floor(radix^j*n)")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(lemma "rem_floor")
(("2"
(lemma
"mod_to_rem")
(("2"
(inst
-2
"radix"
"floor(radix ^ j * n)")
(("2"
(case
"mod(floor(radix ^ j * n), radix) + radix * floor(radix ^ (j - 1) * n)
= rem(radix)(floor(radix ^ j * n)) +
radix * floor(floor(radix ^ j * n) / radix)")
(("1"
(assert)
nil
nil)
("2"
(hide 2 -2)
(("2"
(inst?)
(("2"
(rewrite
-1)
(("2"
(move-terms
1
l
1)
(("2"
(assert)
(("2"
(div-by
1
"radix")
(("2"
(case
"(FORALL (r:real): (floor(r)=floor(floor(radix*r)/radix)))")
(("1"
(inst
-1
"radix ^ (j - 1) * n")
(("1"
(case-replace
"radix ^ j=radix * (radix ^ (j - 1))")
(("1"
(assert)
nil
nil)
("2"
(lemma
"expt_plus")
(("2"
(inst
-1
"1"
"j-1"
"radix")
(("2"
(rewrite
"expt_x1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skeep)
(("2"
(case
"floor(floor(radix * r) / radix) <= r")
(("1"
(case
" r < floor(floor(radix * r) / radix)+1")
(("1"
(assert)
nil
nil)
("2"
(hide
-1
2)
(("2"
(move-terms
1
r
2)
(("2"
(trans-ineq
1
"floor(radix * r) / radix-1+1/radix"
:strict
1)
(("1"
(field
1)
nil
nil)
("2"
(field
1)
(("2"
(case
"floor(radix * r) - radix <
floor(floor(radix * r) / radix) * radix")
(("1"
(assert)
nil
nil)
("2"
(div-by
1
"radix")
(("2"
(grind-reals)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(trans-ineq
1
"floor(radix * r) / radix")
(("1"
(assert)
nil
nil)
("2"
(trans-ineq
1
"(radix * r)/radix")
(("1"
(grind-reals)
nil
nil)
("2"
(grind-reals)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.95 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.
|
