Quelle fubini.prf Sprache: Lisp

(fubini
(integrable_is_integrable1 0
  (integrable_is_integrable1-1 nil 3453179746
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (lemma "integrable_pm_def" ("f0" "f!1"))
        (("" (flatten)
          (("" (hide -2)
            (("" (split)
              (("1" (flatten)
                (("1" (lemma "fubini_tonelli_1" ("h" "minus(f!1)"))
                  (("1" (lemma "fubini_tonelli_1" ("h" "plus(f!1)"))
                    (("1" (assert)
                      (("1"
                        (lemma "integrable1_diff"
                         ("g1" "plus(f!1)" "h1" "minus(f!1)"))
                        (("1"
                          (case-replace
                           "(-[[T1, T2]])(plus(f!1), minus(f!1))=f!1")
                          (("1" (hide-all-but 1)
                            (("1" (apply-extensionality :hide? t)
                              (("1" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "nn_measurable?")
                      (("2"
                        (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]")
                        (("2" (assert)
                          (("2" (skosimp) (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "nn_measurable?")
                    (("2"
                      (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]")
                      (("2" (assert)
                        (("2" (skosimp) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" 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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini nil)
    (T1 formal-type-decl nil fubini nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (fubini_tonelli_1 formula-decl nil fubini_tonelli nil)
    (integrable_minus application-judgement "integrable" fubini nil)
    (minus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (integrable_is_measurable judgement-tcc nil integral nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (integrable_diff application-judgement "integrable" fubini nil)
    (diff_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (integrable1 nonempty-type-eq-decl nil product_integral_def nil)
    (integrable1? const-decl "bool" product_integral_def nil)
    (integrable1_diff judgement-tcc nil product_integral_def nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (integrable_plus application-judgement "integrable" fubini nil)
    (plus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_pm_def formula-decl nil integral nil))
   shostak))
(integrable_is_integrable2 0
  (integrable_is_integrable2-1 nil 3453180306
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (lemma "integrable_pm_def" ("f0" "f!1"))
        (("" (flatten)
          (("" (hide -2)
            (("" (split)
              (("1" (flatten)
                (("1" (lemma "fubini_tonelli_2" ("h" "minus(f!1)"))
                  (("1" (lemma "fubini_tonelli_2" ("h" "plus(f!1)"))
                    (("1" (assert)
                      (("1"
                        (lemma "integrable2_diff"
                         ("g2" "plus(f!1)" "h2" "minus(f!1)"))
                        (("1"
                          (case-replace
                           "(-[[T1, T2]])(plus(f!1), minus(f!1))=f!1")
                          (("1" (apply-extensionality :hide? t)
                            (("1" (hide-all-but 1)
                              (("1" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "nn_measurable?")
                      (("2"
                        (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]")
                        (("2" (assert)
                          (("2" (hide-all-but 1)
                            (("2" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "nn_measurable?")
                    (("2"
                      (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]")
                      (("2" (assert)
                        (("2" (hide-all-but 1) (("2" (grind) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" 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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini nil)
    (T1 formal-type-decl nil fubini nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (fubini_tonelli_2 formula-decl nil fubini_tonelli nil)
    (integrable_minus application-judgement "integrable" fubini nil)
    (minus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_is_measurable judgement-tcc nil integral nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (integrable_diff application-judgement "integrable" fubini nil)
    (diff_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (integrable2 nonempty-type-eq-decl nil product_integral_def nil)
    (integrable2? const-decl "bool" product_integral_def nil)
    (integrable2_diff judgement-tcc nil product_integral_def nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (integrable_plus application-judgement "integrable" fubini nil)
    (plus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_pm_def formula-decl nil integral nil))
   shostak))
(fubini1_TCC1 0
  (fubini1_TCC1-1 nil 3459090851
   ("" (skosimp)
    (("" (lemma "integrable_is_integrable1" ("f" "f!1"))
      (("" (propax) nil nil)) nil))
    nil)
   ((integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" 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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini nil)
    (T1 formal-type-decl nil fubini nil)
    (integrable_is_integrable1 formula-decl nil fubini nil))
   nil))
(fubini1 0
  (fubini1-1 nil 3431174025
   ("" (skosimp)
    (("" (rewrite "integral_pm")
      (("" (lemma "integral_pm" ("f" "integral1(f!1)"))
        (("" (replace -1)
          (("" (hide -1)
            (("" (lemma "fubini_tonelli_3" ("g" "plus(f!1)"))
              (("1" (lemma "fubini_tonelli_3" ("g" "minus(f!1)"))
                (("1" (replace -1)
                  (("1" (replace -2)
                    (("1" (hide -1 -2)
                      (("1" (rewrite "integral_diff" 1 :dir rl)
                        (("1" (rewrite "integral_diff" 1 :dir rl)
                          (("1"
                            (case-replace
                             "plus(integral1(f!1)) - minus(integral1(f!1))=integral1(f!1)")
                            (("1" (hide -1)
                              (("1"
                                (lemma
                                 "integral1_diff"
                                 ("g1" "plus(f!1)" "h1" "minus(f!1)"))
                                (("1"
                                  (case-replace
                                   "plus(f!1) - minus(f!1)=f!1")
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (lemma
                                       "integral_ae_eq"
                                       ("f"
                                        "product_integral_def[T1, T2, S1, S2, mu, nu].integral1(f!1)"
                                        "h"
                                        "product_integral_def[T1, T2, S1, S2, mu, nu].integral1(plus(f!1)) - product_integral_def[T1, T2, S1, S2, mu, nu].integral1(minus(f!1))"))
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide-all-but 1)
                                    (("2"
                                      (apply-extensionality :hide? t)
                                      (("2" (grind) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (name-replace "DRL" "integral1(f!1)")
                              (("2"
                                (hide 2)
                                (("2"
                                  (apply-extensionality :hide? t)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2"
                  (lemma "nn_integrable_is_nn_integrable"
                   ("f" "minus[[T1, T2]](f!1)"))
                  (("2" (assert)
                    (("2" (hide-all-but 1) (("2" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2"
                (lemma "nn_integrable_is_nn_integrable"
                 ("f" "plus[[T1, T2]](f!1)"))
                (("2" (assert)
                  (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((integral_pm formula-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (T1 formal-type-decl nil fubini nil)
    (T2 formal-type-decl nil fubini nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini nil)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini 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/")
    (sigma_finite_measure? const-decl "bool" measure_def nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini nil)
    (integrable_minus application-judgement "integrable" fubini nil)
    (minus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_plus application-judgement "integrable" fubini nil)
    (plus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (fubini_tonelli_3 formula-decl nil fubini_tonelli nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (nn_integrable_is_nn_integrable formula-decl nil integral nil)
    (integrable_minus application-judgement "integrable" fubini nil)
    (minus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_plus application-judgement "integrable" fubini nil)
    (plus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_diff application-judgement "integrable" fubini nil)
    (diff_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integral_ae_eq formula-decl nil integral nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (integral1_diff formula-decl nil product_integral_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (diff_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_diff application-judgement "integrable" fubini nil)
    (integral_diff formula-decl nil integral nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (integral1 const-decl "integrable[T1, S1, mu]" product_integral_def
     nil)
    (integrable1 nonempty-type-eq-decl nil product_integral_def nil)
    (integrable1? const-decl "bool" product_integral_def nil))
   shostak))
(fubini2_TCC1 0
  (fubini2_TCC1-1 nil 3459090851
   ("" (skosimp)
    (("" (lemma "integrable_is_integrable2" ("f" "f!1"))
      (("" (propax) nil nil)) nil))
    nil)
   ((integrable nonempty-type-eq-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (sigma_finite_measure? const-decl "bool" 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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     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)
    (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)
    (T2 formal-type-decl nil fubini nil)
    (T1 formal-type-decl nil fubini nil)
    (integrable_is_integrable2 formula-decl nil fubini nil))
   nil))
(fubini2 0
  (fubini2-1 nil 3431180694
   ("" (skosimp)
    (("" (rewrite "integral_pm")
      (("" (lemma "integral_pm" ("f" "integral2(f!1)"))
        (("" (replace -1)
          (("" (hide -1)
            (("" (lemma "fubini_tonelli_4" ("g" "plus(f!1)"))
              (("1" (lemma "fubini_tonelli_4" ("g" "minus(f!1)"))
                (("1" (replace -1)
                  (("1" (replace -2)
                    (("1" (hide -1 -2)
                      (("1" (rewrite "integral_diff" 1 :dir rl)
                        (("1" (rewrite "integral_diff" 1 :dir rl)
                          (("1"
                            (case-replace
                             "plus(integral2(f!1)) - minus(integral2(f!1))=integral2(f!1)")
                            (("1" (hide -1)
                              (("1"
                                (lemma
                                 "integral2_diff"
                                 ("g2" "plus(f!1)" "h2" "minus(f!1)"))
                                (("1"
                                  (case-replace
                                   "plus(f!1) - minus(f!1)=f!1")
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (lemma
                                       "integral_ae_eq"
                                       ("f"
                                        "product_integral_def[T1, T2, S1, S2, mu, nu].integral2(f!1)"
                                        "h"
                                        "product_integral_def[T1, T2, S1, S2, mu, nu].integral2(plus(f!1)) - product_integral_def[T1, T2, S1, S2, mu, nu].integral2(minus(f!1))"))
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide-all-but 1)
                                    (("2"
                                      (apply-extensionality :hide? t)
                                      (("2" (grind) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (name-replace "DRL" "integral2(f!1)")
                              (("2"
                                (hide 2)
                                (("2"
                                  (apply-extensionality :hide? t)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2"
                  (lemma "nn_integrable_is_nn_integrable"
                   ("f" "minus[[T1, T2]](f!1)"))
                  (("2" (assert)
                    (("2" (hide-all-but 1) (("2" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2"
                (lemma "nn_integrable_is_nn_integrable"
                 ("f" "plus[[T1, T2]](f!1)"))
                (("2" (assert)
                  (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((integral_pm formula-decl nil integral nil)
    (integrable? const-decl "bool" integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (T1 formal-type-decl nil fubini nil)
    (T2 formal-type-decl nil fubini nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini nil)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini 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/")
    (sigma_finite_measure? const-decl "bool" measure_def nil)
    (sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
    (m_times const-decl
     "sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]"
     product_measure nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini nil)
    (integrable_minus application-judgement "integrable" fubini nil)
    (minus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_plus application-judgement "integrable" fubini nil)
    (plus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (fubini_tonelli_4 formula-decl nil fubini_tonelli nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (nn_integrable_is_nn_integrable formula-decl nil integral nil)
    (integrable_minus application-judgement "integrable" fubini nil)
    (minus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_plus application-judgement "integrable" fubini nil)
    (plus_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_diff application-judgement "integrable" fubini nil)
    (diff_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integral_ae_eq formula-decl nil integral nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (integral2_diff formula-decl nil product_integral_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (diff_measurable application-judgement "measurable_function[T, S]"
     fubini nil)
    (integrable_diff application-judgement "integrable" fubini nil)
    (integral_diff formula-decl nil integral nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
    (integral2 const-decl "integrable[T2, S2, nu]" product_integral_def
     nil)
    (integrable2 nonempty-type-eq-decl nil product_integral_def nil)
    (integrable2? const-decl "bool" product_integral_def nil))
   shostak)))

quality94%

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.