Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/measure_integration/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: fubini_tonelli.prf Sprache: Lisp

Original von: PVS^©

(fubini_tonelli
(fubini_tonelli_1 0
  (fubini_tonelli_1-1 nil 3453187626
   ("" (skosimp)
    (("" (lemma "fubini_tonelli_scaf1" ("h" "h!1"))
      (("" (replace 1 -1) (("" (propax) nil nil)) nil)) nil))
    nil)
   ((nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     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)
    (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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (fubini_tonelli_scaf1 formula-decl nil fubini_tonelli_scaf nil))
   shostak))
(fubini_tonelli_2 0
  (fubini_tonelli_2-1 nil 3459562328
   ("" (skosimp)
    (("" (lemma "fubini_tonelli_scaf2" ("h" "h!1"))
      (("" (replace 1 -1) (("" (propax) nil nil)) nil)) nil))
    nil)
   ((nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     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)
    (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)
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (fubini_tonelli_scaf2 formula-decl nil fubini_tonelli_scaf nil))
   shostak))
(fubini_tonelli_3_TCC1 0
  (fubini_tonelli_3_TCC1-1 nil 3431151472
   ("" (skosimp)
    (("" (typepred "g!1")
      (("" (lemma "fubini_tonelli_1" ("h" "g!1"))
        (("1" (assert)
          (("1"
            (lemma
             "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
            (("1" (inst - "g!1") nil nil)) nil))
          nil)
         ("2" (expand "nn_measurable?")
          (("2" (split)
            (("1"
              (use "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
              nil nil)
             ("2" (skosimp) (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     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/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_1 formula-decl nil fubini_tonelli nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil))
   nil))
(fubini_tonelli_3 0
  (fubini_tonelli_3-1 nil 3459216640
   ("" (skosimp)
    (("" (typepred "g!1")
      ((""
        (lemma
         "nn_integrable_is_measurable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]")
        (("" (inst - "g!1")
          (("" (lemma "fubini_tonelli_scaf1" ("h" "g!1"))
            (("1" (flatten)
              (("1" (split -3)
                (("1" (propax) nil nil)
                 ("2"
                  (lemma
                   "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
                  (("2" (inst - "g!1") nil nil)) nil))
                nil))
              nil)
             ("2" (expand "nn_measurable?")
              (("2" (assert)
                (("2" (skosimp)
                  (("2" (typepred "g!1(x!1)") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     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/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_scaf1 formula-decl nil fubini_tonelli_scaf nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil))
   shostak))
(fubini_tonelli_4_TCC1 0
  (fubini_tonelli_4_TCC1-1 nil 3431151472
   ("" (skosimp)
    (("" (typepred "g!1")
      (("" (lemma "fubini_tonelli_2" ("h" "g!1"))
        (("1" (assert)
          (("1"
            (lemma
             "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
            (("1" (inst - "g!1") nil nil)) nil))
          nil)
         ("2" (expand "nn_measurable?")
          (("2"
            (use "nn_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))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     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/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_2 formula-decl nil fubini_tonelli nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil))
   nil))
(fubini_tonelli_4 0
  (fubini_tonelli_4-1 nil 3459746299
   ("" (skosimp)
    (("" (typepred "g!1")
      ((""
        (lemma
         "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
        (("" (inst - "g!1")
          (("" (lemma "fubini_tonelli_scaf2" ("h" "g!1"))
            (("1" (flatten)
              (("1" (split -3)
                (("1" (propax) nil nil)
                 ("2"
                  (lemma
                   "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]")
                  (("2" (inst - "g!1") nil nil)) nil))
                nil))
              nil)
             ("2" (expand "nn_measurable?")
              (("2" (assert)
                (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
    (nn_integrable? const-decl "bool" nn_integral nil)
    (nu formal-const-decl "sigma_finite_measure[T2, S2]" fubini_tonelli
     nil)
    (mu formal-const-decl "sigma_finite_measure[T1, S1]" fubini_tonelli
     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/")
    (S2 formal-const-decl "sigma_algebra[T2]" fubini_tonelli nil)
    (S1 formal-const-decl "sigma_algebra[T1]" fubini_tonelli 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)
    (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)
    (T2 formal-type-decl nil fubini_tonelli nil)
    (T1 formal-type-decl nil fubini_tonelli nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nn_integrable_is_integrable judgement-tcc nil integral nil)
    (fubini_tonelli_scaf2 formula-decl nil fubini_tonelli_scaf nil)
    (nn_measurable? const-decl "bool" measure_space nil)
    (nn_measurable nonempty-type-eq-decl nil measure_space nil)
    (nn_integrable_is_measurable judgement-tcc nil nn_integral nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.