|
(measure_completion_aux
(almost_measurable?_TCC1 0
(almost_measurable?_TCC1-1 nil 3458543747 ("" (assuming-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_completion_aux 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_algebra_union? const-decl "bool" subset_algebra_def nil)
(is_countable const-decl "bool" countability "sets_aux/")
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(member const-decl "bool" sets nil)
(subset_algebra_complement application-judgement "(S)" measure_def
nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/"))
nil))
(empty_almost_measurable 0
(empty_almost_measurable-1 nil 3423745840
("" (skosimp)
(("" (expand "almost_measurable?")
(("" (case "negligible_set?[T, S!1, m!1](emptyset[T])")
(("1" (inst + "emptyset[T]" "emptyset[T]" "emptyset[T]")
(("1" (apply-extensionality :hide? t) (("1" (grind) nil nil))
nil)
("2" (typepred "S!1")
(("2" (expand "sigma_algebra?")
(("2" (expand "subset_algebra_empty?")
(("2" (expand "member") (("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "S!1")
(("2" (typepred "m!1")
(("2" (expand "measure?")
(("2" (expand "sigma_algebra?")
(("2" (flatten)
(("2" (hide -2 -4 -5)
(("2" (expand "measure_empty?")
(("2" (expand "subset_algebra_empty?")
(("2" (expand "member")
(("2" (expand "negligible_set?")
(("2"
(inst + "emptyset[T]")
(("2"
(expand "null_set?")
(("2"
(expand "measurable_set?")
(("2"
(expand "mu_fin?")
(("2"
(expand "mu")
(("2"
(replace -1)
(("2"
(assert)
(("2"
(replace -2)
(("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)
((almost_measurable? const-decl "bool" measure_completion_aux nil)
(null_set? const-decl "bool" measure_theory nil)
(mu_fin? const-decl "bool" measure_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(mu const-decl "nnreal" measure_props nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measure_empty? const-decl "bool" generalized_measure_def 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)
(S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux
nil)
(m!1 skolem-const-decl "measure_type[T, S!1]"
measure_completion_aux nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(member const-decl "bool" sets nil)
(finite_union application-judgement "finite_set[T]"
countable_setofsets "sets_aux/")
(countable_difference application-judgement "countable_set[T]"
countable_setofsets "sets_aux/")
(finite_difference application-judgement "finite_set[T]"
countable_setofsets "sets_aux/")
(union const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil measure_completion_aux nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans 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)
(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/")
(measure? const-decl "bool" generalized_measure_def nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(negligible_set? const-decl "bool" measure_theory nil)
(emptyset const-decl "set" sets nil))
shostak))
(complement_almost_measurable 0
(complement_almost_measurable-1 nil 3423745091
("" (skolem + ("_" "S!1" "m!1"))
((""
(case "FORALL (X: set[T]):
almost_measurable?(S!1, m!1)(X) =>
almost_measurable?(S!1, m!1)(complement(X))")
(("1" (skosimp)
(("1" (split)
(("1" (flatten)
(("1" (inst - "X!1") (("1" (assert) nil nil)) nil)) nil)
("2" (flatten)
(("2" (inst - "complement(X!1)")
(("2" (rewrite "complement_complement")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (expand "almost_measurable?")
(("2" (skosimp)
(("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "difference_intersection")
(("2" (rewrite "demorgan2")
(("2" (rewrite "demorgan1")
(("2" (rewrite "complement_complement")
(("2" (rewrite "union_commutative")
(("2"
(rewrite "distribute_union_intersection")
(("2"
(lemma
"demorgan2"
("a" "complement(N2!1)" "b" "N1!1"))
(("2"
(rewrite "complement_complement")
(("2"
(rewrite
"intersection_commutative")
(("2"
(rewrite
"difference_intersection"
-
:dir
rl)
(("2"
(replace -1 1 rl)
(("2"
(hide -1)
(("2"
(rewrite
"difference_intersection"
+
:dir
rl)
(("2"
(rewrite
"union_commutative")
(("2"
(inst
+
"complement(Y!1)"
"N2!1"
"difference(N1!1, N2!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complement const-decl "set" sets nil)
(almost_measurable? const-decl "bool" measure_completion_aux 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)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_completion_aux nil)
(complement_complement formula-decl nil sets_lemmas nil)
(demorgan2 formula-decl nil sets_lemmas nil)
(distribute_union_intersection formula-decl nil sets_lemmas nil)
(negligible_union application-judgement "negligible" measure_theory
nil)
(subset_algebra_difference application-judgement "(S)" measure_def
nil)
(difference const-decl "set" sets nil)
(negligible_intersection application-judgement "negligible"
measure_theory nil)
(intersection_commutative formula-decl nil sets_lemmas nil)
(union_commutative formula-decl nil sets_lemmas nil)
(intersection const-decl "set" sets nil)
(demorgan1 formula-decl nil sets_lemmas nil)
(subset_algebra_complement application-judgement "(S)" measure_def
nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(negligible_set? const-decl "bool" measure_theory nil)
(union const-decl "set" sets nil)
(difference_intersection formula-decl nil sets_lemmas nil))
shostak))
(Union_almost_measurable 0
(Union_almost_measurable-1 nil 3423746160
("" (skosimp)
((""
(name "SPLIT"
"lambda (X:(XS!1)): choose({Z:[(S!1),negligible[T,S!1,m!1],negligible[T,S!1,m!1]] | X = difference(union(Z`1,Z`2),Z`3)})")
(("1"
(name "F1"
"lambda X: if XS!1(X) THEN SPLIT(X)`1 else emptyset[T] endif")
(("1"
(name "F2"
"lambda X: if XS!1(X) THEN SPLIT(X)`2 else emptyset[T] endif")
(("1"
(name "F3"
"lambda X: if XS!1(X) THEN SPLIT(X)`3 else emptyset[T] endif")
(("1" (hide -4)
(("1" (lemma "countable_image" ("f" "F1" "S" "XS!1"))
(("1" (lemma "countable_image" ("f" "F2" "S" "XS!1"))
(("1" (lemma "countable_image" ("f" "F3" "S" "XS!1"))
(("1" (assert)
(("1" (name-replace "NS2" "image(F3)(XS!1)")
(("1" (name-replace "NS1" "image(F2)(XS!1)")
(("1" (name-replace "YS" "image(F1)(XS!1)")
(("1" (hide -4 -5 -6)
(("1"
(lemma
"negligible_Union[T,S!1,m!1]"
("Z" "NS2"))
(("1"
(lemma
"negligible_Union[T,S!1,m!1]"
("Z" "NS1"))
(("1"
(assert)
(("1"
(split -1)
(("1"
(split -2)
(("1"
(typepred "S!1")
(("1"
(expand "sigma_algebra?")
(("1"
(flatten)
(("1"
(expand
"sigma_algebra_union?")
(("1"
(inst - "YS")
(("1"
(assert)
(("1"
(split -3)
(("1"
(expand
"almost_measurable?"
1)
(("1"
(case
"forall (X:(XS!1)): X = difference(union(F1(X), F2(X)), F3(X))")
(("1"
(inst
+
"Union(YS)"
"Union(NS1)"
"difference(union(Union(YS),Union(NS1)),Union(XS!1))")
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(expand
"union"
1)
(("1"
(expand
"difference"
1)
(("1"
(expand
"member")
(("1"
(case-replace
"Union(XS!1)(x!1)")
(("1"
(flatten)
(("1"
(expand
"Union")
(("1"
(skosimp)
(("1"
(typepred
"a!1")
(("1"
(inst
-
"a!1")
(("1"
(replace
-3
-2)
(("1"
(expand
"difference"
-2)
(("1"
(expand
"union"
-2)
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(split
-2)
(("1"
(inst
2
"F1(a!1)")
(("1"
(expand
"YS")
(("1"
(expand
"image")
(("1"
(expand
"image")
(("1"
(inst
+
"a!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
3
"F2(a!1)")
(("2"
(expand
"NS1")
(("2"
(expand
"image")
(("2"
(expand
"image")
(("2"
(inst
+
"a!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
1
2)
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"negligible_subset[T,S!1,m!1]"
("X"
"difference[T]
(union[T](Union[T](YS), Union[T](NS1)), Union[T](XS!1))"
"E"
"union(Union(NS1),Union(NS2))"))
(("1"
(assert)
(("1"
(hide
2)
(("1"
(expand
"subset?"
1)
(("1"
(expand
"union"
1)
(("1"
(expand
"member")
(("1"
(skosimp*)
(("1"
(expand
"difference"
-1)
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand
"Union"
-1)
(("1"
(skosimp)
(("1"
(typepred
"a!1")
(("1"
(expand
"YS"
-1)
(("1"
(expand
"image")
(("1"
(expand
"image")
(("1"
(skosimp)
(("1"
(typepred
"x!2")
(("1"
(inst
-
"x!2")
(("1"
(expand
"Union")
(("1"
(inst
+
"x!2")
(("1"
(replace
-4
1)
(("1"
(expand
"difference"
1)
(("1"
(expand
"member")
(("1"
(expand
"union"
1)
(("1"
(expand
"member")
(("1"
(replace
-2)
(("1"
(assert)
(("1"
(inst
2
"F3(x!2)")
(("1"
(expand
"NS2")
(("1"
(expand
"image")
(("1"
(expand
"image")
(("1"
(inst
+
"x!2")
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))
nil))
nil))
nil))
nil)
("2"
(rewrite
"negligible_union[T, S!1, m!1]"
1)
nil
nil))
nil))
nil)
("2"
(hide-all-but
(-9 1))
(("2"
(skosimp)
(("2"
(typepred
"X!1")
(("2"
(expand
"F1")
(("2"
(expand
"F2")
(("2"
(expand
"F3")
(("2"
(name
"SP"
"SPLIT(X!1)")
(("2"
(replace
-1)
(("2"
(expand
"SPLIT")
(("2"
(case
"nonempty?({Z: [(S!1), negligible[T, S!1, m!1], negligible[T, S!1, m!1]]
| X!1 = difference(union(Z`1, Z`2), Z`3)})")
(("1"
(lemma
"choose_member"
("a"
"{Z:
[(S!1), negligible[T, S!1, m!1],
negligible[T, S!1, m!1]]
| X!1 = difference(union(Z`1, Z`2), Z`3)}"))
(("1"
(split
-1)
(("1"
(replace
-3)
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(hide
-1
2)
(("2"
(expand
"nonempty?")
(("2"
(expand
"empty?")
(("2"
(expand
"member")
(("2"
(expand
"every")
(("2"
(inst
-3
"X!1")
(("2"
(expand
"almost_measurable?")
(("2"
(skosimp)
(("2"
(inst
-
"(Y!1,N1!1,N2!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred
"x!1")
(("2"
(hide-all-but
(-1 1))
(("2"
(expand
"YS")
(("2"
(expand
"image")
(("2"
(expand
"image")
(("2"
(skosimp)
(("2"
(expand
"F1")
(("2"
(expand
"SPLIT")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-5 1))
(("2"
(expand "every")
(("2"
(skosimp)
(("2"
(typepred "x!1")
(("2"
(expand "NS2")
(("2"
(expand "image")
(("2"
(expand "image")
(("2"
(skosimp)
(("2"
(expand "F3")
(("2"
(expand
"SPLIT")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-5 1))
(("2"
(expand "every")
(("2"
(skosimp)
(("2"
(typepred "x!1")
(("2"
(expand "NS1")
(("2"
(expand "image")
(("2"
(expand "image")
(("2"
(skosimp)
(("2"
(expand "F2")
(("2"
(expand
"SPLIT")
(("2"
(assert)
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)
("2" (skosimp)
(("2" (typepred "X!1")
(("2" (hide 2 -3)
(("2" (expand "every")
(("2" (inst - "X!1")
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (expand "almost_measurable?")
(("2" (skosimp)
(("2" (inst - "(Y!1,N1!1,N2!1)") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(negligible_set? const-decl "bool" measure_theory 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)
(set type-eq-decl nil sets 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_completion_aux nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(negligible_subset formula-decl nil measure_theory nil)
(x!2 skolem-const-decl "(XS!1)" measure_completion_aux nil)
(F3 skolem-const-decl "[set[T] -> set[T]]" measure_completion_aux
nil)
(NS2 skolem-const-decl "set[set[T]]" measure_completion_aux nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(negligible_union judgement-tcc nil measure_theory nil)
(F2 skolem-const-decl "[set[T] -> set[T]]" measure_completion_aux
nil)
(F1 skolem-const-decl "[set[T] -> setof[T]]" measure_completion_aux
nil)
(a!1 skolem-const-decl "(XS!1)" measure_completion_aux nil)
(image const-decl "set[R]" function_image nil)
(XS!1 skolem-const-decl "setofsets[T]" measure_completion_aux nil)
(NS1 skolem-const-decl "set[set[T]]" measure_completion_aux nil)
(m!1 skolem-const-decl "measure_type[T, S!1]"
measure_completion_aux nil)
(YS skolem-const-decl "set[setof[T]]" measure_completion_aux nil)
(Union const-decl "set" sets nil)
(S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux
nil)
(choose_member formula-decl nil sets_lemmas nil)
(every const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(SPLIT skolem-const-decl "[X: (XS!1) ->
({Z: [(S!1), negligible[T, S!1, m!1], negligible[T, S!1, m!1]] |
X = difference(union(Z`1, Z`2), Z`3)})]" measure_completion_aux
nil)
(almost_measurable? const-decl "bool" measure_completion_aux nil)
(member const-decl "bool" sets nil)
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(negligible_Union formula-decl nil measure_theory nil)
(image const-decl "set[R]" function_image nil)
(countable_image formula-decl nil countable_image "sets_aux/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(emptyset const-decl "set" sets nil))
shostak))
(completion_TCC1 0
(completion_TCC1-1 nil 3422591880
("" (skosimp)
(("" (expand "sigma_algebra?")
(("" (split)
(("1" (lemma "empty_almost_measurable" ("S" "S!1" "m" "m!1"))
(("1" (expand "subset_algebra_empty?")
(("1" (expand "member") (("1" (propax) nil nil)) nil))
nil))
nil)
("2"
(lemma "complement_almost_measurable" ("S" "S!1" "m" "m!1"))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.848 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.
|
