SSL IEEE_854_values.prf
Interaktion und
(IEEE_854_valuesnil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"boolean" notequal nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"boolean" notequal nil )"int" integers nil ))nil ))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)): ") "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 )nil IEEE_854_values nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil enumerated_type_defs nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )nil IEEE_854_values nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )"[(finite?) -> digits]" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )"(finite?)" IEEE_854_values nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil IEEE_854_values nil )"int" integers nil )"(finite?)" IEEE_854_values nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil defined_types nil )nil bounded_nat_inductions nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"digits" IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"bool" IEEE_854_values nil )"real" IEEE_854_values nil )"real" exponentiation nil )"real" exponentiation nil )"boolean" notequal nil )"int" integers nil )"posnat" exponentiation nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"odd_int" integers nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nzint" integersnil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176"" (induct-and-simplify "n" ) (("" (grind) nil )) nil )"int" integers nil )"nonneg_rat" nil )"real" exponentiation nil )"real" exponentiation nil )"rat" rationals nil )"rat" rationals nil )"posrat" nil )"real" reals nil )"posnat" exponentiation nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )"posint" nil )"posint" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )"real" sum_hack nil ) (< const-decl "bool" reals nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )"digits" IEEE_854_values nil )nil naturalnumbers nil ))nil ))nil 3321199176"" (grind :rewrites "Sum_value0" ) nil nil )"int" integers nil )"bool" IEEE_854_values nil )"real" IEEE_854_values nil )nil IEEE_854_values nil )"real" exponentiation nil )"real" exponentiation nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"(total_order?[real])" nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"(total_order?[real])" nil ))nil ))nil 3321199176"" (rewrite "zero_finite_d_zero" ) nil nil )"sign_rep" enumerated_type_defs nil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )"bool" reals nil )nil integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (rewrite "zero_finite_d_zero" ) nil nil )"sign_rep" enumerated_type_defs nil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )"bool" reals nil )nil integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))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" "Sum_nonneg" )"2" "2" rewrite "value_digit" )"2" rewrite "max_significand" )"2" "expt_pos" )"2" "2" "pos_times_gt" )"2" "2" nil ))))))))))))))))))))))))))))))))))))))))))))))nil )"fp_num" IEEE_854_values nil )"odd_int" integers nil )nil exponentiation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"int" integers nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"posrat" nil )"rat" rationals nil )"nonneg_rat" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil sum_hack nil )nil exponentiation nil )"integer" IEEE_854_values nil )nil integers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"digits" IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil ) (Sum def-decl "real" sum_hack nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_props nil )"sign_rep" enumerated_type_defs nil )"real" IEEE_854_values nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil ))nil ))nil 3321199176 ("" (tcc) nil nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))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" "2" rewrite "value_digit" )"2" rewrite "min_significand" )"2" "expt_pos" )"2" "2" assert )nil )))))))))))))))))))))))))))"2" (assert )"2" (split)"1" (assert ) nil ) ("2" (assert ) nil ))))))))))))))))nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" IEEE_854_values nil )"odd_int" integers nil )nil exponentiation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil booleans nil )"bool" reals nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"bool" reals nil )nil real_types nil )nil real_types nil )nil integers nil )"above(1)" IEEE_854_values nil )nil real_props nil )nil sum_hack nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nonneg_rat" nil )"posrat" nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )nil naturalnumbers nil )"real" sum_hack nil )"above(1)" IEEE_854_values nil )"bool" reals nil )nil naturalnumbers nil )nil IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )"digits" IEEE_854_values nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil exponentiation nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))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" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" IEEE_854_values nil )"odd_int" integers nil )nil exponentiation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )"integer" IEEE_854_values nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil integers nil )"above(1)" IEEE_854_values nil )"digits" IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )nil IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )"bool" reals nil )nil naturalnumbers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"even_int" integers nil )"nonneg_rat" nil )"int" integers nil )nil exponentiation nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" sum_hack nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sum_hack nil )nil exponentiation nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))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" "1" "1" "expt_pos" )"1" "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" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" IEEE_854_values nil )"odd_int" integers nil )nil exponentiation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil exponentiation nil )nil sum_hack nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nonneg_rat" nil )"posrat" nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"real" sum_hack nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil naturalnumbers nil )"bool" reals nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )nil IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )"digits" IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil integers nil )nil real_types nil )nil real_types nil )"bool" reals nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )"bool" reals nil )nil booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"boolean" notequal nil )) nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"boolean" notequal nil )) nil ))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))") "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" "expt_plus" )"2" "1" "E_max - jt!1" "b" )"2" "E_max" "-jt!1" "b" )"2" replace -1)"2" "2" replace -1)"2" "2" rewrite "expt_x1" )"2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))nil )"fp_num" IEEE_854_values nil )"int" integers nil )"rat" rationals nil )"rat" rationals nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil exponentiation nil )"posrat" nil )"posint" exponentiation nil )nil reals nil )nil bounded_nat_inductions nil )nil defined_types nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nonneg_real" IEEE_854_values nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sum_hack nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"int" integers nil )"nonneg_rat" nil )nil exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"nzrat" rationalsnil )"int" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"digits" IEEE_854_values nil )nil IEEE_854_values nil )"sign_rep" enumerated_type_defs nil )"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil )nil IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )"bool" reals nil )nil integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil booleans nil )nil IEEE_854_values nil )"real" IEEE_854_values nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"int" integers nil )"posreal" IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"boolean" notequal nil )) nil ))nil 3321199176"" (expand "min_fp_pos" )"" (expand "value" )"" (expand "pos" )"" (rewrite "expt_x0" )"" (assert )"" "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)") "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 )"real" IEEE_854_values nil )"odd_int" integers nil )nil exponentiation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" sum_hack nil ) (> const-decl "bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )"bool" reals nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )"digits" IEEE_854_values nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"posrat" nil )nil integers nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )nil reals nil )nil defined_types nil )nil bounded_nat_inductions nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"int" integers nil )"nonneg_rat" nil )"int" integers nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil ))nil ))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" "1" expand "value_digit" )"1" "1" rewrite "zero_times3" )"1" "expt_nonzero" )"1" "1" assert )nil )))))))))))))))"2" (replace -1)"2" expand "d_zero" )"2" expand "value_digit" )"2" nil )))))))))))))))))))))))))))"2" (assert ) nil ))))))nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" IEEE_854_values nil )nil reals nil )nil sum_hack nil )"digits" IEEE_854_values nil )"int" integers nil )nil exponentiation nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )nil integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[(finite?) -> digits]" IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil ) (Sum def-decl "real" sum_hack nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"odd_int" integers nil ))nil ))nil 3321199176"" (rewrite "value0" )"" (expand "pos_zero" ) (("" (propax) nil )))) nil )"{fin | zero?(fin)}" IEEE_854_values nil )"bool" IEEE_854_values nil )nil booleans nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil booleans nil )nil IEEE_854_values nil )nil IEEE_854_values nil ))nil ))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)): ") "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" "Sum(p,(LAMBDA (n: nat): IF n < p THEN shift_left(d!1)(n) * (b ^ (-n))LAMBDA (n: nat): IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))") "1" "1" "expt_plus" )"1" "1" "E_min+jt!1" "b" )"1" replace -1)"1" "1" rewrite "expt_x1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "Sum" )"2" assert )"2" rewrite "shift_left" )"2" assert )"2" case "forall (i:below(p)): Sum(i, LAMBDA (n: nat):IF n < p THEN shift_left(d!1)(n) * (b ^ (-n)) ELSE 0 ENDIF))LAMBDA (n: nat):IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))") "1" "1" assert )nil nil ))nil )"2" "2" "i" "below_induction[p]" )"1" expand "Sum" )"1" expand "Sum" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "Sum" +)"2" replace -2)"2" "2" assert )"2" expand "shift_left" )"2" "expt_plus" )"2" "1" "-(1+jb!1)" "b" )"2" replace "2" rewrite "expt_x1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "fp_num_finite_eta" ) nil nil ))nil ))nil )nil IEEE_854_values nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil enumerated_type_defs nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )nil IEEE_854_values nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )"[(finite?) -> digits]" IEEE_854_values nil )"(finite?)" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )"real" IEEE_854_values nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil IEEE_854_values nil )"int" integers nil )"(finite?)" IEEE_854_values nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil defined_types nil )nil bounded_nat_inductions nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sum_hack nil )"int" integers nil )"real" reals nil )"nonneg_rat" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )nil exponentiation nil )nil exponentiation nil )"posint" exponentiation nil )"posrat" nil )"odd_int" integers nil )nil reals nil )nil bounded_nat_inductions nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"posint" nil )"rat" rationals nil )"nzint" integers nil )"real" reals nil )"nonneg_real" IEEE_854_values nil )"digits" IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "zero?" )"" (expand "pos" )"" (ground)"1" (expand "value" )"1" (replace -1)"1" (rewrite "expt_x0" )"1" (assert )"1" (lemma "pos_times_ge" )"1" (inst?)"1" (lemma "expt_pos" )"1" (inst?)"1" case "(Sum(p, value_digit(d(fin!1))) >= 0 AND b ^ Exp(fin!1) >= 0)" )"1" (assert ) nil nil )"2" (split)"1" "Sum_nonneg" )"1" (inst?) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "value" )"2" (typepred "sign(fin!1)" )"2" (assert )"2" (replace -1)"2" (rewrite "expt_x1" )"2" (lemma "expt_pos" )"2" (inst?)"2" (assert )"2" (lemma "Sum_nonneg" )"2" (inst?)"2" "pos_times_ge" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" sum_hack nil ) (> const-decl "bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )"bool" reals nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"[(finite?) -> digits]" IEEE_854_values nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )nil IEEE_854_values nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil real_types nil )nil sum_hack nil )"(total_order?[real])" nil )nil exponentiation nil )nil real_props nil )"odd_int" integers nil )nil exponentiation nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )nil exponentiation nil )"sign_rep" enumerated_type_defs nil ))nil ))nil 3321199176"" (assert )"" (skosimp*)"" (expand "neg" )"" (expand "zero?" )"" (expand "value" )"" (lemma "expt_pos" )"" (inst - "Exp(fin!1)" "b" )"1" (lemma "Sum_nonneg" )"1" (inst?)"1" (lemma "pos_times_ge" )"1" (ground)"1" (replace -1)"1" (rewrite "expt_x1" )"1" (assert )"1" (inst?) (("1" (assert ) nil )))))))))"2" (typepred "sign(fin!1)" )"2" (assert )"2" (replace -1)"2" rewrite "expt_x0" )"2" assert )"2" "2" (assert ) nil )))))))))))))))))"2" (assert ) nil )))))"2" (assert )"2" (split)"1" (assert ) nil )"2" (assert ) nil ))))))))))))))))))nil )"bool" IEEE_854_values nil )nil exponentiation nil )nil sum_hack nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil enumerated_type_defs nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )nil exponentiation nil )"real" sum_hack nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil naturalnumbers nil )"bool" reals nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )nil IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )"[(finite?) -> digits]" IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil integers nil )nil real_types nil )nil real_types nil )"bool" reals nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )"bool" reals nil )nil integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" IEEE_854_values nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"sign_rep" enumerated_type_defs nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "normal?" )"" (expand "subnormal?" )"" (ground)"" (hide 2)"" case "forall (n:upto(E_max-E_min)),(s:sign_rep),(d:digits): or ") "1" "Exp(fin!1)-E_min" "sign(fin!1)" "d(fin!1)" )"1" (assert )"1" (rewrite "fp_num_finite_eta" )"1" (assert ) nil )))))"2" (assert )"2" (hide 2 3) (("2" (ground) nil )))))))"2" (hide 2 3)"2" (induct "n" 1 "upto_induction[E_max-E_min]" )"1" (expand "normalize" ) (("1" (propax) nil )))"2" (skosimp*)"2" (rewrite "normalize" )"2" (lift-if)"2" (ground)"2" (inst?) (("2" (assert ) nil )))))))))))"3" (skosimp*) (("3" (assert ) nil )))))))"3" (skosimp*) (("3" (assert ) nil ))))))))))))))nil )"bool" IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"[(finite?) -> digits]" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil )"(finite?)" IEEE_854_values nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil IEEE_854_values nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"bool" reals nil )"integer" IEEE_854_values nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )"(finite?)" IEEE_854_values nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil defined_types nil )nil bounded_nat_inductions nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"digits" IEEE_854_values nil )"bool" IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "normal?" )"" (expand "zero?" )"" (ground)"" (rewrite "normal_value" )"" (rewrite "value0" )"" (replace -2)"" (expand "d_zero" )"" (assert ) nil ))))))))))))))))nil )"bool" IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"(finite?)" IEEE_854_values nil )nil IEEE_854_values nil )"digits" IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil booleans nil )nil IEEE_854_values nil )nil IEEE_854_values nil )"bool" IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*) (("" (expand "subnormal?" ) (("" (ground) nil )))) nil )"bool" IEEE_854_values nil )) nil ))nil 3321199176"" (skosimp*)"" (expand "subnormal?" )"" (expand "normal?" ) (("" (ground) nil ))))))nil )"bool" IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"bool" IEEE_854_values nil ))nil ))nil 3321199176"" (skolem-typepred) (("" (ground) nil )) nil )"int" integers nil )"(total_order?[real])" nil )nil IEEE_854_values nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil enumerated_type_defs nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3321199176"" (skolem-typepred) (("" (ground) nil )) nil )"int" integers nil )"(total_order?[real])" nil )nil enumerated_type_defs nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"fp_num" IEEE_854_values nil )) nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"fp_num" IEEE_854_values nil )) nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"fp_num" IEEE_854_values nil )) nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"fp_num" IEEE_854_values nil )) nil ))nil 3321199176"" (skosimp*)"" (expand "toggle_sign" )"" (expand "value" )"" (typepred "sign(fin!1)" )"" (ground)"1" (replace -1)"1" (rewrite "expt_x0" )"1" (rewrite "expt_x1" ) (("1" (assert ) nil )))))))"2" (replace -1)"2" (rewrite "expt_x1" )"2" (rewrite "expt_x0" )"2" (assert ) nil ))))))))))))))))nil )"fp_num" IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )nil enumerated_type_defs nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )"[T, T -> boolean]" equalities nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil exponentiation nil )nil exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"int" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"int" integers nil )"odd_int" integers nil )"nzreal" exponentiation nil )"rat" exponentiation nil )"real" reals nil )"real" IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))" )"1" (expand "toggle_sign" )"1" case "forall (s:sign_rep),(d1:digits),(n:upto(E_max-E_min)): ") "1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide -1 2)"2" (induct "n" 1 "upto_induction[E_max-E_min]" )"1" (expand "normalize" ) (("1" (propax) nil nil )) nil )"2" (skosimp*)"2" (expand "normalize" +)"2" (lift-if)"2" (assert )"2" (ground) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (skolem-typepred) (("3" (ground) nil nil )) nil )"4" (assert ) nil nil ))nil ))nil )"3" (hide -1 2)"3" (skolem-typepred) (("3" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (rewrite "fp_num_finite_eta" ) nil nil ))nil ))nil )nil IEEE_854_values nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil enumerated_type_defs nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )nil IEEE_854_values nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )"[(finite?) -> digits]" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )"(finite?)" IEEE_854_values nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil IEEE_854_values nil )"int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"(finite?)" IEEE_854_values nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil defined_types nil )nil bounded_nat_inductions nil )"(strict_total_order?[real])" real_props nil )"digits" IEEE_854_values nil )"(divides(m))" divides nil )"(divides(n))" divides nil )NOT const-decl "[bool -> bool]" booleans nil )"fp_num" IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))" )"1" (expand "toggle_sign" )"1" case "forall (s:sign_rep),(d1:digits),(n:upto(E_max-E_min)): ") "1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide -1 2)"2" (induct "n" 1 "upto_induction[E_max-E_min]" )"1" (expand "normalize" ) (("1" (propax) nil nil )) nil )"2" (skosimp*)"2" (expand "normalize" +)"2" (lift-if)"2" (assert )"2" (ground) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (skolem-typepred) (("3" (ground) nil nil )) nil )"4" (assert ) nil nil ))nil ))nil )"3" (hide -1 2)"3" (skolem-typepred) (("3" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (rewrite "fp_num_finite_eta" ) nil nil ))nil ))nil )nil IEEE_854_values nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil enumerated_type_defs nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )nil IEEE_854_values nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )"[(finite?) -> digits]" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )"(finite?)" IEEE_854_values nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil IEEE_854_values nil )"int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"(finite?)" IEEE_854_values nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil defined_types nil )nil bounded_nat_inductions nil )"(strict_total_order?[real])" real_props nil )"digits" IEEE_854_values nil )"(divides(m))" divides nil )"(divides(n))" divides nil )NOT const-decl "[bool -> bool]" booleans nil )"fp_num" IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "zero?" )"" (rewrite "toggle_finite" )"" (rewrite "value_toggle" ) (("" (ground) nil ))))))))nil )"bool" IEEE_854_values nil )nil IEEE_854_values nil )"real" reals nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil booleans nil )nil IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "normal?" )"" (rewrite "toggle_d_normalize" )"" (rewrite "toggle_finite" ) (("" (assert ) nil ))))))))nil )"bool" IEEE_854_values nil )nil IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil booleans nil )nil IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "subnormal?" )"" (rewrite "toggle_d_normalize" )"" (rewrite "toggle_Exp_normalize" )"" (rewrite "toggle_zero?" )"" (rewrite "toggle_finite" )"" (assert ) nil ))))))))))))nil )"bool" IEEE_854_values nil )nil IEEE_854_values nil )nil IEEE_854_values nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil booleans nil )nil IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3321199176"" (skosimp*)"" (rewrite "value_digit" )"" (lift-if)"" (split)"1" (flatten)"1" (rewrite "both_sides_times_pos_le1" )"1" (assert ) nil )"2" (lemma "expt_pos" )"2" (inst?) (("2" (assert ) nil )))))))))"2" (flatten)"2" (lemma "expt_pos" )"2" (inst?)"1" (rewrite "pos_times_le" ) (("1" (assert ) nil )))"2" (assert ) nil ))))))))))))))nil )"nonneg_real" IEEE_854_values nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )"int" integers nil )"nnrat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nonneg_rat" nil )"int" integers nil )nil real_props nil )nil real_types nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil exponentiation nil )nil real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176"" (induct "j" )"1" (expand "Sum" )"1" (expand "Sum" )"1" (expand "value_digit" )"1" (rewrite "expt_x0" )"1" (skosimp*)"1" (lift-if) (("1" (ground) nil )))))))))))))"2" (skosimp*)"2" (rewrite "Sum" )"2" (inst?)"2" (lemma "value_digit_le" )"2" (inst?)"2" (assert )"2" (case-replace "b ^ (-(1 + j!1)) * b = b^(-j!1)" )"1" (hide -1) (("1" (assert ) nil )))"2" (hide -1 -2 2)"2" (lemma "expt_plus" )"2" (inst - "-(1+j!1)" "1" "b" )"2" (rewrite "expt_x1" )"2" (assert ) nil )))))))))))))))))))))))"3" (skosimp*) (("3" (assert ) nil ))))nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )nil exponentiation nil )nil exponentiation nil )"posint" exponentiation nil )"int" integers nil )nil reals nil )"rat" rationals nil )"nzint" integers nil )"posrat" nil )nil IEEE_854_values nil )"real" reals nil )"posint" nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )nil exponentiation nil )nil naturalnumbers nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sum_hack nil ) (<= const-decl "bool" reals nil )nil IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )"bool" reals nil )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"posint" nil )"int" integers nil )"rat" rationals nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176"" (induct "j" )"1" (expand "Sum" )"1" (expand "Sum" )"1" (expand "value_digit" )"1" (rewrite "expt_x0" )"1" (case "0 < p" )"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "Sum" )"2" (inst?)"2" (assert )"2" (lemma "value_digit_le" )"2" (inst?)"2" (assert )"2" "b ^ (-(1 + j!1)) * b = b^(-j!1)" )"1" (assert ) nil nil )"2" (hide -1 -2 -3 2)"2" (lemma "expt_plus" )"2" (inst - "-(1+j!1)" "1" "b" )"2" (rewrite "expt_x1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil )nil IEEE_854_values nil )"posrat" nil )"rat" rationals nil )nil reals nil )"int" integers nil )"posint" exponentiation nil )nil exponentiation nil )nil exponentiation nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nzint" integers nil )"real" reals nil )"int" integers nil )"posint" nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"(total_order?[real])" nil )nil exponentiation nil )nil naturalnumbers nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sum_hack nil ) (<= const-decl "bool" reals nil )nil defined_types nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )"posint" nil )"int" integers nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176"" (induct "j" )"1" (expand "Sum" )"1" (skosimp*)"1" (rewrite "value_digit" )"1" (lift-if)"1" (assert )"1" (rewrite "expt_x0" )"1" (assert )"1" (lemma "Sum_nonneg" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "Sum" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )"int" integers nil )"posint" nil )"nonneg_rat" nil )"even_int" integers nil )"nnrat" exponentiation nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil sum_hack nil )nil exponentiation nil )nil naturalnumbers nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" sum_hack nil )"[bool, bool -> bool]" booleans nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3321199176"" (skosimp*)"" (lemma "Sum_d_lt_b" )"" (inst - "d!1" "p-1" )"1" (assert )"1" (lemma "expt_pos" )"1" (inst?) (("1" (assert ) nil )))))))"2" (assert ) nil ))))))nil )nil IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nnrat" exponentiation nil )"rat" rationals nil )"int" integers nil )"(total_order?[real])" nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3321199176"" (skosimp*)"" (lemma "Sum_d_lt1" )"" (inst - "d!1" "p-1" )"1" (lemma "expt_pos" )"1" (inst?) (("1" (assert ) nil ) ("2" (assert ) nil )))))"2" (assert ) nil ))))))nil )nil IEEE_854_values nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"int" integers nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3321199176"" (skosimp*)"" (lemma "Sum_d_ge1" )"" (inst - "d!1" "p-1" )"1" (assert ) nil ) ("2" (assert ) nil ))))))nil )nil IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "value" )"" case "b ^ (Exp(fin!1)) * Sum(p, value_digit(d(fin!1))) >=0" )"1" (typepred "sign(fin!1)" )"1" (prop)"1" (replace -1)"1" (rewrite "expt_x0" )"1" (expand "abs" ) (("1" (assert ) nil )))))))"2" (replace -1)"2" (rewrite "expt_x1" )"2" (expand "abs" )"2" (assert )"2" (lift-if) (("2" (ground) nil )))))))))))))))"2" (hide 2)"2" (lemma "expt_pos" )"2" (inst?)"1" (lemma "Sum_nonneg" )"1" (inst?)"1" (rewrite "pos_times_ge" ) (("1" (assert ) nil )))"2" (assert ) nil )))))"2" (assert ) nil )))))))"3" (assert ) nil ) ("4" (assert ) nil ))))))nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" IEEE_854_values nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil sum_hack nil )nil exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil enumerated_type_defs nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )"real" reals nil )nil exponentiation nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil exponentiation nil )"[numfield -> numfield]" number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )nil IEEE_854_values nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil naturalnumbers nil )"real" sum_hack nil )"above(1)" IEEE_854_values nil )"bool" reals nil )nil naturalnumbers nil )nil IEEE_854_values nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )"[(finite?) -> digits]" IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (expand "Sum" + 1)"" (ground)"" (lift-if)"" (ground)"" (rewrite "value_digit" )"" (rewrite "min_significand" )"" (assert )"" "Sum(p - 1, value_digit(min_significand))=0" )"1" (hide -1)"1" (assert )"1" (lemma "Sum_pos" )"1" (inst?)"1" (ground)"1" "1" "Sum_ge" )"1" "1" "value_digit(d!1)(i!1)" )"1" "1" rewrite "value_digit" )"1" "i!1" )"1" case "d!1(i!1) * b ^ (-i!1) >= b ^ (-(p - 1))" )"1" (assert ) nil )"2" "ge_times_ge_pos" )"2" "b ^ (-(p - 1))" "1" "d!1(i!1)" "b ^ (-i!1)" )"2" "2" "2" "both_sides_expt_gt1_le" )"2" "b" "-(p-1)" "-i!1" )"2" assert )nil )))))))))))))))))))"2" "2" assert )nil )))))))))))))"2" case "d!1=d_zero" )"1" (propax) nil )"2" "2" expand "d_zero" )"2" "2" "2" expand "value_digit" )"2" rewrite "pos_times_gt" )"2" "expt_pos" )"2" "2" assert )nil )))))))))))))))))))))))))))))"2" (hide 2 3 4)"2" case "forall (i:below(p)): Sum(i,value_digit(min_significand)) = 0" )"1" (inst?) nil )"2" (hide 2)"2" (induct "i" 1 "below_induction[p]" )"1" (expand "Sum" ) (("1" (propax) nil )))"2" (skosimp*)"2" rewrite "Sum" +)"2" rewrite "value_digit" )"2" rewrite "min_significand" )"2" nil ))))))))))))))))))))))))))))))))))nil )"real" sum_hack nil )"(total_order?[real])" nil )"nonneg_real" IEEE_854_values nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )"digits" IEEE_854_values nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"nnrat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nonneg_rat" nil )"posrat" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil bounded_nat_inductions nil )nil defined_types nil )nil sum_hack nil )"(strict_total_order?[real])" real_props nil )nil sum_hack nil )"digits" IEEE_854_values nil )"below(p)" IEEE_854_values nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )nil exponentiation nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil exponentiation nil )"posrat" exponentiation nil )nil real_props nil )"digits" IEEE_854_values nil )"posrat" nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil ))nil ))nil 3321199176"" (skosimp*)"" case "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)): ") "1" "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))" )"1" (assert )"1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min" )"1" (assert ) nil nil )) nil ))nil )"2" (assert ) (("2" (rewrite "fp_num_finite_eta" ) nil 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?) nil nil )) nil )) nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil )nil IEEE_854_values nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(finite?)" IEEE_854_values nil )"[(finite?) -> sign_rep]" IEEE_854_valuesnil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )nil naturalnumbers nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil enumerated_type_defs nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"int" integers nil )nil IEEE_854_values nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )"[(finite?) -> digits]" IEEE_854_values nil )nil defined_types nil )nil bounded_nat_inductions nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"digits" IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil IEEE_854_values nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"bool" IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (rewrite "normal_value" )"" (rewrite "abs_value_fin" )"" (expand "normal?" )"" (assert )"" (expand "max_pos" )"" (expand "value" )"" (expand "max_fp_pos" )"" (expand "pos" )"" (rewrite "expt_x0" )"" (assert )"" (prop)"1" (lemma "value_sig_ge1" )"1" (inst?)"1" assert )"1" "both_sides_expt_gt1_le" )"1" "b" "E_min" "(Exp(normalize(fin!1)))" )"1" assert )"1" "le_times_le_pos" )"1" "b^E_min" "1" "Sum(p, value_digit(d(normalize(fin!1))))" "b ^ (Exp(normalize(fin!1)))" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "expt_pos" )"2" (inst?)"2" assert )"2" "both_sides_expt_gt1_le" )"2" "b" "(Exp(normalize(fin!1)))" "E_max" )"2" assert )"2" "le_times_le_pos" )"2" "b ^ (Exp(normalize(fin!1)))" "Sum(p, value_digit(d(normalize(fin!1))))" "Sum(p, value_digit(max_significand))" " b ^ E_max" )"1" assert )"1" "1" rewrite "Sum_le" )"1" "1" "1" expand "value_digit" )"1" "expt_pos" )"1" "1" rewrite "both_sides_times_pos_le1" )"1" expand "max_significand" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "expt_pos" )"2" "2" assert )"2" "Sum_nonneg" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil IEEE_854_values nil )nil IEEE_854_values nil )nil booleans nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"bool" IEEE_854_values nil )"posreal" IEEE_854_values nil )"fp_num" IEEE_854_values nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil exponentiation nil )"odd_int" integers nil )"[(finite?) -> digits]" IEEE_854_values nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil exponentiation nil )"(total_order?[real])" nil )"nonneg_real" IEEE_854_values nil )"real" sum_hack nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )nil real_types nil )nil real_types nil )nil integers nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil IEEE_854_values nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil IEEE_854_values nil )"(finite?)" IEEE_854_values nil )"digits" IEEE_854_values nil )"int" integers nil )"int" integers nil )nil real_props nil )nil sum_hack nil )nil sum_hack nil )nil exponentiation nil )"sign_rep" enumerated_type_defs nil )"real" IEEE_854_values nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posrat" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"(finite?)" IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil IEEE_854_values nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posrat" nil )"real" exponentiation nil )"real" exponentiation nil )"real" IEEE_854_values nil )"bool" IEEE_854_values nil )"boolean" notequal nil )"bool" IEEE_854_values nil )"sign_rep" enumerated_type_defs nil )"fp_num" IEEE_854_values nil )"posreal" IEEE_854_values nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"int" integers nil )"posnat" exponentiation nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"odd_int" integers nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nzint" integersnil ))nil ))nil 3321199176"" (skosimp*)"" (rewrite "normal_value" )"" (rewrite "abs_value_fin" )"" (expand "min_pos" )"" (expand "value" )"" (expand "min_fp_pos" )"" (expand "pos" )"" (rewrite "expt_x0" )"" (assert )"" (expand "subnormal?" )"" (assert )"" (ground)"1" (expand "zero?" )"1" (lemma "both_sides_times_pos_le1" )"1" "b ^ (Exp(normalize(fin!1)))" "Sum(p, value_digit(min_significand))" "Sum(p, value_digit(d(normalize(fin!1))))" )"1" "1" "1" rewrite "normal_value" )"1" rewrite "value0" )"1" rewrite "min_significand_min" )nil )))))))))"2" "expt_pos" )"2" "2" (assert ) nil )))))))))))"2" (lemma "value_sig_lt1" )"2" (inst?)"2" assert )"2" assert )"2" "expt_pos" )"2" "2" "both_sides_times_pos_lt1" )"2" "b ^ (Exp(normalize(fin!1)))" "Sum(p, value_digit(d(normalize(fin!1))))" "1" )"1" (assert ) nil )"2" assert )nil ))))))))))))))))))))))))))))))))))))))))nil )nil IEEE_854_values nil )nil IEEE_854_values nil )nil booleans nil )"[fp_num -> boolean]" IEEE_854_valuesnil )"posreal" IEEE_854_values nil )"fp_num" IEEE_854_values nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil exponentiation nil )"odd_int" integers nil )"bool" IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil IEEE_854_values nil )nil IEEE_854_values nil )"[(finite?) -> digits]" IEEE_854_values nil )"digits" IEEE_854_values nil )"nonneg_real" IEEE_854_values nil )nil IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil )"above(1)" IEEE_854_values nil )"real" sum_hack nil )nil naturalnumbers nil )"[(finite?) -> Exponent]" IEEE_854_valuesnil )nil IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"integer" IEEE_854_values nil )nil integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"above(1)" IEEE_854_values nil )nil integers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"bool" IEEE_854_values nil )nil exponentiation nil )nil real_props nil )"posrat" nil )"(strict_total_order?[real])" real_props nil )nil IEEE_854_values nil )"(total_order?[real])" nil )"sign_rep" enumerated_type_defs nil )"real" IEEE_854_values nil )"posrat" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" reals nil )"nnrat" exponentiation nil )"(finite?)" IEEE_854_values nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (lemma "value_normal" )"" (inst?)"" (lemma "value_subnormal" )"" (inst?)"" (lemma "finite_cover" )"" (inst?)"" (ground)"1" (expand "min_pos" )"1" (rewrite "min_fp_correct" )"1" (lemma "both_sides_expt_gt1_le" )"1" (inst - "b" "(1 + E_min - p)" "E_min" )"1" (ground) nil )))))))))"2" (lemma "both_sides_expt_gt1_le" )"2" (rewrite "max_fp_correct" )"2" (inst - "b" "E_min" "E_max" )"2" (ground)"2" case "b^E_max < b ^ (1 + E_max) - b ^ (1 + E_max - p)" )"1" (ground) nil )"2" (hide -1 -2 -3 -4 -5 2 3 4)"2" "exponent_adjust" )"2" "b" "E_max" "p-1" )"2" assert )nil ))))))))))))))))))))))))))))))))nil )nil IEEE_854_values nil )nil IEEE_854_values nil )nil IEEE_854_values nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil IEEE_854_values nil )"int" integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )"above(1)" IEEE_854_values nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"integer" IEEE_854_values nil )"{i: integer | E_max > i}" IEEE_854_valuesnil )"above(1)" IEEE_854_values nil )nil exponentiation nil )"posreal" IEEE_854_values nil )nil IEEE_854_values nil )"rat" rationals nil )"(total_order?[real])" nil )nil integers nil )nil integers nil )"posrat" nil )nil exponentiation nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[fp_num -> boolean]" IEEE_854_valuesnil )nil booleans nil )nil IEEE_854_values nil ))nil ))nil 3321199176"" (tcc)"1" (rewrite "pos_times_ge" )"1" (assert )"1" (lemma "expt_pos" )"1" (expand "^" )"1" (inst?) (("1" (assert ) nil )))))))))))"2" (lemma "expt_pos" )"2" (expand "^" )"2" (inst?)"2" (assert )"2" (lemma "expt_pos" )"2" (assert )"2" (inst -1 "-n!1" "b" )"2" (assert )"2" (lemma "pos_times_gt" )"2" "d!1(n!1)" "expt(b, m!1) * (1 / (b * expt(b, -(-n!1) - 1)))" )"1" (assert )"1" (prop)"1" (lemma "pos_times_gt" )"1" "expt(b, m!1)" "(1 / (b * expt(b, -(-n!1) - 1)))" )"1" (assert ) nil )"2" "zero_times3" )"2" "2" assert )"2" "expt_nonzero_aux" )"2" "2" assert )nil )))))))))))))))))))"2" (lemma "zero_times3" )"2" (inst?)"2" (assert )"2" "zero_times3" )"2" "2" assert )"2" "expt_nonzero_aux" )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))nil )"boolean" notequal nil )) nil ))nil 3321199176"" (skolem!)"" (induct "m" 1 "upto_induction[n!1+1]" )"1" (rewrite "Sum" )"1" (expand "integer?" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (rewrite "Sum" +)"2" (rewrite "scale_value" )"2" (rewrite "value_digit" )"2" (lift-if)"2" (ground)"2" (case "FORALL (i,j:int): integer?(i+j)" )"1" (inst?)"1" (hide -3 2)"1" (rewrite "associative_mult" :dir rl)"1" (rewrite "expt_plus" :dir rl)"1" case "FORALL (i,j:int): integer?(i*j)" )"1" "1" expand "integer?" )"1" (propax) nil nil ))nil )"2" assert )"2" "2" case "forall (n:nat): integer?(b^n)" )"1" "1" expand "integer?" )"1" (propax) nil nil ))nil ))nil )"2" "2" expand "integer?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "integer?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "integer?" )"2" (propax) nil nil )) nil ))nil )"2" (expand "integer?" 1)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil naturalnumbers nil )nil defined_types nil )"bool" integers nil )"real" sum_hack nil ) (< const-decl "bool" reals nil )"bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bounded_nat_inductions nil )"posint" nil )"int" integers nil )"real" reals nil )"nonneg_real" IEEE_854_values nil )"(strict_total_order?[real])" real_props nil )"nonneg_rat" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"nnrat" exponentiation nil )"int" integers nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" IEEE_854_values nil )"upto(n!1 + 1)" IEEE_854_values nil )"digits" IEEE_854_values nil )nil number_fields nil )"posrat" nil )"posint" nil )"(total_order?[real])" nil )"posrat" exponentiation nil )"int" integers nil )nil exponentiation nil )nil reals nil )"nnreal" nil )"posint" exponentiation nil ))nil ))nil 3321199176 ("" (tcc :defs !) nil nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3321199176"" (skosimp*)"" (case "integer?(scale_value(d!1, p - 1)(n!1))" )"1" (expand "integer?" ) (("1" (assert ) nil )))"2" (hide 2)"2" (rewrite "scale_value" )"2" (rewrite "value_digit" )"2" (lift-if)"2" (ground)"1" "(d!1(n!1) * b ^ (p - 1) * b ^ (-n!1))=(d!1(n!1) * b ^ (p - 1 - n!1))" )"1" (hide -1)"1" (case "FORALL (i,j:int): integer?(i*j)" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (expand "^" )"1" assert )"1" case "FORALL (n:nat): integer_pred(expt(b, n))" )"1" (inst?) nil )"2" "2" "n" )"2" nil )))))))))))))))))"2" (expand "integer?" )"2" (propax) nil )))))))"2" (lemma "expt_plus" )"2" (inst?)"2" (inst -1 "-n!1" )"2" (assert ) nil )))))))))"2" (expand "integer?" )"2" (propax) nil )))))))))))))"3" (assert ) nil ))))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"bool" integers nil )nil booleans nil )nil booleans nil )nil numbers nil )"int" integers nil )"(total_order?[real])" nil )"nnrat" exponentiation nil )"nnreal" nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"posnat" exponentiation nil )"nat" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )"posrat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzreal" exponentiation nil )nil reals nil )"posrat" nil )nil exponentiation nil )"int" integers nil )"nonneg_rat" nil )"(strict_total_order?[real])" real_props nil )"nonneg_real" IEEE_854_values nil ))nil ))nil 3321199178 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3321199176"" (induct "n" )"1" (expand "Sum" ) (("1" (propax) nil )))"2" (skosimp*)"2" (expand "Sum" +)"2" (inst?)"2" (rewrite "scale_value" ) (("2" (assert ) nil ))))))))))nil )"real" reals nil )"nnreal" nil )"real" reals nil )"posint" exponentiation nil )nil naturalnumbers nil )"nonneg_real" IEEE_854_values nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nonneg_real" IEEE_854_values nil )nil real_types nil )"real" sum_hack nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3321199176"" (skosimp*)"" (rewrite "scaled_Sum_i" )"" (rewrite "scale_value_p" )"" (replace-eta "scale_value(d!1, (p - 1))" ) nil ))))))nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil IEEE_854_values nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"nonneg_real" IEEE_854_values nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"nat" IEEE_854_values nil ))nil ))nil 3321199176"" (skosimp*)"" (rewrite "scaled_Sum_i" )"" (lemma "Sum_split" )"" (inst - "scale_value(d!1, i!1)" "p" "i!1+1" )"" (replace -1)"" (hide -1)"" (lemma "floor_plus_int" )"" "Sum(i!1 + 1, scale_value(d!1, i!1))" "Sum(p - (i!1 + 1), LAMBDA (k: nat):") "1" (replace -1)"1" (hide -1)"1" (assert )"1" (lemma "floor_Sum_mant" )"1" (inst?)"1" (hide 2)"1" "1" rewrite "scale_value" )"1" rewrite "value_digit" )"1" "1" "1" "expt_plus" )"1" "(-(1 + i!1 + i!2))" "i!1" "b" )"1" "both_sides_times_pos_le1" )"1" "b ^ (-i!2 - 1)" "d!1(1 + i!1 + i!2)" "(b-1)" )"1" (assert ) nil )"2" "2" "expt_pos" )"2" "2" assert )nil )))))))))))))))"2" "pos_times_le" )"2" "(b-1)" "b ^ (-i!2 - 1)" )"2" "expt_pos" )"2" "2" assert )nil )))))))))))))))))))))))))))))))"2" (hide 2)"2" (lemma "scaled_Sum_int" )"2" (expand "integer?" )"2" (inst?) nil ))))))))))))))))))))))nil )nil IEEE_854_values nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )"(total_order?[real])" nil )"posint" nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" sum_hack nil )"below(p)" IEEE_854_values nil )"digits" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"posrat" nil )nil sum_lemmas nil )"nnreal" nil )nil real_props nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil real_props nil )"rat" rationals nil )nil real_types nil )nil reals nil )"nzint" integers nil )"rat" rationals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"nonneg_rat" nil )"(strict_total_order?[real])" real_props nil )"nonneg_real" IEEE_854_values nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )nil sum_lemmas nil )"int" integers nil )"real" reals nil )nil IEEE_854_values nil )"bool" integers nil )nil floor_ceil nil )"posint" nil )"int" integers nil )nil sum_hack nil )"posint" exponentiation nil ))nil ))nil 3321199176"" (skosimp*)"" (lemma "scaled_Sum_int" )"" (expand "integer?" ) (("" (inst?) nil ))))))nil )nil IEEE_854_values nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil IEEE_854_values nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"(total_order?[real])" nil )"posint" nil )"bool" integers nil ))nil ))nil 3321199176"" (skosimp*)"" (rewrite "Sum" )"" (rewrite "scale_value" )"" (rewrite "value_digit" )"" "(d!1(i!1) * b ^ (-i!1) * b ^ i!1) = d!1(i!1) * (b ^ (-i!1) * b ^ i!1)" )"1" (hide -1)"1" (lemma "expt_plus" )"1" (inst?)"1" (replace -1 :dir rl)"1" (hide -1)"1" (rewrite "expt_x0" )"1" (assert )"1" (lemma "mod_of_mod" )"1" (inst?)"1" replace -1 :dir rl)"1" "1" "mod(Sum(i!1, scale_value(d!1, i!1)),b) = 0" )"1" "1" rewrite "mod_lt_nat" )nil nil ))nil )"2" "2" case "forall (j:upto(i!1)): mod(Sum(j,scale_value(d!1,i!1)),b) = 0" )"1" (inst?) nil nil )"2" "2" "j" "upto_induction[i!1]" )"1" expand "Sum" )"1" rewrite "mod_zero" )nil nil ))nil )"2" "2" expand "Sum" +)"2" rewrite "scale_value" )"2" rewrite "value_digit" )"2" "d!1(jt!1) * b ^ (-jt!1) * b ^ i!1 = d!1(jt!1) * (b ^ (-jt!1) * b ^ i!1)" )"1" "1" "expt_plus" )"1" "1" replace "1" "1" "mod_of_mod" )"1" "1" replace "1" "1" replace "1" "1" "d!1(jt!1) * b ^ ((-jt!1) + i!1) = (d!1(jt!1) * b ^ ((-jt!1) + i!1-1))*b" )"1" "1" "mod_sum" )"1" "0" "b" "_" )"1" rewrite "mod_zero" )"1" "1" assert )nil nil )"2" rewrite "closed_times" )"2" case "forall (n:nat):integer_pred(b^n)" )"1" nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "b ^ ((-jt!1) + i!1 - 1) * b = b^(i!1-jt!1)" )"1" assert )nil nil )"2" "2" "expt_plus" )"2" "i!1-jt!1" "(-1)" "b" )"2" replace "2" rewrite "expt_inverse" )"2" rewrite "expt_x1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "scaled_Sum_int" )"2" "2" assert )"2" expand "integer?" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "closed_times" )"3" case "forall (n:nat):integer_pred(b^n)" )"1" nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "scaled_Sum_int" )"3" "3" assert )"3" expand "integer?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "scaled_Sum_int" )"3" "3" expand "integer?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "scaled_Sum_int" )"3" "3" expand "integer?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "scaled_Sum_int" )"2" "2" expand "integer?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"real" sum_hack nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil integers nil )"above(1)" IEEE_854_values nil )nil naturalnumbers nil )"above(1)" IEEE_854_values nil )nil IEEE_854_values nil )nil real_types nil )"nonneg_real" IEEE_854_values nil )"int" integers nil )"real" reals nil )"nonneg_real" IEEE_854_values nil )"int" integers nil )"nnrat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nonneg_rat" nil )"nzreal" exponentiation nil )nil reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil application-judgement "below(m)" mod nil )AND const-decl "[bool, bool -> bool]" booleans nil )"below(p)" IEEE_854_values nil )"digits" IEEE_854_values nil )nil integers nil )nil integers nil )nil IEEE_854_values nil )"bool" integers nil )"posint" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil mod nil )nil integers nil )"nonneg_rat" nil )nil exponentiation nil )"posrat" nil )nil exponentiation nil )"odd_int" integers nil )"upto(i!1)" IEEE_854_values nil )"int" integers nil )nil mod nil )nil bounded_nat_inductions nil )nil defined_types nil )"(total_order?[real])" nil )nil naturalnumbers nil )"bool" reals nil )"nonneg_int" nil )nil mod nil )nil integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{k | abs(k) < abs(j)}" mod nil )nil mod nil )"posrat" exponentiation nil )nil exponentiation nil )"posrat" nil )nil exponentiation nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )"nnreal" nil )"posint" exponentiation nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.169Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
