Quelle product_sigma.prf
Sprache: Lisp
(product_sigmanil 3459218355"" (skosimp)"" (expand "sigma_times" )"" "generated_sigma_algebra_subset1" "X" "extend ")) "" (expand "subset?" )"" (expand "member" )"" (inst - "cross_product(X!1, Y!1)" )"" (assert )"" (hide 2)"" (expand "fullset" )"" (expand "extend" )"" (prop)"" (expand "measurable_rectangle?" )"" (inst + "X!1" "Y!1" )"" (assert )"" "" expand "cross_product" )"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"bool" sets nil )"set[[T1, T2]]" cross_product"topology/" )"bool" sets nil )nil nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )set type-eq-decl nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"bool" product_sigma_def nil )"sigma_algebra[T1]" product_sigma nil )"sigma_algebra[T2]" product_sigma nil )nil product_sigma_defnil )"bool" booleans nil )"R" extend nil )"set" sets nil )nil product_sigma nil )nil product_sigma nil ))nil 3450413455"" case "FORALL (a, b: (measurable_rectangle?[T1, T2](S1, S2))): ") "1" "disjoint_algebra_construction[[T1,T2]]" "NX" "measurable_rectangle?[T1, T2](S1, S2)" ))"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (expand "member" ) (("2" (propax) nil nil )) nil )) nil )"3" (hide -1 2)"3" (skosimp)"3" (typepred "a!1" )"3" (expand "finite_disjoint_union?" )"3" (expand "member" )"3" (expand "measurable_rectangle?" )"3" (skosimp)"3" "lambda (i:nat): if i=0 then cross_product(X!1,complement(Y!1)) elsif i=1 then cross_product(complement(X!1),complement(Y!1)) elsif i=2 then cross_product(complement(X!1),Y!1) else emptyset endif" "3" )"3" (split)"1" (expand "disjoint?" )"1" (expand "cross_product" )"1" expand "complement" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "1" "1" expand "emptyset" )"1" "i!1=0" )"1" "1" assert )nil nil ))nil )"2" "i!1=1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" "i!1=2" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (hide -1)"2" "2" expand "complement" )"2" expand "cross_product" )"2" expand "member" )"2" expand "emptyset" )"2" expand "IUnion" )"2" "X!1(x!1)" )"1" "Y!1(x!2)" )"1" (assert ) nil nil )"2" assert )"2" "0" )nil nil ))nil ))nil )"2" "Y!1(x!2)" )"1" assert )"1" "2" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (hide -1)"3" case "i!1=0" )"1" assert )"1" "S2" )"1" expand "sigma_algebra?" )"1" expand "subset_algebra_complement?" )"1" "1" "Y!1" )"1" expand "member" )"1" "X!1" "complement(Y!1)" )"1" assert )"1" "1" expand "cross_product" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1=1" )"1" assert )"1" "S2" )"1" "S1" )"1" expand "sigma_algebra?" )"1" expand "subset_algebra_complement?" )"1" "1" expand "member" )"1" "X!1" )"1" "Y!1" )"1" "complement(X!1)" "complement(Y!1)" )"1" assert )"1" "1" "1" expand "cross_product" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1=2" )"1" assert )"1" "S1" )"1" expand "sigma_algebra?" )"1" expand "subset_algebra_complement?" )"1" "1" expand "member" )"1" "X!1" )"1" "complement(X!1)" "Y!1" )"1" assert )"1" expand "cross_product" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )"2" (hide-all-but 1)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "emptyset" )"2" (expand "measurable_rectangle?" )"2" (inst + "emptyset" "emptyset" )"2" (typepred "S2" )"2" (typepred "S1" )"2" (expand "sigma_algebra?" )"2" (flatten)"2" (expand "subset_algebra_empty?" )"2" expand "member" )"2" assert )"2" "2" expand "emptyset" )"2" expand "cross_product" )"2" (propax) 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" (typepred "b!1" )"2" (typepred "a!1" )"2" (expand "measurable_rectangle?" )"2" (skosimp*)"2" "intersection(X!1,X!2)" "intersection(Y!1,Y!2)" )"2" "sigma_algebra_intersection[T1,S1]" "x" "X!1" "y" "X!2" ))"1" "sigma_algebra_intersection[T2,S2]" "x" "Y!1" "y" "Y!2" ))"1" (expand "member" )"1" (assert )"1" (replace -3)"1" (replace -6)"1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_algebra nil )"bool" sets nil )nil subset_algebra_defnil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil )"bool" indexed_sets_aux "sets_aux/" )"set[T]" indexed_sets nil )"(S)" nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )nil sets_lemmas nil )"(strict_total_order?[real])" real_props nil )"bool" subset_algebra_defnil )"set" sets nil )"set" sets nil )"set[[T1, T2]]" cross_product"topology/" )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" subset_algebra_def nil )"bool" sets nil )"(S)" nil )"bool" subset_algebra_def nil )nil product_sigma nil )nil product_sigma nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"bool" product_sigma_def nil )"sigma_algebra[T1]" product_sigma nil )"sigma_algebra[T2]" product_sigma nil )"set" sets nil ))nil 3450331052"" (lemma "rectangle_algebra_aux" )"" "generated_subset_algebra[[T1, T2]](measurable_rectangle?(S1, S2))" )"" (assert ) nil nil )) nil ))nil )"sigma_algebra[T2]" product_sigma nil )"sigma_algebra[T1]" product_sigma nil )"bool" product_sigma_def nil )set type-eq-decl nil sets nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )"subset_algebra" nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil product_sigma nil )nil product_sigma nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil product_sigma nil ))nil ))nil 3450414364"" (lemma "rectangle_algebra_aux" )"" (expand "rectangle_algebra" ) (("" (assert ) nil nil )) nil ))nil )"subset_algebra[[T1, T2]]" nil )nil product_sigma nil ))nil 3455513659"" (skosimp)"" (split)"1" (flatten)"1" (expand "finite_disjoint_unions" )"1" (expand "fullset" )"1" (expand "extend" )"1" (prop)"1" (expand "finite_disjoint_union?" )"1" (skosimp)"1" (expand "member" )"1" case "forall (i:nat): measurable_rectangle?[T1, T2](S1, S2)(E!1(i))" )"1" "image[nat,(measurable_rectangle?(S1, S2))](E!1,{n | n < n!1})" )"1" (split)"1" (replace -3)"1" "1" "1" "IUnion(E!1)(x!1, x!2)" )"1" expand "IUnion" )"1" "1" expand "Union" )"1" "i!1" )"1" "i!1" )"1" "1" "i!1<n!1" )"1" "E!1(i!1)" )"1" assert )"1" expand "image" )"1" "i!1" )nil nil ))nil ))nil ))nil )"2" assert )"2" expand "empty?" )"2" "(x!1,x!2)" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" expand "Union" )"2" "2" "a!1" )"2" assert )"2" expand "image" )"2" "i!1" )"2" "i!1" )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) nil nil ))nil ))nil )"2" "finite_image[nat, (measurable_rectangle?(S1, S2))]" "f" "E!1" "S" "{n | n < n!1}" ))"1" (propax) nil nil )"2" "2" expand "is_finite" )"2" "n!1" "lambda (i:{n | n < n!1}): i" )"2" expand "injective?" )"2" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" "x!1" )"3" "y!1" )"3" expand "image" )"3" "i!1" )"3" "i!2" )"3" "i!1" )"3" "i!2" )"3" expand "disjoint?" -8)"3" replace -4)"3" replace -6)"3" "3" "i!1" "i!2" )"3" "i!1=i!2" )"3" assert )"3" expand "disjoint?" )"3" expand "intersection" )"3" expand "empty?" )"3" "3" "x!2" )"3" expand "member" )"3" "3" 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 )"2" (hide -1 -2 2)"2" (skosimp)"2" (inst - "i!1" )"2" "i!1<n!1" )"1" (flatten) nil nil )"2" assert )"2" rewrite "emptyset_is_empty?" )"2" replace -1)"2" expand "measurable_rectangle?" )"2" "emptyset" "emptyset" )"2" "1" "1" (grind) nil nil ))nil )"2" "S1" )"2" expand "sigma_algebra?" )"2" expand "subset_algebra_empty?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "S2" )"3" expand "sigma_algebra?" )"3" expand "subset_algebra_empty?" )"3" expand "member" )"3" 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 "finite_disjoint_unions" )"2" (expand "extend" )"2" (expand "fullset" )"2" (prop)"2" (expand "finite_disjoint_union?" )"2" case "forall (n:nat,R,Z): is_finite(R) & card(R) <= n & Union(LAMBDA (t: setof[[T1, T2]]): IF measurable_rectangle?(S1, S2)(t) THEN R(t)OR disjoint?(x, y)) => EXISTS (E: sequence[set [[T1, T2]]]), n:AND AND AND ") "1" (inst - "card(R!1)" "R!1" "Z!1" )"1" (assert )"1" (replace -4) (("1" (propax) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (induct "n" )"1" (skosimp)"1" (expand "<=" -2)"1" (split)"1" (assert ) nil nil )"2" "card_is_0" ("S" "R!2" ))"2" replace -2 -1)"2" replace -1)"2" "2" "Z!2=emptyset[[T1,T2]]" )"1" "1" "lambda (i:nat): emptyset[[T1,T2]]" "0" )"1" "1" (grind) nil nil )"2" "2" expand "emptyset" )"2" expand "IUnion" )"2" nil nil ))nil ))nil ))nil )"3" "3" assert )"3" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace -2 1 rl)"2" "2" expand "emptyset" )"2" expand "Union" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "<=" -3)"2" (split -3)"1" "R!2" "Z!2" )"1" assert )"1" replace -5)"1" (propax) nil nil ))nil ))nil ))nil )"2" "nonempty_card" ("S" "R!2" ))"2" "2" "2" "1" "card_rest" ("S" "R!2" ))"1" "1" expand "nonempty?" -1)"1" replace 1)"1" replace -3)"1" "1" "choose_rest" "a" "R!2" ))"1" replace 1)"1" "rest(R!2)" "Union(rest(R!2))" )"1" "1" "1" "extensionality_postulate" "f" "Union(extend " "g" "IUnion(E!1)" ))"1" "1" "1" "1" "1" case "Z!2 = union(choose(R!2), IUnion(E!1))" )"1" case "forall (i:nat): disjoint?(choose(R!2),E!1(i))" )"1" "lambda (i:nat): if i=0 then choose(R!2) else E!1(i-1) endif" "n!1+1" )"1" "1" expand "disjoint?" "1" "1" "i!1=0" )"1" assert )"1" "j!2-1" )nil nil ))nil )"2" replace "2" "j!2=0" )"1" "i!1-1" )"1" "1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" "i!1-1" "j!2-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" replace "1" "1" expand "union" )"1" expand "member" )"1" "choose(R!2)(x!1, x!2)" )"1" expand "IUnion" )"1" "0" )nil nil ))nil )"2" assert )"2" "IUnion(E!1)(x!1, x!2)" )"1" expand "IUnion" )"1" "1" "i!1+1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" "2" replace "2" "2" "i!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"3" "3" expand "member" )"3" "i!1=0" )"1" assert )nil nil )"2" assert )"2" "i!1-1" )"2" "2" assert )"2" "i!1 < 1 + n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" "2" expand "disjoint?" "2" expand "intersection" )"2" expand "empty?" "2" expand "member" )"2" "2" "x!1" )"2" "IUnion(E!1)(x!1)" )"1" expand "extend" )"1" expand "Union" )"1" "1" "a!1" )"1" assert )"1" "choose(R!2)" "a!1" )"1" "choose_not_member" "a" "R!2" ))"1" assert )"1" expand "member" )"1" "1" assert )nil nil )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "rest" )"2" expand "remove" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "IUnion" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" expand "union" )"2" expand "member" )"2" "choose(R!2)(x!1, x!2)" )"1" expand "Union" )"1" "choose(R!2)" )nil nil ))nil )"2" assert )"2" "(x!1,x!2)" )"2" "IUnion(E!1)(x!1, x!2)" )"1" expand "Union" )"1" "1" "a!1" )"1" expand "extend" )"1" "1" "a!1" )"1" assert )"1" expand "rest" )"1" expand "remove" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "extend" )"2" expand "Union" )"2" "2" "a!1" )"2" assert )"2" "a!1" )"2" expand "rest" )"2" expand "remove" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_rest" "A" "R!2" ))"2" nil nil ))nil )"3" assert )nil nil )"4" "4" expand "extend" )"4" nil nil ))nil ))nil )"5" "5" "x!1" )"5" "y!1" )"5" "x!1" "y!1" )"1" "1" nil nil )"2" nil nil ))nil )"2" expand "rest" )"2" expand "remove" )"2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil )"3" expand "rest" )"3" expand "remove" )"3" expand "member" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setofsets[T]" nil )"R" extend nil )"bool" subset_algebra_def nil )"bool" sets nil )"set" sets nil )"bool" subset_algebra_def nil )"set[[T1, T2]]" cross_product"topology/" )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )nil sets_lemmas nil )"sequence[set[[T1, T2]]]" product_sigma nil )"bool" reals nil )"set[R]" function_image nil )"bool" indexed_sets_aux "sets_aux/" )"set" sets nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )nil function_image_aux nil )"bool" finite_sets nil )nil finite_sets nil )"bool" functions nil )nil nat_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" product_sigma nil )"nat" product_sigma nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"[bool, bool -> bool]" booleans nil )"set[T]" indexed_sets nil )"bool" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil product_sigma nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )nil product_sigma nil )set type-eq-decl nil sets nil )"bool" product_sigma_def nil )"sigma_algebra[T1]" product_sigma nil )"sigma_algebra[T2]" product_sigma nil )nil sequences nil )"set" sets nil )"posint" nil )"int" integers nil )nil functions nil )"(extend " product_sigma nil) "(LAMBDA (t: setof[[T1, T2]]): IF measurable_rectangle?(S1, S2)(t) THEN R!2(t) ELSE FALSE ENDIF)" nil )"nat" product_sigma nil )"nat" product_sigma nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"set" sets nil )nil sets_lemmas nil )"(LAMBDA (t: setof[[T1, T2]]): IF measurable_rectangle?[T1, T2](S1, S2)(t) THEN rest(R!2)(t)" product_sigma nil) "set[(measurable_rectangle?(S1, S2))]" nil )"(p)" sets nil )"set" sets nil )nil finite_sets nil )"(rest(R!2))" product_sigma nil )"(rest(R!2))" product_sigma nil )"set" sets nil )nil sets_lemmas nil )"bool" sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )"finite_set[T]" "sets_aux/" )"countable_set[T]" "sets_aux/" )"boolean" notequal nil )"(S)" sigma_algebranil )nil finite_sets nil )nil naturalnumbers nil )nil defined_types nil )"set[(measurable_rectangle?(S1, S2))]" nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )OR const-decl "[bool, bool -> bool]" booleans nil ))nil 3455519645"" (skosimp)"" (typepred "r2!1" )"" (typepred "r1!1" )"" (expand "measurable_rectangle?" )"" (skosimp*)"" (expand "finite_disjoint_union?" )"" "lambda (i:nat): if i=0 then cross_product(intersection(X!1,X!2),intersection(Y!1,Y!2)) else emptyset endif" "1" )"" (split)"1" (grind) nil nil )"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil )"3" (skosimp)"3" (case-replace "i!1=0" )"1" (assert )"1" (expand "member" )"1" "intersection(X!1, X!2)" "intersection(Y!1, Y!2)" )"1" "sigma_algebra_intersection[T1,S1]" "x" "X!1" "y" "X!2" ))"1" expand "member" )"1" assert )"1" "sigma_algebra_intersection[T2,S2]" "x" "Y!1" "y" "Y!2" ))"1" expand "member" )"1" expand "cross_product" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "emptyset_is_empty?" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra[T2]" product_sigma nil )"sigma_algebra[T1]" product_sigma nil )"bool" product_sigma_def nil )set type-eq-decl nil sets nil )nil product_sigma nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil product_sigma nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(S)" nil )"bool" subset_algebra_def nil )"(total_order?[real])" nil )"bool" indexed_sets_aux "sets_aux/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"boolean" notequal nil )"set[T]" indexed_sets nil )nil sigma_algebra nil )"(strict_total_order?[real])" real_props nil )nil sets_lemmas nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"set" sets nil )"set" sets nil )"set[[T1, T2]]" cross_product"topology/" )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil ))nil 3455520014"" (skosimp)"" (typepred "r!1" )"" (expand "measurable_rectangle?" )"" (skosimp)"" (expand "finite_disjoint_union?" )"" "lambda (i:nat): if i=0 then cross_product(complement(X!1), Y!1) elsif i=1 then cross_product(X!1, complement(Y!1)) elsif i=2 then cross_product(complement(X!1),complement(Y!1)) else emptyset endif" "3" )"" (split)"1" (expand "disjoint?" )"1" (skosimp) (("1" (grind) nil nil )) nil )) nil )"2" (apply-extensionality :hide? t)"2" (replace -1)"2" (hide -1)"2" (expand "complement" )"2" (expand "member" )"2" (expand "cross_product" )"2" (case-replace "X!1(x!1)" )"1" "Y!1(x!2)" )"1" assert )"1" expand "IUnion" )"1" assert )"1" expand "emptyset" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" expand "emptyset" )"2" "1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "Y!1(x!2)" )"1" assert )"1" expand "IUnion" )"1" assert )"1" (inst + "0" ) nil nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" assert )"2" "2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "cross_product" )"3" (expand "complement" )"3" (expand "empty?" )"3" (expand "member" )"3" (skosimp)"3" (assert )"3" (case-replace "i!1=0" )"1" assert )"1" "complement(X!1)" "Y!1" )"1" assert )"1" "sigma_algebra_complement[T1,S1]" "x" "X!1" ))"1" expand "member" )"1" assert )"1" "1" expand "complement" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1=1" )"1" assert )"1" "X!1" "complement(Y!1)" )"1" "sigma_algebra_complement[T2,S2]" "x" "Y!1" ))"1" expand "member" )"1" assert )"1" "1" expand "complement" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1=2" )"1" assert )"1" "sigma_algebra_complement[T2,S2]" "x" "Y!1" ))"1" "sigma_algebra_complement[T1,S1]" "x" "X!1" ))"1" expand "member" )"1" "complement(X!1)" "complement(Y!1)" )"1" assert )"1" "1" expand "complement" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "emptyset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra[T2]" product_sigma nil )"sigma_algebra[T1]" product_sigma nil )"bool" product_sigma_def nil )set type-eq-decl nil sets nil )nil product_sigma nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil product_sigma nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"set[[T1, T2]]" cross_product"topology/" )"set" sets nil )"set" sets nil )nil sigma_algebra nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"set[T]" indexed_sets nil )"bool" indexed_sets_aux "sets_aux/" )"bool" sets nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" subset_algebra_def nil )"(S)" nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.99 Sekunden
(vorverarbeitet am 2026-04-25)
¤ *© Formatika GbR, Deutschland
2026-05-26
