| products/sources/formale sprachen/PVS/float/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: IEEE_854_values.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(IEEE_854_values
(value_digit_TCC1 0 (value_digit_TCC1-1 nil 3321199176 ("" (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) (>= 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) (nat nonempty-type-eq-decl nil naturalnumbers 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) (/= const-decl "boolean" notequal nil)) nil)) (value_TCC1 0 (value_TCC1-1 nil 3321199176 ("" (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) (fp_num type-decl nil IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (/= const-decl "boolean" notequal nil)) nil)) (shift_left_TCC1 0 (shift_left_TCC1-1 nil 3321199176 ("" (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) (< 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (shift_left_TCC2 0 (shift_left_TCC2-1 nil 3321199176 ("" (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) (< 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (normalize_TCC1 0 (normalize_TCC1-1 nil 3321199176 ("" (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) (fp_num type-decl nil IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (normalize_TCC2 0 (normalize_TCC2-1 nil 3321199176 ("" (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) (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)) nil)) (normalize_TCC3 0 (normalize_TCC3-1 nil 3321199176 ("" (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) (fp_num type-decl nil IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (normalize_TCC4 0 (normalize_TCC4-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (normalize_idempotent 0 (normalize_idempotent-1 nil 3321199176 ("" (skosimp*) (("" (case-replace "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))") (("1" (hide -1) (("1" (case "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)): normalize(normalize(finite(s,n+E_min,d)))=normalize(finite(s,n+E_min,d))") (("1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "n" 1 "upto_induction[E_max-E_min]") (("1" (skosimp*) (("1" (expand "normalize") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "normalize" +) (("2" (lift-if) (("2" (ground) (("1" (rewrite "normalize") nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "fp_num_finite_eta") nil nil)) nil)) nil)) nil) ((fp_num type-decl nil IEEE_854_values nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values 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) (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (sign_rep type-eq-decl nil enumerated_type_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (> const-decl "bool" reals nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values nil) (Exponent type-eq-decl nil IEEE_854_values nil) (< const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (b formal-const-decl "above(1)" IEEE_854_values nil) (finite adt-constructor-decl "[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil) (sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values nil) (Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values nil) (d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (normalize def-decl "(finite?)" IEEE_854_values nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (digits type-eq-decl nil IEEE_854_values nil) (int_plus_int_is_int application-judgement "int" integers nil) (fin!1 skolem-const-decl "(finite?)" IEEE_854_values nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (upto_induction formula-decl nil bounded_nat_inductions nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (shift_left const-decl "digits" IEEE_854_values nil) (fp_num_finite_eta formula-decl nil IEEE_854_values nil)) nil)) (subnormal?_TCC1 0 (subnormal?_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil 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) (zero? const-decl "bool" IEEE_854_values nil) (value const-decl "real" IEEE_854_values nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_expt application-judgement "int" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil)) nil)) (normal?_TCC1 0 (normal?_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (max_significand_TCC1 0 (max_significand_TCC1-1 nil 3321199176 ("" (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) (< 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers 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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (min_significand_TCC1 0 (min_significand_TCC1-1 nil 3321199176 ("" (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) (< 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (min_significand_TCC2 0 (min_significand_TCC2-1 nil 3321199176 ("" (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) (< 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (d_zero_TCC1 0 (d_zero_TCC1-1 nil 3321199176 ("" (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) (< 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (Sum_value0 0 (Sum_value0-1 nil 3321199176 ("" (induct-and-simplify "n") (("" (grind) nil)) nil) ((minus_int_is_int application-judgement "int" integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_minus_real_is_real application-judgement "real" 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" 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) (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) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (Sum def-decl "real" sum_hack 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)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (b formal-const-decl "above(1)" IEEE_854_values 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_zero const-decl "digits" IEEE_854_values nil) (nat_induction formula-decl nil naturalnumbers nil)) nil)) (zero_finite_d_zero 0 (zero_finite_d_zero-1 nil 3321199176 ("" (grind :rewrites "Sum_value0") nil nil) ((minus_int_is_int application-judgement "int" integers nil) (zero? const-decl "bool" IEEE_854_values nil) (value const-decl "real" IEEE_854_values nil) (Sum_value0 formula-decl nil IEEE_854_values nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil)) nil)) (max_fp_pos_TCC1 0 (max_fp_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (min_fp_pos_TCC1 0 (min_fp_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (pos_zero_TCC1 0 (pos_zero_TCC1-1 nil 3321199176 ("" (rewrite "zero_finite_d_zero") nil nil) ((pos const-decl "sign_rep" enumerated_type_defs nil) (sign_rep type-eq-decl nil enumerated_type_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (Exponent type-eq-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (> const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (AND 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) (zero_finite_d_zero formula-decl nil IEEE_854_values nil)) nil)) (neg_zero_TCC1 0 (neg_zero_TCC1-1 nil 3321199176 ("" (rewrite "zero_finite_d_zero") nil nil) ((neg const-decl "sign_rep" enumerated_type_defs nil) (sign_rep type-eq-decl nil enumerated_type_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (Exponent type-eq-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (> const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (AND 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) (zero_finite_d_zero formula-decl nil IEEE_854_values nil)) nil)) (max_pos_TCC1 0 (max_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((pos const-decl "sign_rep" enumerated_type_defs nil) (max_fp_pos const-decl "fp_num" IEEE_854_values nil)) nil)) (max_pos_TCC2 0 (max_pos_TCC2-1 nil 3321199176 ("" (expand "value") (("" (expand "max_fp_pos") (("" (expand "pos") (("" (rewrite "expt_x0") (("" (lemma "pos_times_gt") (("" (assert) (("" (inst?) (("" (assert) (("" (lemma "expt_pos") (("" (inst?) (("" (assert) (("" (case "Sum(p, value_digit(max_significand)) > 0") (("1" (ground) nil) ("2" (hide -1 -2 2) (("2" (expand "Sum") (("2" (assert) (("2" (lemma "Sum_nonneg") (("2" (inst?) (("2" (rewrite "value_digit") (("2" (rewrite "max_significand") (("2" (lemma "expt_pos") (("2" (inst?) (("2" (lemma "pos_times_gt") (("2" (inst?) (("2" (ground) nil)))))))))))))))))))))))))))))))))))))))))))))) nil) ((max_fp_pos const-decl "fp_num" IEEE_854_values nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x0 formula-decl nil exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals 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) (minus_int_is_int application-judgement "int" integers nil) (Sum_nonneg formula-decl nil sum_hack nil) (expt_pos formula-decl nil exponentiation nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (integer nonempty-type-from-decl nil integers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (max_significand const-decl "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) (b formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Sum def-decl "real" sum_hack nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (pos_times_gt formula-decl nil real_props nil) (pos const-decl "sign_rep" enumerated_type_defs nil) (value const-decl "real" IEEE_854_values nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil)) nil)) (min_pos_TCC1 0 (min_pos_TCC1-1 nil 3321199176 ("" (tcc) nil nil) ((pos const-decl "sign_rep" enumerated_type_defs nil) (min_fp_pos const-decl "fp_num" IEEE_854_values nil)) nil)) (min_pos_TCC2 0 (min_pos_TCC2-1 nil 3321199176 ("" (expand "min_fp_pos") (("" (expand "value") (("" (expand "pos") (("" (rewrite "expt_x0") (("" (lemma "expt_pos") (("" (inst?) (("1" (assert) (("1" (lemma "pos_times_gt") (("1" (inst?) (("1" (assert) (("1" (case "Sum(p, value_digit(min_significand)) > 0") (("1" (assert) (("1" (assert) nil))) ("2" (hide -1 -2 2) (("2" (expand "Sum") (("2" (lemma "Sum_nonneg") (("2" (inst?) (("2" (rewrite "value_digit") (("2" (rewrite "min_significand") (("2" (lemma "expt_pos") (("2" (inst?) (("2" (assert) nil))))))))))))))))))))))))))) ("2" (assert) (("2" (split) (("1" (assert) nil) ("2" (assert) nil)))))))))))))))) nil) ((int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (value const-decl "real" IEEE_854_values nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x0 formula-decl nil exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[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) (integer nonempty-type-from-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values 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) (above nonempty-type-eq-decl nil integers nil) (b formal-const-decl "above(1)" IEEE_854_values nil) (pos_times_gt formula-decl nil real_props nil) (Sum_nonneg formula-decl nil sum_hack nil) (minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Sum def-decl "real" sum_hack nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (digits type-eq-decl nil IEEE_854_values nil) (value_digit const-decl "nonneg_real" IEEE_854_values nil) (min_significand const-decl "digits" IEEE_854_values nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" 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) (expt_pos formula-decl nil exponentiation nil) (pos const-decl "sign_rep" enumerated_type_defs nil) (min_fp_pos const-decl "fp_num" IEEE_854_values nil)) nil)) (max_neg_TCC1 0 (max_neg_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((neg const-decl "sign_rep" enumerated_type_defs nil) (max_fp_neg const-decl "fp_num" IEEE_854_values nil)) nil)) (max_neg_TCC2 0 (max_neg_TCC2-1 nil 3321199176 ("" (expand "max_fp_neg") (("" (expand "value") (("" (expand "neg") (("" (rewrite "expt_x1") (("" (lemma "expt_pos") (("" (inst?) (("" (lemma "Sum_pos") (("" (inst?) (("" (assert) (("" (lemma "pos_times_gt") (("" (inst?) (("" (ground) (("1" (inst + "0") (("1" (rewrite "value_digit") (("1" (rewrite "expt_x0") (("1" (rewrite "max_significand") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "0") (("2" (rewrite "value_digit") (("2" (rewrite "expt_x0") (("2" (rewrite "max_significand") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (inst + "0") (("3" (rewrite "value_digit") (("3" (rewrite "max_significand") (("3" (rewrite "expt_x0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (value const-decl "real" IEEE_854_values nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x1 formula-decl nil exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[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) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" IEEE_854_values 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)" IEEE_854_values nil) (max_significand const-decl "digits" IEEE_854_values nil) (value_digit const-decl "nonneg_real" IEEE_854_values nil) (digits type-eq-decl nil IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (minus_even_is_even application-judgement "even_int" integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (expt_x0 formula-decl nil exponentiation nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (Sum def-decl "real" sum_hack nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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) (Sum_pos formula-decl nil sum_hack nil) (expt_pos formula-decl nil exponentiation nil) (neg const-decl "sign_rep" enumerated_type_defs nil) (max_fp_neg const-decl "fp_num" IEEE_854_values nil)) nil)) (min_neg_TCC1 0 (min_neg_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((neg const-decl "sign_rep" enumerated_type_defs nil) (min_fp_neg const-decl "fp_num" IEEE_854_values nil)) nil)) (min_neg_TCC2 0 (min_neg_TCC2-1 nil 3321199176 ("" (expand "min_fp_neg") (("" (expand "value") (("" (expand "neg") (("" (rewrite "expt_x1") (("" (assert) (("" (lemma "expt_pos") (("" (inst?) (("" (lemma "Sum_pos") (("" (inst?) (("" (lemma "pos_times_gt") (("" (inst?) (("" (ground) (("1" (inst + "p-1") (("1" (rewrite "value_digit") (("1" (rewrite "min_significand") (("1" (hide 1 3 4 5 6) (("1" (hide -1) (("1" (lemma "expt_pos") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 1 3 4 5 6) (("2" (inst + "p-1") (("2" (expand "value_digit") (("2" (expand "min_significand") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -1 1 3 4 5 6) (("3" (inst + "p-1") (("3" (expand "value_digit") (("3" (expand "min_significand") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (value const-decl "real" IEEE_854_values nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x1 formula-decl nil exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (expt_pos formula-decl nil exponentiation nil) (Sum_pos formula-decl nil sum_hack 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Sum def-decl "real" sum_hack nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (digits type-eq-decl nil IEEE_854_values nil) (value_digit const-decl "nonneg_real" IEEE_854_values nil) (min_significand const-decl "digits" IEEE_854_values nil) (b formal-const-decl "above(1)" IEEE_854_values 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}" IEEE_854_values nil) (E_max formal-const-decl "integer" IEEE_854_values 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (neg const-decl "sign_rep" enumerated_type_defs nil) (min_fp_neg const-decl "fp_num" IEEE_854_values nil)) nil)) (max_fp_correct_TCC1 0 (max_fp_correct_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (max_fp_correct_TCC2 0 (max_fp_correct_TCC2-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (max_fp_correct 0 (max_fp_correct-1 nil 3321199176 ("" (rewrite "max_pos") (("" (rewrite "max_fp_pos") (("" (rewrite "value") (("" (rewrite "pos") (("" (rewrite "expt_x0") (("" (assert) (("" (case "forall (i:upto(p)):Sum(i, (LAMBDA (n: nat): IF n < p THEN max_significand(n) * (b ^ (-n)) ELSE 0 ENDIF)) * b ^ E_max = b ^ (1 + E_max) - b ^ (1 + E_max - i)") (("1" (inst?) (("1" (expand "value_digit") (("1" (propax) nil))))) ("2" (hide 2) (("2" (induct "i" 1 "upto_induction[p]") (("1" (rewrite "Sum") (("1" (assert) nil))) ("2" (skosimp*) (("2" (expand "Sum" +) (("2" (replace -2) (("2" (hide -2) (("2" (assert) (("2" (rewrite "max_significand") (("2" (lemma "expt_plus") (("2" (inst-cp - "1" "E_max - jt!1" "b") (("2" (inst - "E_max" "-jt!1" "b") (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "expt_x1") (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))))) nil) ((max_fp_pos const-decl "fp_num" IEEE_854_values nil) (int_minus_int_is_int application-judgement "int" integers nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt_plus formula-decl nil exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_exp application-judgement "posint" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (upto_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (value_digit const-decl "nonneg_real" IEEE_854_values nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Sum def-decl "real" sum_hack nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (expt_x0 formula-decl nil exponentiation nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (max_significand const-decl "digits" IEEE_854_values nil) (digits type-eq-decl nil IEEE_854_values nil) (pos const-decl "sign_rep" enumerated_type_defs nil) (finite adt-constructor-decl "[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil) (b formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (above nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (Exponent type-eq-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (> const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sign_rep type-eq-decl nil enumerated_type_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (number nonempty-type-decl nil numbers nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (boolean nonempty-type-decl nil booleans nil) (fp_num type-decl nil IEEE_854_values nil) (value const-decl "real" IEEE_854_values nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (max_pos const-decl "posreal" IEEE_854_values nil)) nil)) (min_fp_correct_TCC1 0 (min_fp_correct_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (min_fp_correct 0 (min_fp_correct-1 nil 3321199176 ("" (expand "min_fp_pos") (("" (expand "value") (("" (expand "pos") (("" (rewrite "expt_x0") (("" (assert) (("" (case-replace "Sum(p,value_digit(min_significand))= b^(1-p)") (("1" (hide -1) (("1" (lemma "expt_plus") (("1" (inst - "(1 - p)" "E_min" "b") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Sum") (("2" (expand "value_digit") (("2" (expand "min_significand") (("2" (case "forall (i:below(p)):Sum(i, LAMBDA (n: nat): IF n < p THEN IF n < p - 1 THEN 0 ELSE 1 ENDIF * b ^ (-n) ELSE 0 ENDIF) = 0") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct-and-rewrite "i" 1 "Sum") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((value const-decl "real" IEEE_854_values nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x0 formula-decl nil exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities 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) (Sum def-decl "real" sum_hack nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (b formal-const-decl "above(1)" IEEE_854_values 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) (min_significand const-decl "digits" IEEE_854_values nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt_plus formula-decl nil exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values nil) (nzreal nonempty-type-eq-decl nil reals nil) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (pos const-decl "sign_rep" enumerated_type_defs nil) (min_fp_pos const-decl "fp_num" IEEE_854_values nil)) nil)) (value0 0 (value0-1 nil 3321199176 ("" (skosimp*) (("" (expand "value") (("" (rewrite "zero_times3") (("1" (rewrite "zero_times3") (("1" (lemma "expt_nonzero") (("1" (inst? :copy? t) (("1" (assert) (("1" (hide -2) (("1" (inst?) (("1" (assert) (("1" (hide -1) (("1" (rewrite "Sum_zero") (("1" (prop) (("1" (expand "d_zero") (("1" (apply-extensionality) (("1" (expand "value_digit") (("1" (inst?) (("1" (rewrite "zero_times3") (("1" (lemma "expt_nonzero") (("1" (inst?) (("1" (assert) nil))))))))))))))) ("2" (replace -1) (("2" (expand "d_zero") (("2" (expand "value_digit") (("2" (propax) nil))))))))))))))))))))))))))) ("2" (assert) nil)))))) nil) ((int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (value const-decl "real" IEEE_854_values nil) (nzreal nonempty-type-eq-decl nil reals nil) (Sum_zero formula-decl nil sum_hack nil) (d_zero const-decl "digits" IEEE_854_values nil) (minus_int_is_int application-judgement "int" integers nil) (expt_nonzero formula-decl nil exponentiation nil) (Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values nil) (Exponent type-eq-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values nil) (E_max formal-const-decl "integer" IEEE_854_values nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values nil) (sign_rep type-eq-decl nil enumerated_type_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (fp_num type-decl nil 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) (b formal-const-decl "above(1)" IEEE_854_values nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (p formal-const-decl "above(1)" IEEE_854_values nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Sum def-decl "real" sum_hack nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (zero_times3 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (value_of_zero 0 (value_of_zero-1 nil 3321199176 ("" (rewrite "value0") (("" (expand "pos_zero") (("" (propax) nil)))) nil) ((pos_zero const-decl "{fin | zero?(fin)}" IEEE_854_values nil) (zero? const-decl "bool" IEEE_854_values nil) (bool nonempty-type-eq-decl nil booleans nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (boolean nonempty-type-decl nil booleans nil) (fp_num type-decl nil IEEE_854_values nil) (value0 formula-decl nil IEEE_854_values nil)) nil)) (normal_value 0 (normal_value-1 nil 3321199176 ("" (skosimp*) (("" (case-replace "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))") (("1" (hide -1) (("1" (case "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)): value(finite(s,n+E_min,d))=value(normalize(finite(s,n+E_min,d)))") (("1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "n" 1 "upto_induction[E_max-E_min]") (("1" (skosimp*) (("1" (expand "normalize") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "normalize") (("2" (lift-if) (("2" (ground) (("2" (inst?) (("2" (replace -3 :dir rl) (("2" (hide -3) (("2" (expand "value") (("2" (expand "value_digit") (("2" (case-replace "Sum(p,(LAMBDA (n: nat): IF n < p THEN shift_left(d!1)(n) * (b ^ (-n)) ELSE 0 ENDIF))=b*Sum(p,(LAMBDA (n: nat): IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))") (("1" (hide -1) (("1" (lemma "expt_plus") (("1" (inst - "1" "E_min+jt!1" "b") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "expt_x1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.95 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
