Impressum IEEE_link.prf
Interaktion und
(IEEE_linknil 3321372494 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3321372494"" (assuming-tcc)"" (lemma "Base_values" ) (("" (assert ) nil nil )) nil )) nil )nil IEEE_link nil )) nil ))nil 3321372494"" (assuming-tcc)"" (lemma "Exponent_range" ) (("" (propax) nil nil )) nil )) nil )nil IEEE_link nil )"int" integers nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321372494"" (lemma "Significand_size" ) (("" (propax) nil nil )) nil )nil IEEE_link nil )) nil ))nil 3321372494"" (lemma "E_balance" ) (("" (propax) nil nil )) nil )nil IEEE_link nil )) nil ))nil 3321372494"" (lemma "Exponent_Adjustment" ) (("" (propax) nil nil )) nil )nil IEEE_link nil )) nil ))nil 3321373471"" (lemma "E_min_neg" ) (("" (assert ) nil nil )) nil )"int" integers nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil IEEE_854 nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil ))nil ))nil 3321373471"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321373471"" (skeep) (("" (assert ) nil nil )) nil ) nil nil ))nil 3321614391"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321373471"" (skeep)"" (case "FORALL (i,j:int): integer?(i*j)" )"1" "(-1) ^ sign[radix, p, E_max, E_min](ieee)" "radix ^ (p - 1) ") "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) * AND ") "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) * AND ") "1" case "FORALL (i,j:int): integer?(i+j)" )"1" "1" assert )"1" expand "integer?" )"1" (propax) nil nil ))nil ))nil ))nil )"2" "2" "2" expand "integer?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 2)"2" "1" expand "value_digit" )"1" (propax) nil nil ))nil )"2" expand "value_digit" )"2" "d!1(jt!1) * radix ^ (p - 1) * radix ^ (-jt!1)= ") "1" rewrite "expt_plus" :dir rl)"1" "1" case "FORALL (i,j:int): integer?(i*j)" )"1" "1" expand "integer?" )"1" (propax) nil nil ))nil )"2" "2" case "0 <= (-jt!1) - 1 + p " )"1" assert )"1" expand "^" )"1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "integer?" )"2" 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 )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" integers nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )nil reals nil )nil exponentiation nil )"posrat" nil )"posrat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"posnat" exponentiation nil )"int" integers nil )"nonneg_rat" nil )"upto(p)" IEEE_link nil )"digits[radix, p, E_max, E_min]" IEEE_linknil )"int" integers nil )"real" reals nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil bounded_nat_inductions nil )nil defined_types nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"nzrat" rationalsnil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )"integer" IEEE_link nil )nil IEEE_854 nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )nil naturalnumbers nil )"real" sum_hack nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )nil integers nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil IEEE_854_values nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"[(finite?) -> digits]" IEEE_854_values nil )"(finite?[radix, p, E_max, E_min])" nil )"above(1)" IEEE_link nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"odd_int" integers nil )"int" exponentiation nil )"nzreal" exponentiation nil )"int" integers nil )"real" reals nil )"nnrat" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321373471"" (skeep)"" case "value[radix, p, E_max, E_min](ieee) = ") "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" "abs((-1) ^ sign[radix, p, E_max, E_min](ieee))=1" )"1" expand "abs" 1 1)"1" "value_sig_lt_b" )"1" "1" " radix ^ p=radix*radix^ (p - 1)" )"1" "radix ^ (p - 1)" )nil nil )"2" "expt_plus" )"2" "1" "p-1" "radix" )"2" rewrite "expt_x1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sign[radix, p, E_max, E_min](ieee)" )"2" "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" "radix ^ E_min" :strict 1)"1" (rewrite "Exp_increq_1" )"1" "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) ") "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 )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil IEEE_854_values nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[(finite?) -> digits]" IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )nil IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil ) (Sum def-decl "real" sum_hack nil )"[numfield, numfield -> numfield]" number_fields nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )nil enumerated_type_defs nil )nil naturalnumbers nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"bool" reals nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" float nil )nil float nil )"real" IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"odd_int" integers nil )"int" integers nil )"nzrat" rationalsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil IEEE_854_values nil )"bool" IEEE_854_values nil )nil IEEE_854_values nil )"rat" rationals nil )"posreal" IEEE_854_values nil )"[bool, bool -> bool]" booleans nil )nil IEEE_854_values nil )nil float nil )nil IEEE_854_values nil )"Format" IEEE_link nil )"{j: posint | j >= i}" nil )"integer" IEEE_link nil )nil IEEE_854 nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"posint" exponentiation nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )NOT const-decl "[bool -> bool]" booleans nil )nil exponentiation nil )nil exponentiation nil )nil reals nil )nil real_types nil )nil extra_real_props nil )nil reals nil )nil real_props nil )nil IEEE_854_values nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sum_hack nil )"nnreal" nil )"{r: posrat | r >= q}" nil )nil real_props nil )"posnat" float nil )"int" integers nil )"(total_order?[real])" nil )"bool" float nil )nil IEEE_link nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil ))nil ))nil 3321378670"" (skeep) (("" (assert ) nil nil )) nil ) nil nil ))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" "vNum(b)=radix ^ p" )"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 )"integer" IEEE_link nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" float nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )"Format" IEEE_link nil )"bool" float nil )nil float nil )nil float nil )"above(1)" IEEE_link nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integers nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" float nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil IEEE_854 nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" float nil )"[numfield, numfield -> numfield]" number_fields nil )"above(1)" IEEE_link nil )nil reals nil )nil exponentiation nil )"posint" exponentiation nil )"posrat" nil )"rat" rationals nil )nil real_props nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil extra_real_props nil )nil reals nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )"posnat" float nil )"nonneg_int" nil )"{j: posint | j >= i}" nil )"nonneg_rat" nil )"{r: posrat | r >= q}" nil )nil real_props nil )nil exponentiation nil )"posrat" nil )nil exponentiation nil )"bool" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil float nil )"bool" float nil )"(strict_total_order?[real])" real_props nil )"{j: nonneg_int | j >= i}" nil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil )"int" integers nil )nil float nil ))nil ))nil 3321378670"" (skosimp*)"" (typepred "f!1" ) (("" (grind-reals) nil nil )) nil )) nil )"integer" IEEE_link nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" float nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )"Format" IEEE_link nil )"bool" float nil )nil float nil )nil float nil )"above(1)" IEEE_link nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integers nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil ))nil ))nil 3321381545"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321381545"" (skosimp*)"" (typepred "f!1" )"" (expand * "FtoR" "value" )"" "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, LAMBDA (i: below(p)):") "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)): ") "1" (inst?)"1" (copy -2)"1" (rewrite -2)"1" (rewrite "expt_x0" )"1" (assert )"1" "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" "1" "1" (assert ) nil nil )"2" (grind-reals) nil nil )"3" "3" "0-p=-p" )"1" rewrite "expt_inverse" )"1" "radix ^ p" )"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" 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" "Sum(jt!1, LAMBDA (i: below(p)):") "1" expand "value_digit" )"1" "1" "mod(floor((radix ^ (1 - p + jt!1)) * abs(Fnum(f!1))), radix) * ") "1" rewrite "expt_plus" :dir rl)"1" assert )"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)+ ") "1" "1" assert )nil nil ))nil )"2" "2" "2" "rem_floor" )"2" "mod_to_rem" )"2" "radix" "floor(radix ^ j * n)" )"2" case "mod(floor(radix ^ j * n), radix) + radix * floor(radix ^ (j - 1) * n) ") "1" assert )nil nil )"2" "2" "2" rewrite "2" "2" assert )"2" "radix" )"2" case "(FORALL (r:real): (floor(r)=floor(floor(radix*r)/radix)))" )"1" "radix ^ (j - 1) * n" )"1" "radix ^ j=radix * (radix ^ (j - 1))" )"1" assert )nil nil )"2" "expt_plus" )"2" "1" "j-1" "radix" )"2" rewrite "expt_x1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "floor(floor(radix * r) / radix) <= r" )"1" case " r < floor(floor(radix * r) / radix)+1" )"1" assert )nil nil )"2" "2" "2" "floor(radix * r) / radix-1+1/radix" "1" nil nil )"2" "2" case "floor(radix * r) - radix < ") "1" assert )nil nil )"2" "radix" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "floor(radix * r) / radix" )"1" assert )nil nil )"2" "(radix * r)/radix" )"1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "(-jt!1) + jt!1=0" )"1" rewrite "expt_x0" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" rewrite -2 :dir rl)"2" " Sum(jt!1, LAMBDA (i: below(p)):") "1" "1" "expt_plus" )"1" "1" "jt!1 - 1" "radix" )"1" rewrite "expt_x1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "E_max_gt_E_min" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "E_max_gt_E_min" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (lemma "E_max_gt_E_min" ) (("3" (propax) nil nil ))nil ))nil )"2" (lemma "E_max_gt_E_min" ) (("2" (propax) nil nil ))nil ))nil )"2" (lemma "E_max_gt_E_min" ) (("2" (propax) nil nil ))nil ))nil )"2" (lemma "expt_plus" )"2" (inst -1 "Fexp(f!1)" "p-1" "radix" )"2" (assert ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"integer" IEEE_link nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" float nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )"Format" IEEE_link nil )"bool" float nil )nil float nil )nil float nil )"above(1)" IEEE_link nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integers nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"above(1)" IEEE_link nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"posrat" nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nzrat" rationalsnil )"nnreal" nil )"{f: (Fcanonic?(b)) | abs(FtoR(f)) < radix ^ (E_max + 1)}" nil )"upto(p)" IEEE_link nil )"nonneg_int" nil )nil mod_lems "ints/" )"rat" rationals nil )nil euclidean_division nil )"{r: mod(b) | EXISTS q: x = b * q + r}" nil )"[bool, bool -> bool]" booleans nil )nil extra_real_props nil )"rat" rationals nil )"rat" rationals nil )nil real_props nil )nil real_types nil )nil real_props nil )"real" reals nil )nil real_props nil )nil modulo_arithmetic nil )nil exponentiation nil )"real" reals nil )"posint" nil )"odd_int" integersnil )"nzint" integers nil )nil extra_real_propsnil )"posint" nil )nil integers nil )nil integers nil )"posnat" float nil )"bool" float nil )"bool" float nil )"bool" float nil )"posrat" nil )nil exponentiation nil )nil reals nil )nil floor_ceil nil )nil bounded_nat_inductions nil )nil defined_types nil )"(total_order?[real])" nil )"posint" exponentiation nil )"nonneg_int" nil )nil floor_ceil nil )nil naturalnumbers nil )"nat" floor_ceil nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"sign_rep" enumerated_type_defs nil )"sign_rep" enumerated_type_defs nil )nil exponentiation nil )nil real_props nil )nil exponentiation nil )"int" integers nil )nil extra_real_props nil )"{r: nonneg_rat | r >= q}" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"nonneg_rat" nil )nil application-judgement "below(m)" mod nil )nil naturalnumbers nil )"sign_rep" fp_round_aux nil )nil enumerated_type_defs nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil )"{k | abs(k) < abs(j)}" mod nil )nil integers nil )"nonneg_real" IEEE_854_values nil )nil IEEE_854_values nil )"integer" IEEE_link nil )"real" sum_hack nil )nil reals nil )"integer" IEEE_link nil )nil IEEE_854 nil )nil real_props nil )"rat" rationals nil )"int" integers nil )"real" IEEE_854_values nil )"{j: nonneg_int | j >= i}" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"posint" nil ))nil ))nil 3321634233 ("" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil )"{j: nonneg_int | j >= i}" nil )"nat" exponentiation nil )"(total_order?[real])" nil )nil exponent_props "reals/" )"Format" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posnat" float nil )"bool" float nil )"boolean" notequal nil )"int" integers nil )"int" integers nil )"int" integers nil ))nil ))nil 3321634271"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321634234"" (skeep)"" (lemma "value_nonzero" )"" (inst -1 "float_to_IEEE(Fnormalize(b)(f))" )"1" (split)"1" (assert ) (("1" (flatten) (("1" (assert ) nil nil )) nil ))nil )"2" (expand "zero?" )"2" (assert ) (("2" (grind-reals) nil nil )) nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854_values nil )"(total_order?[real])" nil )"bool" IEEE_854_values nil )"{x: (finite?) | FtoR(f) = value(x)}" nil )"real" IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" float nil )"bool" float nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"{x: (Fcanonic?(b)) | FtoR(x) = FtoR(f):: real AND Fexp(x) <= Fexp(f)}" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"float[radix]" IEEE_link nil )"Format" IEEE_link nil )"bool" float nil )nil float nil )nil float nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil ))nil 3321634826"" (skeep)"" (lemma "Sterbenz" )"" (inst -1 "b" "IEEE_to_float(ieee)" "IEEE_to_float(ieee2)" )"" (split)"1" "float_to_IEEE(Fnormalize(b)(Fminus(IEEE_to_float(ieee2), IEEE_to_float(ieee))))" )"1" case "value(float_to_IEEE(Fnormalize(b) ") "1" (copy -2)"1" (rewrite -2)"1" (rewrite "FnormalizeCorrect" )"1" (rewrite "FminusCorrect" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil )"2" (lemma "E_max_gt_E_min" )"2" (rewrite "FnormalizeCorrect" )"2" (rewrite "FminusCorrect" )"2" "abs(FtoR(IEEE_to_float(ieee2)))" "1" (expand "abs" ) (("1" (grind-reals) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil )"4" (assert ) nil nil ) ("5" (assert ) nil nil ))nil ))nil ))nil ))nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil float nil )nil IEEE_854 nil )"integer" IEEE_link nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil float nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil float nil )"{x: (finite?) | FtoR(f) = value(x)}" nil )"bool" float nil )"bool" reals nil )"{x: (Fcanonic?(b)) | FtoR(x) = FtoR(f):: real AND Fexp(x) <= Fexp(f)}" nil )"(finite?)" IEEE_link nil )"(finite?)" IEEE_link nil )"float" float nil )"(strict_total_order?[real])" real_props nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"{x: (Fbounded?(b)) | AND " IEEE_link nil) "[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )"real" float nil )"real" IEEE_854_values nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" float nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )nil float nil )"Format" IEEE_link nil )nil float nil )nil naturalnumbers nil ))nil 3321716069 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3321716069"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321716129"" (skeep)"" (expand "RND_Min" )"" (grind-reals)"" (rewrite "RND_aux_alt_def" )"" (expand "RND_aux_alt" )"" (assert )"" (expand "b" )"" (expand "vNum" )"" (rewrite "expt_plus" :dir rl)"" "((-(-E_min - 1 + p) - 1) + p)=E_min" )"1" (grind-reals)"1" (hide -1)"1" (expand "fp_round" )"1" (expand "over_under?" )"1" expand "abs" 2)"1" "1" "floor(0)=0" )"1" expand "FtoR" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" expand "round_exceptions" )"2" expand "round_exceptions_x" )"2" expand "abs" 3)"2" "1" "1" "1" rewrite "max_fp_correct" )"1" "radix ^ E_min" )"1" assert )nil nil )"2" "radix ^ E_max" )"1" rewrite "Exp_increq_1" )"1" " E_max_gt_E_min" )"1" assert )nil nil ))nil ))nil )"2" "2" "radix ^ E_max+radix ^ E_max" )"1" "1" assert )"1" rewrite "Exp_increq_1" )nil nil ))nil ))nil )"2" rewrite "expt_plus" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" " E_max_gt_E_min" )"2" expand "underflow" )"2" "2" expand "round_under" )"2" expand "FtoR" )"2" "-(-E_min - 1 + p)=(1 + E_min - p)" )"1" "radix ^ (1 + E_min - p)" )"1" expand "round" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flip-ineq 2)"2" (expand "fp_round" )"2" (expand "over_under?" )"2" "1" expand "round_exceptions" )"1" expand "round_exceptions_x" )"1" expand "overflow" )"1" "1" " max_fp_correct" )"1" expand "abs" )"1" expand "FtoR" )"1" "floor(ln(r * radix / radix ^ p) / ln(radix))=(E_max + 1) - p" )"1" "floor(r * radix ^ (-((E_max + 1) - p)))=radix^p-1" )"1" rewrite -3)"1" assert )"1" rewrite "expt_plus" nil nil ))nil ))nil )"2" "2" case " radix ^ p - 1<= r * radix ^ (-((E_max + 1) - p))" )"1" case "r * radix ^ (-((E_max + 1) - p)) < (radix ^ p-1)+1" )"1" assert )"1" case "FORALL (g:real,i:int): g<i+1 => i<= g=> floor(g)=i" )"1" "1" assert )nil nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "radix ^ (1 + E_max)*radix ^ (-(1 + E_max - p))" "1" nil nil )"2" rewrite "expt_plus" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "radix ^ (-((E_max + 1) - p))" )"2" " max_pos" )"1" "radix ^ (-(1 + E_max - p))" )"1" nil nil ))nil )"2" "radix ^ (-((E_max + 1) - p))" )"2" rewrite "2" assert )"2" rewrite "expt_plus" "2" rewrite "expt_plus" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (g:real,i:int): g<i+1 => i<= g=> floor(g)=i" )"1" "1" "1" nil nil )"2" "ln(radix)" )"1" rewrite "ln_expt" "1" "ln_increasing" )"1" expand "increasing?" )"1" "1" "1" nil nil )"2" "radix ^ p" )"2" rewrite "expt_plus" "2" " max_pos*radix" )"1" "radix" )"1" nil nil ))nil )"2" rewrite "2" assert )"2" "2" "radix ^ (1 + E_max)+radix ^ (1 + E_max)" )"1" "1" assert )"1" "radix ^ ((1 + E_max - p)+1)" )"1" "expt_plus" )"1" "(1 + E_max - p)" "1" "radix" )"1" rewrite "expt_x1" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "Exp_increq_1" )nil nil ))nil ))nil ))nil )"2" "2" "radix ^ (1 + E_max)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "radix" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "ln(radix) > 0" )"1" "1" assert )nil nil )"2" nil nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "radix" )"2" rewrite "ln_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "ln(radix)" )"1" rewrite "ln_expt" "1" "ln_strict_increasing" )"1" expand "strict_increasing?" )"1" "1" "1" nil nil )"2" "radix ^ p" )"2" rewrite "expt_plus" "2" "radix ^ (2 + E_max)= radix ^ (1 + E_max)*radix" )"1" nil nil )"2" "expt_plus" )"2" "1+E_max" "1" "radix" )"2" rewrite "expt_x1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "radix" )"2" rewrite "ln_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "round_scaled" )"2" "scale(abs(r))=floor(ln(r * radix / radix ^ p) / ln(radix))" )"1" expand "FtoR" )"1" expand "round" )"1" (assert ) nil nil ))nil ))nil )"2" "2" expand "abs" 1)"2" expand "scale" )"2" "2" "Exp_of_unique" )"2" "2" "r" )"2" "1" nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" "hathat_int" )"4" "(floor(ln(r * radix / radix ^ p) / ln(radix)) - 1 + p)" )"4" rewrite "4" "4" expand "^^" )"4" "exp(ln(r * radix / radix ^ p) / ln(radix) * ln(radix) + ") "1" "exp_increasing" )"1" expand "increasing?" )"1" "1" "1" nil nil )"2" "2" assert )"2" "ln(radix)" )"1" assert )nil nil )"2" case "ln(radix) > 0" )"1" "1" assert )nil nil )"2" nil nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "radix" )"2" "1" rewrite "ln_1" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "ln_div" )"2" rewrite "hathat_int" "2" expand "^^" )"2" rewrite "ln_exp" )"2" "ln(r * radix) + ln(radix) * p - p * ln(radix) - ln(radix) ") "1" rewrite "ln_div" "1" "r * radix / radix=r" )"1" rewrite "exp_ln" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" rewrite "hathat_int" "5" rewrite "hathat_int" "5" expand "^^" )"5" "exp((ln(r * radix / exp(p * ln(radix))) / ln(radix)-1) * " "1" rewrite "ln_div" )"1" rewrite "ln_exp" )"1" rewrite "ln_mult" )"1" "(((ln(r) + ln(radix) - p * ln(radix)) / ln(radix) - 1) * ") "1" rewrite "exp_ln" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "2" "1" nil nil )"2" "2" assert )"2" "ln(radix)" )"1" nil nil )"2" case "ln(radix) > 0" )"1" "1" assert )nil nil )"2" nil nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "radix" )"2" "1" rewrite "ln_1" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(Fcanonic?(b))" float nil )nil float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_link nil )"int" integers nil )"posrat" nil )"posnat" float nil )"[T, T -> boolean]" equalities nil )"{i: int | b ^ (i + p - 1) <= x & x < b ^ (i + p)}" nil )"{i: int | b ^ i <= x & x < b ^ (i + 1)}" nil )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )nil real_props nil )nil real_props nil )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil real_props nil )nil ln_exp "lnexp_fnd/" )nil real_props nil )"nnreal" expt "lnexp_fnd/" )nil float nil )nil ln_exp "lnexp_fnd/" )nil real_props nil )nil real_props nil )nil real_props nil )nil ln_exp "lnexp_fnd/" )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_types nil )nil real_props nil )nil real_props nil )nil fp_round_aux nil )"real" fp_round_aux nil )"[real, exception]" over_under nil )nil extra_real_propsnil )nil real_props nil )"real" reals nil )nil real_props nil )"odd_int" integersnil )"even_int" integersnil )"real" reals nil )nil ln_exp "lnexp_fnd/" )nil extra_real_propsnil )"bool" real_fun_preds "reals/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )"bool" real_fun_preds "reals/" )nil real_props nil )nil real_props nil )"posreal" nil )"rat" rationals nil )nil real_props nil )nil real_props nil )"odd_int" integers nil )nil real_props nil )nil exponentiation nil )nil real_props nil )nil real_props nil )nil real_props nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" ln_exp "lnexp_fnd/" )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )nil real_props nil )"bool" over_under nil )nil real_props nil )nil real_props nil )"{j: nonneg_int | j >= i}" nil )"nat" floor_ceil nil )"nonneg_rat" nil )"real" float nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[real, exception]" real_to_fp nil )"(strict_total_order?[real])" real_props nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil IEEE_854 nil )"posreal" IEEE_854_values nil )nil real_types nil )nil real_types nil )"bool" reals nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"posrat" nil )nil exponentiation nil )nil real_props nil )nil float nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )"rat" rationals nil )nil IEEE_854_values nil )"[real, exception]" over_under nil )"real" over_under nil )nil extra_real_props nil )nil extra_real_props nil )"(to_neg?)" enumerated_type_defs nil )"[rounding_mode -> boolean]" nil )"integer" round nil )nil enumerated_type_defs nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil real_props nil )"rat" rationals nil )"real" real_to_fp nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" real_to_fp nil )"real" reals nil )nil exponentiation nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"integer" IEEE_link nil )"above(1)" IEEE_link nil )"boolean" notequal nil )nil reals nil )"Format" IEEE_link nil )"(Fcanonic?(b))" float nil )"int" integers nil )"real" reals nil )"nnreal" nil )"posint" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"nnrat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3321717384"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321717385"" (skeep)"" (expand "RND_Max" )"" (rewrite "FoppCorrect" )"" (expand "RND_Min" )"" (grind-reals)"1" (rewrite "FoppCorrect" )"1" (lemma "round_value2" )"1" (inst -1 "float_to_IEEE(RND_aux(b)(r))" "to_pos" )"1" (split)"1" (assert ) nil nil ) ("2" (propax) nil nil ))nil )"2" (trans-ineq 1 "max_pos" :strict 2)"1" (assert ) nil nil )"2" (rewrite "max_fp_correct" )"2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "FpredFoppFsucc" )"2" (rewrite "FoppCorrect" )"2" (rewrite "FoppCorrect" )"2" (assert )"2" "FtoR(Fsucc(b)(RND_aux(b)(r)))=FtoR(RND_aux(b)(r))+Fulp(b)(RND_aux(b)(r))" )"1" (rewrite "FulpCanonic" )"1" (mult-by 2 "-1" )"1" (assert )"1" (hide -1)"1" rewrite "RND_aux_alt_def" )"1" expand "RND_aux_alt" )"1" expand "b" )"1" expand "vNum" )"1" rewrite "expt_plus" :dir rl)"1" "((-(-E_min - 1 + p) - 1) + p)=E_min" )"1" "1" expand "FtoR" )"1" expand *"fp_round" "over_under?" )"1" expand "abs" )"1" expand "round_exceptions" )"1" expand "round_exceptions_x" )"1" expand "underflow" )"1" "1" expand "round_under" )"1" expand "round" )"1" "-(-E_min - 1 + p)=1 + E_min - p" )"1" "radix ^ (1 + E_min - p)" )"1" " (radix ^ (1 + E_min - p) + ") "1" case "FORALL (g:real): not floor(g)=g => ceiling(g)=floor(g)+1" )"1" "1" "1" assert )nil nil )"2" " radix ^ (1 + E_min - p)" )"2" case "radix ^ (-(1 + E_min - p)) * r * radix ^ (1 + E_min - p)=r" )"1" assert )nil nil )"2" "2" "r" )"2" case "(radix ^ (-(1 + E_min - p)) * r * radix ^ (1 + E_min - p) / r)= ") "1" replace "1" rewrite "expt_plus" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a" "floor(ln(r * radix / radix ^ p) / ln(radix))" )"2" "2" replace -2)"2" "2" expand "fp_round" )"2" "2" expand "over_under?" )"2" expand "abs" )"2" expand "round_scaled" )"2" expand "abs" )"2" expand "FtoR" )"2" "scale(r)=a" )"1" "radix ^ a" )"1" "(radix ^ a + floor(r * radix ^ (-a)) * radix ^ a) / radix ^ a ") "1" expand "round" )"1" "radix ^ (-a)" )"1" "(floor(r * radix ^ (-a)) * radix ^ a * radix ^ (-a)) ") "1" assert )nil nil )"2" "2" "(floor(r * radix ^ (-a)))" )"2" "((floor(r * radix ^ (-a)) * radix ^ a * radix ^ (-a)) / ") "1" rewrite "expt_plus" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "2" expand "scale" )"2" "2" "Exp_of_unique" )"2" "2" "r" )"2" case "0 < ln(radix)" )"1" "1" nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" rewrite "hathat_int" "4" expand "^^" )"4" "exp(ln(radix) *((ln(r * radix / radix ^ p) / ln(radix))) + ln(radix) * p - ln(radix))" )"1" "exp_increasing" )"1" expand "increasing?" )"1" "1" "1" nil nil )"2" "2" "2" assert )"2" "ln(radix)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "ln_div" )"2" rewrite "ln_expt" )"2" rewrite "ln_mult" )"2" assert )"2" rewrite "exp_ln" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" rewrite "hathat_int" "5" expand "^^" )"5" "exp(ln(radix) * (ln(r * radix / radix ^ p) / ln(radix)-1) + ln(radix) * p)" "1" rewrite "ln_div" )"1" rewrite "ln_expt" )"1" rewrite "ln_mult" )"1" "(ln(radix) * ") "1" rewrite "exp_ln" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "2" "1" nil nil )"2" "2" "2" assert )"2" "ln(radix)" )"2" "ln(r * radix / radix ^ p) / ln(radix)-1" "1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "radix" )"2" rewrite "ln_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "E_max_gt_E_min" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "FsuccDiff" :dir rl)"1" (assert ) nil nil )"2" (lemma "RleRoundedR0" )"2" "isMin?" "b" "RND_Min(b)(r)" "r" )"2" (split)"1" expand "RND_Min" )"1" (propax) nil nil ))nil )"2" (assert ) nil nil )"3" (rewrite "RND_Min_isMin" ) nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"3" (rewrite "FcanonicBounded" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(Fcanonic?(b))" float nil )nil float nil )"float" float nil )"real" float nil )"bool" float nil )"real" reals nil )"odd_int" integers nil )nil real_props nil )nil reals nil )"posint" exponentiation nil )"nnreal" nil )"int" integers nil )"(Fcanonic?(b))" float nil )"posnat" float nil )"real" ln_exp "lnexp_fnd/" )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" fp_round_aux nil )"{i: int | b ^ i <= x & x < b ^ (i + 1)}" nil )"[bool, bool -> bool]" booleans nil )"even_int" integersnil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"bool" real_fun_preds "reals/" )nil real_props nil )nil real_props nil )nil real_props nil )nil ln_exp "lnexp_fnd/" )nil float nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )"real" reals nil )"bool" real_fun_preds "reals/" )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil real_props nil )"nnreal" expt "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil fp_round_aux nil )"{i | " IEEE_link nil )"{i: int | b ^ (i + p - 1) <= x & x < b ^ (i + p)}" nil )"[real, exception]" real_to_fp nil )"rat" rationals nil )"rat" rationals nil )"integer" round nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | x <= i & i < x + 1}" floor_ceil nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil extra_real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )"posrat" nil )nil real_props nil )nil exponentiation nil )nil extra_real_props nil )"rat" rationals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" over_under nil )"[real, exception]" over_under nil )"real" real_to_fp nil )"real" real_to_fp nil )"bool" over_under nil )"real" reals nil )nil exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil float nil )nil real_props nil )"real" reals nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )"bool" float nil )nil float nil )"(total_order?[real])" nil )"(Fcanonic?(b))" float nil )nil real_types nil )"bool" reals nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" float nil )"real" IEEE_link nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"[T, T -> boolean]" equalities nil )"real" IEEE_854_values nil )"{x: (finite?) | FtoR(f) = value(x)}" nil )nil enumerated_type_defs nil )"[rounding_mode -> boolean]" nil )"(to_pos?)" enumerated_type_defs nil )nil IEEE_854_values nil )"int" integers nil )"rat" rationals nil )"bool" reals nil )nil real_types nil )"posreal" IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )nil IEEE_854 nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )nil real_to_fp nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"Format" IEEE_link nil )"(Fcanonic?(b))" float nil )"bool" float nil )nil float nil )nil naturalnumbers nil )nil float nil )nil float nil )"real" reals nil ))nil 3321786254 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil ))nil ))nil 3321786254 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"boolean" notequal nil ))nil ))nil 3321786255"" (skeep)"" (expand "round_scaled" )"" (case-replace "abs(-r)=abs(r)" )"1" (expand "round" ) (("1" (grind-reals) nil nil )) nil )"2" (hide 2)"2" (expand "abs" ) (("2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil )"int" integers nil )"real" reals nil )"real" fp_round_aux nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"integer" round nil )"int" integers nil )"rat" rationals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"rat" rationals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3321805125"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321718237"" (skeep)"" (case "FORALL (g:real): abs(-g)=abs(g)" )"1" (expand "fp_round" )"1" (expand "over_under?" )"1" (rewrite -1)"1" (grind-reals)"1" (expand "round_exceptions" )"1" (expand "round_exceptions_x" )"1" (expand "overflow" )"1" (case "max_pos=-max_neg" )"1" (grind-reals)"1" (expand "trap_over" )"1" (grind-reals)"1" (rewrite "fp_round_opp_aux" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand "trap_over" )"2" (grind-reals)"2" (rewrite "fp_round_opp_aux" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2 3)"2" expand * "max_pos" "max_neg" "max_fp_pos" "max_fp_neg" "value" "pos" "neg" )"2" (rewrite "expt_x0" )"2" (rewrite "expt_x1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "round_exceptions" )"2" (expand "round_exceptions_x" )"2" (grind-reals)"1" (expand "overflow" )"1" (case "max_pos=-max_neg" )"1" (grind-reals)"1" (expand "trap_over" )"1" (grind-reals)"1" rewrite "fp_round_opp_aux" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "trap_over" )"2" (grind-reals)"2" rewrite "fp_round_opp_aux" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2 3)"2" expand * "max_pos" "max_neg" "max_fp_pos" "max_fp_neg" "value" "pos" "neg" )"2" (rewrite "expt_x1" )"2" rewrite "expt_x0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "underflow" )"2" (case "tiny?(r, to_neg)=tiny?(-r, to_pos)" )"1" case "round_under(r, to_neg)=-round_under(-r, to_pos)" )"1" (grind-reals)"1" (rewrite "fp_round_opp_aux" )"1" (assert ) nil nil )) nil ))nil )"2" (rewrite "fp_round_opp_aux" )"2" (hide 4)"2" expand "round_under" )"2" expand "round" )"2" (grind-reals) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 4)"2" (expand "tiny?" )"2" (rewrite "fp_round_opp_aux" )"2" case "abs(-round_scaled(-r, to_pos)) =abs(round_scaled(-r, to_pos))" )"1" assert )"1" (grind-reals) nil nil ))nil )"2" "2" "AA" "round_scaled(-r, to_pos)" )"2" expand "abs" 1)"2" (grind-reals) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (rewrite "fp_round_opp_aux" ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "abs" ) (("2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"bool" over_under nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nnrat" exponentiation nil )"[real, exception]" real_to_fp nil )"negreal" IEEE_854_values nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"posreal" IEEE_854_values nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )"nzreal" real_typesnil )"real" over_under nil )"integer" IEEE_link nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil IEEE_link nil )nil real_props nil )"int" integers nil )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"fp_num" IEEE_854_values nil )"sign_rep" enumerated_type_defs nil )"sign_rep" enumerated_type_defs nil )"real" IEEE_854_values nil )"fp_num" IEEE_854_values nil )nil exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"odd_int" integers nil )nil exponentiation nil )"[real, exception]" over_under nil )"posrat" exponentiation nil )"real" real_to_fp nil )"[real, exception]" over_under nil )"real" fp_round_aux nil )"real" over_under nil )"int" integers nil )"integer" round nil )"rat" rationals nil )"rat" rationals nil )nil reals nil )nil enumerated_type_defs nil )"bool" over_under nil )"[rounding_mode -> boolean]" nil )"(to_neg?)" enumerated_type_defs nil )"[rounding_mode -> boolean]" nil )"(to_pos?)" enumerated_type_defs nil )"real" real_to_fp nil ))nil 3321882585 ("" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"nat" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"Format" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" float nil )"float" float nil )"(Fcanonic?(b))" float nil )"boolean" notequal nil )"posnat" float nil )"int" integers nil )"rat" rationals nil )"int" integers nil )"posint" exponentiation nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"posint" nil )"int" integers nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil ))"RWB" 3508763454"" (skeep)"" (lemma "RND_Min_isMin" )"" (inst?)"" (expand "isMin?" )"" (lemma "RND_Max_isMax" )"" (inst?)"" (expand "isMax?" )"" (flatten)"" (expand "RND_EClosest" )"" " abs(FtoR(RND_Min(b)(r)) - r)=r - FtoR[radix](RND_Min(b)(r))" )"1" "abs(FtoR(RND_Max(b)(r)) - r)=FtoR[radix](RND_Max(b)(r)) - r" )"1" (hide-all-but 1)"1" (grind-reals)"1" (lemma "MaxSuccMin" )"1" "b" "RND_Min(b)(r)" "RND_Max(b)(r)" "r" )"1" "1" case "r=(FtoR(RND_Max(b)(r))+FtoR(RND_Min(b)(r)))/2" )"1" "1" "1" expand "RND_Min" )"1" "extra_tegies" "extra_real_props" ))"1" "1" expand "abs" )"1" "(r * radix ^ (-Fexp(RND_aux(b)(r))))=(Fnum(RND_aux(b)(r)))+1/2" )"1" expand "even?" )"1" "1" replace -4)"1" "ceiling(2 * j!1 + 1 / 2)=2 * j!1 + 1" )"1" "floor((2 * j!1 + 1) / 2)=j!1" )"1" expand "FtoR" )"1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "1 / 2 + 2 * j!1=-1/2+(2*j!1+1)" )"1" rewrite "ceiling_plus_int" )"1" "ceiling(-(1 / 2))=0" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "expt_inverse" )"2" "2" "2" replace "2" "2" "FtoR(Fsucc(b)(RND_aux(b)(r)))=FtoR(RND_aux(b)(r))+radix ^ Fexp(RND_aux(b)(r))" )"1" expand "FtoR" )"1" nil nil ))nil )"2" "2" "2" rewrite "FsuccDiff" )"1" rewrite "FulpCanonic" )nil nil )"2" "RleRoundedR0" )"2" "isMin?" "b" "RND_Min(b)(r)" "r" )"2" "1" expand "RND_Min" )"1" nil nil ))nil )"2" nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "AA" "Fpred(b)(Fopp(RND_aux(b)(-r)))" )"2" "2" replace -2)"2" "2" expand "abs" )"2" case "RND_aux(b)(-r)=Fopp(Fsucc(b)(AA))" )"1" "1" expand "Fopp" "1" "r * radix ^ (-Fexp(Fsucc(b)(AA)))=Fnum(Fsucc(b)(AA))-1/2" )"1" "ceiling(Fnum(Fsucc(b)(AA)) - 1 / 2)=Fnum(Fsucc(b)(AA))" )"1" "floor(Fnum(Fsucc(b)(AA)) / 2)=(Fnum(Fsucc(b)(AA))-1)/2" )"1" expand "FtoR" )"1" "1" "1" case "radix ^ Fexp(Fsucc(b)(AA))=FtoR(Fsucc(b)(AA))-FtoR(AA)" )"1" expand "FtoR" "1" assert )nil nil ))nil )"2" "Fsucc(b)(AA)=Fopp(Fpred(b)(Fopp(AA)))" )"1" "1" "radix ^ Fexp(Fopp(Fpred(b)(Fopp(AA))))=radix ^ Fexp((Fpred(b)(Fopp(AA))))" )"1" rewrite "FoppCorrect" )"1" " FtoR[radix](AA)=-FtoR(Fopp(AA))" )"1" "-FtoR(Fpred(b)(Fopp(AA))) - -(FtoR[radix]((Fopp(AA)))) ") "1" rewrite "FpredDiff" )"1" rewrite "FulpCanonic" )"1" "Fpred(b)(Fopp(AA))=Fopp(RND_Max(b)(r))" )"1" "FcanonicOpp" )"1" "1" "b" "RND_Max(b)(r)" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "2" expand "Fopp" "2" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" replace "2" "2" rewrite "FpredFoppFsucc" )"2" rewrite "FoppCorrect" )"2" assert )"2" "FtoR(Fsucc(b)(RND_aux(b)(-r)))" "1" rewrite "FsuccPos" )"1" "RleRoundedR0" )"1" "isMin?" "b" "RND_Min(b)(-r)" "-r" )"1" "1" expand "RND_Min" )"1" nil nil ))nil )"2" assert )nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace "3" "3" "FcanonicOpp" )"3" "b" "Fpred(b)(Fopp(RND_aux(b)(-r)))" )"3" "3" rewrite "3" rewrite "FpredCanonic" )"3" "FcanonicOpp" )"3" "b" "RND_aux(b)(-r)" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" rewrite "FoppCorrect" )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil )"2" rewrite "FpredFoppFsucc" )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "odd?(Fnum(Fsucc(b)(AA)))" )"1" expand "odd?" )"1" "1" "1" replace "1" assert )"1" "(1 + 2 * j!1) / 2=1/2+j!1" )"1" rewrite "floor_plus_int" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "EvenFsuccOdd" )"2" replace "2" "2" rewrite "FpredCanonic" )"2" "FcanonicOpp" )"2" "b" "RND_aux(b)(-r)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" rewrite "expt_inverse" )"2" "2" "2" "2" replace "2" "2" "FtoR(AA)=FtoR(Fsucc(b)(AA))-radix ^ Fexp(Fsucc(b)(AA))" )"1" expand "FtoR" "1" nil nil ))nil )"2" "2" "Fsucc(b)(AA)=Fopp(Fpred(b)(Fopp(AA)))" )"1" "Fexp(Fopp(Fpred(b)(Fopp(AA))))=Fexp((Fpred(b)(Fopp(AA))))" )"1" rewrite "FoppCorrect" )"1" "FtoR[radix](AA)=-FtoR(Fopp(AA))" )"1" case "radix ^ Fexp((Fpred(b)(Fopp(AA))))=FtoR(Fopp(AA))-FtoR(Fpred(b)(Fopp(AA)))" )"1" assert )nil nil )"2" rewrite "FpredDiff" )"1" rewrite "FulpCanonic" )"1" "1" "FcanonicOpp" )"1" "b" "Fpred(b)(Fopp(AA))" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" rewrite "FpredFoppFsucc" )"2" rewrite "FoppCorrect" )"2" rewrite "FoppCorrect" )"2" "FtoR(Fsucc(b)(RND_aux(b)(-r)))" "1" rewrite "FsuccPos" )"1" "RleRoundedR0" )"1" "isMin?" "b" "RND_Min(b)(-r)" "-r" )"1" "1" expand "RND_Min" )"1" nil nil ))nil )"2" assert )nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace "3" "3" rewrite "FpredFoppFsucc" )"3" "Fopp(Fopp(Fsucc(b)(RND_aux(b)(-r))))=Fsucc(b)(RND_aux(b)(-r))" )"1" rewrite "FsuccCanonic" )nil nil )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "Fopp" )"2" nil nil ))nil ))nil )"2" rewrite "FpredFoppFsucc" )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" rewrite "FsuccFpred" )"1" expand "Fopp" "1" nil nil ))nil )"2" "FcanonicOpp" )"2" "b" "RND_aux(b)(-r)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind-reals) nil nil ))nil )"2" (propax) nil nil )"3" rewrite "RND_Max_isMax" )nil nil )"4" rewrite "RND_Min_isMin" )nil nil )"5" (assert ) nil nil )"6" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "MaxSuccMin" )"2" "b" "RND_Min(b)(r)" "RND_Max(b)(r)" "r" )"2" "1" replace -1)"1" expand "RND_Min" )"1" "1" expand "abs" )"1" "r * radix ^ (-Fexp(RND_aux(b)(r))) ") "1" "ceiling(Fnum(RND_aux(b)(r)) + 1 / 2)=Fnum(RND_aux(b)(r)) + 1" )"1" "floor((Fnum(RND_aux(b)(r)) + 1) / 2)= ") "1" "1" "FtoR(Fsucc(b)(RND_aux(b)(r)))=FtoR(RND_aux(b)(r))+Fulp(b)(RND_aux(b)(r))" )"1" rewrite "FulpCanonic" )"1" expand "FtoR" "1" nil nil ))nil ))nil )"2" rewrite "FsuccDiff" "1" assert )nil nil )"2" "RleRoundedR0" )"2" "isMin?" "b" "RND_Min(b)(r)" "r" )"2" "1" expand "RND_Min" )"1" nil nil ))nil )"2" nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "FcanonicBounded" )nil nil ))nil ))nil )"2" "2" case "odd?(Fnum(RND_aux(b)(r)))" )"1" expand "odd?" )"1" "1" replace -1)"1" nil nil ))nil ))nil ))nil )"2" "even_or_odd" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" rewrite "expt_inverse" )"2" "2" "(radix ^ Fexp(RND_aux(b)(r))) + ") "1" nil nil )"2" "2" "FtoR(Fsucc(b)(RND_aux(b)(r)))=FtoR(RND_aux(b)(r))+Fulp(b)(RND_aux(b)(r))" )"1" rewrite "FulpCanonic" )"1" expand "FtoR" "1" nil nil ))nil ))nil )"2" rewrite "FsuccDiff" "1" assert )nil nil )"2" "RleRoundedR0" )"2" "isMin?" "b" "RND_Min(b)(r)" "r" )"2" "1" expand "RND_Min" )"1" nil nil ))nil )"2" nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "FsuccFpred" )"1" expand "abs" )"1" "Fexp(RND_aux(b)(-r))=Fexp(Fopp(RND_aux(b)(-r)))" )"1" "AA" "Fopp(RND_aux(b)(-r))" )"1" "r * radix ^ (-Fexp(AA))=Fnum(AA)-1/2" )"1" "ceiling(Fnum(AA) - 1 / 2)=Fnum(AA)" )"1" "floor(Fnum(AA) / 2)=Fnum(AA) / 2" )"1" expand "FtoR" "1" nil nil ))nil )"2" case "even?(Fnum(AA))" )"1" case "even?(Fnum(AA))" )"1" expand "even?" )"1" "1" "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" case "AA=Fsucc(b)(Fpred(b)(AA))" )"1" "1" rewrite "OddFsuccEven" )"1" "even_or_odd" )"1" "Fnum(Fpred(b)(AA))" )"1" assert )nil nil ))nil ))nil )"2" rewrite "FpredCanonic" )nil nil ))nil ))nil )"2" rewrite "FsuccFpred" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" rewrite "expt_inverse" )"2" "2" "2 * (Fnum(AA) * (radix ^ Fexp(AA))) - (radix ^ Fexp(AA)) ") "1" nil nil )"2" "2" "2 * (Fnum(AA) * (radix ^ Fexp(AA))) - (radix ^ Fexp(AA))=2*FtoR(AA)-(radix ^ Fexp(AA))" )"1" "1" "1" assert )"1" "FtoR[radix](AA)=-FtoR(Fopp(AA))" )"1" "Fpred(b)(AA)=Fopp(Fsucc(b)(Fopp(AA)))" )"1" "radix ^ Fexp(AA)=Fulp(b)(Fopp(AA))" )"1" rewrite "FsuccDiff" "1" assert )"1" rewrite "FoppCorrect" )"1" assert )"1" rewrite "FoppCorrect" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" case "FtoR(AA) <= 0" )"1" assert )nil nil )"2" "RleRoundedLessR0" )"2" "isMax?" "b" "RND_Max(b)(r)" "r" )"2" "1" assert )nil nil )"2" assert )nil nil )"3" rewrite "RND_Max_isMax" )nil nil )"4" rewrite "isMax_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "FcanonicOpp" )"3" "b" "AA" )"3" assert )nil nil ))nil ))nil ))nil )"2" rewrite "FulpCanonic" )"1" assert )"1" expand "Fopp" )"1" nil nil ))nil ))nil )"2" "FcanonicOpp" )"2" "b" "AA" )"2" assert )nil nil ))nil ))nil ))nil )"3" rewrite "FoppBounded" )"3" rewrite "FcanonicBounded" )nil nil ))nil ))nil )"2" rewrite "FsuccFoppFpred" )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "FtoR" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Fopp" 1)"2" nil nil ))nil ))nil ))nil )"2" "2" "FcanonicOpp" )"2" "b" "RND_aux(b)(-r)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" rewrite "RND_Max_isMax" )nil nil )"4" rewrite "RND_Min_isMin" )nil nil )"5" (assert ) nil nil )"6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "abs" 1)"2" (grind-reals) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (expand "abs" 1)"2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil float nil )"bool" float nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil float nil )"real" float nil )"bool" float nil )"(Fcanonic?(b))" float nil )"posrat" nil )nil float nil )nil float nil )nil float nil )nil float nil )nil real_props nil )nil float nil )nil naturalnumbers nil )"even_int" integersnil )"even_int" integersnil )"real" float nil )nil real_props nil )nil float nil )"(strict_total_order?[real])" real_props nil )nil extra_tegies nil )nil float nil )"bool" integers nil )"nat" floor_ceil nil )nil floor_ceil nil )nil extra_real_props nil )"even_int" integersnil )"even_int" integersnil )nil float nil )"int" integers nil )nil float nil )nil float nil )nil extra_tegies nil )nil float nil )nil float nil )"[bool, bool -> bool]" booleans nil )nil float nil )nil float nil )"rat" rationals nil )nil float nil )"float" float nil )"float" float nil )"(total_order?[real])" nil )"(Fcanonic?(b))" float nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"rat" rationals nil )"{i | x <= i & i < x + 1}" floor_ceil nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil integers nil )"odd_int" integers nil )"odd_int" integers nil )"rat" rationals nil )"nzrat" rationalsnil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil floor_ceil nil )"int" integers nil )nil extra_tegies nil )"posint" nil )"nzrat" rationals nil )"odd_int" integers nil )"posrat" nil )"bool" integers nil )nil reals nil )nil exponentiation nil )nil float nil )nil float nil )nil float nil )"bool" float nil )nil float nil )nil float nil )nil float nil )"[bool, bool -> bool]" booleans nil )"float" float nil )nil real_props nil )nil reals nil )nil real_props nil )nil extra_tegies nil )nil real_props nil )"posrat" nil )nil real_props nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_props nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"int" integers nil )"rat" rationals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(Fcanonic?(b))" float nil )"real" IEEE_link nil )"(Fcanonic?(b))" float nil )"real" reals nil )"bool" float nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" IEEE_link nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" reals nil ))nil )"RWB" 3507894068 ("" (skeep) (("" (postpone) nil nil )) nil ) nil nil 3321798760"" (skeep)"" (lemma "RND_Min_isMin" )"" (inst?)"" (expand "isMin?" )"" (lemma "RND_Max_isMax" )"" (inst?)"" (expand "isMax?" )"" (flatten)"" (expand "RND_EClosest" )"" " abs(FtoR(RND_Min(b)(r)) - r)=r - FtoR[radix](RND_Min(b)(r))" )"1" "abs(FtoR(RND_Max(b)(r)) - r)=FtoR[radix](RND_Max(b)(r)) - r" )"1" (hide-all-but 1)"1" (grind-reals)"1" (lemma "MaxSuccMin" )"1" "b" "RND_Min(b)(r)" "RND_Max(b)(r)" "r" )"1" "1" case "r=(RND_Max(b)(r)+RND_Min(b)(r))/2" )"1" "1" "1" expand "RND_Min" )"1" "1" "1" expand "abs" )"1" "(r * radix ^ (-Fexp(RND_aux(b)(r))))=(Fnum(RND_aux(b)(r)))+1/2" )"1" expand "even?" )"1" "1" replace -4)"1" "ceiling(2 * j!1 + 1 / 2)=2 * j!1 + 1" )"1" "floor((2 * j!1 + 1) / 2)=j!1" )"1" expand "FtoR" )"1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" assert )"2" "1 / 2 + 2 * j!1=-1/2+(2*j!1+1)" )"1" rewrite "ceiling_plus_int" )"1" "ceiling(-(1 / 2))=0" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "expt_inverse" )"2" "2" "2" replace "2" "2" "Fsucc(b)(RND_aux(b)(r))=RND_aux(b)(r)+radix ^ Fexp(RND_aux(b)(r))" )"1" expand "FtoR" )"1" nil nil ))nil )"2" "2" "2" rewrite "FsuccDiff" )"1" rewrite "FulpCanonic" )nil nil )"2" "RleRoundedR0" )"2" "isMin?" "b" "RND_Min(b)(r)" "r" )"2" "1" expand "RND_Min" )"1" nil nil ))nil )"2" nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "AA" "Fpred(b)(Fopp(RND_aux(b)(-r)))" )"2" "2" replace -2)"2" "2" expand "abs" )"2" case "RND_aux(b)(-r)=Fopp(Fsucc(b)(AA))" )"1" "1" expand "Fopp" "1" "r * radix ^ (-Fexp(Fsucc(b)(AA)))=Fnum(Fsucc(b)(AA))-1/2" )"1" "ceiling(Fnum(Fsucc(b)(AA)) - 1 / 2)=Fnum(Fsucc(b)(AA))" )"1" "floor(Fnum(Fsucc(b)(AA)) / 2)=(Fnum(Fsucc(b)(AA))-1)/2" )"1" expand "FtoR" )"1" "1" "1" case "radix ^ Fexp(Fsucc(b)(AA))=Fsucc(b)(AA)-AA" )"1" expand "FtoR" "1" assert )nil nil ))nil )"2" "Fsucc(b)(AA)=Fopp(Fpred(b)(Fopp(AA)))" )"1" "1" "radix ^ Fexp(Fopp(Fpred(b)(Fopp(AA))))=radix ^ Fexp((Fpred(b)(Fopp(AA))))" )"1" rewrite "FoppCorrect" )"1" " FtoR[radix](AA)=-(Fopp(AA))" )"1" "-FtoR(Fpred(b)(Fopp(AA))) - -(FtoR[radix]((Fopp(AA)))) ") "1" rewrite "FpredDiff" )"1" rewrite "FulpCanonic" )"1" "Fpred(b)(Fopp(AA))=Fopp(RND_Max(b)(r))" )"1" "FcanonicOpp" )"1" "1" "b" "RND_Max(b)(r)" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "2" expand "Fopp" "2" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" replace "2" "2" rewrite "FpredFoppFsucc" )"2" rewrite "FoppCorrect" )"2" assert )"2" "FtoR(Fsucc(b)(RND_aux(b)(-r)))" "1" rewrite "FsuccPos" )"1" "RleRoundedR0" )"1" "isMin?" "b" "RND_Min(b)(-r)" "-r" )"1" "1" expand "RND_Min" )"1" nil nil ))nil )"2" assert )nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace "3" "3" "FcanonicOpp" )"3" "b" "Fpred(b)(Fopp(RND_aux(b)(-r)))" )"3" "3" rewrite "3" rewrite "FpredCanonic" )"3" "FcanonicOpp" )"3" "b" "RND_aux(b)(-r)" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" rewrite "FoppCorrect" )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil )"2" rewrite "FpredFoppFsucc" )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "odd?(Fnum(Fsucc(b)(AA)))" )"1" expand "odd?" )"1" "1" "1" replace "1" assert )"1" "(1 + 2 * j!1) / 2=1/2+j!1" )"1" rewrite "floor_plus_int" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "EvenFsuccOdd" )"2" replace "2" "2" rewrite "FpredCanonic" )"2" "FcanonicOpp" )"2" "b" "RND_aux(b)(-r)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" rewrite "expt_inverse" )"2" "2" "2" "2" replace "2" "2" "AA=Fsucc(b)(AA)-radix ^ Fexp(Fsucc(b)(AA))" )"1" expand "FtoR" "1" nil nil ))nil )"2" "2" "Fsucc(b)(AA)=Fopp(Fpred(b)(Fopp(AA)))" )"1" "Fexp(Fopp(Fpred(b)(Fopp(AA))))=Fexp((Fpred(b)(Fopp(AA))))" )"1" rewrite "FoppCorrect" )"1" "FtoR[radix](AA)=-(Fopp(AA))" )"1" case "radix ^ Fexp((Fpred(b)(Fopp(AA))))=Fopp(AA)-Fpred(b)(Fopp(AA))" )"1" assert )nil nil )"2" rewrite "FpredDiff" )"1" rewrite "FulpCanonic" )"1" "1" "FcanonicOpp" )"1" "b" "Fpred(b)(Fopp(AA))" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" rewrite "FpredFoppFsucc" )"2" rewrite "FoppCorrect" )"2" rewrite "FoppCorrect" )"2" "FtoR(Fsucc(b)(RND_aux(b)(-r)))" "1" rewrite "FsuccPos" )"1" "RleRoundedR0" )"1" "isMin?" "b" "RND_Min(b)(-r)" "-r" )"1" "1" expand "RND_Min" )"1" nil nil ))nil )"2" assert )nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace "3" "3" rewrite "FpredFoppFsucc" )"3" "Fopp(Fopp(Fsucc(b)(RND_aux(b)(-r))))=Fsucc(b)(RND_aux(b)(-r))" )"1" rewrite "FsuccCanonic" )nil nil )"2" expand "Fopp" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "Fopp" )"2" nil nil ))nil ))nil )"2" rewrite "FpredFoppFsucc" )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" rewrite "FsuccFpred" )"1" expand "Fopp" "1" nil nil ))nil )"2" "FcanonicOpp" )"2" "b" "RND_aux(b)(-r)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind-reals) nil nil ))nil )"2" (propax) nil nil )"3" rewrite "RND_Max_isMax" )nil nil )"4" rewrite "RND_Min_isMin" )nil nil )"5" (assert ) nil nil )"6" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "MaxSuccMin" )"2" "b" "RND_Min(b)(r)" "RND_Max(b)(r)" "r" )"2" "1" replace -1)"1" expand "RND_Min" )"1" "1" expand "abs" )"1" "r * radix ^ (-Fexp(RND_aux(b)(r))) ") "1" "ceiling(Fnum(RND_aux(b)(r)) + 1 / 2)=Fnum(RND_aux(b)(r)) + 1" )"1" "floor((Fnum(RND_aux(b)(r)) + 1) / 2)= ") "1" "1" "Fsucc(b)(RND_aux(b)(r))=RND_aux(b)(r)+Fulp(b)(RND_aux(b)(r))" )"1" rewrite "FulpCanonic" )"1" expand "FtoR" "1" nil nil ))nil ))nil )"2" rewrite "FsuccDiff" "1" assert )nil nil )"2" "RleRoundedR0" )"2" "isMin?" "b" "RND_Min(b)(r)" "r" )"2" "1" expand "RND_Min" )"1" nil nil ))nil )"2" nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "FcanonicBounded" )nil nil ))nil ))nil )"2" "2" case "odd?(Fnum(RND_aux(b)(r)))" )"1" expand "odd?" )"1" "1" replace -1)"1" nil nil ))nil ))nil ))nil )"2" "even_or_odd" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" rewrite "expt_inverse" )"2" "2" "(radix ^ Fexp(RND_aux(b)(r))) + ") "1" nil nil )"2" "2" "Fsucc(b)(RND_aux(b)(r))=RND_aux(b)(r)+Fulp(b)(RND_aux(b)(r))" )"1" rewrite "FulpCanonic" )"1" expand "FtoR" "1" nil nil ))nil ))nil )"2" rewrite "FsuccDiff" "1" assert )nil nil )"2" "RleRoundedR0" )"2" "isMin?" "b" "RND_Min(b)(r)" "r" )"2" "1" expand "RND_Min" )"1" nil nil ))nil )"2" nil nil )"3" rewrite "RND_Min_isMin" )nil nil )"4" rewrite "isMin_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "FsuccFpred" )"1" expand "abs" )"1" "Fexp(RND_aux(b)(-r))=Fexp(Fopp(RND_aux(b)(-r)))" )"1" "AA" "Fopp(RND_aux(b)(-r))" )"1" "r * radix ^ (-Fexp(AA))=Fnum(AA)-1/2" )"1" "ceiling(Fnum(AA) - 1 / 2)=Fnum(AA)" )"1" "floor(Fnum(AA) / 2)=Fnum(AA) / 2" )"1" expand "FtoR" "1" nil nil ))nil )"2" case "even?(Fnum(AA))" )"1" expand "even?" )"1" "1" "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" case "AA=Fsucc(b)(Fpred(b)(AA))" )"1" "1" rewrite "OddFsuccEven" )"1" "even_or_odd" )"1" "Fnum(Fpred(b)(AA))" )"1" assert )nil nil ))nil ))nil )"2" rewrite "FpredCanonic" )nil nil ))nil ))nil )"2" rewrite "FsuccFpred" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" rewrite "expt_inverse" )"2" "2" "2 * (Fnum(AA) * (radix ^ Fexp(AA))) - (radix ^ Fexp(AA)) ") "1" nil nil )"2" "2" "2 * (Fnum(AA) * (radix ^ Fexp(AA))) - (radix ^ Fexp(AA))=2*AA-(radix ^ Fexp(AA))" )"1" "1" "1" assert )"1" "FtoR[radix](AA)=-(Fopp(AA))" )"1" "Fpred(b)(AA)=Fopp(Fsucc(b)(Fopp(AA)))" )"1" "radix ^ Fexp(AA)=Fulp(b)(Fopp(AA))" )"1" rewrite "FsuccDiff" "1" assert )"1" rewrite "FoppCorrect" )"1" assert )"1" rewrite "FoppCorrect" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" case "AA <= 0" )"1" assert )nil nil )"2" "RleRoundedLessR0" )"2" "isMax?" "b" "RND_Max(b)(r)" "r" )"2" "1" assert )nil nil )"2" assert )nil nil )"3" rewrite "RND_Max_isMax" )nil nil )"4" rewrite "isMax_RoundedMode" )nil nil )"5" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "FcanonicOpp" )"3" "b" "AA" )"3" assert )nil nil ))nil ))nil ))nil )"2" rewrite "FulpCanonic" )"1" assert )"1" expand "Fopp" )"1" nil nil ))nil ))nil )"2" "FcanonicOpp" )"2" "b" "AA" )"2" assert )nil nil ))nil ))nil ))nil )"3" rewrite "FoppBounded" )"3" rewrite "FcanonicBounded" )nil nil ))nil ))nil )"2" rewrite "FsuccFoppFpred" )"2" expand "Fopp" "2" nil nil ))nil ))nil ))nil )"2" rewrite "FoppCorrect" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "FtoR" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Fopp" 1)"2" nil nil ))nil ))nil ))nil )"2" "2" "FcanonicOpp" )"2" "b" "RND_aux(b)(-r)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" rewrite "RND_Max_isMax" )nil nil )"4" rewrite "RND_Min_isMin" )nil nil )"5" (assert ) nil nil )"6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "abs" 1)"2" (grind-reals) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (expand "abs" 1)"2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil float nil )"bool" float nil )nil float nil )"real" float nil )"bool" float nil )"(Fcanonic?(b))" float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )"real" float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )"float" float nil )"float" float nil )"(Fcanonic?(b))" float nil )nil float nil )nil float nil )nil float nil )"bool" float nil )nil float nil )nil float nil )nil float nil )"float" float nil )"(Fcanonic?(b))" float nil )"(Fcanonic?(b))" float nil )"bool" float nil )nil float nil )nil float nil ))nil 3321717897"" (skeep) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3321786922"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321717898"" (skeep)"" (case "0 <= r" )"1" (rewrite "Roundings_eq_pos" )"1" (expand "abs" ) (("1" (propax) nil nil )) nil )) nil )"2" (flip-ineq 1)"2" "FtoR[radix](RND_Min(b)(r))=-FtoR[radix](RND_Max(b)(-r))" )"1" " fp_round(r, to_neg)= -fp_round(-r, to_pos)" )"1" (rewrite "Roundings_eq_neg" )"1" (expand "abs" 1)"1" (case "max_pos=-max_neg" )"1" (assert ) nil nil )"2" expand * "max_pos" "max_neg" "max_fp_pos" "max_fp_neg" "value" "pos" "neg" )"2" (rewrite "expt_x0" )"2" (rewrite "expt_x1" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (lemma "E_max_gt_E_min" )"3" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (rewrite "fp_round_opp" ) nil nil )"3" (lemma "E_max_gt_E_min" ) (("3" (propax) nil nil ))nil ))nil )"2" (hide 2 3 -2)"2" (lemma "isMin_Unique" )"2" (expand "Unique?" )"2" "b" "r" "RND_Min(b)(r)" "Fopp(RND_Max(b)(-r))" )"1" (rewrite "FoppCorrect" )"1" (split)"1" (propax) nil nil )"2" (case-replace "r=--r" )"1" (rewrite "MaxOppMin" )"1" (rewrite -1 :dir rl)"1" (rewrite "RND_Max_isMax" ) nil nil ))nil )"2" (rewrite "FcanonicBounded" ) nil nil ))nil )"2" (assert ) nil nil ))nil )"3" (rewrite "RND_Min_isMin" ) nil nil ))nil ))nil )"2" (rewrite "FoppBounded" )"2" (rewrite "FcanonicBounded" ) nil nil )) nil )"3" (rewrite "FcanonicBounded" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"(total_order?[real])" nil )nil IEEE_link nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil integers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"above(1)" IEEE_link nil )nil float nil )"real" float nil )nil naturalnumbers nil )nil float nil )"bool" float nil )"(Fcanonic?(b))" float nil )"Format" IEEE_link nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"(Fcanonic?(b))" float nil )nil IEEE_link nil )nil IEEE_link nil )"nzreal" real_typesnil )"bool" reals nil )nil real_types nil )nil real_types nil )"posreal" IEEE_854_values nil )nil real_types nil )"bool" reals nil )nil real_types nil )"negreal" IEEE_854_values nil )nil exponentiation nil )"odd_int" integers nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )nil exponentiation nil )"fp_num" IEEE_854_values nil )"real" IEEE_854_values nil )"sign_rep" enumerated_type_defs nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil )nil enumerated_type_defs nil )"real" real_to_fp nil )"[rounding_mode -> boolean]" nil )"(to_neg?)" enumerated_type_defs nil )"[rounding_mode -> boolean]" nil )"(to_pos?)" enumerated_type_defs nil )nil IEEE_854 nil )"above(1)" IEEE_link nil )nil integers nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil float nil )"float" float nil )"real" IEEE_link nil )"bool" float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )"bool" float nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil ))nil 3321787154"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321787155"" (skeep)"" (case "0 < r" )"1" (rewrite "Roundings_eq_neg" )"1" (expand "abs" ) (("1" (propax) nil nil )) nil )) nil )"2" (case "fp_round(r, to_pos)= - fp_round(-r, to_neg)" )"1" (case "fp_round(-r, to_neg)=FtoR[radix](RND_Min(b)(-r))" )"1" case "-FtoR[radix](RND_Min(b)(-r))= FtoR[radix](RND_Max(b)(r))" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (rewrite "FoppCorrect" :dir rl)"2" (lemma "isMax_Unique" )"2" (expand "Unique?" )"2" "b" "r" "Fopp(RND_Min(b)(-r))" "RND_Max(b)(r)" )"1" (split)"1" (propax) nil nil )"2" (rewrite "RND_Max_isMax" ) nil nil )"3" (case-replace "r=--r" )"1" (rewrite "MinOppMax" )"1" (rewrite "RND_Min_isMin" ) nil nil )"2" (rewrite "FcanonicBounded" ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (rewrite "FcanonicBounded" ) nil nil )"3" (rewrite "FoppBounded" )"3" (rewrite "FcanonicBounded" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "Roundings_eq_pos" )"2" (expand "abs" ) (("2" (grind-reals) nil nil )) nil ))nil ))nil )"2" (rewrite "fp_round_opp" )"1" (assert ) nil nil )"2" (case-replace "r=0" )"1" (hide-all-but 1)"1" (expand "fp_round" ) (("1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (lemma "E_max_gt_E_min" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzrat" rationals nil )"nnrat" exponentiation nil )"int" integers nil )"posrat" exponentiation nil )nil IEEE_link nil )nil IEEE_link nil )"Format" IEEE_link nil )"(Fcanonic?(b))" float nil )"bool" float nil )nil float nil )nil naturalnumbers nil )"real" float nil )nil float nil )nil float nil )"real" IEEE_link nil )"float" float nil )"bool" float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil float nil )"bool" float nil )nil float nil )"(Fcanonic?(b))" float nil )nil IEEE_link nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil enumerated_type_defs nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"real" real_to_fp nil )"[rounding_mode -> boolean]" nil )"(to_pos?)" enumerated_type_defs nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[rounding_mode -> boolean]" nil )"(to_neg?)" enumerated_type_defs nil ))nil 3321788177 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3321788177"" (skeep)"" (lemma "E_max_gt_E_min" ) (("" (propax) nil nil )) nil )) nil )"integer" IEEE_link nil )"integer" IEEE_link nil )"integer" IEEE_link nil )nil integers nil )"above(1)" IEEE_link nil )"above(1)" IEEE_link nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854 nil ))nil ))nil 3321788178"" (skeep)"" (case "abs(r) <= max_pos" )"1" (rewrite "RND_EClosest2" )"1" (rewrite "Roundings_eq_1" :dir rl)"1" (rewrite "Roundings_eq_2" :dir rl)"1" (grind-reals)"1" (expand "fp_round" )"1" (grind-reals)"1" (expand "round_exceptions" )"1" (expand "round_exceptions_x" )"1" (expand "underflow" )"1" (grind-reals)"1" (expand "round_under" )"1" (expand "round" )"1" expand "round_to_even" )"1" case "radix ^ (-(1 + E_min - p)) * r - ") "1" (assert ) nil nil )"2" "2" "(radix ^ (1 + E_min - p))" )"2" assert )"2" "(radix ^ (1 + E_min - p)) * radix ^ (-(1 + E_min - p)) * r=r" )"1" (assert ) nil nil )"2" "2" "r" )"2" rewrite "expt_plus" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "round_scaled" )"2" (div-by 4 "radix ^ (scale(abs(r)))" )"2" (expand "round" )"2" (expand "round_to_even" )"2" case "radix ^ (-scale(abs(r))) * r - ") "1" (assert ) nil nil )"2" (hide 5)"2" assert )"2" "(radix ^(scale(abs(r))))" )"2" assert )"2" "radix ^ (scale(abs(r))) * radix ^ (-scale(abs(r))) * r=r" )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.899Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
