Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: DirectionSwitch.vdmrt Sprache: VDM

Original von: PVS^©

(complete_integral
(IMP_integral_TCC1 0
  (IMP_integral_TCC1-1 nil 3458543751
   ("" (typepred "mu")
    (("" (expand "complete_measure?") (("" (flatten) nil nil)) nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil complete_integral nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" complete_integral 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)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (complete_measure? const-decl "bool" generalized_measure_def nil)
    (complete_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (mu formal-const-decl "complete_measure" complete_integral nil))
   nil))
(complete_integral_ae_eq 0
  (complete_integral_ae_eq-1 nil 3410758578
   ("" (skosimp)
    (("" (lemma "ae_eq_measurable" ("f" "h!1" "g" "f!1"))
      (("" (split -1)
        (("1" (lemma "integral_ae_eq" ("f" "f!1" "h" "h!1"))
          (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)
         ("2" (hide 2)
          (("2" (expand "ae_eq?")
            (("2" (expand "restrict")
              (("2" (expand "pointwise_ae?")
                (("2" (expand "ae?")
                  (("2" (expand "fullset")
                    (("2" (expand "ae_in?")
                      (("2" (skosimp)
                        (("2" (inst + "E!1")
                          (("2" (skosimp)
                            (("2" (inst - "x!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((mu formal-const-decl "complete_measure" complete_integral nil)
    (complete_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (complete_measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (S formal-const-decl "sigma_algebra" complete_integral nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil complete_integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (ae_eq_measurable formula-decl nil complete_measure_theory nil)
    (restrict const-decl "R" restrict nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     complete_integral nil)
    (subset_algebra_fullset name-judgement "(S)" complete_integral nil)
    (ae? const-decl "bool" measure_theory nil)
    (ae_in? const-decl "bool" measure_theory nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (set type-eq-decl nil sets nil)
    (TRUE const-decl "bool" booleans nil)
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (pointwise_ae? const-decl "bool" measure_theory nil)
    (ae_eq? const-decl "bool" measure_theory nil)
    (integral_ae_eq formula-decl nil integral nil))
   shostak))
(complete_measurable_ae_0 0
  (complete_measurable_ae_0-1 nil 3410758703
   ("" (skosimp)
    (("" (lemma "ae_eq_measurable" ("f" "h!1" "g" "lambda (x:T): 0"))
      (("1" (split -1)
        (("1" (lemma "measurable_ae_0" ("h" "h!1"))
          (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)
         ("2" (hide 2)
          (("2" (expand "ae_0?")
            (("2" (expand "ae_eq?") (("2" (propax) nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (lemma "const_measurable" ("c" "0"))
          (("2" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((mu formal-const-decl "complete_measure" complete_integral nil)
    (complete_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (complete_measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (S formal-const-decl "sigma_algebra" complete_integral nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil complete_integral nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (ae_eq_measurable formula-decl nil complete_measure_theory nil)
    (ae_eq? const-decl "bool" measure_theory nil)
    (ae_0? const-decl "bool" measure_theory nil)
    (measurable_ae_0 formula-decl nil integral nil)
    (const_measurable formula-decl nil measure_space nil))
   shostak))
(monotone_convergence_complete 0
  (monotone_convergence_complete-1 nil 3410767863
   ("" (skosimp)
    (("" (expand "ae_monotonic_converges?")
      (("" (expand "monotonic_converges?")
        (("" (flatten)
          (("" (split)
            (("1" (lemma "monotone_convergence" ("F" "F!1"))
              (("1" (replace -2)
                (("1" (replace -4)
                  (("1" (flatten)
                    (("1" (skosimp)
                      (("1" (typepred "f!1")
                        (("1" (inst - "f!1")
                          (("1" (assert)
                            (("1" (expand "converges_upto?")
                              (("1"
                                (flatten)
                                (("1"
                                  (assert)
                                  (("1"
                                    (lemma
                                     "ae_convergence_eq"
                                     ("F" "F!1" "f" "f!1" "g" "h!1"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (lemma
                                         "complete_integral_ae_eq"
                                         ("f" "f!1" "h" "h!1"))
                                        (("1"
                                          (assert)
                                          (("1"
                                            (flatten)
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (lemma "monotone_convergence" ("F" "-F!1"))
              (("1" (split -1)
                (("1" (case-replace "bounded?(integral o -F!1)")
                  (("1" (flatten)
                    (("1" (skosimp)
                      (("1" (inst - "f!1")
                        (("1" (assert)
                          (("1"
                            (lemma "complete_integral_ae_eq"
                             ("f" "-f!1" "h" "h!1"))
                            (("1" (case-replace "ae_eq?(-f!1, h!1)")
                              (("1"
                                (flatten)
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "converges_upto?")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (split)
                                        (("1"
                                          (rewrite
                                           "metric_convergence_def")
                                          (("1"
                                            (rewrite
                                             "metric_convergence_def")
                                            (("1"
                                              (expand
                                               "metric_converges_to")
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (inst - "r!1")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (inst + "n!1")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "i!1")
                                                          (("1"
                                                            (expand
                                                             "ball")
                                                            (("1"
                                                              (expand
                                                               "member")
                                                              (("1"
                                                                (rewrite
                                                                 "integral_opp"
                                                                 -4)
                                                                (("1"
                                                                  (replace
                                                                   -4
                                                                   1
                                                                   rl)
                                                                  (("1"
                                                                    (expand
                                                                     "o ")
                                                                    (("1"
                                                                      (expand
                                                                       "-")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (rewrite
                                                                           "integral_opp"
                                                                           -7)
                                                                          (("1"
                                                                            (name-replace
                                                                             "DRL1"
                                                                             "integral(f!1)")
                                                                            (("1"
                                                                              (name-replace
                                                                               "DRL2"
                                                                               "integral(F!1(i!1))")
                                                                              (("1"
                                                                                (hide-all-but
                                                                                 (-7
                                                                                  1))
                                                                                (("1"
                                                                                  (grind)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (typepred
                                                                                 "mu")
                                                                                (("2"
                                                                                  (expand
                                                                                   "complete_measure?")
                                                                                  (("2"
                                                                                    (flatten)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (typepred
                                                                               "mu")
                                                                              (("2"
                                                                                (expand
                                                                                 "complete_measure?")
                                                                                (("2"
                                                                                  (flatten)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (typepred "mu")
                                              (("2"
                                                (expand
                                                 "complete_measure?")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (typepred "mu")
                                            (("2"
                                              (expand
                                               "complete_measure?")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (flatten)
                                          (("2"
                                            (hide-all-but (-7 2))
                                            (("2"
                                              (expand "increasing?")
                                              (("2"
                                                (expand "decreasing?")
                                                (("2"
                                                  (expand "-")
                                                  (("2"
                                                    (expand "o ")
                                                    (("2"
                                                      (skosimp)
                                                      (("2"
                                                        (inst
                                                         -
                                                         "x!1"
                                                         "y!1")
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (rewrite
                                                             "integral_opp")
                                                            (("2"
                                                              (rewrite
                                                               "integral_opp")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but (1 -3 -6))
                                (("2"
                                  (expand "ae_convergence?")
                                  (("2"
                                    (expand "ae_eq?")
                                    (("2"
                                      (expand "restrict")
                                      (("2"
                                        (expand "ae_convergence_in?")
                                        (("2"
                                          (expand "pointwise_ae?")
                                          (("2"
                                            (expand "ae?")
                                            (("2"
                                              (expand "fullset")
                                              (("2"
                                                (expand "ae_in?")
                                                (("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (typepred
                                                     "union(E!1,E!2)")
                                                    (("2"
                                                      (inst
                                                       +
                                                       "union(E!1, E!2)")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (inst
                                                           -
                                                           "x!1")
                                                          (("2"
                                                            (inst
                                                             -
                                                             "x!1")
                                                            (("2"
                                                              (expand
                                                               "union")
                                                              (("2"
                                                                (expand
                                                                 "member")
                                                                (("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (expand
                                                                       "-")
                                                                      (("2"
                                                                        (expand
                                                                         "-")
                                                                        (("2"
                                                                          (hide
                                                                           -1
                                                                           1
                                                                           2)
                                                                          (("2"
                                                                            (rewrite
                                                                             "metric_convergence_def")
                                                                            (("2"
                                                                              (rewrite
                                                                               "metric_convergence_def")
                                                                              (("2"
                                                                                (expand
                                                                                 "metric_converges_to")
                                                                                (("2"
                                                                                  (typepred
                                                                                   "abs(h!1(x!1)+f!1(x!1))")
                                                                                  (("2"
                                                                                    (expand
                                                                                     ">=")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "<="
                                                                                       -1)
                                                                                      (("2"
                                                                                        (split
                                                                                         -1)
                                                                                        (("1"
                                                                                          (inst
                                                                                           -
                                                                                           "abs(f!1(x!1) + h!1(x!1))/2")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "abs(f!1(x!1) + h!1(x!1))/2")
                                                                                            (("1"
                                                                                              (skosimp*)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 -
                                                                                                 "n!1+n!2")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -
                                                                                                   "n!1+n!2")
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "ball")
                                                                                                      (("1"
                                                                                                        (grind)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (hide-all-but
                                                                                           (-1
                                                                                            1))
                                                                                          (("2"
                                                                                            (grind)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (typepred "mu")
                                (("3"
                                  (expand "complete_measure?")
                                  (("3" (flatten) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide-all-but (1 -4))
                    (("2" (expand "-")
                      (("2" (expand "o ")
                        (("2" (expand "bounded?")
                          (("2" (flatten)
                            (("2" (split)
                              (("1"
                                (hide -1)
                                (("1"
                                  (expand "bounded_above?")
                                  (("1"
                                    (expand "bounded_below?")
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (inst + "-a!1")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (inst - "x!1")
                                            (("1"
                                              (rewrite "integral_opp")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide -2)
                                (("2"
                                  (expand "bounded_above?")
                                  (("2"
                                    (expand "bounded_below?")
                                    (("2"
                                      (skosimp)
                                      (("2"
                                        (inst + "-a!1")
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (inst - "x!1")
                                            (("2"
                                              (rewrite "integral_opp")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (typepred "mu")
                    (("3" (expand "complete_measure?")
                      (("3" (flatten) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (hide-all-but (-1 1))
                  (("2" (expand "ae_increasing?")
                    (("2" (expand "ae_decreasing?")
                      (("2" (skosimp)
                        (("2" (inst + "E!1")
                          (("2" (skosimp)
                            (("2" (inst - "x!1")
                              (("2"
                                (skosimp)
                                (("2"
                                  (assert)
                                  (("2"
                                    (inst - "i!1" "j!1")
                                    (("2"
                                      (expand "-")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "-")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skolem + ("n!1"))
                (("2" (expand "-") (("2" (propax) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((ae_monotonic_converges? const-decl "bool" measure_theory nil)
    (- const-decl "sequence[[T -> real]]" pointwise_convergence nil)
    (ae_decreasing? const-decl "bool" measure_theory nil)
    (ae_increasing? const-decl "bool" measure_theory nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (bounded? const-decl "bool" real_fun_preds "reals/")
    (O const-decl "T3" function_props nil)
    (integral const-decl "real" integral nil)
    (ae_eq? const-decl "bool" measure_theory nil)
    (increasing? const-decl "bool" real_fun_preds "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (decreasing? const-decl "bool" real_fun_preds "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (metric_convergence_def formula-decl nil metric_space
     "metric_space/")
    (metric_converges_to const-decl "bool" metric_space_def
     "metric_space/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil) (member const-decl "bool" sets nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_ge_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)
    (minus_real_is_real application-judgement "real" reals nil)
    (integral_opp formula-decl nil integral nil)
    (ball const-decl "set[T]" metric_space_def "metric_space/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (ae_convergence? const-decl "bool" measure_theory nil)
    (restrict const-decl "R" restrict nil)
    (pointwise_ae? const-decl "bool" measure_theory nil)
    (fullset const-decl "set" sets nil)
    (TRUE const-decl "bool" booleans nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (f!1 skolem-const-decl "integrable[T, S, mu]" complete_integral
     nil)
    (x!1 skolem-const-decl "({x | TRUE})" complete_integral nil)
    (h!1 skolem-const-decl "[T -> real]" complete_integral nil)
    (abs_nat formula-decl nil abs_lems "reals/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (union const-decl "set" sets nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (set type-eq-decl nil sets nil)
    (negligible_union application-judgement "negligible"
     complete_integral nil)
    (ae_in? const-decl "bool" measure_theory nil)
    (ae? const-decl "bool" measure_theory nil)
    (subset_algebra_fullset name-judgement "(S)" complete_integral nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     complete_integral nil)
    (ae_convergence_in? const-decl "bool" measure_theory nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (integrable_opp application-judgement "integrable"
     complete_integral nil)
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (mu formal-const-decl "complete_measure" complete_integral nil)
    (complete_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (complete_measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (S formal-const-decl "sigma_algebra" complete_integral nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil complete_integral nil)
    (sequence type-eq-decl nil sequences nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (monotone_convergence formula-decl nil integral_convergence nil)
    (converges_upto? const-decl "bool" convergence_aux "metric_space/")
    (complete_integral_ae_eq formula-decl nil complete_integral nil)
    (ae_convergence_eq formula-decl nil measure_theory nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (monotonic_converges? const-decl "bool" convergence_aux
     "metric_space/"))
   shostak))
(dominated_convergence_complete 0
  (dominated_convergence_complete-1 nil 3410772397
   ("" (skosimp)
    (("" (lemma "dominated_convergence" ("F" "F!1" "f" "f!1"))
      (("" (replace -2)
        (("" (split -1)
          (("1" (skosimp)
            (("1"
              (lemma "ae_convergence_eq"
               ("F" "F!1" "g" "h!1" "f" "g!1"))
              (("1" (assert)
                (("1"
                  (lemma "complete_integral_ae_eq"
                   ("f" "g!1" "h" "h!1"))
                  (("1" (assert)
                    (("1" (flatten) (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (expand "ae_convergent?")
              (("2" (inst + "h!1") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((mu formal-const-decl "complete_measure" complete_integral nil)
    (complete_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (complete_measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (S formal-const-decl "sigma_algebra" complete_integral nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil complete_integral nil)
    (sequence type-eq-decl nil sequences nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (dominated_convergence formula-decl nil integral_convergence nil)
    (ae_convergence_eq formula-decl nil measure_theory nil)
    (complete_integral_ae_eq formula-decl nil complete_integral nil)
    (ae_convergent? const-decl "bool" measure_theory nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.112 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.