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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: PVS

Original von: PVS©

(integral_bounded
 (IMP_integral_prep_TCC1 0
  (IMP_integral_prep_TCC1-1 nil 3282561874
   ("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
   ((connected_domain formula-decl nil integral_bounded nil)) shostak))
 (IMP_integral_prep_TCC2 0
  (IMP_integral_prep_TCC2-1 nil 3282561874
   ("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil integral_bounded nil)) shostak))
 (int_to_bnd_TCC1 0
  (int_to_bnd_TCC1-1 nil 3282561874
   ("" (skosimp*) (("" (assertnil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (int_to_bnd_TCC2 0
  (int_to_bnd_TCC2-1 nil 3282561874
   ("" (skosimp*) (("" (assertnil nil)) 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))
   shostak))
 (int_to_bnd 0
  (int_to_bnd-2 nil 3477651374
   ("" (skosimp*)
    ((""
      (case "(FORALL (eps: posreal):
                                                      (EXISTS (EP: partition[T](a!1,b!1)):
                                                        (FORALL (j: below(length(EP)-1)):
                                                          FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1))
                                                            IMPLIES
                                                             abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))")
      (("1" (assert)
        (("1" (inst - "1000")
          (("1" (skosimp*)
            (("1" (inst + "EP!1")
              (("1" (skosimp*)
                (("1" (inst - "j!1")
                  (("1" (expand "bounded_on?")
                    (("1"
                      (inst +
                       "1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))")
                      (("1" (skosimp*)
                        (("1" (inst?)
                          (("1" (assert)
                            (("1" (lemma "abs_diff")
                              (("1"
                                (inst
                                 -
                                 "f!1(x!1)"
                                 "f!1(EP!1`seq(j!1))")
                                (("1" (assertnil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (typepred "EP!1")
                        (("2" (inst - "j!1") (("2" (assertnil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp*)
          (("2" (assert)
            (("2" (lemma "Lemma_1[T]")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (inst -1 "eps!1")
                    (("2" (skosimp*)
                      (("2"
                        (name "EP"
                              "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)")
                        (("1" (inst + "EP")
                          (("1" (skosimp*)
                            (("1" (case "T_pred(xx!1)")
                              (("1"
                                (case
                                 "abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0")
                                (("1"
                                  (cross-mult 1)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (name
                                       "SecJ"
                                       "(EP`seq(1 + j!1) - EP`seq(j!1))")
                                      (("1"
                                        (name
                                         "F_DIF"
                                         "(f!1((EP)(j!1)) - f!1(xx!1))")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (rewrite
                                             "abs_mult"
                                             :dir
                                             rl)
                                            (("1"
                                              (case-replace
                                               "EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) +
                                                                                                                                                                   (EP`seq(j!1) * f!1(EP`seq(j!1))-
                                                                                                                                                                     EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF")
                                              (("1"
                                                (hide -1)
                                                (("1"
                                                  (lemma "abs_neg")
                                                  (("1"
                                                    (inst
                                                     -
                                                     "SecJ * F_DIF")
                                                    (("1"
                                                      (replace -1)
                                                      (("1"
                                                        (hide -1)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "EP"
                                                           "EP"
                                                           "gxis(a!1,b!1,EP,j!1,true,xx!1)"
                                                           "gxis(a!1,b!1,EP,j!1,false,xx!1)")
                                                          (("1"
                                                            (split -5)
                                                            (("1"
                                                              (expand
                                                               "Rie_sum")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (rewrite
                                                                     "sigma_minus[below[length(EP)-1]]")
                                                                    (("1"
                                                                      (case-replace
                                                                       "(LAMBDA (i: below(length(EP) - 1)):
                                                                                                                                                                                                                                                                                      EP`seq(i) *
                                                                                                                                                                                                                                                                                       f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i))
                                                                                                                                                                                                                                                                                       +
                                                                                                                                                                                                                                                                                       EP`seq(1 + i) *
                                                                                                                                                                                                                                                                                        f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
                                                                                                                                                                                                                                                                                       -
                                                                                                                                                                                                                                                                                       EP`seq(i) *
                                                                                                                                                                                                                                                                                        f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
                                                                                                                                                                                                                                                                                       -
                                                                                                                                                                                                                                                                                       EP`seq(1 + i) *
                                                                                                                                                                                                                                                                                        f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i)))
                                                                                                                                                                                                                                                                     =                (LAMBDA (i: below(length(EP) - 1)):
                                                                                                                                                                                                                                                                                                                                                                          IF i = j!1 THEN
                                                                                                                                                                                                                                                                                                                                                           (EP`seq(1 + j!1) - EP`seq(j!1)) * (f!1(EP(j!1)) - f!1(xx!1))
                                                                                                                                                                                                                                                                                                                                                                           ELSE 0
                                                                                                                                                                                                                                                                                                                                                                          ENDIF)")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (hide
                                                                           -1)
                                                                          (("1"
                                                                            (case-replace
                                                                             "EP`seq(1 + j!1) * f!1(EP`seq(j!1)) -
                                                                                                                                                                                                                                                                                                                               EP`seq(1 + j!1) * f!1(xx!1)
                                                                                                                                                                                                                                                                                                                               +
                                                                                                                                                                                                                                                                                                                               (EP`seq(j!1) * f!1(xx!1) -
                                                                                                                                                                                                                                                                                                                                 EP`seq(j!1) * f!1(EP`seq(j!1)))
                                                                                                                                                                                                                                                                                                     = SecJ*F_DIF")
                                                                            (("1"
                                                                              (hide
                                                                               -1)
                                                                              (("1"
                                                                                (case
                                                                                 "j!1 < length(EP) - 2")
                                                                                (("1"
                                                                                  (lemma
                                                                                   "sigma_below[length(EP)-1].sigma_split_ge")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "_"
                                                                                     "length(EP) - 2"
                                                                                     "0"
                                                                                     "j!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (inst?)
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (replace
                                                                                             -1)
                                                                                            (("1"
                                                                                              (hide
                                                                                               -1)
                                                                                              (("1"
                                                                                                (case-replace
                                                                                                 "sigma(1 + j!1, length(EP) - 2,
                                                                                                                                                                                                                                                                                                                                                                                                       (LAMBDA (i: below(length(EP) - 1)):
                                                                                                                                                                                                                                                                                                                                                                                                          IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0")
                                                                                                (("1"
                                                                                                  (hide
                                                                                                   -1)
                                                                                                  (("1"
                                                                                                    (rewrite
                                                                                                     "sigma_last_ge")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (case
                                                                                                         "sigma(0, j!1 - 1,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               (LAMBDA (i: below(length(EP) - 1)):
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (lemma
                                                                                                           "sigma_restrict_eq[below(length(EP)-1)]")
                                                                                                          (("2"
                                                                                                            (inst?)
                                                                                                            (("2"
                                                                                                              (inst
                                                                                                               -
                                                                                                               "(LAMBDA (i: below(length(EP) - 1)): 0)")
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "restrict")
                                                                                                                (("2"
                                                                                                                  (replace
                                                                                                                   -1)
                                                                                                                  (("2"
                                                                                                                    (hide
                                                                                                                     -1)
                                                                                                                    (("2"
                                                                                                                      (lemma
                                                                                                                       "sigma_const[below(length(EP)-1)]")
                                                                                                                      (("2"
                                                                                                                        (inst?)
                                                                                                                        (("2"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("3"
                                                                                                          (skosimp*)
                                                                                                          (("3"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (hide
                                                                                                   2)
                                                                                                  (("2"
                                                                                                    (lemma
                                                                                                     "sigma_restrict_eq[below(length(EP)-1)]")
                                                                                                    (("1"
                                                                                                      (inst?)
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         -
                                                                                                         "(LAMBDA (i: below(length(EP) - 1)): 0)")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "restrict")
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -1)
                                                                                                            (("1"
                                                                                                              (hide
                                                                                                               -1)
                                                                                                              (("1"
                                                                                                                (lemma
                                                                                                                 "sigma_const[below(length(EP)-1)]")
                                                                                                                (("1"
                                                                                                                  (inst?)
                                                                                                                  (("1"
                                                                                                                    (assert)
                                                                                                                    nil
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (hide
                                                                                                       2)
                                                                                                      (("2"
                                                                                                        (skosimp*)
                                                                                                        (("2"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("3"
                                                                                                  (skosimp*)
                                                                                                  (("3"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (case
                                                                                   "j!1 = length(EP) - 2")
                                                                                  (("1"
                                                                                    (rewrite
                                                                                     "sigma_last_ge")
                                                                                    (("1"
                                                                                      (case-replace
                                                                                       "sigma(0, length(EP) - 3,
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          (LAMBDA (i: below(length(EP) - 1)):
                                                                                                                                                                                                                                                                                                                                                                                                                                                                             IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil)
                                                                                       ("2"
                                                                                        (lemma
                                                                                         "sigma_restrict_eq[below(length(EP)-1)]")
                                                                                        (("1"
                                                                                          (inst?)
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "(LAMBDA (i: below(length(EP) - 1)): 0)")
                                                                                            (("1"
                                                                                              (expand
                                                                                               "restrict")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (lemma
                                                                                                   "sigma_const[below(length(EP)-1)]")
                                                                                                  (("1"
                                                                                                    (inst?)
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (skosimp*)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("3"
                                                                                        (skosimp*)
                                                                                        (("3"
                                                                                          (assert)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide
                                                                         -1
                                                                         2)
                                                                        (("2"
                                                                          (apply-extensionality
                                                                           1
                                                                           :hide?
                                                                           t)
                                                                          (("2"
                                                                            (expand
                                                                             "gxis")
                                                                            (("2"
                                                                              (lift-if)
                                                                              (("2"
                                                                                (ground)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (expand
                                                                         "gxis")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (lemma
                                                               "N_from_delta")
                                                              (("2"
                                                                (inst?)
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("3"
                                                              (lemma
                                                               "N_from_delta")
                                                              (("3"
                                                                (inst?)
                                                                (("3"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2" (assertnil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (typepred "EP")
                                    (("2"
                                      (inst - "j!1")
                                      (("2" (assertnil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (lemma "connected_domain")
                                  (("2"
                                    (expand "connected?")
                                    (("2"
                                      (inst?)
                                      (("2"
                                        (inst?)
                                        (("2" (assertnil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide 2)
                          (("2" (case "(b!1 - a!1) / delta!1 > 0")
                            (("1" (assertnil nil)
                             ("2" (cross-mult 1) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (hide 2)
        (("3" (skosimp*)
          (("3" (typepred "EP!1")
            (("3" (inst - "j!1") (("3" (assertnil nil)) nil)) nil))
          nil))
        nil)
       ("4" (hide 2)
        (("4" (skosimp*)
          (("4" (lemma "connected_domain")
            (("4" (expand "connected?")
              (("4" (inst - "_" "_" "xx!1")
                (("4" (inst?)
                  (("4" (inst?) (("4" (assertnil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (partition type-eq-decl nil integral_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-subtype-decl nil integral_bounded nil)
    (T_pred const-decl "[real -> boolean]" integral_bounded nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (a!1 skolem-const-decl "T" integral_bounded nil)
    (b!1 skolem-const-decl "T" integral_bounded nil)
    (EP!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded
     nil)
    (j!1 skolem-const-decl "below(length(EP!1) - 1)" integral_bounded
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (abs_diff formula-decl nil abs_lems "reals/")
    (real_le_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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (bounded_on? const-decl "bool" integral_bounded nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Lemma_1 formula-decl nil integral_prep nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (j!1 skolem-const-decl "below(length(EP) - 1)" integral_bounded
     nil)
    (EP skolem-const-decl
     "{fs: finite_sequence[{x | a!1 <= x AND x <= b!1}] |
         length(fs) > 1 AND
          seq(fs)(0) = a!1 AND
           seq(fs)(length(fs) - 1) = b!1 AND
            (FORALL (ii: below(length(fs) - 1)):
               seq(fs)(ii) < seq(fs)(1 + ii))}" integral_bounded nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (abs_neg formula-decl nil abs_lems "reals/")
    (FALSE const-decl "bool" booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (gxis const-decl "(xis?(a, b, P))" integral_prep nil)
    (xis? const-decl "bool" integral_def nil)
    (N_from_delta formula-decl nil integral_def nil)
    (Rie_sum const-decl "real" integral_def nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (sigma_split_ge formula-decl nil sigma_below "reals/")
    (sigma_restrict_eq formula-decl nil sigma "reals/")
    (sigma_nat application-judgement "nat" sigma_below "reals/")
    (sigma_const formula-decl nil sigma "reals/")
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (restrict const-decl "[T -> real]" sigma "reals/")
    (sigma_last_ge formula-decl nil sigma_below "reals/")
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (sigma def-decl "real" sigma "reals/")
    (int_below type-eq-decl nil sigma_below "reals/")
    (sigma_minus formula-decl nil sigma "reals/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (abs_mult formula-decl nil real_props nil)
    (connected_domain formula-decl nil integral_bounded nil)
    (connected? const-decl "bool" deriv_domain_def nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (integer nonempty-type-from-decl nil integers nil)
    (eq_partition const-decl "partition(a, b)" integral_def nil)
    (above nonempty-type-eq-decl nil integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil)
  (int_to_bnd-1 nil 3282561219
   ("" (skosimp*)
    ((""
      (case "(FORALL (eps: posreal):
                                               (EXISTS (EP: partition[T](a!1,b!1)):
                                                 (FORALL (j: below(length(EP)-1)):
                                                   FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1))
                                                     IMPLIES
                                                      abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))")
      (("1" (assert)
        (("1" (inst - "1000")
          (("1" (skosimp*)
            (("1" (inst + "EP!1")
              (("1" (skosimp*)
                (("1" (inst - "j!1")
                  (("1" (expand "bounded_on?")
                    (("1"
                      (inst +
                       "1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))")
                      (("1" (skosimp*)
                        (("1" (inst?)
                          (("1" (assert)
                            (("1" (lemma "abs_diff")
                              (("1"
                                (inst
                                 -
                                 "f!1(x!1)"
                                 "f!1(EP!1`seq(j!1))")
                                (("1" (assertnil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (typepred "EP!1")
                        (("2" (inst - "j!1") (("2" (assertnil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp*)
          (("2" (assert)
            (("2" (lemma "Lemma_1[T]")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (inst -1 "eps!1")
                    (("2" (skosimp*)
                      (("2"
                        (name "EP"
                              "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)")
                        (("1" (inst + "EP")
                          (("1" (skosimp*)
                            (("1" (case "T_pred(xx!1)")
                              (("1"
                                (case
                                 "abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0")
                                (("1"
                                  (cross-mult 1)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (name
                                       "SecJ"
                                       "(EP`seq(1 + j!1) - EP`seq(j!1))")
                                      (("1"
                                        (name
                                         "F_DIF"
                                         "(f!1((EP)(j!1)) - f!1(xx!1))")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (rewrite
                                             "abs_mult"
                                             :dir
                                             rl)
                                            (("1"
                                              (case-replace
                                               "EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) +
                                                                                                                                                       (EP`seq(j!1) * f!1(EP`seq(j!1))-
                                                                                                                                                         EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF")
                                              (("1"
                                                (hide -1)
                                                (("1"
                                                  (lemma "abs_neg")
                                                  (("1"
                                                    (inst
                                                     -
                                                     "SecJ * F_DIF")
                                                    (("1"
                                                      (replace -1)
                                                      (("1"
                                                        (hide -1)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "EP"
                                                           "EP"
                                                           "gxis(a!1,b!1,EP,j!1,true,xx!1)"
                                                           "gxis(a!1,b!1,EP,j!1,false,xx!1)")
                                                          (("1"
                                                            (split -5)
                                                            (("1"
                                                              (expand
                                                               "Rie_sum")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (rewrite
                                                                     "sigma_minus[below[length(EP)-1]]")
                                                                    (("1"
                                                                      (case-replace
                                                                       "(LAMBDA (i: below(length(EP) - 1)):
                                                                                                                                                                                                                                                                    EP`seq(i) *
                                                                                                                                                                                                                                                                     f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i))
                                                                                                                                                                                                                                                                     +
                                                                                                                                                                                                                                                                     EP`seq(1 + i) *
                                                                                                                                                                                                                                                                      f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
                                                                                                                                                                                                                                                                     -
                                                                                                                                                                                                                                                                     EP`seq(i) *
                                                                                                                                                                                                                                                                      f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
                                                                                                                                                                                                                                                                     -
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.143 Sekunden  (vorverarbeitet)  ¤





Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


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