| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/float/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 61 kB |
|
Quelle over_under.prf Sprache: Lisp |
|||||||||
|
(over_under
(over_under?_TCC1 0 (over_under?_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil) ((NOT const-decl "[bool -> bool]" booleans 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}" over_under nil) (E_max formal-const-decl "integer" over_under nil) (integer nonempty-type-from-decl nil integers nil) (p formal-const-decl "above(1)" over_under nil) (b formal-const-decl "above(1)" over_under 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) (/= const-decl "boolean" notequal nil) (minus_int_is_int application-judgement "int" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (infinity_TCC1 0 (infinity_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (trap_over_TCC1 0 (trap_over_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (overflow_TCC1 0 (overflow_TCC1-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) (nzreal nonempty-type-eq-decl nil reals nil) (> const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (posreal nonempty-type-eq-decl nil real_types 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) (above nonempty-type-eq-decl nil integers nil) (b formal-const-decl "above(1)" over_under nil) (p formal-const-decl "above(1)" over_under nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (max_pos const-decl "posreal" IEEE_854_values nil) (pos const-decl "sign_rep" enumerated_type_defs 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) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_expt application-judgement "int" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (exact_underflow_TCC1 0 (exact_underflow_TCC1-1 nil 3321205307 ("" (tcc :defs !) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (exact_underflow_TCC2 0 (exact_underflow_TCC2-1 nil 3321205307 ("" (skolem-typepred) (("" (assert) nil nil)) nil) ((posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (E_max formal-const-decl "integer" over_under nil) (integer nonempty-type-from-decl nil integers nil) (b formal-const-decl "above(1)" over_under nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" 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) (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) (nzreal nonempty-type-eq-decl nil reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (/= const-decl "boolean" notequal 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_under_TCC1 0 (round_under_TCC1-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) (nzreal nonempty-type-eq-decl nil reals nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (b formal-const-decl "above(1)" over_under nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nat_exp application-judgement "nat" exponentiation nil) (nat_expt application-judgement "nat" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (expt def-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (round_under_TCC2 0 (round_under_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) (nzreal nonempty-type-eq-decl nil reals nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (b formal-const-decl "above(1)" over_under nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nat_exp application-judgement "nat" exponentiation nil) (nat_expt application-judgement "nat" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (expt def-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (round_under_correct_TCC1 0 (round_under_correct_TCC1-1 nil 3321205307 ("" (assert) (("" (expand "min_pos") (("" (lemma "min_fp_correct") (("" (replace -1) (("" (hide -1) (("" (lemma "expt_pos") (("" (inst?) (("" (assert) (("" (expand "abs") (("" (lemma "expt_plus") (("" (inst - "E_min" "1-p" "b") (("" (replace -1) (("" (hide -1) (("" (lemma "both_sides_times_pos_lt2") (("" (inst - "b^E_min" "b^(1-p)" "1") (("1" (lemma "expt_gt1_neg") (("1" (inst - "b" "p-1") (("1" (ground) nil))))) ("2" (lemma "expt_pos") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))) nil) ((min_pos const-decl "posreal" IEEE_854_values nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_pos formula-decl nil exponentiation nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt_plus formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (expt_gt1_neg formula-decl nil exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (int_minus_int_is_int application-judgement "int" integers nil) (min_fp_correct 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)" over_under nil) (p formal-const-decl "above(1)" over_under nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil)) nil)) (round_under_correct 0 (round_under_correct-1 nil 3321205307 ("" (skosimp*) (("" (expand "round_under") (("" (rewrite "round_int") (("1" (lemma "expt_plus") (("1" (inst - "(1 + E_min - p)" "(-(1 + E_min - p))" "b") (("1" (rewrite "expt_x0") (("1" (rewrite "associative_mult") (("1" (assert) nil))))))))) ("2" (hide 2) (("2" (expand "min_pos") (("2" (lemma "min_fp_correct") (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "expt_plus" :dir rl) (("2" (rewrite "expt_x0") (("2" (assert) nil)))))))))))))))))))) nil) ((round_under const-decl "real" over_under nil) (min_fp_correct formula-decl nil IEEE_854_values nil) (real_times_real_is_real application-judgement "real" reals nil) (expt_plus formula-decl nil exponentiation nil) (expt_x0 formula-decl nil exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (associative_mult formula-decl nil number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (posrat_exp application-judgement "posrat" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rounding_mode type-decl nil enumerated_type_defs nil) (min_pos const-decl "posreal" IEEE_854_values nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (p formal-const-decl "above(1)" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (E_max formal-const-decl "integer" over_under nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (b formal-const-decl "above(1)" over_under nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (round_int formula-decl nil round nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) nil)) (round_under_value_TCC1 0 (round_under_value_TCC1-1 nil 3321205307 ("" (skosimp*) (("" (prop) (("1" (expand "subnormal?") (("1" (expand "zero?") (("1" (ground) nil))))) ("2" (lemma "value_subnormal") (("2" (inst?) (("2" (assert) nil)))))))) nil) ((zero? const-decl "bool" IEEE_854_values nil) (subnormal? const-decl "bool" IEEE_854_values nil) (fp_num type-decl nil IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (value_subnormal 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)" over_under nil) (p formal-const-decl "above(1)" over_under nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil)) nil)) (round_under_value 0 (round_under_value-1 nil 3321205307 ("" (skosimp*) (("" (expand "round_under") (("" (rewrite "round_int") (("1" (lemma "expt_plus") (("1" (inst - "(1 + E_min - p)" "(-(1 + E_min - p))" "b") (("1" (rewrite "expt_x0") (("1" (ground) (("1" (rewrite "associative_mult") (("1" (assert) (("1" (rewrite "associative_mult" :dir rl) (("1" (assert) nil))))))))))))))) ("2" (hide 2) (("2" (case "integer?(b ^ (-(1 + E_min - p)) * value(fin!1))") (("1" (expand "integer?") (("1" (propax) nil))) ("2" (hide 2) (("2" (expand "subnormal?") (("2" (rewrite "normal_value") (("2" (expand "value") (("2" (prop) (("2" (replace -1) (("2" (assert) (("2" (case-replace "b ^ (-(1 + E_min - p)) * (Sum(p, value_digit(d(normalize(fin!1)))) * (-1) ^ sign(normalize(fin!1)) * b ^ E_min) = (-1)^sign(normalize(fin!1)) *(Sum(p,scale_value_p(d(normalize(fin!1)))))") (("1" (hide -1) (("1" (assert) (("1" (case-replace "scale_value_p(d(normalize(fin!1))) = scale_value(d(normalize(fin!1)),p-1)") (("1" (hide -1) (("1" (lemma "scaled_Sum_int") (("1" (inst?) (("1" (case "FORALL (i,j:int): integer?(i*j)") (("1" (inst?) (("1" (expand "integer?") (("1" (propax) nil))))) ("2" (hide -1 -2 -3 2 3) (("2" (expand "integer?") (("2" (propax) nil))))))))))))) ("2" (hide -1 -2 2 3) (("2" (apply-extensionality) (("1" (expand "scale_value_p") (("1" (propax) nil))) ("2" (expand "scale_value") (("2" (expand "value_digit") (("2" (hide 2) (("2" (skosimp*) (("2" (lift-if) (("2" (assert) (("2" (rewrite "associative_mult" :dir rl) (("2" (rewrite "expt_plus" :dir rl) (("2" (ground) (("1" (rewrite "closed_times") (("1" (rewrite "closed_times") (("1" (case "forall (n:nat): integer_pred(b^n)") (("1" (inst?) nil) ("2" (skosimp*) (("2" (assert) nil))))))))) ("2" (rewrite "pos_times_ge") (("2" (lemma "expt_pos") (("2" (inst?) (("2" (assert) nil))))))))))))))))))))))))))))))))))) ("2" (hide -1 -2 2 3) (("2" (assert) (("2" (lemma "scaled_Sum") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (lemma "expt_plus") (("2" (inst - "E_min" "(-(1 + E_min - p))" "b") (("2" (replace -1) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))) nil) ((round_under const-decl "real" over_under nil) (normal_value formula-decl nil IEEE_854_values nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (scaled_Sum formula-decl nil IEEE_854_values nil) (scale_value const-decl "nonneg_real" IEEE_854_values nil) (scaled_Sum_int formula-decl nil IEEE_854_values nil) (fin!1 skolem-const-decl "(finite?)" over_under nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (closed_times formula-decl nil integers nil) (posint_exp application-judgement "posint" exponentiation nil) (associative_mult formula-decl nil number_fields nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (= const-decl "[T, T -> boolean]" equalities 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) (normalize def-decl "(finite?)" IEEE_854_values nil) (sign_rep type-eq-decl nil enumerated_type_defs nil) (sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values nil) (scale_value_p const-decl "nat" IEEE_854_values nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (subnormal? const-decl "bool" IEEE_854_values nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (integer? const-decl "bool" integers nil) (expt_plus formula-decl nil exponentiation nil) (expt_x0 formula-decl nil exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (nzreal nonempty-type-eq-decl nil reals nil) (posrat_exp application-judgement "posrat" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rounding_mode type-decl nil enumerated_type_defs nil) (value const-decl "real" IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (fp_num type-decl nil IEEE_854_values nil) (p formal-const-decl "above(1)" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (E_max formal-const-decl "integer" over_under nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (b formal-const-decl "above(1)" over_under nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (round_int formula-decl nil round nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) nil)) (round_under_error_TCC1 0 (round_under_error_TCC1-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) (nzreal nonempty-type-eq-decl nil reals nil) (minus_odd_is_odd application-judgement "odd_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) (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) (minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (round_under_error 0 (round_under_error-1 nil 3321205307 ("" (skosimp*) (("" (expand "round_under") (("" (case-replace "abs(r!1 - b ^ (1 + E_min - p) * round(b ^ (-(1 + E_min - p)) * r!1, mode!1)) = abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, mode!1))" (("1" (hide -1 -2) (("1" (rewrite "abs") (("1" (lemma "expt_pos") (("1" (inst?) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt2") (("1" (inst - "b^(1+E_min-p)" "_" "1") (("1" (inst?) (("1" (lemma "round1") (("1" (inst?) (("1" (assert) nil))))))))))))))))))))) ("2" (hide -1 2) (("2" (rewrite "abs_mult" :dir rl) (("2" (rewrite "expt_plus" :dir rl) (("2" (rewrite "expt_x0") (("2" (assert) nil))))))))) ("3" (assert) nil) ("4" (assert) nil)))))) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (round_under const-decl "real" over_under nil) (expt_plus formula-decl nil exponentiation nil) (expt_x0 formula-decl nil exponentiation nil) (abs_mult formula-decl nil real_props nil) (expt_pos formula-decl nil exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (round1 formula-decl nil round nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (round const-decl "integer" round nil) (rounding_mode type-decl nil enumerated_type_defs nil) (p formal-const-decl "above(1)" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (E_max formal-const-decl "integer" over_under nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (b formal-const-decl "above(1)" over_under nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (minus_int_is_int application-judgement "int" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (round_under_near 0 (round_under_near-1 nil 3321205307 ("" (skosimp*) (("" (expand "round_under") (("" (hide -1) (("" (case-replace "abs(r!1 - b ^ (1 + E_min - p) * round(b ^ (-(1 + E_min - p)) * r!1, to_nearest)) = abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, to_neares (("1" (hide -1) (("1" (expand "abs" + 1) (("1" (lemma "expt_pos") (("1" (inst?) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt2") (("1" (inst - "b^(1+E_min-p)" "_" "1/2") (("1" (expand "round") (("1" (inst?) (("1" (rewrite "times_div1") (("1" (lemma "round_to_even1") (("1" (inst?) (("1" (assert) nil))))))))))))))))) ("2" (assert) (("2" (split) (("1" (assert) nil) ("2" (assert) nil))))))))))))) ("2" (hide 2) (("2" (rewrite "abs_mult" :dir rl) (("2" (rewrite "expt_plus" :dir rl) (("2" (rewrite "expt_x0") (("2" (assert) nil))))))))) ("3" (assert) nil) ("4" (assert) nil)))))))) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (round_under const-decl "real" over_under nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (b formal-const-decl "above(1)" over_under nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (p formal-const-decl "above(1)" over_under nil) (rounding_mode type-decl nil enumerated_type_defs nil) (round const-decl "integer" round nil) (to_nearest? adt-recognizer-decl "[rounding_mode -> boolean]" enumerated_type_defs nil) (to_nearest adt-constructor-decl "(to_nearest?)" enumerated_type_defs nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div1 formula-decl nil real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (round_to_even1 formula-decl nil round nil) (round_to_even const-decl "integer" round nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (expt_pos formula-decl nil exponentiation nil) (abs_mult formula-decl nil real_props nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (expt_x0 formula-decl nil exponentiation nil) (expt_plus formula-decl nil exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (round_under_pos 0 (round_under_pos-1 nil 3321205307 ("" (skosimp*) (("" (expand "round_under") (("" (hide -1) (("" (expand "round") (("" (lemma "both_sides_times_pos_ge2") (("" (lemma "expt_pos") (("" (inst - "(-(1 + E_min - p))" "b") (("1" (inst - "b ^ (-(1 + E_min - p))" "b ^ (1 + E_min - p) * ceiling(b ^ (-(1 + E_min - p)) * r!1)" "r!1") (("1" (replace -2 :dir rl) (("1" (hide -2) (("1" (rewrite "associative_mult") (("1" (rewrite "associative_mult" :dir rl) (("1" (rewrite "expt_plus" :dir rl) (("1" (rewrite "expt_x0") (("1" (assert) nil))))))))))))) ("2" (assert) nil) ("3" (assert) nil) ("4" (assert) nil))) ("2" (assert) nil)))))))))))))) nil) ((round_under const-decl "real" over_under nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (round const-decl "integer" round nil) (expt_pos formula-decl nil exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nzreal nonempty-type-eq-decl nil reals nil) (ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (expt_x0 formula-decl nil exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (expt_plus formula-decl nil exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (associative_mult formula-decl nil number_fields nil) (b formal-const-decl "above(1)" over_under 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) (p formal-const-decl "above(1)" over_under nil) (above nonempty-type-eq-decl nil integers nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (E_max formal-const-decl "integer" over_under nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (minus_int_is_int application-judgement "int" integers nil) (both_sides_times_pos_ge2 formula-decl nil real_props nil)) nil)) (round_under_neg 0 (round_under_neg-1 nil 3321205307 ("" (skosimp*) (("" (hide -1) (("" (expand "round_under") (("" (expand "round") (("" (lemma "both_sides_times_pos_le2") (("" (inst - "b ^ (-(1 + E_min - p))" "b ^ (1 + E_min - p) * floor(b ^ (-(1 + E_min - p)) * r!1)" "r!1") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (rewrite "associative_mult") (("1" (rewrite "associative_mult" :dir rl) (("1" (rewrite "expt_plus" :dir rl) (("1" (rewrite "expt_x0") (("1" (assert) nil))))))))))))) ("2" (assert) nil) ("3" (lemma "expt_pos") (("3" (inst?) (("1" (assert) nil) ("2" (assert) nil))))) ("4" (assert) nil)))))))))))) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (round const-decl "integer" round nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (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)" over_under nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" 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" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (p formal-const-decl "above(1)" over_under nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_x0 formula-decl nil exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (expt_plus formula-decl nil exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (associative_mult formula-decl nil number_fields nil) (both_sides_times_pos_le2 formula-decl nil real_props nil) (round_under const-decl "real" over_under nil)) nil)) (round_under_zero 0 (round_under_zero-1 nil 3321205307 ("" (skosimp*) (("" (expand "round_under") (("" (rewrite "abs_mult") (("" (expand "round") (("" (case "forall (r1,r2:real): abs(sgn(r1)*r2) = abs(r2)") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (case "forall (r:real): abs(floor(abs(r)))=floor(abs(r))") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "both_sides_times_pos_le2") (("1" (inst - "abs(b ^ (-(1 + E_min - p)))" "abs(b ^ (1 + E_min - p)) * floor(abs(b ^ (-(1 + E_min - p)) * r!1))" "abs(r!1)") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (hide -1) (("1" (rewrite "abs_mult" :dir rl) (("1" (rewrite "associative_mult") (("1" (rewrite "associative_mult" :dir rl) (("1" (rewrite "abs_mult" :dir rl) (("1" (rewrite "expt_plus" :dir rl) (("1" (rewrite "expt_x0") (("1" (expand "abs" + 2) (("1" (assert) nil))))))))))))))))))))) ("2" (hide -1 2) (("2" (lemma "expt_pos") (("2" (inst?) (("2" (expand "abs") (("2" (assert) nil))))))))))))))))))) ("2" (hide -1 2) (("2" (grind) nil))))))))))) ("2" (hide -1 2) (("2" (tcc) nil)))))))))))) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (round_under const-decl "real" over_under nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (expt_plus formula-decl nil exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt_x0 formula-decl nil exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (associative_mult formula-decl nil number_fields nil) (both_sides_times_pos_le2 formula-decl nil real_props nil) (sgn const-decl "int" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (to_zero adt-constructor-decl "(to_zero?)" enumerated_type_defs nil) (to_zero? adt-recognizer-decl "[rounding_mode -> boolean]" enumerated_type_defs nil) (nzreal nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (round const-decl "integer" round nil) (rounding_mode type-decl nil enumerated_type_defs nil) (p formal-const-decl "above(1)" over_under nil) (E_min formal-const-decl "{i: integer | E_max > i}" over_under nil) (E_max formal-const-decl "integer" over_under nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (b formal-const-decl "above(1)" over_under nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (abs_mult formula-decl nil real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_int_is_int application-judgement "int" integers nil)) nil))) ¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28