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: Sprache: Isabelle

Original von: PVS^©

("product_measure" product_measure m_times1_def 0 (m_times1_def-1 nil 3460264845 3474962740 ("" (skosimp) (("" (lemma "m_times_alt" ("mu" "mu!1" "nu" "nu!1" "M" "intersection(cross_product(A_of(mu!1)(i!1),fullset[T2]),M!1)")) (("1" (lemma "x_sum_eq" ("S" "(LAMBDA j:
                   x_sum(LAMBDA i:
                           to_measure(product_measure_approx
                                      (mu!1, nu!1)(i, j))
                                     (intersection
                                      (cross_product
                                       (A_of(mu!1)(i!1), fullset[T2]),
                                       M!1))))" "T" "(LAMBDA j:
                   to_measure(product_measure_approx(mu!1, nu!1)(i!1, j))
                             (M!1))")) (("1" (case "forall (i,j:nat): product_measure_approx
                                    (mu!1, nu!1)(i, j)
                                   (intersection
                                    (cross_product
                                     (A_of(mu!1)(i!1), fullset[T2]),
                                     M!1)) = if i = i!1 then product_measure_approx(mu!1,nu!1)(i!1,j)(M!1) else 0 endif") (("1" (split -2) (("1" (name-replace "DRL1" "x_sum((LAMBDA j:
                    x_sum(LAMBDA i:
                            to_measure(product_measure_approx
                                       (mu!1, nu!1)(i, j))
                                      (intersection
                                       (cross_product
                                        (A_of(mu!1)(i!1), fullset[T2]),
                                        M!1)))))") (("1" (name-replace "RHS" "x_sum(LAMBDA j:
                   to_measure(product_measure_approx(mu!1, nu!1)(i!1, j))
                             (M!1))") (("1" (case "x_eq(m_times(mu!1, nu!1)
                  (intersection(cross_product(A_of(mu!1)(i!1),
                                              fullset[T2]),
                                M!1)),m_times1(mu!1, nu!1, i!1)(M!1))") (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 2) (("2" (name-replace "MI" "intersection(cross_product
                                            (A_of(mu!1)(i!1), fullset[T2]),
                                            M!1)") (("2" (expand "m_times1") (("2" (expand "m_times") (("2" (lemma "x_sum_eq" ("S" "LAMBDA i:
                   x_sum(LAMBDA j:
                           to_measure(product_measure_approx
                                      (mu!1, nu!1)(i, j))
                                     (MI))" "T" "LAMBDA i:
                   x_sum(LAMBDA j:
                           to_measure(product_measure_approx
                                      (contraction[T1, S1]
                                       (mu!1, A_of(mu!1)(i!1)),
                                       nu!1)
                                      (i, j))
                                     (M!1))")) (("1" (postpone) nil nil) ("2" (hide 2 -1) (("2" (expand "sigma_finite_measure?") (("2" (expand "measure_sigma_finite?") (("2" (inst + "A_of(mu!1)") (("2" (rewrite "A_of_def1") (("2" (skosimp) (("2" (expand "contraction") (("2" (lemma "A_of_def2" ("mu" "mu!1" "n" "i!1")) (("2" (lemma "m_monotone[T1,S1,mu!1]" ("a" "intersection(A_of(mu!1)(i!1), A_of(mu!1)(i!2))" "b" "A_of(mu!1)(i!1)")) (("1" (expand "x_le") (("1" (assert) (("1" (expand "intersection") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil) ("4" (expand "MI") (("4" (hide-all-but 1) (("4" (lemma "cross_product_is_sigma_times" ("X" "A_of(mu!1)(i!1)" "Y" "fullset[T2]")) (("4" (typepred "M!1") (("4" (lemma "measurable_intersection" ("a" "cross_product(A_of(mu!1)(i!1), fullset[T2])" "b" "M!1")) (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (assert) (("2" (skolem + "j!1") (("2" (inst - "_" "j!1") (("2" (expand "to_measure") (("2" (name-replace "PIJ" "product_measure_approx(mu!1, nu!1)(i!1, j!1)(M!1)") (("2" (case-replace "(LAMBDA (i:nat):
                   (TRUE,
                    product_measure_approx(mu!1, nu!1)
                                          (i, j!1)
                                          (intersection
                                           (cross_product
                                            (A_of(mu!1)(i!1), fullset[T2]),
                                            M!1))))=(LAMBDA (i: nat): (TRUE,IF i = i!1 THEN PIJ ELSE 0 ENDIF))") (("1" (hide-all-but 1) (("1" (expand "x_eq") (("1" (expand "x_sum") (("1" (lemma "single_nz_series_conv" ("a" "(LAMBDA (i_1: nat):
                             IF i_1 = i!1 THEN PIJ ELSE 0 ENDIF)" "n" "i!1")) (("1" (lemma "single_nz_series_limit" ("a" "(LAMBDA (i_1: nat):
                             IF i_1 = i!1 THEN PIJ ELSE 0 ENDIF)" "n" "i!1")) (("1" (case-replace "FORALL (m:nat):
         i!1 /= m =>
          (LAMBDA (i_1: nat): IF i_1 = i!1 THEN PIJ ELSE 0 ENDIF)(m) = 0") (("1" (replace -3) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (inst - "x!1") nil nil) ("2" (hide-all-but 1) (("2" (lemma "cross_product_is_sigma_times" ("X" "A_of(mu!1)(i!1)" "Y" "fullset[T2]")) (("2" (lemma "measurable_intersection" ("a" "cross_product(A_of(mu!1)(i!1), fullset[T2])" "b" "M!1")) (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skolem + ("i!2" "j!2")) (("2" (expand "product_measure_approx") (("2" (name-replace "NUJ" "fm_contraction[T2, S2](nu!1, A_of(nu!1)(j!2))") (("2" (typepred "A_of(mu!1)") (("2" (expand "disjoint_indexed_measurable?") (("2" (expand "disjoint?") (("2" (inst - "i!2" "i!1") (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (expand "intersection" -1) (("2" (expand "member") (("2" (expand "fm_times") (("2" (lemma "x_section_integrable[T1,T2,S1,S2]" ("mu" "fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!2))" "nu" "NUJ" "M" "intersection(cross_product(A_of(mu!1)(i!1),
                                                 fullset[T2]),
                                   M!1)")) (("1" (lemma "measure_eq_integrable?[T1,S1]" ("mu" "to_measure(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!2)))" "nu" "contraction[T1, S1](mu!1, A_of(mu!1)(i!2))" "f" "NUJ o
            x_section(intersection(cross_product(A_of(mu!1)(i!1),
                                                 fullset[T2]),
                                   M!1))")) (("1" (lemma "measure_eq_integral[T1,S1]" ("mu" "to_measure(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!2)))" "nu" "contraction[T1, S1](mu!1, A_of(mu!1)(i!2))" "f" "NUJ o
            x_section(intersection(cross_product(A_of(mu!1)(i!1),
                                                 fullset[T2]),
                                   M!1))")) (("1" (replace -3) (("1" (case-replace "FORALL (E: (S1)):
         x_eq(to_measure(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!2)))(E),
              contraction[T1, S1](mu!1, A_of(mu!1)(i!2))(E))") (("1" (flatten) (("1" (replace -2) (("1" (rewrite "contraction_integral[T1,S1]" 1) (("1" (hide-all-but (-5 1)) (("1" (case-replace "i!2 = i!1") (("1" (hide -2) (("1" (lemma "x_section_integrable" ("nu" "NUJ" "mu" "fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1))" "M" "M!1")) (("1" (lemma "measure_eq_integrable?[T1,S1]" ("mu" "to_measure(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1)))" "nu" "contraction[T1, S1](mu!1, A_of(mu!1)(i!1))" "f" "NUJ o x_section(M!1)")) (("1" (lemma "measure_eq_integral[T1,S1]" ("mu" "to_measure(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1)))" "nu" "contraction[T1, S1](mu!1, A_of(mu!1)(i!1))" "f" "NUJ o x_section(M!1)")) (("1" (case-replace "FORALL (E: (S1)):
         x_eq(to_measure(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1)))(E),
              contraction[T1, S1](mu!1, A_of(mu!1)(i!1))(E))") (("1" (replace -4) (("1" (replace -2) (("1" (rewrite "contraction_integral[T1, S1]" 1) (("1" (case-replace "*[T1](phi[T1, S1](A_of(mu!1)(i!1)),
                 NUJ o
                  x_section(intersection(cross_product
                                         (A_of(mu!1)(i!1), fullset[T2]),
                                         M!1)))=*[T1](phi[T1, S1](A_of(mu!1)(i!1)), NUJ o x_section(M!1))") (("1" (apply-extensionality :hide? t) (("1" (hide-all-but 1) (("1" (expand "*") (("1" (expand "phi") (("1" (expand "fullset") (("1" (expand "cross_product") (("1" (expand "o") (("1" (expand "intersection") (("1" (expand "member") (("1" (lift-if 1) (("1" (assert) (("1" (expand "x_section") (("1" (expand "x_section") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "contraction") (("2" (expand "fm_contraction") (("2" (expand "to_measure") (("2" (expand "x_eq") (("2" (lemma "A_of_def2" ("mu" "mu!1" "n" "i!1")) (("2" (lemma "m_monotone[T1,S1,mu!1]" ("a" "intersection(A_of(mu!1)(i!1), E!1)" "b" "A_of(mu!1)(i!1)")) (("1" (expand "x_le") (("1" (assert) (("1" (expand "intersection") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil) ("4" (expand "measurable_set?") (("4" (skosimp) (("4" (rewrite "A_of_def2") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (rewrite "A_of_def2") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "(((reals@real_fun_ops[T1].*)
                (phi[T1, S1](A_of(mu!1)(i!2)),
                 NUJ o
                  x_section(intersection(cross_product
                                         (A_of(mu!1)(i!1), fullset[T2]),
                                         M!1)))))=lambda (x:T1): 0") (("1" (rewrite "integral_zero[T1, S1, mu!1]" 2) nil nil) ("2" (apply-extensionality :hide? t) (("2" (hide 2 3) (("2" (inst - "x!1") (("2" (expand "*") (("2" (expand "phi") (("2" (expand "member") (("2" (case-replace "A_of(mu!1)(i!2)(x!1)") (("1" (expand "o") (("1" (case-replace "(x_section(intersection(cross_product(A_of(mu!1)(i!1),
                                                fullset[T2]),
                                  M!1))
                    (x!1))=emptyset[T2]") (("1" (typepred "NUJ") (("1" (expand "finite_measure?") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (expand "fullset") (("2" (expand "cross_product") (("2" (expand "intersection") (("2" (expand "x_section") (("2" (expand "member") (("2" (expand "x_section") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "contraction") (("2" (expand "fm_contraction") (("2" (expand "to_measure") (("2" (expand "x_eq") (("2" (skosimp) (("2" (lemma "A_of_def2" ("mu" "mu!1" "n" "i!2")) (("2" (lemma "m_monotone[T1,S1,mu!1]" ("a" "intersection(A_of(mu!1)(i!2), E!1)" "b" "A_of(mu!1)(i!2)")) (("1" (expand "x_le") (("1" (assert) (("1" (expand "intersection") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil) ("4" (expand "measurable_set?") (("4" (skosimp) (("4" (rewrite "A_of_def2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (rewrite "A_of_def2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "cross_product_is_sigma_times" ("X" "A_of[T1, S1](mu!1)(i!1)" "Y" "fullset[T2]")) (("2" (lemma "measurable_intersection" ("a" "cross_product(A_of[T1, S1](mu!1)(i!1), fullset[T2])" "b" "M!1")) (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 568 390 t shostak))("product_measure" product_measure m_times2_TCC1 0 (m_times2_TCC1-1 nil 3460264247 3474962739 ("" (expand "measurable_set?") (("" (propax) nil nil)) nil) proved ((measurable_set? const-decl "bool" measure_space_def nil)) 186 100 t nil))("product_measure" product_measure m_times1_TCC1 0 (m_times1_TCC1-1 nil 3460264247 3474962739 ("" (expand "measurable_set?") (("" (propax) nil nil)) nil) proved ((measurable_set? const-decl "bool" measure_space_def nil)) 102 100 t nil))("fubini_tonelli_scaf" fubini_tonelli_scaf IMP_product_integral_def_TCC2 0 (IMP_product_integral_def_TCC2-1 nil 3476699996 3476701789 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 7808 60 t nil))("fubini_tonelli_scaf" fubini_tonelli_scaf IMP_product_integral_def_TCC1 0 (IMP_product_integral_def_TCC1-1 nil 3476699996 3476701776 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 11687 60 t nil))("fubini_tonelli_scaf" fubini_tonelli_scaf IMP_integral_TCC1 0 (IMP_integral_TCC1-1 nil 3476699996 3476701843 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 8493 90 t nil))("fubini_tonelli" fubini_tonelli fubini_tonelli_3_TCC2 0 (fubini_tonelli_3_TCC2-1 nil 3476707031 nil ("" (subtype-tcc) nil nil) nil nil nil nil nil nil))("fubini_tonelli" fubini_tonelli IMP_product_integral_def_TCC2 0 (IMP_product_integral_def_TCC2-1 nil 3476707031 3476707896 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 7366 30 t nil))("fubini_tonelli" fubini_tonelli IMP_product_integral_def_TCC1 0 (IMP_product_integral_def_TCC1-1 nil 3476707031 3476707873 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 8647 30 t nil))("fubini_tonelli" fubini_tonelli IMP_integral_TCC1 0 (IMP_integral_TCC1-1 nil 3476707031 3476707882 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 3489 50 t nil))("fubini" fubini integrable_is_integrable1_TCC2 0 (integrable_is_integrable1_TCC2-1 nil 3476707033 3476708493 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 5485 150 t nil))("fubini" fubini integrable_is_integrable1_TCC1 0 (integrable_is_integrable1_TCC1-1 nil 3476707033 3476708484 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 7602 150 t nil))("fubini" fubini f_TCC1 0 (f_TCC1-1 nil 3476707033 3476708472 ("" (assert) (("" (postpone) nil nil)) nil) unfinished nil 9593 150 t nil))

¤ Dauer der Verarbeitung: 0.36 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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