(monotone_classesnil 3453992461"" (skosimp)"" (skolem + "a!1" )"" (typepred "a!1" )"" (lemma "generated_sigma_algebra_subset1" ("X" "C" ))"" (expand "subset?" )"" (inst - "a!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil sets nil )nil defined_types nil )nil nil )"(S)" nil )"(S)" nil )"bool" sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil monotone_classes nil )set type-eq-decl nil sets nil )"bool" sets nil )"(nonempty?[set[T]])" monotone_classes nil ))nil ))nil 3454001130"" (skosimp)"" (name "S" "generated_sigma_algebra(C)" )"" (name "TT" "{E:(S) | mu!1(E)=nu!1(E)}" )"1" (case "forall (x:set[T]): S(x) => TT(x)" )"1" (skosimp)"1" (typepred "x!1" )"1" (inst - "x!1" )"1" (expand "S" )"1" (expand "TT" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" case "generated_sigma_algebra(generated_subset_algebra(C))=S" )"1" "monotone_class[T]" "B" "generated_subset_algebra[T](C)" "C" "{x:set[T] | S(x) & mu!1(x) = nu!1(x)}" ))"1" (replace -2 -1)"1" (split)"1" (expand "subset?" )"1" (inst - "x!1" )"1" (expand "member" )"1" (assert )"1" expand "TT" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 2)"2" (expand "subset?" )"2" (skosimp)"2" (expand "member" )"2" "disjoint_algebra_construction" "NX" "C" ))"2" replace -7)"2" expand "member" )"2" "generated_sigma_algebra_subset1[T]" "X" "generated_subset_algebra(C)" ))"2" expand "subset?" -1)"2" "x!2" )"2" expand "member" )"2" assert )"2" replace -2 -3)"2" "2" expand "finite_disjoint_unions" )"2" expand "fullset" )"2" expand "extend" )"2" "2" expand "finite_disjoint_union?" )"2" "2" expand "member" )"2" "mu!1" )"2" "nu!1" )"2" expand "finite_measure?" )"2" "2" case "disjoint_indexed_measurable?[T, (generated_sigma_algebra(C))](E!1)" )"1" "E!1" )"1" "E!1" )"1" replace "1" "1" "zero_tail_series_limit" "n" "n!1" "a" "nu!1 o E!1" ))"1" "1" "zero_tail_series_limit" "n" "n!1" "a" "mu!1 o E!1" ))"1" "1" rewrite "convergence_sequences.limit_def" "1" rewrite "convergence_sequences.limit_def" "1" replace "1" replace "1" replace "1" replace "1" "1" expand "o " )"1" expand "series" )"1" "sigma_eq" "low" "0" "high" "n!1" "F" "LAMBDA (x: nat): mu!1(E!1(x))" "G" "LAMBDA (x: nat): nu!1(E!1(x))" ))"1" assert )"1" "1" "1" "n!2" )"1" "1" assert )"1" "n!2" )"1" expand "<=" "1" "1" assert )"1" "E!1(n!2)" )nil nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" "m!1" )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" "m!1" )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil )"3" "3" "n!2" )"3" "n!2" )"3" "3" "n!2)"1" "generated_sigma_algebra_subset1[T]" "X" "C" ))"1" expand "subset?" )"1" "E!1(n!2)" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )"2" "generated_sigma_algebra[T](C)" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -3)"2" (expand "monotone?" )"2" (skosimp)"2" (expand "member" )"2" "sigma_algebra_IUnion[T,S]" "SS" "E!1" ))"1" "sigma_algebra_IIntersection[T,S]" "SS" "E!1" ))"1" expand "member" )"1" replace -1)"1" replace -2)"1" "1" "1" "m_increasing_convergence[T,S,to_measure(mu!1)]" "E" "E!1" ))"1" assert )"1" "m_increasing_convergence[T,S,to_measure(nu!1)]" "E" "E!1" ))"1" assert )"1" expand "to_measure" )"1" "MU" "mu!1(IUnion(E!1))" )"1" "NU" "nu!1(IUnion(E!1))" )"1" expand "o " )"1" expand "x_converges?" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))" )"1" "convergence_sequences.limit_lemma" "v" "LAMBDA (i: nat): nu!1(E!1(i))" ))"1" "convergence_sequences.limit_lemma" "v" "LAMBDA (i: nat): mu!1(E!1(i))" ))"1" replace "1" replace "1" "cnv_seq_diff" "s1" "LAMBDA (i: nat): mu!1(E!1(i))" "l1" "MU" "s2" "LAMBDA (i: nat): nu!1(E!1(i))" "l2" "NU" ))"1" assert )"1" "cnv_seq_const" "a" "0" ))"1" expand "const_fun" )"1" expand "-" "1" "(LAMBDA (x: nat): mu!1(E!1(x)) - nu!1(E!1(x)))=(LAMBDA (x: nat): 0)" )"1" "convergence_sequences.unique_limit" "u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "MU-NU" ))"1" assert )nil nil ))nil )"2" "1" "x!2" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil )"3" "3" assert )"3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )"1" replace -8)"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "to_measure[T, (generated_sigma_algebra(C))](nu!1)" )"2" expand "measure?" )"2" expand "to_measure" )"2" expand "measure_empty?" )"2" "2" assert )"2" expand "measure_countably_additive?" )"2" "2" "X!1" )"2" expand "o " )"2" "X!1" )"2" "2" "1" "1" assert )nil nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1" )"2" expand "measurable_set?" )"2" "n!1" )"2" nil nil ))nil ))nil ))nil )"3" "1" "1" replace -7)"1" assert )nil nil ))nil ))nil )"2" "to_measure[T, (generated_sigma_algebra(C))](mu!1)" )"2" "2" expand "measure?" )"2" "2" expand "measure_empty?" )"2" expand "to_measure" )"2" assert )"2" "2" expand "measure_countably_additive?" )"2" "2" "X!1" )"1" expand "o " )"1" nil nil ))nil )quality 100%
¤ Dauer der Verarbeitung: 0.47 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
