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