| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 459 kB |
|
Quellcode-Bibliothek measure_completion_aux.prfSprache: Lisp |
|||||||||||||||
|
(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]] | (("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")) (("2" (expand "subset_algebra_complement?") (("2" (skosimp) (("2" (typepred "x!1") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "sigma_algebra_union?") (("3" (skosimp) (("3" (lemma "Union_almost_measurable" ("S" "S!1" "m" "m!1" "XS" "X!1")) (("3" (assert) (("3" (expand "every") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra_union? const-decl "bool" subset_algebra_def nil) (Union_almost_measurable formula-decl nil measure_completion_aux nil) (every const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (complement_almost_measurable formula-decl nil measure_completion_aux nil) (subset_algebra_complement application-judgement "(S)" measure_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (almost_measurable? const-decl "bool" measure_completion_aux nil) (subset_algebra_complement? const-decl "bool" subset_algebra_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/") (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 nonempty-type-eq-decl nil 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) (empty_almost_measurable formula-decl nil measure_completion_aux 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/") (member const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)) nil)) (generated_completion 0 (generated_completion-1 nil 3423804357 ("" (skosimp) (("" (expand "extend") (("" (expand "union") (("" (expand "member") (("" (expand "fullset") (("" (expand "generated_sigma_algebra") (("" (apply-extensionality :hide? t) (("" (expand "Intersection") (("" (case-replace "completion(S!1, m!1)(x!1)") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "completion") (("1" (expand "almost_measurable?") (("1" (skosimp) (("1" (inst-cp - "Y!1") (("1" (assert) (("1" (inst-cp - "N1!1") (("1" (inst - "N2!1") (("1" (assert) (("1" (expand "sigma_algebra?") (("1" (flatten) (("1" (lemma "sigma_algebra_union[T,a!1]") (("1" (inst - "Y!1" "N1!1") (("1" (expand "member") (("1" (lemma "sigma_algebra_difference[T,a!1]" ("x" "union(Y!1, N1!1)" "y" "N2!1")) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (inst - "completion(S!1, m!1)") (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (split) (("1" (expand "completion") (("1" (expand "almost_measurable?") (("1" (inst + "x!2" "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (expand "null_set?") (("2" (typepred "m!1") (("2" (expand "measure?") (("2" (flatten) (("2" (expand "measure_empty?") (("2" (expand "mu_fin?") (("2" (expand "mu") (("2" (replace -1) (("2" (expand "measurable_set?") (("2" (assert) (("2" (split) (("1" (assert) (("1" (typepred "S!1") (("1" (expand "sigma_algebra?") (("1" (expand "subset_algebra_empty?") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (inst + "emptyset[T]" "x!2" "emptyset[T]") (("1" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil)) nil) ("2" (hide -1) (("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (typepred "S!1") (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (expand "sigma_algebra?") (("1" (expand "subset_algebra_empty?") (("1" (expand "member") (("1" (flatten) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (typepred "S!1") (("3" (expand "sigma_algebra?") (("3" (expand "subset_algebra_empty?") (("3" (expand "member") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extend const-decl "R" extend nil) (member const-decl "bool" sets nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas 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) (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) (x!2 skolem-const-decl "setof[T]" measure_completion_aux nil) (emptyset const-decl "set" sets nil) (difference const-decl "set" sets nil) (mu_fin? const-decl "bool" measure_props nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (mu const-decl "nnreal" measure_props nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (null_set? const-decl "bool" measure_theory nil) (sigma_algebra_union formula-decl nil sigma_algebra nil) (sigma_algebra_difference formula-decl nil sigma_algebra nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (almost_measurable? const-decl "bool" measure_completion_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (set type-eq-decl nil sets nil) (Intersection const-decl "set" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (subset? const-decl "bool" sets nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (IF const-decl "[boolean, T, T -> T]" if_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) (TRUE const-decl "bool" booleans nil) (FALSE const-decl "bool" booleans nil) (completion const-decl "sigma_algebra[T]" measure_completion_aux nil) (T formal-type-decl nil measure_completion_aux nil) (boolean nonempty-type-decl nil booleans nil) (fullset const-decl "set" sets nil) (union const-decl "set" sets nil)) shostak)) (completion_extends 0 (completion_extends-1 nil 3423809053 ("" (skosimp) (("" (expand "completion") (("" (expand "almost_measurable?") (("" (inst + "X!1" "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (typepred "m!1") (("1" (typepred "S!1") (("1" (expand "sigma_algebra?") (("1" (expand "subset_algebra_empty?") (("1" (expand "member") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (flatten) (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((completion const-decl "sigma_algebra[T]" measure_completion_aux 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) (X!1 skolem-const-decl "set[T]" measure_completion_aux nil) (set type-eq-decl nil sets nil) (S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux 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) (emptyset const-decl "set" sets nil) (negligible_set? const-decl "bool" measure_theory nil) (m!1 skolem-const-decl "measure_type[T, S!1]" 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) (negligible nonempty-type-eq-decl nil measure_theory nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (difference const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (null_set? const-decl "bool" measure_theory nil) (mu_fin? const-decl "bool" measure_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (mu const-decl "nnreal" measure_props nil) (measurable_set? const-decl "bool" measure_space_def nil) (almost_measurable? const-decl "bool" measure_completion_aux nil)) shostak)) (negligible_completion 0 (negligible_completion-1 nil 3423809165 ("" (skosimp) (("" (expand "completion") (("" (expand "almost_measurable?") (("" (typepred "S!1") (("" (typepred "m!1") (("" (expand "measure?") (("" (expand "measure_empty?") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (expand "member") (("" (flatten) (("" (inst + "emptyset[T]" "X!1" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (assert) (("1" (expand "mu") (("1" (expand "mu_fin?") (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((completion const-decl "sigma_algebra[T]" measure_completion_aux 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_completion_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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/") (member const-decl "bool" sets nil) (set type-eq-decl nil 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_set? const-decl "bool" measure_theory nil) (X!1 skolem-const-decl "set[T]" measure_completion_aux nil) (emptyset const-decl "set" sets nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (union const-decl "set" sets nil) (difference const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (null_set? const-decl "bool" measure_theory nil) (mu_fin? const-decl "bool" measure_props nil) (mu const-decl "nnreal" measure_props nil) (measurable_set? const-decl "bool" measure_space_def nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (measure_empty? const-decl "bool" generalized_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/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (almost_measurable? const-decl "bool" measure_completion_aux nil)) shostak)) (m_completions 0 (m_completions-1 nil 3423809289 ("" (skosimp) (("" (expand "is_completion") (("" (assert) (("" (skosimp*) (("" (replace -4) (("" (hide -1 -4) (("" (typepred "N1!1") (("" (typepred "N1!2") (("" (typepred "N2!1") (("" (typepred "N2!2") (("" (name "NN" "union(union(N1!1, N2!1),union(N1!2, N2!2))") (("" (case "negligible_set?[T, S!1, m!1](NN)") (("1" (hide -2 -3 -4 -5 -6) (("1" (expand "negligible_set?") (("1" (skosimp) (("1" (case "subset?(A!1,union(B!1,X!2))") (("1" (case "subset?(B!1,union(A!1,X!2))") (("1" (expand "null_set?") (("1" (flatten) (("1" (expand "measurable_set?") (("1" (lemma "m_monotone[T,S!1,m!1]" ("a" "A!1" "b" "union(B!1, X!2)")) (("1" (assert) (("1" (lemma "m_monotone[T,S!1,m!1]" ("a" "B!1" "b" "union(A!1, X!2)")) (("1" (assert) (("1" (lemma "m_union[T,S!1,m!1]" ("a" "B!1" "b" "X!2")) (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (lemma "m_union[T,S!1,m!1]" ("a" "A!1" "b" "X!2")) (("1" (case "x_le(m!1(A!1), m!1(B!1))") (("1" (case "x_le(m!1(B!1), m!1(A!1))") (("1" (hide-all-but (-1 -2 1)) (("1" (expand "x_le") (("1" (expand "x_eq") (("1" (case-replace "m!1(A!1)`1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1 -2 -9 -10)) (("2" (expand "x_le") (("2" (flatten) (("2" (assert) (("2" (expand "x_add") (("2" (flatten) (("2" (assert) (("2" (replace -6) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -4 -2 -8 -9)) (("2" (expand "x_le") (("2" (expand "x_add") (("2" (flatten) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (replace -6) (("2" (flatten) (("2" (assert) nil nil)) 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" (rewrite "measurable_union[T,S!1]") nil nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (rewrite "measurable_union[T,S!1]") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1 -6)) (("2" (expand "difference") (("2" (expand "union") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!1") (("2" (rewrite "extensionality_postulate" -3 :dir rl) (("2" (inst - "x!1") (("2" (expand "NN") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -5 1)) (("2" (expand "subset?") (("2" (expand "union") (("2" (expand "difference") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "NN") (("2" (rewrite "extensionality_postulate" -3 :dir rl) (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 1 rl) (("2" (rewrite "negligible_union[T, S!1, m!1]" +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_completion const-decl "bool" measure_completion_aux nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (NN skolem-const-decl "set[T]" measure_completion_aux nil) (extensionality_postulate formula-decl nil functions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (difference const-decl "set" sets nil) (null_set? const-decl "bool" measure_theory nil) (measurable_set? const-decl "bool" measure_space_def nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (measurable_union judgement-tcc nil measure_space_def nil) (mu_fin? const-decl "bool" measure_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (mu const-decl "nnreal" measure_props nil) (m_union formula-decl nil measure_props nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (m_monotone formula-decl nil measure_props nil) (negligible_union judgement-tcc nil measure_theory nil) (union const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (negligible_union application-judgement "negligible" measure_theory 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) (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) (negligible nonempty-type-eq-decl nil measure_theory nil)) shostak)) (choose_completion_TCC1 0 (choose_completion_TCC1-1 nil 3423832401 ("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (expand "completion") (("" (expand "almost_measurable?") (("" (skosimp) (("" (inst - "Y!1") (("" (inst + "N1!1" "N2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (almost_measurable? const-decl "bool" measure_completion_aux 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) (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) (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) (completion const-decl "sigma_algebra[T]" measure_completion_aux nil) (empty? const-decl "bool" sets nil)) nil)) (choose_completion 0 (choose_completion-1 nil 3423832482 ("" (skosimp) (("" (expand "is_completion") (("" (assert) (("" (case "nonempty?({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X!1 = difference(union(Y, N1), N2)})") (("1" (lemma "choose_member" ("a" "{Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X!1 = difference(union(Y, N1), N2)}")) (("1" (split -1) (("1" (name-replace "YY" "choose({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X!1 = difference(union(Y, N1), N2)})") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "Y!1") (("2" (inst + "N1!1" "N2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_completion const-decl "bool" measure_completion_aux 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) (nonempty? const-decl "bool" sets 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) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (choose_member formula-decl nil sets_lemmas nil) (completion const-decl "sigma_algebra[T]" measure_completion_aux nil) (almost_measurable? const-decl "bool" measure_completion_aux nil) (empty? const-decl "bool" sets nil)) shostak)) (completion_TCC2 0 (completion_TCC2-1 nil 3423805251 ("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (typepred "X!1") (("" (expand "completion") (("" (expand "almost_measurable?") (("" (skosimp) (("" (inst - "Y!1") (("" (inst + "N1!1" "N2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (negligible_set? const-decl "bool" measure_theory nil) (set type-eq-decl nil sets nil) (almost_measurable? const-decl "bool" measure_completion_aux 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) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def 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) (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) (completion const-decl "sigma_algebra[T]" measure_completion_aux nil) (empty? const-decl "bool" sets nil)) nil)) (completion_TCC3 0 (completion_TCC3-1 nil 3423805251 ("" (skosimp) (("" (case "forall (X: (completion(S!1, m!1))): nonempty?({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X = difference[T](union[T](Y, N1), N2)})") (("1" (expand "complete_measure?") (("1" (case-replace "measure?(LAMBDA (X: (completion(S!1, m!1))): m!1(choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X = difference[T](union[T](Y, N1), N2)})))") (("1" (expand "measure_complete?") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "completion") (("1" (expand "almost_measurable?") (("1" (skosimp) (("1" (case "m!1(Y!1)=(TRUE, 0)") (("1" (inst + "emptyset[T]" "x!1" "emptyset[T]") (("1" (apply-extensionality 1 :hide? t) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (typepred "S!1") (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (expand "sigma_algebra?") (("1" (expand "subset_algebra_empty?") (("1" (expand "member") (("1" (flatten) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "negligible_subset[T, S!1, m!1]" ("X" "x!1" "E" "a!1")) (("1" (assert) nil nil) ("2" (replace -2) (("2" (hide -2 2 -3 -4 -6 -5) (("2" (lemma "negligible_union[T, S!1, m!1]" ("E1" "Y!1" "E2" "N1!1")) (("1" (lemma "negligible_subset[T, S!1, m!1]" ("X" "difference(union(Y!1, N1!1), N2!1)" "E" "union(Y!1,N1!1)")) (("1" (assert) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (typepred "Y!1") (("2" (expand "negligible_set?") (("2" (inst + "Y!1") (("2" (expand "null_set?") (("2" (expand "measurable_set?") (("2" (expand "mu") (("2" (expand "mu_fin?") (("2" (replace -2) (("2" (assert) (("2" (expand "subset?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (typepred "S!1") (("4" (expand "sigma_algebra?") (("4" (expand "subset_algebra_empty?") (("4" (expand "member") (("4" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "m_completions" ("S" "S!1" "m" "m!1" "X" "a!1" "A" "choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): a!1 = difference[T](union[T](Y, N1), N2)})" "B" "Y!1")) (("1" (assert) (("1" (expand "is_completion") (("1" (split -1) (("1" (expand "x_eq") (("1" (replace -6 -1) (("1" (flatten) (("1" (assert) (("1" (hide-all-but (-1 -2 1)) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (lemma "choose_member[(S!1)]" ("a" "{Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): a!1 = difference[T](union[T](Y, N1), N2)}")) (("2" (split -1) (("1" (name-replace "YY" "choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): a!1 = difference[T](union[T](Y, N1), N2)})") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but (-1 -2)) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "Y!1") (("2" (inst + "N1!1" "N2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst + "N1!1" "N2!1") nil nil)) nil)) nil)) nil) ("2" (inst -3 "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "measure?") (("2" (split) (("1" (expand "measure_empty?") (("1" (lemma "m_completions" ("S" "S!1" "m" "m!1" "X" "emptyset[T]" "A" "choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): emptyset[T] = difference[T](union[T](Y, N1), N2)})" "B" "emptyset[T]")) (("1" (case-replace "S!1(emptyset[T])") (("1" (case-replace "completion(S!1, m!1)(emptyset[T])") (("1" (split -3) (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (flatten) (("1" (replace -1) (("1" (expand "x_eq") (("1" (flatten) (("1" (replace -3) (("1" (name-replace "YY" "choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): emptyset[T] = difference[T](union[T](Y, N1), N2)})") (("1" (hide-all-but (-3 -4 1)) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide 2) (("3" (lemma "choose_completion" ("S" "S!1" "m" "m!1" "X" "emptyset[T]")) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (expand "is_completion") (("4" (assert) (("4" (inst + "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality 1 :hide? t) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (lemma "null_emptyset[T,S!1,m!1]") (("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (inst + "emptyset[T]" "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (flatten) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("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)) nil) ("2" (inst - "emptyset[T]") (("2" (hide 2 3) (("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (inst + "emptyset[T]" "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (typepred "S!1") (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (expand "sigma_algebra?") (("1" (expand "subset_algebra_empty?") (("1" (expand "member") (("1" (flatten) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (typepred "S!1") (("3" (expand "sigma_algebra?") (("3" (expand "subset_algebra_empty?") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (inst-cp - "IUnion(X!1)") (("2" (case "forall (n:nat): almost_measurable?(S!1,m!1)(X!1(n))") (("1" (case "forall (n:nat): completion(S!1, m!1)(X!1(n))") (("1" (lemma "choose_member[(S!1)]" ("a" "{Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): IUnion(X!1) = difference[T](union[T](Y, N1), N2)}")) (("1" (split -1) (("1" (name-replace "XXS" "choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): IUnion(X!1) = difference[T](union[T](Y, N1), N2)})") (("1" (expand "member") (("1" (skosimp) (("1" (expand "o ") (("1" (typepred "XXS") (("1" (hide -2) (("1" (name "F1" "lambda (n:nat): choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X!1(n) = difference[T](union[T](Y, N1), N2)})") (("1" (case-replace "(LAMBDA (x: nat): m!1(choose[(S!1)] ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X!1(x) = difference[T](union[T](Y, N1), N2)}))) = m!1 o F1") (("1" (hide -1 -2) (("1" (name "F12" "lambda (n:nat): choose({Z:[negligible[T, S!1, m!1],negligible[T, S!1, m!1]] | X!1(n) = di (("1" (name "NS1" "IUnion(lambda (n:nat): F12(n)`1)") (("1" (lemma "negligible_IUnion" ("ES" "LAMBDA (n: nat): F12(n)`1")) (("1" (lemma "negligible_IUnion" ("ES" "LAMBDA (n: nat): F12(n)`2")) (("1" (replace -3) (("1" (name-replace "NS2" "IUnion[nat, T](LAMBDA (n: nat): F12(n)`2)") (("1" (hide -3 -4) (("1" (case "forall (X:(S!1),N:null_set[T,S!1,m!1]): x_eq(m!1(difference(X,N)),m!1(X))") (("1" (expand "negligible_set?" (-2 -3)) (("1" (skolem -2 ("N!2")) (("1" (skolem -3 ("N!1")) (("1" (flatten) (("1" (lemma "measurable_union[T,S!1]" ("a" "N!1" "b" "N!2")) (("1" (name "G1" "lambda (n:nat): difference(F1(n),union[T](N!1, N!2))") (("1" (name "H1" "LAMBDA (n: nat): union(F1(n), union[T](N!1, N!2))") (("1" (case "forall (n:nat): subset?(G1(n),X!1(n)) & subset?(X!1(n),H1(n))") (("1" (case "disjoint?(G1)") (("1" (case "forall (n:nat): measurable_set?[T,S!1](G1(n))") (("1" (case "forall (n:nat): measurable_set?[T,S!1](F1(n))") (("1" (case "forall (n:nat): measurable_set?[T,S!1](H1(n))") (("1" (case "forall (n:nat): x_eq(m!1(G1(n)),m!1(F1(n)))") (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (flatten) (("1" (expand "measure_countably_additive?") (("1" (inst - "G1") (("1" (lemma "measurable_IUnion[T,S!1]" ("SS" "G1")) (("1" (expand "measurable_set?") (("1" (assert) (("1" (case "x_eq(x_sum(m!1 o G1), m!1(XXS))") (("1" (case "x_eq(x_sum(m!1 o F1),x_sum(m!1 o G1))") (("1" (hide-all-but (-1 -2 1)) (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -5 -7 -8)) (("2" (expand "x_sum") (("2" (expand "o ") (("2" (expand "x_eq") (("2" (case-replace "(FORALL (i:nat): m!1(F1(i))`1)") (("1" (case-replace "FORALL (i:nat): m!1(G1(i))`1") (("1" (case-replace "(LAMBDA (i:nat): m!1(F1(i))`2)=(LAMBDA (i:nat): m!1(G1(i))`2)") (("1" (assert) (("1" (apply-extensionality :hide? t) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (prop) (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "m_completions" ("S" "S!1" "m" "m!1" "X" "IUnion(X!1)" "A" "IUnion(G1)" "B" "XXS")) (("2" (replace -24) (("2" (replace -19) (("2" (replace -2) (("2" (split -1) (("1" (hide-all-but (-1 -4 1)) (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "is_completion") (("2" (inst + "difference(IUnion(X!1),IUnion(G1))" "emptyset[T]") (("1" (rewrite "difference_emptyset1" 1) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "difference") (("1" (expand "union") (("1" (expand "member") (("1" (hide-all-but (-9 1)) (("1" (case-replace "IUnion(X!1)(x!1)") (("1" (flatten) nil nil) ("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst + "i!1") (("2" (flatten) (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (case "FORALL (n: nat): x_eq(m!1(F1(n)), m!1(H1(n)))") (("1" (lemma "negligible_subset[T, S!1, m!1]" ("X" "difference[T](IUnion[nat, T](X!1), IUnion[nat, T](G1))" "E" "difference[T](IUnion[nat, T](H1), IUnion[nat, T](G1))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "subset?" 1) (("2" (skosimp) (("2" (expand "member") (("2" (expand "difference" (-1 1)) (("2" (expand "member") (("2" (flatten) (("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst -11 "i!1") (("2" (flatten) (("2" (expand "subset?" -12) (("2" (expand "member") (("2" (inst -12 "x!1") (("2" (inst 2 "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "negligible_subset[T,S!1,m!1]" ("X" "difference[T](IUnion[nat, T](H1), IUnion[nat, T](G1))" "E" "IUnion(lambda (n:nat): difference(H1(n),IUnion[nat, T](G1)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (hide-all-but (-10 1)) (("2" (expand "subset?" 1) (("2" (expand "difference") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "H1") (("2" (expand "IUnion") (("2" (skosimp) (("2" (expand "G1") (("2" (expand "difference" (1 2)) (("2" (expand "union" (1 -1)) (("2" (expand "member") (("2" (expand "union" 2) (("2" (expand "member") (("2" (split -1) (("1" (inst + "i!1") (("1" (assert) (("1" (inst + "i!1") (("1" (assert) (("1" (replace -2 -3) (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (inst 2 "0") nil nil)) nil) ("3" (replace -1) (("3" (inst 2 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "negligible_IUnion[T, S!1, m!1]" 1) (("2" (hide 2) (("2" (skosimp) (("2" (case-replace "difference[T](H1(n!1), IUnion[nat, T](G1))=union[T](N!1, N!2)") (("1" (expand "negligible_set?") (("1" (inst + "union[T](N!1, N!2)") (("1" (split) (("1" (rewrite "null_union[T,S!1,m!1]") nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "H1") (("2" (apply-extensionality 1 :hide? t) (("2" (expand "difference" 1) (("2" (expand "union" 1 1) (("2" (expand "member") (("2" (case-replace "union[T](N!1, N!2)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (expand "G1") (("1" (expand "difference") (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (flatten) (("2" (expand "IUnion") (("2" (expand "G1") (("2" (expand "difference") (("2" (expand "member") (("2" (inst + "n!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) ("2" (hide 2) (("2" (skosimp) (("2" (expand "H1" 1) (("2" (case "FORALL (X: (S!1), N: null_set[T, S!1, m!1]): x_eq(m!1(X), m!1(union(X, N)))") (("1" (inst - "F1(n!1)" "union[T](N!1, N!2)") (("1" (rewrite "null_union[T,S!1,m!1]") nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "m_monotone[T,S!1,m!1]" ("a" "X!2" "b" "union(X!2, N!3)")) (("1" (split) (("1" (lemma "m_disjoint_union[T,S!1,m!1]" ("a" "X!2" "b" "difference(N!3,X!2)")) (("1" (rewrite "difference_disjoint") (("1" (case-replace "union(X!2, difference(N!3, X!2))=union(X!2, N!3)") (("1" (hide -1) (("1" (lemma "m_monotone[T,S!1,m!1]" ("a" "difference(N!3, X!2)" "b" "N!3")) (("1" (split -1) (("1" (case-replace "m!1(N!3)=(TRUE,0)") (("1" (hide -1) (("1" (expand "x_le") (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (expand "x_add") (("1" (case-replace "m!1(X!2)`1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!3") (("2" (expand "null_set?") (("2" (expand "mu_fin?") (("2" (expand "mu") (("2" (flatten) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (typepred "N!3") (("2" (expand "null_set?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "measurable_difference[T,S!1]") (("2" (typepred "N!3") (("2" (expand "null_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (rewrite "measurable_union[T,S!1]") (("1" (expand "measurable_set?") (("1" (typepred "N!3") (("1" (expand "null_set?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "N!3") (("3" (expand "null_set?") (("3" (flatten) (("3" (lemma "measurable_union[T,S!1]" ("a" "X!2" "b" "N!3")) (("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) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "is_completion") (("3" (inst + "N1!1" "N2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (assert) (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -2 "n!1") (("2" (inst -3 "n!1") (("2" (inst -9 "F1(n!1)" "union[T](N!1, N!2)") (("1" (expand "G1") (("1" (propax) nil nil)) nil) ("2" (rewrite "null_union[T,S!1,m!1]" 1) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (expand "H1") (("2" (expand "null_set?") (("2" (flatten) (("2" (rewrite "measurable_union[T,S!1]" 1) (("2" (expand "F1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "F1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "G1") (("2" (expand "null_set?") (("2" (flatten) (("2" (rewrite "measurable_difference[T,S!1]" 1) (("2" (expand "F1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-14 1 -7 -9)) (("2" (expand "disjoint?") (("2" (skosimp) (("2" (inst - "i!1" "j!1") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (expand "intersection") (("2" (expand "member") (("2" (skosimp) (("2" (expand "G1") (("2" (expand "union") (("2" (expand "difference") (("2" (expand "member") (("2" (flatten) (("2" (hide 4 5) (("2" (case "forall (i:nat): X!1(i) = difference(union(F1(i),F12(i)`1),F12(i)`2)") (("1" (inst-cp - "i!1") (("1" (inst - "j!1") (("1" (inst - "x!1") (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (expand "union") (("1" (expand "difference") (("1" (expand "member") (("1" (replace -1) (("1" (replace -2) (("1" (expand "subset?") (("1" (expand "NS2") (("1" (expand "IUnion") (("1" (expand "member") (("1" (expand "NS1") (("1" (expand "IUnion") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) (("1" (inst-cp + "j!1") (("1" (assert) (("1" (inst + "i!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) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -6 -7 -8 -11 1 -15)) (("2" (skosimp) (("2" (expand "G1") (("2" (expand "H1") (("2" (expand "NS2") (("2" (expand "NS1") (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "IUnion") (("2" (split) (("1" (skosimp) (("1" (expand "union" -1) (("1" (expand "difference" -1) (("1" (expand "member") (("1" (flatten) (("1" (expand "F12") (("1" (inst - "x!1") (("1" (assert) (("1" (inst + "n!1") (("1" (inst - "x!1") (("1" (assert) (("1" (inst + "n!1") (("1" (lemma "choose_member[[negligible[T, S!1, m!1], negligible[T, S!1, m!1]]]" ("a" "{Z: [negligible[T, S!1, m!1], negligible[T, S!1, m!1]] | X!1(n!1) = difference[T](union[T](F1(n!1), Z`1), Z`2)}")) (("1" (case "nonempty?[[negligible[T, S!1, m!1], negligible[T, S!1, m!1]]] ({Z: [negligible[T, S!1, m!1], negligible[T, S!1, m!1]] | X!1(n!1) = difference[T](union[T](F1(n!1), Z`1), Z`2)})") (("1" (split -2) (("1" (name-replace "CN" "choose({Z: [negligible[T, S!1, m!1], negligible[T, S!1, m!1]] | X!1(n!1) = difference[T](union[T](F1(n!1), Z`1), Z`2)})") (("1" (expand "member") (("1" (replace -1 3) (("1" (expand "union") (("1" (expand "difference") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil) ("2" (hide -1 5 6) (("2" (inst -5 "X!1(n!1)") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (skosimp) (("2" (hide-all-but (-1 -3 -4 -5)) (("2" (inst - "F12(n!1)") (("2" (apply-extensionality :hide? t) 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" (expand "union" 1) (("2" (expand "member") (("2" (flatten) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (assert) (("2" (expand "F12") (("2" (inst + "n!1") (("2" (inst + "n!1") (("2" (case "nonempty?({Z: [negligible[T, S!1, m!1], negligible[T, S!1, m!1]] | X!1(n!1) = difference[T](union[T](F1(n!1), Z`1), Z`2)})") (("1" (lemma "choose_member[[negligible[T, S!1, m!1], negligible[T, S!1, m!1]]]" ("a" "{Z: [negligible[T, S!1, m!1], negligible[T, S!1, m!1]] | X!1(n!1) = difference[T](union[T](F1(n!1), Z`1), Z`2)}")) (("1" (split -1) (("1" (name-replace "CN" "choose({Z: [negligible[T, S!1, m!1], negligible[T, S!1, m!1]] | X!1(n!1) = difference[T](union[T](F1(n!1), Z`1), Z`2)})") (("1" (expand "member") (("1" (replace -1 -3) (("1" (expand "union" -3) (("1" (expand "difference" -3) (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 5 6) (("2" (inst -5 "X!1(n!1)") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (inst - "F12(n!1)") (("2" (apply-extensionality 1 :hide? t) 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" (expand "null_set?") (("2" (flatten) nil nil)) nil) ("3" (expand "null_set?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (typepred "X!2") (("2" (typepred "N!1") (("2" (lemma "m_monotone[T,S!1,m!1]" ("a" "difference(X!2, N!1)" "b" "X!2")) (("1" (split -1) (("1" (lemma "m_union[T,S!1,m!1]" ("a" "difference(X!2, N!1)" "b" "N!1")) (("1" (case "subset?(X!2,union(difference(X!2, N!1), N!1))") (("1" (lemma "m_monotone[T,S!1,m!1]" ("a" "X!2" "b" "union(difference(X!2, N!1), N!1)")) (("1" (assert) (("1" (name-replace "ML" "m!1(difference(X!2, N!1))") (("1" (case-replace "m!1(N!1)=(TRUE,0)") (("1" (name-replace "MR" "m!1(X!2)") (("1" (name-replace "MM" "m!1(union(difference(X!2, N!1), N!1))") (("1" (hide-all-but (-2 -4 -5 1)) (("1" (expand "x_le") (("1" (expand "x_eq") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (expand "null_set?") (("2" (flatten) (("2" (expand "mu_fin?") (("2" (expand "mu") (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "measurable_union[T,S!1]") nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (expand "null_set?") (("2" (flatten) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "null_set?") (("3" (flatten) (("3" (rewrite "measurable_difference[T, S!1]") (("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lemma "measurable_difference[T, S!1]" ("a" "X!2" "b" "N!1")) (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (expand "measurable_set?") (("2" (typepred "N!1") (("2" (expand "null_set?") (("2" (expand "measurable_set?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -8 -1 -2 -6) (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -5 "X!1(n!1)") (("2" (skosimp) (("2" (skosimp) (("2" (lemma "choose_completion" ("S" "S!1" "m" "m!1" "X" "X!1(n!1)")) (("2" (case-replace "completion(S!1, m!1)(X!1(n!1))") (("1" (expand "is_completion") (("1" (skosimp) (("1" (inst - "(N1!3,N2!3)") (("1" (expand "F1") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (inst + "x!1" "N1!2" "N2!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "F1") (("2" (expand "o") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -7 "X!1(n!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "n!1") (("2" (expand "completion") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (typepred "X!1(n!1)") (("2" (expand "completion") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "completion") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "almost_measurable?") (("2" (skosimp) (("2" (inst - "Y!1") (("2" (inst + "N1!1" "N2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (completion const-decl "sigma_algebra[T]" 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) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def 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) (choose const-decl "(p)" sets nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (choose_member formula-decl nil sets_lemmas nil) (empty? const-decl "bool" sets nil) (is_completion const-decl "bool" measure_completion_aux nil) (m_completions formula-decl nil measure_completion_aux 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) (emptyset const-decl "set" sets nil) (m!1 skolem-const-decl "measure_type[T, S!1]" measure_completion_aux nil) (x!1 skolem-const-decl "set[T]" measure_completion_aux nil) (member const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (measurable_set? const-decl "bool" measure_space_def nil) (mu const-decl "nnreal" measure_props nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (mu_fin? const-decl "bool" measure_props nil) (null_set? const-decl "bool" measure_theory nil) (subset? const-decl "bool" sets nil) (negligible_union judgement-tcc nil measure_theory nil) (negligible_subset formula-decl nil measure_theory nil) (TRUE const-decl "bool" booleans nil) (almost_measurable? const-decl "bool" measure_completion_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (measure_complete? const-decl "bool" generalized_measure_def nil) (measure_countably_additive? 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) (IUnion const-decl "set[T]" indexed_sets nil) (X!1 skolem-const-decl "disjoint_indexed_measurable[T, completion(S!1, m!1)]" measure_completion_aux nil) (O const-decl "T3" function_props nil) (negligible_IUnion judgement-tcc nil measure_theory nil) (sequence type-eq-decl nil sequences nil) (m_union formula-decl nil measure_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (measurable_union judgement-tcc nil measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (F12 skolem-const-decl "[n: nat -> ({Z: [negligible[T, S!1, m!1], negligible[T, S!1, m!1]] | X!1(n) = difference[T](union[T](F1(n), Z`1), Z`2)})]" measure_completion_aux nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (F1 skolem-const-decl "[n: nat -> ({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X!1(n) = difference[T](union[T](Y, N1), N2)})]" measure_completion_aux nil) (measurable_IUnion judgement-tcc nil measure_space_def nil) (difference_emptyset1 formula-decl nil sets_lemmas nil) (m_monotone formula-decl nil measure_props nil) (m_disjoint_union formula-decl nil measure_props nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (difference_disjoint formula-decl nil sets_lemmas nil) (measurable_difference judgement-tcc nil measure_space_def nil) (N!1 skolem-const-decl "set[T]" measure_completion_aux nil) (N!2 skolem-const-decl "set[T]" measure_completion_aux nil) (H1 skolem-const-decl "[nat -> set[T]]" measure_completion_aux nil) (null_union judgement-tcc nil measure_theory nil) (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (G1 skolem-const-decl "[nat -> set[T]]" measure_completion_aux nil) (disjoint? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (NS2 skolem-const-decl "negligible[T, S!1, m!1]" measure_completion_aux nil) (NS1 skolem-const-decl "negligible[T, S!1, m!1]" measure_completion_aux nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (null_set nonempty-type-eq-decl nil measure_theory nil) (negligible_IUnion application-judgement "negligible" measure_theory nil) (choose_completion formula-decl nil measure_completion_aux 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/") (null_emptyset judgement-tcc nil measure_theory nil) (complete_measure? const-decl "bool" generalized_measure_def nil)) nil)) (completion_measurable_TCC1 0 (completion_measurable_TCC1-1 nil 3423805251 ("" (skosimp) (("" (typepred "X!1") (("" (expand "completion") (("" (expand "almost_measurable?") (("" (inst + "X!1" "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (typepred "S!1") (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (expand "sigma_algebra?") (("1" (expand "subset_algebra_empty?") (("1" (expand "member") (("1" (flatten) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_completion_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (almost_measurable? const-decl "bool" measure_completion_aux nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (mu const-decl "nnreal" measure_props nil) (mu_fin? const-decl "bool" measure_props nil) (null_set? const-decl "bool" measure_theory nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (difference const-decl "set" sets nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (set type-eq-decl nil sets nil) (S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux 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) (m!1 skolem-const-decl "measure_type[T, S!1]" measure_completion_aux nil) (negligible_set? const-decl "bool" measure_theory nil) (emptyset const-decl "set" sets 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/") (completion const-decl "sigma_algebra[T]" measure_completion_aux nil)) nil)) (completion_measurable 0 (completion_measurable-1 nil 3423854412 ("" (skosimp) (("" (expand "completion") (("" (lemma "m_completions" ("S" "S!1" "m" "m!1" "X" "X!1" "B" "X!1" "A" "choose({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): X!1 = difference(union(Y, N1), N2)})")) (("1" (case-replace "completion(S!1, m!1)(X!1)") (("1" (case-replace "is_completion(S!1, m!1)(X!1, X!1)") (("1" (assert) (("1" (hide 2) (("1" (lemma "choose_completion" ("S" "S!1" "m" "m!1" "X" "X!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (expand "is_completion") (("2" (assert) (("2" (inst + "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (inst + "X!1" "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "X!1") (("2" (typepred "X!1") (("2" (inst + "emptyset[T]" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((completion const-decl "complete_measure[T, completion(S, m)]" measure_completion_aux nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (completion const-decl "sigma_algebra[T]" measure_completion_aux nil) (null_emptyset judgement-tcc nil measure_theory nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (emptyset const-decl "set" sets nil) (m!1 skolem-const-decl "measure_type[T, S!1]" measure_completion_aux nil) (S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux 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/") (choose_completion formula-decl nil measure_completion_aux nil) (is_completion const-decl "bool" measure_completion_aux nil) (almost_measurable? const-decl "bool" measure_completion_aux nil) (m_completions formula-decl nil measure_completion_aux 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) (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) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (negligible_set? const-decl "bool" measure_theory nil) (negligible nonempty-type-eq-decl nil measure_theory nil) (= const-decl "[T, T -> boolean]" equalities nil) (difference const-decl "set" sets nil) (union const-decl "set" sets nil)) shostak)) (completion_negligible_TCC1 0 (completion_negligible_TCC1-1 nil 3423805251 ("" (skosimp) (("" (expand "completion") (("" (expand "almost_measurable?") (("" (typepred "S!1") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (expand "member") (("" (flatten) (("" (inst + "emptyset[T]" "N!1" "emptyset[T]") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (expand "null_set?") (("1" (expand "measurable_set?") (("1" (expand "mu_fin?") (("1" (expand "mu") (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (flatten) (("1" (replace -1) (("1" (assert) 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) ((completion const-decl "sigma_algebra[T]" measure_completion_aux 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_completion_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (mu const-decl "nnreal" measure_props nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (mu_fin? const-decl "bool" measure_props nil) (null_set? const-decl "bool" measure_theory nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (union const-decl "set" sets nil) (difference const-decl "set" sets nil) (negligible nonempty-type-eq-decl nil measure_theory 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) (m!1 skolem-const-decl "measure_type[T, S!1]" measure_completion_aux nil) (negligible_set? const-decl "bool" measure_theory nil) (emptyset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux nil) (member const-decl "bool" sets 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) (almost_measurable? const-decl "bool" measure_completion_aux nil)) nil)) (completion_negligible 0 (completion_negligible-1 nil 3423812753 ("" (skosimp) (("" (expand "completion") (("" (typepred "N!1") (("" (expand "negligible_set?") (("" (skosimp) (("" (lemma "m_completions" ("S" "S!1" "m" "m!1" "X" "N!1" "A" "choose({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): N!1 = difference(union(Y, N1), N2)})" "B" "emptyset[T]")) (("1" (split -1) (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (name-replace "MM" "m!1(choose({Y: (S!1) | EXISTS (N1, N2: negligible[T, S!1, m!1]): N!1 = difference(union(Y, N1), N2)}))") (("1" (typepred "m!1") (("1" (expand "measure?") (("1" (expand "measure_empty?") (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-3 -4 1)) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (inst + "emptyset[T]" "N!1" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("3" (typepred "S!1") (("3" (expand "sigma_algebra?") (("3" (expand "subset_algebra_empty?") (("3" (expand "member") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (typepred "S!1") (("4" (expand "sigma_algebra?") (("4" (expand "subset_algebra_empty?") (("4" (expand "member") (("4" (flatten) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (lemma "choose_completion" ("S" "S!1" "m" "m!1" "X" "N!1")) (("5" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "completion") (("2" (expand "almost_measurable?") (("2" (inst + "emptyset[T]" "N!1" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("3" (typepred "S!1") (("3" (expand "sigma_algebra?") (("3" (expand "subset_algebra_empty?") (("3" (expand "member") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (expand "is_completion") (("6" (typepred "S!1") (("6" (expand "sigma_algebra?") (("6" (expand "subset_algebra_empty?") (("6" (expand "member") (("6" (flatten) (("6" (assert) (("6" (inst + "N!1" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "emptyset[T]") (("1" (hide 2) (("1" (inst + "N!1" "emptyset[T]") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (expand "negligible_set?") (("2" (inst + "emptyset[T]") (("2" (split) (("1" (rewrite "null_emptyset[T,S!1,m!1]") nil nil) ("2" (grind) nil nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((completion const-decl "complete_measure[T, completion(S, m)]" measure_completion_aux nil) (emptyset const-decl "set" sets nil) (union const-decl "set" sets nil) (difference const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (m_completions formula-decl nil measure_completion_aux nil) (is_completion const-decl "bool" measure_completion_aux nil) (choose_completion formula-decl nil measure_completion_aux nil) (almost_measurable? const-decl "bool" measure_completion_aux nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (null_emptyset judgement-tcc nil measure_theory nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (m!1 skolem-const-decl "measure_type[T, S!1]" measure_completion_aux nil) (S!1 skolem-const-decl "sigma_algebra[T]" measure_completion_aux nil) (completion const-decl "sigma_algebra[T]" measure_completion_aux nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas 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) (measure_empty? const-decl "bool" generalized_measure_def nil) (TRUE const-decl "bool" booleans nil) (empty? const-decl "bool" sets 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) (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) (negligible nonempty-type-eq-decl nil measure_theory nil)) shostak)))
¤ Dauer der Verarbeitung: 0.665 Sekunden (vorverarbeitet am 2026-04-25) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26