|
(product_finite_measure
(x_section_bounded_TCC1 0
(x_section_bounded_TCC1-1 nil 3450064167
("" (skosimp)
(("" (expand "x_section")
((""
(lemma "x_section_measurable[T1,T2]"
("Z" "M!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]" product_finite_measure
nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
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 product_finite_measure nil)
(T2 formal-type-decl nil product_finite_measure nil))
nil))
(x_section_bounded 0
(x_section_bounded-1 nil 3450064365
("" (skosimp)
(("" (expand "o ")
(("" (split)
(("1" (assert) nil nil)
("2" (expand "x_section")
(("2"
(lemma "x_section_measurable[T1,T2]"
("Z" "M!1" "x" "x!1" "S1" "S1" "S2" "S2"))
(("2" (expand "member")
(("2"
(lemma "fm_monotone[T2,S2,nu!1]"
("A" "x_section(M!1, x!1)" "B" "fullset[T2]"))
(("2" (split)
(("1" (propax) nil nil)
("2" (expand "subset?")
(("2" (skosimp)
(("2" (expand "member")
(("2" (expand "fullset")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(x_section const-decl "[T1 -> set[T2]]" cross_product "topology/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(subset_algebra_fullset name-judgement "(S)" product_finite_measure
nil)
(fm_monotone formula-decl nil finite_measure nil)
(x_section const-decl "set[T2]" cross_product "topology/")
(fullset const-decl "set" sets 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)
(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]" product_finite_measure
nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
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 product_finite_measure nil)
(T2 formal-type-decl nil product_finite_measure nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(y_section_bounded_TCC1 0
(y_section_bounded_TCC1-1 nil 3450064167
("" (skosimp)
(("" (expand "y_section")
((""
(lemma "y_section_measurable[T1,T2]"
("Z" "M!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]" product_finite_measure
nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
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 product_finite_measure nil)
(T2 formal-type-decl nil product_finite_measure nil))
nil))
(y_section_bounded 0
(y_section_bounded-1 nil 3450064193
("" (skosimp)
(("" (expand "o")
(("" (split)
(("1" (assert) nil nil)
("2" (expand "y_section")
(("2"
(lemma "y_section_measurable[T1,T2]"
("Z" "M!1" "y" "y!1" "S1" "S1" "S2" "S2"))
(("2" (expand "member")
(("2"
(lemma "m_monotone[T1,S1,to_measure(mu!1)]"
("a" "y_section(M!1, y!1)" "b" "fullset[T1]"))
(("1" (split)
(("1" (expand "to_measure")
(("1" (expand "x_le") (("1" (propax) nil nil))
nil))
nil)
("2" (expand "subset?")
(("2" (expand "fullset")
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil)
("3" (expand "measurable_set?")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(y_section const-decl "[T2 -> set[T1]]" cross_product "topology/")
(member const-decl "bool" sets nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(subset? const-decl "bool" sets nil)
(subset_algebra_fullset name-judgement "(S)" product_finite_measure
nil)
(m_monotone formula-decl nil measure_props nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(y_section const-decl "set[T1]" cross_product "topology/")
(fullset const-decl "set" sets 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)
(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]" product_finite_measure
nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
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 product_finite_measure nil)
(T2 formal-type-decl nil product_finite_measure nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(x_section_measurable 0
(x_section_measurable-1 nil 3430980741
("" (skosimp)
(("" (name "F" "lambda M: nu!1 o x_section(M)")
(("1" (case-replace "nu!1 o x_section(M!1) = F(M!1)")
(("1" (hide-all-but 1)
(("1"
(case "forall x,M: 0 <= F(M)(x) & F(M)(x) <= nu!1(fullset[T2])")
(("1"
(name "U"
"{M:set[[T1,T2]] | sigma_times(S1,S2)(M) & measurable_function?[T1,S1](F(M))}")
(("1"
(case "forall (R:measurable_rectangle(S1,S2)): U(R)")
(("1"
(case "FORALL (a, b: (U)): disjoint?(a,b) => U(union(a, b))")
(("1" (case "FORALL (a: (U)): U(complement(a))")
(("1" (case "monotone?(U)")
(("1" (lemma "monotone_class" ("C" "U"))
(("1" (typepred "rectangle_algebra")
(("1" (typepred "M!1")
(("1" (inst -3 "rectangle_algebra")
(("1"
(split -3)
(("1"
(expand "subset?")
(("1"
(inst - "M!1")
(("1"
(expand "member")
(("1"
(split)
(("1"
(expand "U")
(("1" (propax) nil nil))
nil)
("2"
(hide 2)
(("2"
(expand "sigma_times" -1)
(("2"
(lemma
"generated_sigma_algebra_subset2"
("X"
"extend
[setof[[T1, T2]],
measurable_rectangle[T1, T2](S1, S2),
bool, FALSE]
(fullset
[measurable_rectangle
[T1, T2](S1, S2)])"
"Y"
"generated_sigma_algebra(rectangle_algebra)"))
(("2"
(name-replace
"SA"
"generated_sigma_algebra(extend
[setof[[T1, T2]],
measurable_rectangle[T1, T2](S1, S2),
bool, FALSE]
(fullset
[measurable_rectangle
[T1, T2](S1, S2)]))")
(("2"
(split -1)
(("1"
(expand "subset?")
(("1"
(inst - "M!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"subset?")
(("2"
(expand
"fullset")
(("2"
(expand
"extend")
(("2"
(expand
"member")
(("2"
(skosimp)
(("2"
(prop)
(("2"
(lemma
"generated_sigma_algebra_subset1"
("X"
"rectangle_algebra"))
(("2"
(expand
"subset?")
(("2"
(inst
-
"x!1")
(("2"
(assert)
(("2"
(hide-all-but
(-1
1))
(("2"
(expand
"rectangle_algebra")
(("2"
(expand
"finite_disjoint_unions")
(("2"
(expand
"fullset")
(("2"
(expand
"extend")
(("2"
(prop)
(("2"
(expand
"finite_disjoint_union?")
(("2"
(inst
+
"lambda (i:nat): if i = 0 then x!1 else emptyset[[T1,T2]] endif"
"1")
(("2"
(split)
(("1"
(hide
-1)
(("1"
(grind)
nil
nil))
nil)
("2"
(apply-extensionality
:hide?
t)
(("2"
(expand
"IUnion")
(("2"
(case-replace
"x!1(x!2, x!3)")
(("1"
(inst
+
"0")
nil
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(expand
"emptyset")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(case-replace
"i!1=0")
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(rewrite
"emptyset_is_empty?")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "subset?")
(("2"
(skosimp)
(("2"
(expand "member")
(("2"
(expand "rectangle_algebra")
(("2"
(expand
"finite_disjoint_unions")
(("2"
(hide -3)
(("2"
(expand "fullset")
(("2"
(expand "extend")
(("2"
(prop)
(("2"
(expand
"finite_disjoint_union?")
(("2"
(skosimp)
(("2"
(case
"forall (n:nat): U(IUnion(n,E!1))")
(("1"
(case-replace
"IUnion(E!1)=IUnion(n!1,E!1)")
(("1"
(inst
-
"n!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
(1 -4))
(("2"
(apply-extensionality
:hide?
t)
(("2"
(expand
"IUnion")
(("2"
(expand
"image")
(("2"
(expand
"Union")
(("2"
(case-replace
"EXISTS (i: nat): E!1(i)(x!2, x!3)")
(("1"
(skosimp)
(("1"
(inst
-
"i!1")
(("1"
(flatten)
(("1"
(case-replace
"i!1)
(("1"
(inst
+
"E!1(i!1)")
(("1"
(inst
+
"i!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"empty?")
(("2"
(inst
-3
"(x!2,x!3)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
1
2)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred
"a!1")
(("2"
(skolem
-
"n!2")
(("2"
(inst
+
"n!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-7
-1
-8
-3))
(("2"
(induct
"n")
(("1"
(rewrite
"IUnion_0_def")
(("1"
(inst
-
"0")
(("1"
(flatten)
(("1"
(inst
-5
"E!1(0)")
(("1"
(assert)
(("1"
(rewrite
"emptyset_is_empty?")
(("1"
(replace
-2)
(("1"
(hide-all-but
1)
(("1"
(expand
"measurable_rectangle?")
(("1"
(inst
+
"emptyset"
"emptyset")
(("1"
(split)
(("1"
(apply-extensionality
:hide?
t)
(("1"
(grind)
nil
nil))
nil)
("2"
(typepred
"S1")
(("2"
(expand
"sigma_algebra?")
(("2"
(flatten)
(("2"
(expand
"subset_algebra_empty?")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(typepred
"S2")
(("3"
(expand
"sigma_algebra?")
(("3"
(flatten)
(("3"
(expand
"subset_algebra_empty?")
(("3"
(expand
"member")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(rewrite
"IUnion_n_def")
(("2"
(inst
-5
"E!1(1 + j!1)")
(("1"
(inst
-4
"IUnion(j!1, E!1)"
"E!1(1 + j!1)")
(("1"
(split)
(("1"
(propax)
nil
nil)
("2"
(hide-all-but
(-2
1))
(("2"
(expand
"disjoint?")
(("2"
(expand
"disjoint?")
(("2"
(expand
"intersection")
(("2"
(expand
"IUnion")
(("2"
(expand
"empty?")
(("2"
(skosimp)
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(expand
"image")
(("2"
(expand
"Union")
(("2"
(skosimp)
(("2"
(typepred
"a!1")
(("2"
(skolem
-
"n!2")
(("2"
(inst
-
"n!2"
"1+j!1")
(("2"
(assert)
(("2"
(inst
-
"x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-
"1+j!1")
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(rewrite
"emptyset_is_empty?")
(("2"
(replace
-3)
(("2"
(hide-all-but
1)
(("2"
(expand
"measurable_rectangle?")
(("2"
(inst
+
"emptyset"
"emptyset")
(("2"
(split)
(("1"
(apply-extensionality
:hide?
t)
(("1"
(grind)
nil
nil))
nil)
("2"
(typepred
"S1")
(("2"
(expand
"sigma_algebra?")
(("2"
(flatten)
(("2"
(expand
"subset_algebra_empty?")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(typepred
"S2")
(("3"
(expand
"sigma_algebra?")
(("3"
(flatten)
(("3"
(expand
"subset_algebra_empty?")
(("3"
(expand
"member")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.77 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
