|
(measure_contraction
(contraction_TCC1 0
(contraction_TCC1-1 nil 3431406180
("" (skosimp)
(("" (assert)
(("" (lemma "measurable_intersection[T,S]")
(("" (inst - "A!1" "E!1")
(("" (expand "measurable_set?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((measurable_intersection application-judgement "measurable_set"
measure_contraction 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)
(measurable_intersection judgement-tcc nil measure_space_def nil)
(T formal-type-decl nil measure_contraction 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)
(S formal-const-decl "sigma_algebra" measure_contraction nil))
nil))
(contraction_TCC2 0
(contraction_TCC2-1 nil 3431406180
("" (expand "measurable_set?") (("" (propax) nil nil)) nil)
((measurable_set? const-decl "bool" measure_space_def nil)) nil))
(contraction_TCC3 0
(contraction_TCC3-1 nil 3431406180
("" (skosimp)
(("" (typepred "mu!1")
(("" (expand "measure?")
(("" (flatten)
(("" (split)
(("1" (expand "measure_empty?")
(("1"
(case-replace
"intersection[T](A!1, emptyset[T])=emptyset[T]")
(("1" (hide-all-but 1)
(("1" (apply-extensionality :hide? t)
(("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "measure_countably_additive?")
(("2" (skosimp)
(("2"
(inst -
"lambda (n:nat): intersection[T](A!1, X!1(n))")
(("1" (expand "o")
(("1"
(name-replace "LHS"
"x_sum(LAMBDA (x: nat): mu!1(intersection[T](A!1, X!1(x))))")
(("1"
(case-replace
"IUnion(LAMBDA (n: nat): intersection[T](A!1, X!1(n)))=intersection[T](A!1, IUnion(X!1))")
(("1" (hide -1)
(("1" (assert)
(("1" (hide 1 -2)
(("1"
(lemma
"measurable_intersection[T,S]"
("a" "A!1" "b" "IUnion(X!1)"))
(("1"
(expand "measurable_set?")
(("1"
(case-replace
"IUnion(LAMBDA (n: nat): intersection[T](A!1, X!1(n)))=intersection[T](A!1, IUnion(X!1))")
(("1"
(hide-all-but 1)
(("1"
(apply-extensionality :hide? t)
(("1"
(expand "intersection")
(("1"
(expand "IUnion")
(("1"
(expand "member")
(("1"
(case-replace
"A!1(x!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "measurable_set?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (skosimp)
(("2"
(lemma "measurable_intersection[T,S]"
("a" "A!1" "b" "X!1(x!1)"))
(("1" (expand "measurable_set?")
(("1" (propax) nil nil)) nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (typepred "X!1")
(("2" (expand "disjoint_indexed_measurable?")
(("2" (expand "disjoint?")
(("2" (expand "disjoint?")
(("2" (expand "intersection")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(skosimp)
(("2"
(skosimp)
(("2"
(inst - "i!1" "j!1")
(("2"
(assert)
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but 1)
(("3" (skosimp)
(("3"
(lemma "measurable_intersection[T,S]"
("a" "A!1" "b" "X!1(n!1)"))
(("1" (expand "measurable_set?")
(("1" (propax) nil nil)) nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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/")
(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)
(S formal-const-decl "sigma_algebra" measure_contraction 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)
(T formal-type-decl nil measure_contraction nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
measure_contraction nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(X!1 skolem-const-decl "disjoint_indexed_measurable[T, S]"
measure_contraction nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(A!1 skolem-const-decl "measurable_set[T, S]" measure_contraction
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)
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(measurable_intersection judgement-tcc nil measure_space_def nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(O const-decl "T3" function_props nil)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(subset_algebra_intersection application-judgement "(S)"
measure_contraction nil)
(measure_empty? const-decl "bool" generalized_measure_def nil)
(member const-decl "bool" sets nil)
(subset_algebra_emptyset name-judgement "(S)" measure_contraction
nil)
(measurable_emptyset name-judgement "measurable_set"
measure_contraction nil)
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_intersection1 application-judgement "finite_set[T]"
countable_setofsets "sets_aux/")
(countable_intersection2 application-judgement "countable_set[T]"
countable_setofsets "sets_aux/")
(measurable_intersection application-judgement "measurable_set"
measure_contraction nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(intersection const-decl "set" sets nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(emptyset const-decl "set" sets nil))
nil))
(fm_contraction_TCC1 0
(fm_contraction_TCC1-1 nil 3456294370 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil measure_contraction nil)
(set type-eq-decl nil sets 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)
(S formal-const-decl "sigma_algebra" measure_contraction nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil))
nil))
(fm_contraction_TCC2 0
(fm_contraction_TCC2-1 nil 3456294370
("" (skosimp)
(("" (lemma "contraction_TCC3" ("mu" "mu!1" "A" "A!1"))
(("" (typepred "A!1")
(("" (typepred "mu!1")
(("" (lemma "measure_monotone" ("f" "mu!1" "b" "A!1"))
(("" (replace -2)
(("" (expand "x_le")
(("" (expand "finite_measure?")
(("" (expand "measure?" -5)
(("" (hide -2)
(("" (flatten)
(("" (split)
(("1" (expand "measure_empty?")
(("1" (replace -4) (("1" (assert) nil nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "X!1")
(("2"
(expand "measure_countably_additive?")
(("2"
(inst -6 "X!1")
(("2"
(expand "o ")
(("2"
(expand "x_eq")
(("2"
(flatten)
(("2"
(hide -5)
(("2"
(inst-cp
-
"intersection[T](A!1, IUnion(X!1))")
(("2"
(split -3)
(("1"
(flatten)
(("1"
(replace -1)
(("1"
(replace -7)
(("1"
(replace -8 1 rl)
(("1"
(hide -8)
(("1"
(expand
"x_sum")
(("1"
(case-replace
"FORALL (i:nat): mu!1(intersection[T](A!1, X!1(i)))`1")
(("1"
(lift-if
1)
(("1"
(prop)
(("1"
(rewrite
"limit_lemma")
(("1"
(hide-all-but
(-6
-8
1))
(("1"
(skolem
+
"i!1")
(("1"
(lemma
"measurable_intersection"
("a"
"A!1"
"b"
"X!1(i!1)"))
(("1"
(expand
"measurable_set?")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
1)
(("2"
(propax)
nil
nil))
nil)
("3"
(skosimp)
(("3"
(hide-all-but
(-5
1
-3))
(("3"
(expand
"disjoint_indexed_measurable?")
(("3"
(expand
"measurable_set?")
(("3"
(lemma
"measurable_intersection"
("a"
"A!1"
"b"
"X!1(i!1)"))
(("1"
(assert)
(("1"
(expand
"measurable_set?")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) 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)
((measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(set type-eq-decl nil sets 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/")
(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)
(S formal-const-decl "sigma_algebra" measure_contraction 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)
(T formal-type-decl nil measure_contraction nil)
(contraction_TCC3 subtype-tcc nil measure_contraction nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
measure_contraction nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(measure_empty? const-decl "bool" generalized_measure_def 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)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(series const-decl "sequence[real]" series "series/")
(convergent? const-decl "bool" convergence_sequences "analysis/")
(sequence type-eq-decl nil sequences nil)
(limit_lemma formula-decl nil convergence_sequences "analysis/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(measurable_intersection judgement-tcc nil measure_space_def nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(O const-decl "T3" function_props nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(measure_monotone formula-decl nil measure_def nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(sigma_finite_contraction_def_TCC1 0
(sigma_finite_contraction_def_TCC1-1 nil 3457156931
("" (skosimp)
(("" (expand "measurable_set?")
(("" (lemma "A_of_TCC1" ("f" "nu!1"))
((""
(lemma "choose_member"
("a" "{X: disjoint_indexed_measurable[T, S] |
IUnion[nat, T](X) = fullset[T] AND (FORALL i: nu!1(X(i))`1)}"))
(("" (split)
(("1" (expand "member")
(("1" (flatten)
(("1" (inst - "i!1")
(("1" (expand "A_of") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "nonempty?") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((measurable_set? const-decl "bool" measure_space_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def 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)
(fullset const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(choose_member formula-decl nil sets_lemmas nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
measure_contraction nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(A_of_TCC1 subtype-tcc nil measure_def nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(sigma_finite_measure? const-decl "bool" measure_def nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(T formal-type-decl nil measure_contraction 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)
(S formal-const-decl "sigma_algebra" measure_contraction nil))
nil))
(sigma_finite_contraction_def 0
(sigma_finite_contraction_def-1 nil 3457156932
("" (skosimp)
(("" (typepred "nu!1")
(("" (expand "sigma_finite_measure?")
(("" (expand "measure?")
(("" (flatten)
(("" (expand "measure_countably_additive?")
(("" (inst - "lambda i: intersection(A_of(nu!1)(i),E!1)")
(("1" (name "AA" "A_of(nu!1)")
(("1" (replace -1)
(("1" (expand "fm_contraction")
(("1" (expand "o ")
(("1" (expand "A_of")
(("1" (lemma "A_of_TCC1" ("f" "nu!1"))
(("1"
(lemma "choose_member"
("a"
"{X: disjoint_indexed_measurable[T, S] |
IUnion[nat, T](X) = fullset[T] AND (FORALL i: nu!1(X(i))`1)}"))
(("1"
(split)
(("1"
(replace -3)
(("1"
(expand "member")
(("1"
(flatten)
(("1"
(hide -3 -4)
(("1"
(case-replace
"IUnion(LAMBDA i: intersection(AA(i), E!1))=E!1")
(("1"
(hide -1)
(("1"
(lemma
"x_sum_eq"
("S"
"LAMBDA i: nu!1(intersection(AA(i), E!1))"
"T"
"LAMBDA i: (TRUE, nu!1(intersection(AA(i), E!1))`2)"))
(("1"
(split)
(("1"
(expand "x_eq")
(("1"
(flatten)
(("1"
(replace -1 * rl)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(hide -1 -3 -4)
(("2"
(inst - "i!1")
(("2"
(lemma
"measure_monotone"
("f"
"nu!1"
"a"
"intersection(AA(i!1), E!1)"
"b"
"AA(i!1)"))
(("2"
(split)
(("1"
(expand
"x_le")
(("1"
(assert)
(("1"
(flatten)
(("1"
(expand
"x_eq")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred
"nu!1")
(("2"
(expand
"sigma_finite_measure?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("3"
(hide-all-but
1)
(("3"
(expand
"intersection")
(("3"
(expand
"subset?")
(("3"
(expand
"member")
(("3"
(skosimp)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(lemma
"measurable_intersection"
("a"
"AA(i!1)"
"b"
"E!1"))
(("1"
(expand
"measurable_set?")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2"
(apply-extensionality
:hide?
t)
(("2"
(lemma
"extensionality_postulate"
("f"
"IUnion[nat, T](AA)"
"g"
"fullset[T]"))
(("2"
(flatten)
(("2"
(split -2)
(("1"
(hide -2 -3)
(("1"
(inst - "x!1")
(("1"
(expand
"fullset")
(("1"
(expand
"IUnion")
(("1"
(skosimp)
(("1"
(case-replace
"E!1(x!1)")
(("1"
(expand
"intersection")
(("1"
(expand
"member")
(("1"
(inst
+
"i!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(expand
"intersection")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "nonempty?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "A_of[T, S](nu!1)")
(("2" (expand "disjoint_indexed_measurable?")
(("2" (expand "disjoint?")
(("2" (skosimp)
(("2" (inst - "i!1" "j!1")
(("2" (assert)
(("2"
(expand "disjoint?")
(("2"
(expand "intersection")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3"
(lemma "measurable_intersection"
("a" "A_of[T, S](nu!1)(i!1)" "b" "E!1"))
(("1" (expand "measurable_set?")
(("1" (propax) nil nil)) nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(S formal-const-decl "sigma_algebra" measure_contraction 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)
(T formal-type-decl nil measure_contraction nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(measure? const-decl "bool" generalized_measure_def nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
measure_contraction nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(= const-decl "[T, T -> boolean]" equalities nil)
(fm_contraction const-decl "finite_measure" measure_contraction
nil)
(choose_member formula-decl nil sets_lemmas nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(fullset const-decl "set" sets nil)
(nonempty? const-decl "bool" sets nil)
(x_sum_eq formula-decl nil extended_nnreal "extended_nnreal/")
(TRUE const-decl "bool" booleans nil)
(measure_monotone formula-decl nil measure_def nil)
(subset? const-decl "bool" sets nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(measurable_fullset name-judgement "measurable_set[T, S]"
measure_contraction nil)
(subset_algebra_fullset name-judgement "(S)" measure_contraction
nil)
(measurable_intersection judgement-tcc nil measure_space_def nil)
(extensionality_postulate formula-decl nil functions nil)
(member const-decl "bool" sets nil)
(A_of_TCC1 subtype-tcc nil measure_def nil)
(O const-decl "T3" function_props 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)
(set type-eq-decl nil sets nil)
(intersection const-decl "set" sets nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(nu!1 skolem-const-decl "sigma_finite_measure[T, S]"
measure_contraction nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(E!1 skolem-const-decl "measurable_set[T, S]" measure_contraction
nil))
shostak))
(contraction_is_sigma_finite 0
(contraction_is_sigma_finite-1 nil 3460361064
("" (skosimp)
(("" (typepred "nu!1")
(("" (expand "sigma_finite_measure?")
(("" (flatten)
(("" (expand "measure_sigma_finite?")
(("" (skosimp)
(("" (inst + "X!1")
(("" (replace -2)
(("" (skosimp)
(("" (inst - "i!1")
(("" (expand "contraction")
((""
(lemma "m_monotone[T,S,nu!1]"
("a" "intersection(A!1, X!1(i!1))" "b"
"X!1(i!1)"))
(("1" (expand "x_le")
(("1" (assert)
(("1"
(hide-all-but 1)
(("1"
(expand "intersection")
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1" (skosimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil)
("3" (expand "measurable_set?")
(("3" (typepred "A!1")
(("3"
(typepred "X!1(i!1)")
(("3"
(lemma
"measurable_intersection"
("a" "A!1" "b" "X!1(i!1)"))
(("1"
(expand "measurable_set?")
(("1" (propax) nil nil))
nil)
("2"
(expand "measurable_set?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(S formal-const-decl "sigma_algebra" measure_contraction 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)
(T formal-type-decl nil measure_contraction nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(intersection const-decl "set" sets nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(set type-eq-decl nil sets nil)
(m_monotone formula-decl nil measure_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset_algebra_fullset name-judgement "(S)" measure_contraction
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
measure_contraction nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
measure_contraction nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(measurable_intersection judgement-tcc nil measure_space_def nil)
(contraction const-decl "measure_type" measure_contraction nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def 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)
(measure_sigma_finite? const-decl "bool" measure_def nil))
nil))
(contraction_isf 0
(contraction_isf-1 nil 3431719231
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (expand "isf?")
(("1" (split)
(("1" (lemma "phi_is_simple[T,S]" ("X" "A!1"))
(("1" (lemma "simple_times" ("h1" "phi(A!1)" "h2" "f!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil)
("2" (typepred "A!1")
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (expand "mu_fin?")
(("2" (expand "contraction")
(("2" (expand "nonzero_set?")
(("2" (expand "intersection")
(("2" (expand "phi")
(("2" (expand "member")
(("2" (expand "*")
(("2"
(case-replace
"{x: T | IF A!1(x) THEN 1 ELSE 0 ENDIF * f!1(x) /= 0}={x_1: T | A!1(x_1) AND f!1(x_1) /= 0}")
(("2" (hide -1 2)
(("2"
(apply-extensionality :hide? t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "isf?")
(("2" (flatten)
(("2" (hide -1)
(("2" (expand "nonzero_set?")
(("2" (expand "mu_fin?")
(("2" (expand "contraction")
(("2" (expand "intersection")
(("2" (expand "phi")
(("2" (expand "member")
(("2" (expand "*")
(("2"
(case-replace
"{x: T | IF A!1(x) THEN 1 ELSE 0 ENDIF * f!1(x) /= 0}={x_1: T | A!1(x_1) AND f!1(x_1) /= 0}")
(("2"
(hide -1 2)
(("2"
(apply-extensionality :hide? t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((isf? const-decl "bool" isf nil)
(mu_fin? const-decl "bool" measure_props nil)
(nonzero_set? const-decl "set[T]" isf nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_times_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(contraction const-decl "measure_type" measure_contraction nil)
(S formal-const-decl "sigma_algebra" measure_contraction 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)
(T formal-type-decl nil measure_contraction nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(set type-eq-decl nil sets nil)
(phi_is_simple judgement-tcc nil measure_space nil)
(simple_times judgement-tcc nil measure_space 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)
(simple? const-decl "bool" measure_space nil)
(simple nonempty-type-eq-decl nil measure_space 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(phi const-decl "nat" measure_space nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(contraction_isf_integral_TCC1 0
(contraction_isf_integral_TCC1-1 nil 3431698665
("" (skosimp)
(("" (typepred "f!1")
(("" (rewrite "contraction_isf")
(("" (expand "isf?")
(("" (expand "simple?") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((isf nonempty-type-eq-decl nil isf nil)
(isf? const-decl "bool" isf nil)
(contraction const-decl "measure_type" measure_contraction nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(set type-eq-decl nil sets 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/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S formal-const-decl "sigma_algebra" measure_contraction 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)
(T formal-type-decl nil measure_contraction nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(simple nonempty-type-eq-decl nil measure_space nil)
(simple? const-decl "bool" measure_space nil)
(contraction_isf formula-decl nil measure_contraction nil))
nil))
(contraction_isf_integral 0
(contraction_isf_integral-1 nil 3431720982
("" (skosimp)
(("" (typepred "f!1")
(("" (lemma "contraction_isf" ("mu" "mu!1" "A" "A!1" "f" "f!1"))
(("" (assert)
(("" (expand "isf_integral")
(("" (expand "mu")
(("" (expand "contraction")
((""
(case "FORALL (c: real):
NOT c = 0 IMPLIES
S(inverse_image[T, real]
(((reals@real_fun_ops[T].*)(phi[T, S](A!1), f!1)),
singleton[real](c)))")
(("1"
(case-replace "(LAMBDA (c:real):
IF c = 0 THEN 0
ELSE c *
mu!1(intersection(A!1,
inverse_image[T, real]
(f!1, singleton[real](c))))`2
ENDIF)=(LAMBDA (c:real):
IF c = 0 THEN 0
ELSE c *
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.157 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.
|
