Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: include_form.fd   Sprache: Lisp

(IEEE_854_values
 (value_digit_TCC1 0
  (value_digit_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (value_TCC1 0
  (value_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (shift_left_TCC1 0
  (shift_left_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (shift_left_TCC2 0
  (shift_left_TCC2-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (normalize_TCC1 0
  (normalize_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (normalize_TCC2 0
  (normalize_TCC2-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (normalize_TCC3 0
  (normalize_TCC3-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (normalize_TCC4 0
  (normalize_TCC4-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((/= const-decl "boolean" notequal nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (normalize_idempotent 0
  (normalize_idempotent-1 nil 3321199176
   ("" (skosimp*)
    (("" (case-replace "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
      (("1" (hide -1)
        (("1"
          (case "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
              normalize(normalize(finite(s,n+E_min,d)))=normalize(finite(s,n+E_min,d))")
          (("1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
            (("1" (assertnil nil) ("2" (assertnil 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" (assertnil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert) (("2" (rewrite "fp_num_finite_eta"nil nil))
        nil))
      nil))
    nil)
   ((fp_num type-decl nil IEEE_854_values nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (sign_rep type-eq-decl nil enumerated_type_defs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (Exponent type-eq-decl nil IEEE_854_values nil)
    (< const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (finite adt-constructor-decl
     "[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil)
    (sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
          nil)
    (Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values
     nil)
    (d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (normalize def-decl "(finite?)" IEEE_854_values nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (fin!1 skolem-const-decl "(finite?)" IEEE_854_values nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pred type-eq-decl nil defined_types nil)
    (upto_induction formula-decl nil bounded_nat_inductions nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (shift_left const-decl "digits" IEEE_854_values nil)
    (fp_num_finite_eta formula-decl nil IEEE_854_values nil))
   nil))
 (subnormal?_TCC1 0
  (subnormal?_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (zero? const-decl "bool" IEEE_854_values nil)
    (value const-decl "real" IEEE_854_values nil)
    (^ const-decl "real" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_expt application-judgement "int" exponentiation nil)
    (nzreal_expt application-judgement "nzreal" exponentiation nil)
    (nzint_times_nzint_is_nzint application-judgement "nzint" integers
     nil))
   nil))
 (normal?_TCC1 0
  (normal?_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (max_significand_TCC1 0
  (max_significand_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (min_significand_TCC1 0
  (min_significand_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (min_significand_TCC2 0
  (min_significand_TCC2-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (d_zero_TCC1 0
  (d_zero_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (Sum_value0 0
  (Sum_value0-1 nil 3321199176
   ("" (induct-and-simplify "n") (("" (grind) nil)) nil)
   ((minus_int_is_int application-judgement "int" integers nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Sum def-decl "real" sum_hack nil) (< const-decl "bool" reals nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (d_zero const-decl "digits" IEEE_854_values nil)
    (nat_induction formula-decl nil naturalnumbers nil))
   nil))
 (zero_finite_d_zero 0
  (zero_finite_d_zero-1 nil 3321199176
   ("" (grind :rewrites "Sum_value0"nil nil)
   ((minus_int_is_int application-judgement "int" integers nil)
    (zero? const-decl "bool" IEEE_854_values nil)
    (value const-decl "real" IEEE_854_values nil)
    (Sum_value0 formula-decl nil IEEE_854_values nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil))
   nil))
 (max_fp_pos_TCC1 0
  (max_fp_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (min_fp_pos_TCC1 0
  (min_fp_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (pos_zero_TCC1 0
  (pos_zero_TCC1-1 nil 3321199176
   ("" (rewrite "zero_finite_d_zero"nil nil)
   ((pos const-decl "sign_rep" enumerated_type_defs nil)
    (sign_rep type-eq-decl nil enumerated_type_defs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (Exponent type-eq-decl nil IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (> const-decl "bool" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (zero_finite_d_zero formula-decl nil IEEE_854_values nil))
   nil))
 (neg_zero_TCC1 0
  (neg_zero_TCC1-1 nil 3321199176
   ("" (rewrite "zero_finite_d_zero"nil nil)
   ((neg const-decl "sign_rep" enumerated_type_defs nil)
    (sign_rep type-eq-decl nil enumerated_type_defs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (Exponent type-eq-decl nil IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (> const-decl "bool" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (zero_finite_d_zero formula-decl nil IEEE_854_values nil))
   nil))
 (max_pos_TCC1 0
  (max_pos_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((pos const-decl "sign_rep" enumerated_type_defs nil)
    (max_fp_pos const-decl "fp_num" IEEE_854_values nil))
   nil))
 (max_pos_TCC2 0
  (max_pos_TCC2-1 nil 3321199176
   ("" (expand "value")
    (("" (expand "max_fp_pos")
      (("" (expand "pos")
        (("" (rewrite "expt_x0")
          (("" (lemma "pos_times_gt")
            (("" (assert)
              (("" (inst?)
                (("" (assert)
                  (("" (lemma "expt_pos")
                    (("" (inst?)
                      (("" (assert)
                        ((""
                          (case "Sum(p, value_digit(max_significand)) > 0")
                          (("1" (ground) nil)
                           ("2" (hide -1 -2 2)
                            (("2" (expand "Sum")
                              (("2"
                                (assert)
                                (("2"
                                  (lemma "Sum_nonneg")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (rewrite "value_digit")
                                      (("2"
                                        (rewrite "max_significand")
                                        (("2"
                                          (lemma "expt_pos")
                                          (("2"
                                            (inst?)
                                            (("2"
                                              (lemma "pos_times_gt")
                                              (("2"
                                                (inst?)
                                                (("2"
                                                  (ground)
                                                  nil))))))))))))))))))))))))))))))))))))))))))))))
    nil)
   ((max_fp_pos const-decl "fp_num" IEEE_854_values nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_x0 formula-decl nil exponentiation nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (Sum_nonneg formula-decl nil sum_hack nil)
    (expt_pos formula-decl nil exponentiation nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (integer nonempty-type-from-decl nil integers nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (max_significand const-decl "digits" IEEE_854_values nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil) (Sum def-decl "real" sum_hack nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (pos_times_gt formula-decl nil real_props nil)
    (pos const-decl "sign_rep" enumerated_type_defs nil)
    (value const-decl "real" IEEE_854_values nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (int_exp application-judgement "int" exponentiation nil))
   nil))
 (min_pos_TCC1 0
  (min_pos_TCC1-1 nil 3321199176 ("" (tcc) nil nil)
   ((pos const-decl "sign_rep" enumerated_type_defs nil)
    (min_fp_pos const-decl "fp_num" IEEE_854_values nil))
   nil))
 (min_pos_TCC2 0
  (min_pos_TCC2-1 nil 3321199176
   ("" (expand "min_fp_pos")
    (("" (expand "value")
      (("" (expand "pos")
        (("" (rewrite "expt_x0")
          (("" (lemma "expt_pos")
            (("" (inst?)
              (("1" (assert)
                (("1" (lemma "pos_times_gt")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1"
                        (case "Sum(p, value_digit(min_significand)) > 0")
                        (("1" (assert) (("1" (assertnil)))
                         ("2" (hide -1 -2 2)
                          (("2" (expand "Sum")
                            (("2" (lemma "Sum_nonneg")
                              (("2"
                                (inst?)
                                (("2"
                                  (rewrite "value_digit")
                                  (("2"
                                    (rewrite "min_significand")
                                    (("2"
                                      (lemma "expt_pos")
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (assert)
                                          nil)))))))))))))))))))))))))))
               ("2" (assert)
                (("2" (split)
                  (("1" (assertnil) ("2" (assertnil))))))))))))))))
    nil)
   ((int_exp application-judgement "int" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (value const-decl "real" IEEE_854_values nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_x0 formula-decl nil exponentiation nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (above nonempty-type-eq-decl nil integers nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (pos_times_gt formula-decl nil real_props nil)
    (Sum_nonneg formula-decl nil sum_hack nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Sum def-decl "real" sum_hack nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (min_significand const-decl "digits" IEEE_854_values nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (expt_pos formula-decl nil exponentiation nil)
    (pos const-decl "sign_rep" enumerated_type_defs nil)
    (min_fp_pos const-decl "fp_num" IEEE_854_values nil))
   nil))
 (max_neg_TCC1 0
  (max_neg_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((neg const-decl "sign_rep" enumerated_type_defs nil)
    (max_fp_neg const-decl "fp_num" IEEE_854_values nil))
   nil))
 (max_neg_TCC2 0
  (max_neg_TCC2-1 nil 3321199176
   ("" (expand "max_fp_neg")
    (("" (expand "value")
      (("" (expand "neg")
        (("" (rewrite "expt_x1")
          (("" (lemma "expt_pos")
            (("" (inst?)
              (("" (lemma "Sum_pos")
                (("" (inst?)
                  (("" (assert)
                    (("" (lemma "pos_times_gt")
                      (("" (inst?)
                        (("" (ground)
                          (("1" (inst + "0")
                            (("1" (rewrite "value_digit")
                              (("1"
                                (rewrite "expt_x0")
                                (("1"
                                  (rewrite "max_significand")
                                  (("1" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst + "0")
                            (("2" (rewrite "value_digit")
                              (("2"
                                (rewrite "expt_x0")
                                (("2"
                                  (rewrite "max_significand")
                                  (("2" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (inst + "0")
                            (("3" (rewrite "value_digit")
                              (("3"
                                (rewrite "max_significand")
                                (("3"
                                  (rewrite "expt_x0")
                                  (("3" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_exp application-judgement "int" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (value const-decl "real" IEEE_854_values nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (above nonempty-type-eq-decl nil integers nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (max_significand const-decl "digits" IEEE_854_values nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pos_times_gt formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (expt_x0 formula-decl nil exponentiation nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (Sum def-decl "real" sum_hack nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Sum_pos formula-decl nil sum_hack nil)
    (expt_pos formula-decl nil exponentiation nil)
    (neg const-decl "sign_rep" enumerated_type_defs nil)
    (max_fp_neg const-decl "fp_num" IEEE_854_values nil))
   nil))
 (min_neg_TCC1 0
  (min_neg_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((neg const-decl "sign_rep" enumerated_type_defs nil)
    (min_fp_neg const-decl "fp_num" IEEE_854_values nil))
   nil))
 (min_neg_TCC2 0
  (min_neg_TCC2-1 nil 3321199176
   ("" (expand "min_fp_neg")
    (("" (expand "value")
      (("" (expand "neg")
        (("" (rewrite "expt_x1")
          (("" (assert)
            (("" (lemma "expt_pos")
              (("" (inst?)
                (("" (lemma "Sum_pos")
                  (("" (inst?)
                    (("" (lemma "pos_times_gt")
                      (("" (inst?)
                        (("" (ground)
                          (("1" (inst + "p-1")
                            (("1" (rewrite "value_digit")
                              (("1"
                                (rewrite "min_significand")
                                (("1"
                                  (hide 1 3 4 5 6)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (lemma "expt_pos")
                                      (("1"
                                        (inst?)
                                        (("1" (assertnil 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" (assertnil 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" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_exp application-judgement "int" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (value const-decl "real" IEEE_854_values nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (expt_pos formula-decl nil exponentiation nil)
    (Sum_pos formula-decl nil sum_hack nil)
    (pos_times_gt formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Sum def-decl "real" sum_hack nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (min_significand const-decl "digits" IEEE_854_values nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (above nonempty-type-eq-decl nil integers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (integer nonempty-type-from-decl nil integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (neg const-decl "sign_rep" enumerated_type_defs nil)
    (min_fp_neg const-decl "fp_num" IEEE_854_values nil))
   nil))
 (max_fp_correct_TCC1 0
  (max_fp_correct_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (max_fp_correct_TCC2 0
  (max_fp_correct_TCC2-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (max_fp_correct 0
  (max_fp_correct-1 nil 3321199176
   ("" (rewrite "max_pos")
    (("" (rewrite "max_fp_pos")
      (("" (rewrite "value")
        (("" (rewrite "pos")
          (("" (rewrite "expt_x0")
            (("" (assert)
              ((""
                (case "forall (i:upto(p)):Sum(i,
          (LAMBDA (n: nat):
             IF n < p THEN max_significand(n) * (b ^ (-n)) ELSE 0 ENDIF))
        * b ^ E_max
        = b ^ (1 + E_max) - b ^ (1 + E_max - i)")
                (("1" (inst?)
                  (("1" (expand "value_digit") (("1" (propax) nil)))))
                 ("2" (hide 2)
                  (("2" (induct "i" 1 "upto_induction[p]")
                    (("1" (rewrite "Sum") (("1" (assertnil)))
                     ("2" (skosimp*)
                      (("2" (expand "Sum" +)
                        (("2" (replace -2)
                          (("2" (hide -2)
                            (("2" (assert)
                              (("2"
                                (rewrite "max_significand")
                                (("2"
                                  (lemma "expt_plus")
                                  (("2"
                                    (inst-cp - "1" "E_max - jt!1" "b")
                                    (("2"
                                      (inst - "E_max" "-jt!1" "b")
                                      (("2"
                                        (replace -1)
                                        (("2"
                                          (hide -1)
                                          (("2"
                                            (replace -1)
                                            (("2"
                                              (hide -1)
                                              (("2"
                                                (rewrite "expt_x1")
                                                (("2"
                                                  (assert)
                                                  nil))))))))))))))))))))))))))))))))))))))))))))))
    nil)
   ((max_fp_pos const-decl "fp_num" IEEE_854_values nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (expt_plus formula-decl nil exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (upto_induction formula-decl nil bounded_nat_inductions nil)
    (pred type-eq-decl nil defined_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (Sum def-decl "real" sum_hack nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (expt_x0 formula-decl nil exponentiation nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (int_exp application-judgement "int" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (max_significand const-decl "digits" IEEE_854_values nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (pos const-decl "sign_rep" enumerated_type_defs nil)
    (finite adt-constructor-decl
     "[[sign_rep, Exponent, digits] -> (finite?)]" IEEE_854_values nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (above nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (Exponent type-eq-decl nil IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (> const-decl "bool" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sign_rep type-eq-decl nil enumerated_type_defs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (value const-decl "real" IEEE_854_values nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (max_pos const-decl "posreal" IEEE_854_values nil))
   nil))
 (min_fp_correct_TCC1 0
  (min_fp_correct_TCC1-1 nil 3321199176 ("" (tcc :defs !) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (min_fp_correct 0
  (min_fp_correct-1 nil 3321199176
   ("" (expand "min_fp_pos")
    (("" (expand "value")
      (("" (expand "pos")
        (("" (rewrite "expt_x0")
          (("" (assert)
            ((""
              (case-replace
               "Sum(p,value_digit(min_significand))= b^(1-p)")
              (("1" (hide -1)
                (("1" (lemma "expt_plus")
                  (("1" (inst - "(1 - p)" "E_min" "b")
                    (("1" (assertnil nil)) nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (expand "Sum")
                  (("2" (expand "value_digit")
                    (("2" (expand "min_significand")
                      (("2"
                        (case "forall (i:below(p)):Sum(i,
                   LAMBDA (n: nat):
                     IF n < p THEN IF n < p - 1 THEN 0 ELSE 1 ENDIF * b ^ (-n)
                     ELSE 0
                     ENDIF)
                 = 0")
                        (("1" (inst?) (("1" (assertnil nil)) nil)
                         ("2" (hide 2)
                          (("2" (induct-and-rewrite "i" 1 "Sum"nil
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((value const-decl "real" IEEE_854_values nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_x0 formula-decl nil exponentiation nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (int_exp application-judgement "int" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Sum def-decl "real" sum_hack nil) (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (min_significand const-decl "digits" IEEE_854_values nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (expt_plus formula-decl nil exponentiation nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (pred type-eq-decl nil defined_types nil)
    (below_induction formula-decl nil bounded_nat_inductions nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (pos const-decl "sign_rep" enumerated_type_defs nil)
    (min_fp_pos const-decl "fp_num" IEEE_854_values nil))
   nil))
 (value0 0
  (value0-1 nil 3321199176
   ("" (skosimp*)
    (("" (expand "value")
      (("" (rewrite "zero_times3")
        (("1" (rewrite "zero_times3")
          (("1" (lemma "expt_nonzero")
            (("1" (inst? :copy? t)
              (("1" (assert)
                (("1" (hide -2)
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (hide -1)
                        (("1" (rewrite "Sum_zero")
                          (("1" (prop)
                            (("1" (expand "d_zero")
                              (("1"
                                (apply-extensionality)
                                (("1"
                                  (expand "value_digit")
                                  (("1"
                                    (inst?)
                                    (("1"
                                      (rewrite "zero_times3")
                                      (("1"
                                        (lemma "expt_nonzero")
                                        (("1"
                                          (inst?)
                                          (("1"
                                            (assert)
                                            nil)))))))))))))))
                             ("2" (replace -1)
                              (("2"
                                (expand "d_zero")
                                (("2"
                                  (expand "value_digit")
                                  (("2"
                                    (propax)
                                    nil)))))))))))))))))))))))))))
         ("2" (assertnil))))))
    nil)
   ((int_exp application-judgement "int" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (value const-decl "real" IEEE_854_values nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (Sum_zero formula-decl nil sum_hack nil)
    (d_zero const-decl "digits" IEEE_854_values nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (expt_nonzero formula-decl nil exponentiation nil)
    (Exp adt-accessor-decl "[(finite?) -> Exponent]" IEEE_854_values
     nil)
    (Exponent type-eq-decl nil IEEE_854_values nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_values
     nil)
    (E_max formal-const-decl "integer" IEEE_854_values nil)
    (integer nonempty-type-from-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
          nil)
    (sign_rep type-eq-decl nil enumerated_type_defs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (d adt-accessor-decl "[(finite?) -> digits]" IEEE_854_values nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (value_digit const-decl "nonneg_real" IEEE_854_values nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (digits type-eq-decl nil IEEE_854_values nil)
    (b formal-const-decl "above(1)" IEEE_854_values nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (p formal-const-decl "above(1)" IEEE_854_values nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil) (Sum def-decl "real" sum_hack nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (zero_times3 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   nil))
 (value_of_zero 0
  (value_of_zero-1 nil 3321199176
   ("" (rewrite "value0")
    (("" (expand "pos_zero") (("" (propax) nil)))) nil)
   ((pos_zero const-decl "{fin | zero?(fin)}" IEEE_854_values nil)
    (zero? const-decl "bool" IEEE_854_values nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (fp_num type-decl nil IEEE_854_values nil)
    (value0 formula-decl nil IEEE_854_values nil))
   nil))
 (normal_value 0
  (normal_value-1 nil 3321199176
   ("" (skosimp*)
    (("" (case-replace "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
      (("1" (hide -1)
        (("1"
          (case "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
              value(finite(s,n+E_min,d))=value(normalize(finite(s,n+E_min,d)))")
          (("1" (inst - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
            (("1" (assertnil nil) ("2" (assertnil nil)) nil)
           ("2" (hide 2)
            (("2" (induct "n" 1 "upto_induction[E_max-E_min]")
              (("1" (skosimp*)
                (("1" (expand "normalize") (("1" (propax) nil nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (rewrite "normalize")
                  (("2" (lift-if)
                    (("2" (ground)
                      (("2" (inst?)
                        (("2" (replace -3 :dir rl)
                          (("2" (hide -3)
                            (("2" (expand "value")
                              (("2"
                                (expand "value_digit")
                                (("2"
                                  (case-replace
                                   "Sum(p,(LAMBDA (n: nat):
                       IF n < p THEN shift_left(d!1)(n) * (b ^ (-n))
                       ELSE 0
                       ENDIF))=b*Sum(p,(LAMBDA (n: nat): IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))")
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (lemma "expt_plus")
                                      (("1"
                                        (inst - "1" "E_min+jt!1" "b")
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (rewrite "expt_x1")
                                              (("1" (assertnil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
--> --------------------

--> maximum size reached

--> --------------------

[ Verzeichnis aufwärts0.95unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik