Quelle  sum_lemmas.prf  Sprache: unbekannt

(sum_lemmas
 (mant_digit_fun_TCC1 0
  (mant_digit_fun_TCC1-1 nil 3321198912 ("" (tcc) 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/= const-decl "boolean" notequal nil)
    (minus_int_is_int application-judgement "int" integers nil))
   nil))
 (Sum_pos_less_1_TCC1 0
  (Sum_pos_less_1_TCC1-1 nil 3321198912 ("" (tcc) 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)
    (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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (b formal-const-decl "above(1)" sum_lemmas nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (mant_digit_fun type-eq-decl nil sum_lemmas 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)
    (/= const-decl "boolean" notequal nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   nil))
 (Sum_pos_less_1 0
  (Sum_pos_less_1-1 nil 3321198912
   ("" (induct "i")
    (("1" (expand "Sum")
      (("1" (rewrite "expt_x0") (("1" (assert) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (rewrite "Sum")
        (("2" (inst?)
          (("2" (assert)
            (("2" (typepred "d!1")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (case-replace "b ^ (-j!1 - 1) * b = b^(-j!1)")
                    (("1" (assert)
                      (("1" (skosimp*) (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (hide -1 -2 2)
                      (("2" (lemma "expt_plus")
                        (("2" (inst - "(-(j!1+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))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (expt_plus formula-decl nil exponentiation nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (expt_x0 formula-decl nil exponentiation nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (b formal-const-decl "above(1)" sum_lemmas nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (mant_digit_fun type-eq-decl nil sum_lemmas nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (Sum def-decl "real" sum_hack nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   nil))
 (floor_Sum_mant 0
  (floor_Sum_mant-1 nil 3321198912
   ("" (skosimp*)
    (("" (lemma "Sum_pos_less_1")
      (("" (inst?)
        (("" (lemma "expt_pos")
          (("" (inst?)
            (("1" (case "1-b^(-i!1)<1")
              (("1" (case "Sum(i!1, d!1) < 1")
                (("1" (flatten)
                  (("1" (hide -2 -3 -5)
                    (("1" (assert)
                      (("1"
                        (case "forall (r:real): floor(r)=0 iff 0<=r & r<1")
                        (("1" (inst?) (("1" (assert) nil)))
                         ("2" (hide -1 -2 2) (("2" (tcc) nil)))))))))))
                 ("2" (assert) nil)))
               ("2" (assert) nil) ("3" (assert) nil)))
             ("2" (split)
              (("1" (assert) nil) ("2" (assert) nil))))))))))))
    nil)
   ((Sum_pos_less_1 formula-decl nil sum_lemmas nil)
    (expt_pos formula-decl nil exponentiation nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (< const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integer nonempty-type-from-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (Sum def-decl "real" sum_hack nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (mant_digit_fun type-eq-decl nil sum_lemmas nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (b formal-const-decl "above(1)" sum_lemmas nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (minus_int_is_int application-judgement "int" integers nil))
   nil)))