|
(finite_fubini_scaf
(mu_TCC1 0
(mu_TCC1-1 nil 3458551591
("" (typepred "S1")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (flatten)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T1 formal-type-decl nil finite_fubini_scaf 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)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil))
nil))
(nu_TCC1 0
(nu_TCC1-1 nil 3458551591
("" (typepred "S2")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (flatten)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T2 formal-type-decl nil finite_fubini_scaf 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)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil))
nil))
(measurable_x_section 0
(measurable_x_section-1 nil 3458807198
("" (skosimp)
(("" (typepred "m!1")
(("" (rewrite "measurable_gt")
(("" (rewrite "measurable_gt")
(("" (skosimp)
(("" (inst - "c!1")
((""
(lemma "x_section_measurable"
("S1" "S1" "S2" "S2" "Z"
"{z: [T1, T2] | m!1(z) > c!1}" "x" "x!1"))
(("" (expand "member")
(("" (assert)
(("" (expand "x_section") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(x_section const-decl "set[T2]" cross_product "topology/")
(x_section_measurable formula-decl nil product_sigma_def nil)
(set type-eq-decl nil sets nil) (> const-decl "bool" reals nil)
(measurable_gt formula-decl nil measure_space_def nil))
shostak))
(measurable_y_section 0
(measurable_y_section-1 nil 3458807343
("" (skosimp)
(("" (typepred "m!1")
(("" (rewrite "measurable_gt")
(("" (rewrite "measurable_gt")
(("" (skosimp)
(("" (inst - "c!1")
((""
(lemma "y_section_measurable"
("S1" "S1" "S2" "S2" "Z"
"{z: [T1, T2] | m!1(z) > c!1}" "y" "y!1"))
(("" (expand "member")
(("" (assert)
(("" (expand "y_section") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(y_section const-decl "set[T1]" cross_product "topology/")
(y_section_measurable formula-decl nil product_sigma_def nil)
(set type-eq-decl nil sets nil) (> const-decl "bool" reals nil)
(measurable_gt formula-decl nil measure_space_def nil))
shostak))
(isf_x_section 0
(isf_x_section-1 nil 3458807584
("" (skosimp)
(("" (typepred "i!1")
(("" (expand "isf?")
(("" (flatten)
(("" (expand "simple?")
(("" (flatten)
(("" (expand "mu_fin?")
(("" (expand "to_measure")
(("" (hide -3)
((""
(lemma "finite_subset[real]"
("A" "image(i!1, fullset[[T1, T2]])" "s"
"image(LAMBDA y: i!1(x!1, y), fullset[T2])"))
(("1" (assert)
(("1" (split)
(("1" (assert)
(("1" (hide -1 -3)
(("1"
(lemma
"measurable_x_section"
("m" "i!1" "x" "x!1"))
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "fullset")
(("2"
(expand "image")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(skosimp*)
(("2"
(inst + "(x!1,x!3)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
finite_fubini_scaf nil)
(subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
finite_fubini_scaf nil)
(subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
nil)
(finite_subset formula-decl nil finite_sets nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(image const-decl "set[R]" function_image nil)
(fullset const-decl "set" sets nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_x_section formula-decl nil finite_fubini_scaf nil)
(subset? const-decl "bool" sets nil)
(TRUE const-decl "bool" booleans nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux nil)
(mu_fin? const-decl "bool" measure_props nil)
(simple? const-decl "bool" measure_space nil))
shostak))
(isf_y_section 0
(isf_y_section-1 nil 3458807902
("" (skosimp)
(("" (typepred "i!1")
(("" (expand "isf?")
(("" (expand "simple?")
(("" (flatten)
(("" (lemma "measurable_y_section" ("y" "y!1" "m" "i!1"))
(("" (assert)
(("" (expand "mu_fin?")
(("" (expand "to_measure")
(("" (hide-all-but (-3 1))
((""
(lemma "finite_subset[real]"
("A" "image(i!1, fullset[[T1, T2]])" "s"
"image(LAMBDA x: i!1(x, y!1), fullset[T1])"))
(("" (assert)
(("" (hide-all-but 1)
(("" (expand "fullset")
((""
(expand "image")
((""
(expand "subset?")
((""
(expand "member")
((""
(skosimp*)
((""
(inst + "(x!2, y!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(simple? const-decl "bool" measure_space nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_y_section formula-decl nil finite_fubini_scaf nil)
(mu_fin? const-decl "bool" measure_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(TRUE const-decl "bool" booleans nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(image const-decl "set[R]" function_image nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(finite_subset formula-decl nil finite_sets nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
finite_fubini_scaf nil)
(subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
finite_fubini_scaf nil)
(subset_algebra_fullset name-judgement "(S)" finite_fubini_scaf
nil))
shostak))
(integral_phi1_TCC1 0
(integral_phi1_TCC1-1 nil 3458818643
("" (skosimp)
((""
(lemma "isf_x_section"
("i" "phi[[T1, T2], sigma_times(S1, S2)](E!1)" "x" "x!1"))
(("1" (propax) nil nil)
("2" (rewrite "isf_phi")
(("2" (expand "mu_fin?")
(("2" (expand "product_measure")
(("2" (expand "to_measure")
(("2" (expand "measurable_set?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((phi const-decl "nat" measure_space 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)
(set type-eq-decl nil sets nil)
(isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(isf_x_section formula-decl nil finite_fubini_scaf nil)
(phi_is_simple application-judgement "simple" finite_fubini_scaf
nil)
(isf_phi judgement-tcc nil isf nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(integral_phi1_TCC2 0
(integral_phi1_TCC2-1 nil 3458818643
("" (skosimp)
(("" (expand "x_section")
((""
(lemma "x_section_measurable"
("Z" "E!1" "x" "x1!1" "S1" "S1" "S2" "S2"))
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((x_section const-decl "[T1 -> set[T2]]" cross_product "topology/")
(member const-decl "bool" sets nil)
(x_section_measurable formula-decl nil product_sigma_def 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)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(set type-eq-decl nil sets nil)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(T2 formal-type-decl nil finite_fubini_scaf nil))
nil))
(integral_phi1 0
(integral_phi1-1 nil 3458818650
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("1" (expand "x_section")
(("1" (expand "o ")
(("1"
(lemma "isf_integral_phi[T2, S2, to_measure(nu)]"
("E" "x_section(E!1, x!1)"))
(("1" (expand "mu")
(("1" (expand "to_measure")
(("1" (expand "x_section" -1 1)
(("1" (expand "phi")
(("1" (expand "member") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "mu_fin?")
(("2" (expand "to_measure")
(("2" (expand "measurable_set?")
(("2"
(lemma "x_section_measurable"
("Z" "E!1" "x" "x!1" "S1" "S1" "S2" "S2"))
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2"
(lemma "isf_phi[T2, S2, to_measure(nu)]"
("E" "x_section(E!1)(x!1)"))
(("1" (expand "x_section")
(("1" (expand "x_section")
(("1" (expand "phi")
(("1" (expand "member") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "mu_fin?")
(("2" (expand "to_measure")
(("2" (hide 2)
(("2"
(lemma "x_section_measurable"
("Z" "E!1" "x" "x!1" "S1" "S1" "S2" "S2"))
(("2" (expand "member")
(("2" (expand "measurable_set?")
(("2" (expand "x_section" 1)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T1 formal-type-decl nil finite_fubini_scaf nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(x_section const-decl "[T1 -> set[T2]]" cross_product "topology/")
(O const-decl "T3" function_props nil)
(isf_integral const-decl "real" isf nil)
(isf nonempty-type-eq-decl nil isf nil)
(T2 formal-type-decl nil finite_fubini_scaf 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)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(isf? const-decl "bool" isf nil) (set type-eq-decl nil sets nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
(phi const-decl "nat" measure_space nil)
(E!1 skolem-const-decl "(sigma_times(S1, S2))" finite_fubini_scaf
nil)
(x_section_measurable formula-decl nil product_sigma_def nil)
(mu const-decl "nnreal" measure_props nil)
(member const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(x_section const-decl "set[T2]" cross_product "topology/")
(mu_fin? const-decl "bool" measure_props nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(isf_integral_phi formula-decl nil isf nil)
(isf_phi judgement-tcc nil isf nil))
shostak))
(integral_phi2_TCC1 0
(integral_phi2_TCC1-1 nil 3458819223
("" (skosimp)
((""
(lemma "isf_y_section"
("i" "phi[[T1, T2], sigma_times(S1, S2)](E!1)" "y" "y!1"))
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (rewrite "isf_phi")
(("2" (expand "mu_fin?")
(("2" (expand "product_measure")
(("2" (expand "to_measure")
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((phi const-decl "nat" measure_space 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)
(set type-eq-decl nil sets nil)
(isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(isf_y_section formula-decl nil finite_fubini_scaf nil)
(phi_is_simple application-judgement "simple" finite_fubini_scaf
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(mu_fin? const-decl "bool" measure_props nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(isf_phi judgement-tcc nil isf nil))
nil))
(integral_phi2_TCC2 0
(integral_phi2_TCC2-1 nil 3458819223
("" (skosimp)
(("" (expand "y_section")
((""
(lemma "y_section_measurable"
("Z" "E!1" "y" "x1!1" "S1" "S1" "S2" "S2"))
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((y_section const-decl "[T2 -> set[T1]]" cross_product "topology/")
(member const-decl "bool" sets nil)
(y_section_measurable formula-decl nil product_sigma_def 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)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(set type-eq-decl nil sets nil)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(T2 formal-type-decl nil finite_fubini_scaf nil))
nil))
(integral_phi2 0
(integral_phi2-1 nil 3458819232
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("1" (expand "o")
(("1" (expand "y_section")
(("1"
(lemma "isf_integral_phi[T1, S1, to_measure(mu)]"
("E" "y_section(E!1, x!1)"))
(("1" (expand "y_section" -1 1)
(("1" (expand "phi")
(("1" (expand "member")
(("1" (assert)
(("1" (expand "mu" -1)
(("1" (expand "to_measure")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "mu_fin?")
(("2" (expand "to_measure")
(("2" (hide 2)
(("2"
(lemma "y_section_measurable"
("Z" "E!1" "y" "x!1" "S1" "S1" "S2" "S2"))
(("2" (expand "member")
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2"
(lemma "isf_y_section"
("y" "y!1" "i" "phi[[T1, T2], sigma_times(S1, S2)](E!1)"))
(("1" (propax) nil nil)
("2" (rewrite "isf_phi")
(("2" (expand "mu_fin?")
(("2" (expand "product_measure")
(("2" (expand "to_measure")
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T2 formal-type-decl nil finite_fubini_scaf nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(y_section const-decl "[T2 -> set[T1]]" cross_product "topology/")
(O const-decl "T3" function_props nil)
(isf_integral const-decl "real" isf nil)
(isf nonempty-type-eq-decl nil isf nil)
(T1 formal-type-decl nil finite_fubini_scaf 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)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(isf? const-decl "bool" isf nil) (set type-eq-decl nil sets nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(phi const-decl "nat" measure_space nil)
(E!1 skolem-const-decl "(sigma_times(S1, S2))" finite_fubini_scaf
nil)
(y_section_measurable formula-decl nil product_sigma_def nil)
(member const-decl "bool" sets nil)
(mu const-decl "nnreal" measure_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(y_section const-decl "set[T1]" cross_product "topology/")
(mu_fin? const-decl "bool" measure_props nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(isf_integral_phi formula-decl nil isf nil)
(phi_is_simple application-judgement "simple" finite_fubini_scaf
nil)
(isf_y_section formula-decl nil finite_fubini_scaf nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(isf_phi judgement-tcc nil isf nil))
shostak))
(integral_phi3_TCC1 0
(integral_phi3_TCC1-1 nil 3458889572 ("" (subtype-tcc) nil nil)
((integral const-decl "real" integral nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(isf? const-decl "bool" isf nil)
(phi_is_simple application-judgement "simple" finite_fubini_scaf
nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(integral_phi3_TCC2 0
(integral_phi3_TCC2-1 nil 3458889572
("" (skosimp)
(("" (lemma "integral_phi1" ("E" "E!1"))
(("" (replace -1) (("" (rewrite "x_section_integrable") nil nil))
nil))
nil))
nil)
((S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(integral_phi1 formula-decl nil finite_fubini_scaf nil)
(x_section_integrable formula-decl nil product_finite_measure 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)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil))
nil))
(integral_phi3 0
(integral_phi3-1 nil 3458889984
("" (skosimp)
(("" (rewrite "isf_integral_phi")
(("1" (expand "mu")
(("1" (expand "product_measure")
(("1" (expand "to_measure")
(("1" (expand "fm_times")
(("1" (rewrite "integral_phi1") nil nil)) nil))
nil))
nil))
nil)
("2" (expand "mu_fin?")
(("2" (expand "product_measure")
(("2" (expand "to_measure")
(("2" (typepred "E!1")
(("2" (expand "measurable_set?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((AND const-decl "[bool, bool -> bool]" booleans nil)
(isf_integral_phi formula-decl nil isf nil)
(set type-eq-decl nil sets nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(T2 formal-type-decl nil finite_fubini_scaf 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]" finite_fubini_scaf nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf 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)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(phi_is_simple application-judgement "simple" finite_fubini_scaf
nil)
(integral_phi1 formula-decl nil finite_fubini_scaf nil)
(mu const-decl "nnreal" measure_props nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(integral_phi4_TCC1 0
(integral_phi4_TCC1-1 nil 3458889572
("" (skosimp)
(("" (rewrite "integral_phi2")
(("" (rewrite "y_section_integrable") nil nil)) nil))
nil)
((integral_phi2 formula-decl nil finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(T2 formal-type-decl nil finite_fubini_scaf 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]" finite_fubini_scaf nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def 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)
(y_section_integrable formula-decl nil product_finite_measure nil))
nil))
(integral_phi4 0
(integral_phi4-1 nil 3458890113
("" (skosimp)
(("" (rewrite "isf_integral_phi")
(("1" (expand "mu")
(("1" (expand "product_measure")
(("1" (expand "to_measure")
(("1" (rewrite "finite_product_alt")
(("1" (rewrite "integral_phi2") nil nil)) nil))
nil))
nil))
nil)
("2" (expand "mu_fin?")
(("2" (expand "measurable_set?")
(("2" (expand "product_measure")
(("2" (expand "to_measure") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((AND const-decl "[bool, bool -> bool]" booleans nil)
(isf_integral_phi formula-decl nil isf nil)
(set type-eq-decl nil sets nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(T2 formal-type-decl nil finite_fubini_scaf 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]" finite_fubini_scaf nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf 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)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(phi_is_simple application-judgement "simple" finite_fubini_scaf
nil)
(integral_phi2 formula-decl nil finite_fubini_scaf nil)
(finite_product_alt formula-decl nil product_finite_measure nil)
(mu const-decl "nnreal" measure_props nil))
shostak))
(isf_integral_x_TCC1 0
(isf_integral_x_TCC1-1 nil 3458807583
("" (skosimp)
(("" (lemma "isf_x_section" ("x" "x!1" "i" "i!1"))
(("" (propax) nil nil)) nil))
nil)
((isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(isf_x_section formula-decl nil finite_fubini_scaf nil))
nil))
(isf_integral_x 0
(isf_integral_x-1 nil 3458808015
("" (skosimp)
((""
(lemma
"isf_induction[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu,nu))]"
("P"
"lambda i: integrable?(LAMBDA x: isf_integral(LAMBDA y: i(x, y)))"))
(("1" (inst - "i!1")
(("1" (assert)
(("1" (hide 2)
(("1" (split)
(("1" (rewrite "isf_integral_zero")
(("1" (rewrite "integrable_zero") nil nil)) nil)
("2" (skosimp)
(("2"
(case-replace "(LAMBDA x:
isf_integral(LAMBDA y: (c!1 * phi(E!1) + i!2)(x, y)))=+[T1](*[T1](c!1,LAMBDA x:
isf_integral(LAMBDA y: phi(E!1)(x, y))),LAMBDA x: isf_integral(LAMBDA y: i!2(x, y)))")
(("1" (hide -1)
(("1" (rewrite "integrable_add")
(("1" (skosimp)
(("1" (rewrite "isf_x_section") nil nil)) nil)
("2" (rewrite "integrable_scal")
(("1" (rewrite "integral_phi1")
(("1" (rewrite "x_section_integrable")
(("1" (typepred "E!1")
(("1"
(expand "measurable_set?")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (typepred "E!1")
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (skosimp)
(("2" (rewrite "isf_x_section") nil nil))
nil))
nil)
("3" (skosimp)
(("3" (rewrite "isf_x_section") nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality :hide? t)
(("1"
(lemma
"isf_phi[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]"
("E" "E!1"))
(("1"
(lemma
"isf_scal[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]"
("c" "c!1" "i"
"phi[[T1, T2], sigma_times(S1, S2)](E!1)"))
(("1" (typepred "i!2")
(("1" (expand "+" 1)
(("1"
(expand "*" 1)
(("1"
(assert)
(("1"
(lemma
"isf_integral_add[T2,S2,to_measure(nu)]"
("i1"
"LAMBDA y: i!2(x!1, y)"
"i2"
"LAMBDA y:c!1 * phi(E!1)(x!1, y)"))
(("1"
(expand "+" -1 1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(rewrite
"isf_integral_scal"
1
:dir
rl)
(("1"
(expand "*")
(("1"
(propax)
nil
nil))
nil)
("2"
(rewrite
"isf_x_section"
1)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"isf_x_section"
("i"
"(*[[T1, T2]](c!1, phi[[T1, T2], sigma_times(S1, S2)](E!1)))"
"x"
"x!1"))
(("2"
(expand "*")
(("2" (propax) nil nil))
nil))
nil)
("3"
(rewrite "isf_x_section" 1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (rewrite "isf_x_section") nil nil)) nil)
("3" (skosimp)
(("3" (rewrite "isf_x_section") nil nil)) nil)
("4" (skosimp)
(("4" (rewrite "isf_x_section") nil nil)) nil))
nil))
nil)
("3" (skosimp)
(("3" (rewrite "isf_x_section") nil nil)) nil)
("4" (skosimp)
(("4" (rewrite "isf_x_section") nil nil)) nil)
("5" (skosimp)
(("5" (rewrite "isf_x_section") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (rewrite "isf_x_section") nil nil)) nil))
nil))
nil)
((nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def 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)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(isf_integral const-decl "real" isf nil)
(integrable? const-decl "bool" integral nil)
(pred type-eq-decl nil defined_types nil)
(isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(isf_induction formula-decl nil isf nil)
(isf_add application-judgement "isf" finite_fubini_scaf nil)
(integrable_add application-judgement "integrable"
finite_fubini_scaf nil)
(simple_add application-judgement "simple" finite_fubini_scaf nil)
(integrable_zero formula-decl nil integral nil)
(isf_integral_zero formula-decl nil isf nil)
(isf_phi application-judgement "isf" finite_fubini_scaf nil)
(simple_scal application-judgement "simple" finite_fubini_scaf nil)
(integrable_scal application-judgement "integrable"
finite_fubini_scaf nil)
(isf_scal application-judgement "isf" finite_fubini_scaf nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(set type-eq-decl nil sets nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(phi const-decl "nat" measure_space nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable_add judgement-tcc nil integral nil)
(isf_x_section formula-decl nil finite_fubini_scaf nil)
(integral_phi1 formula-decl nil finite_fubini_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(x_section_integrable formula-decl nil product_finite_measure nil)
(integrable_scal judgement-tcc nil integral nil)
(i!2 skolem-const-decl
"isf[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu, nu))]"
finite_fubini_scaf nil)
(E!1 skolem-const-decl "(mu_fin?)" finite_fubini_scaf nil)
(c!1 skolem-const-decl "real" finite_fubini_scaf nil)
(isf_scal judgement-tcc nil isf nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(isf_integral_scal formula-decl nil isf nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(isf_integral_add formula-decl nil isf nil)
(isf_phi judgement-tcc nil isf nil))
shostak))
(isf_integral_y_TCC1 0
(isf_integral_y_TCC1-1 nil 3458807583
("" (skosimp)
(("" (lemma "isf_y_section" ("y" "y!1" "i" "i!1"))
(("" (propax) nil nil)) nil))
nil)
((isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(nu formal-const-decl "finite_measure[T2, S2]" finite_fubini_scaf
nil)
(mu formal-const-decl "finite_measure[T1, S1]" finite_fubini_scaf
nil)
(fm_times const-decl
"finite_measure[[T1, T2], sigma_times(S1, S2)]"
product_finite_measure nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_scaf nil)
(S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_scaf 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 finite_fubini_scaf nil)
(T1 formal-type-decl nil finite_fubini_scaf nil)
(isf_y_section formula-decl nil finite_fubini_scaf nil))
nil))
(isf_integral_y 0
(isf_integral_y-1 nil 3458816919
("" (skosimp)
((""
(lemma
"isf_induction[[T1, T2], sigma_times(S1, S2), to_measure(fm_times(mu,nu))]"
("P"
"lambda i: integrable?(LAMBDA y: isf_integral(LAMBDA x: i(x, y)))"))
(("1" (inst - "i!1")
(("1" (assert)
(("1" (hide 2)
(("1" (rewrite "isf_integral_zero")
(("1" (rewrite "integrable_zero")
(("1" (skosimp)
(("1"
(case "forall y: isf?(phi(lambda x: E!1(x,y)))")
(("1" (expand "+" 1)
(("1" (expand "*" 1)
(("1"
(case "forall y: isf_integral(LAMBDA x:
i!2(x, y) + c!1 * phi(E!1)(x, y)) = isf_integral(LAMBDA x: i!2(x, y))+c!1*isf_integral(phi(LAMBDA x: E!1(x, y)))")
(("1" (rewrite "extensionality_postulate" -1)
(("1" (replace -1)
(("1"
(hide -1)
(("1"
(lemma
"integrable_add"
("f1"
"LAMBDA (y):
isf_integral(LAMBDA x: i!2(x, y))"
"f2"
"lambda y: c!1 * isf_integral(phi(LAMBDA x: E!1(x, y)))"))
(("1"
(expand "+" -1)
(("1" (propax) nil nil))
nil)
("2"
(hide 2)
(("2"
(hide -2)
(("2"
(lemma
"integrable_scal[T2, S2, to_measure(nu)]"
("c"
"c!1"
"f"
"lambda y: isf_integral[T1, S1, to_measure(mu)]
(phi[T1, S1](LAMBDA x: E!1(x, y)))"))
(("1"
(expand "*" -1)
(("1" (propax) nil nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"integral_phi2"
("E" "E!1"))
(("1"
(expand "phi")
(("1"
(expand "member")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"y_section_integrable"
("mu"
"mu"
"M"
"E!1"
"nu"
"nu"))
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.103 Sekunden
(vorverarbeitet)
¤
|
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.
|
