Quelle subset_algebra_def.prf
Sprache: Lisp
(subset_algebra_defnil 3313473197"" (expand "subset_algebra_union?" )"" (expand "sigma_algebra_union?" )"" (skosimp*)"" (typepred "x!1" )"" (typepred "y!1" )"" (name "U" "union(singleton(x!1),singleton(y!1))" )"" (inst - "U" )"" "(FORALL (x: (extend[setof[T], (S!1), bool, FALSE](U))): ") "1" (split -5)"1" (expand "member" )"1" (expand "extend" )"1" (expand "Union" )"1" (expand "union" )"1" (assert )"1" "{x: T | LAMBDA (t: setof[T]):IF (S!1)(t) THEN U(t) ELSE FALSE ENDIF)):OR member(x, y!1)}") "1" "1" "1" expand "member" )"1" "x!1(x!2)" )"1" "x!1" )"1" expand "U" )"1" expand "singleton" )"1" expand "union" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "y!1(x!2)" )"1" "y!1" )"1" expand "U" )"1" expand "singleton" )"1" expand "union" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "a!1" )"2" assert )"2" expand "U" -1)"2" expand "singleton" )"2" expand "union" )"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 )"2" (hide 2)"2" (expand "extend" )"2" (expand "is_countable[set[T]]" )"2" "lambda (x:setof[T]): IF x = x!1 THEN 0 ELSE 1 ENDIF" )"2" (expand "injective?" )"2" "2" expand "restrict" )"2" "x1!1" )"2" "x2!1" )"2" assert )"2" expand "U" )"2" expand "singleton" )"2" expand "union" )"2" expand "member" )"2" "2" "1" "1" assert )nil nil )"2" assert )nil nil ))nil )"2" "1" assert )nil nil )"2" assert )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 "x!2" )"2" (expand "extend" )"2" (case-replace "S!1(x!2)" )"1" (expand "member" )"1" (propax) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )"(singleton?)" sets nil )"bool" sets nil )"set" sets nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"non_empty_finite_set[T]" countable_props "sets_aux/" )"bool" sets nil )"bool" countability "sets_aux/" )"R" restrict nil )"bool" functions 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 )"set" sets nil )"[bool, bool -> bool]" booleans nil )"(S!1)" subset_algebra_def nil )"setofsets[T]" subset_algebra_def nil )"non_empty_finite_set[(S!1)]" nil )"(S!1)" subset_algebra_def nil )IF const-decl "[boolean, T, T -> T]" if_def nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" booleans nil )"R" extend nil )"bool" subset_algebra_def nil ))nil 3313474506"" (skosimp*)"" (expand "sigma_algebra?" )"" (expand "subset_algebra?" )"" (flatten)"" (assert )"" (rewrite "sigma_union_implies_subset_union" ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def nil )nil nil )nil subset_algebra_def nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil ))nil 3426521314"" (expand "subset_algebra?" )"" (expand "emptyset" )"" (expand "fullset" )"" (expand "singleton" )"" (expand "union" )"" (expand "member" )"" (expand "subset_algebra_empty?" )"" (expand "subset_algebra_complement?" )"" (expand "complement" )"" (expand "subset_algebra_union?" )"" (expand "union" )"" (expand "member" )"" (expand "emptyset" )"" (split)"1" "1" "1" "1" "x!1" )"1" "1" replace -1)"1" (assert ) nil nil ))nil )"2" replace -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!1" )"2" "y!1" )"2" "1" replace -1)"1" assert )"1" "1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "1" (assert ) nil nil )"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 )"set" sets nil )"(singleton?)" sets nil )"bool" sets nil )"bool" subset_algebra_defnil )"bool" subset_algebra_def nil )nil booleans nil )nil subset_algebra_def nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" booleans nil )"bool" booleans nil )"set" sets nil )"bool" subset_algebra_def nil )"set" sets nil )"set" sets nil )"bool" subset_algebra_def nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil ))nil 3426521314"" (expand "trivial_subset_algebra" )"" (expand "emptyset" )"" (expand "fullset" )"" (expand "singleton" )"" (expand "union" )"" (expand "sigma_algebra?" )"" (expand "subset_algebra_empty?" )"" (expand "emptyset" )"" (expand "member" )"" (expand "subset_algebra_complement?" )"" (expand "complement" )"" (expand "sigma_algebra_union?" )"" (expand "Union" )"" (expand "member" )"" "1" "1" "1" "1" "x!1" )"1" "1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "a!1" )"2" "a!1" )"2" "1" (assert ) nil nil )"2" "a!1" )"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 )"set" sets nil )"(singleton?)" sets nil )"bool" subset_algebra_def nil )"bool" subset_algebra_defnil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )"bool" booleans nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil subset_algebra_def nil )nil booleans nil )"set" sets nil )"set" sets nil )"bool" sets nil )"bool" subset_algebra_def nil )"set" sets nil )"set" sets nil )"(subset_algebra?)" nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil ))nil 3426521314"" (skolem + ("A" ))"" (typepred "A" )"" (expand "subset_algebra?" )"" (expand "sigma_algebra?" )"" (flatten)"" (replace -1)"" (replace -2)"" (expand "subset_algebra_union?" )"" (expand "sigma_algebra_union?" )"" (skosimp)"" "add[set[T]](x!1,singleton[set[T]](y!1))" )"" "Union(add[set[T]](x!1, singleton[set[T]](y!1)))=union(x!1, y!1)" )"1" (split -4)"1" (propax) nil nil )"2" (rewrite "finite_countable[set[T]]" )nil nil )"3" (hide-all-but 1)"3" "3" "x!2" )"3" expand "singleton" )"3" expand "add" )"3" expand "member" )"3" "1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" expand "union" )"2" expand "singleton" )"2" expand "add" )"2" expand "member" )"2" expand "Union" )"2" "x!1(x!2)" )"1" (inst + "x!1" ) nil nil )"2" "y!1(x!2)" )"1" "y!1" )nil nil )"2" assert )"2" "2" "a!1" )"2" "1" assert )nil nil )"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 subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" subset_algebra_def nil )"set" sets nil ) (Union const-decl "set" sets nil )"[T, T -> boolean]" equalities nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )nil countable_props "sets_aux/" )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )OR const-decl "[bool, bool -> bool]" booleans nil )"(singleton?)" sets nil )"bool" sets nil )"(nonempty?)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )"bool" subset_algebra_def nil )"bool" subset_algebra_def nil ))nil ))nil 3426523512"" (expand "sigma_algebra?" )"" (split)"1" (expand "subset_algebra_empty?" ) (("1" (grind) nil nil ))nil )"2" (grind) nil nil ) ("3" (grind) nil nil ))nil ))nil )"set" sets nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"setofsets" sets nil )"(partial_order?[set[T]])" nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"bool" subset_algebra_def nil )"set" sets nil )"bool" subset_algebra_defnil )"bool" countability "sets_aux/" )"set" sets nil )"bool" subset_algebra_def nil )"bool" subset_algebra_def nil )"(nonempty?[set[T]])" nil ))nil 3426521314"" (skosimp)"" (expand "Intersection" )"" (expand "sigma_algebra?" )"" (split)"1" (expand "subset_algebra_empty?" )"1" (expand "member" )"1" (skosimp)"1" (typepred "a!1" )"1" (expand "sigma_algebra?" )"1" (flatten)"1" (expand "subset_algebra_empty?" )"1" (expand "member" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subset_algebra_complement?" )"2" (skosimp)"2" (expand "member" )"2" (skosimp)"2" (typepred "a!1" )"2" (expand "sigma_algebra?" )"2" (flatten)"2" (expand "subset_algebra_complement?" )"2" (expand "member" )"2" (typepred "x!1" )"2" "a!1" )"2" (inst - "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "sigma_algebra_union?" )"3" (skosimp)"3" (expand "member" )"3" (skosimp)"3" (typepred "a!1" )"3" (expand "sigma_algebra?" )"3" (flatten)"3" (expand "sigma_algebra_union?" )"3" (inst - "X!2" )"3" (assert )"3" expand "member" )"3" "3" "x!1" )"3" expand "subset?" )"3" "x!1" )"3" assert )"3" expand "member" )"3" "x!1" )"3" "a!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 )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"bool" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" subset_algebra_def nil )"setofsets[T]" subset_algebra_def nil )"({Y | sigma_algebra?(Y) AND subset?[setof[T]](X!1, Y)})" nil )"({x | AND subset?[setof[T]](X!1, Y)})):" subset_algebra_def nil) "bool" subset_algebra_defnil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(partial_order?[set[T]])" nil )"bool" subset_algebra_def nil )"bool" subset_algebra_def nil ))nil ))nil 3426523538"" (skosimp)"" (expand "generated_sigma_algebra" )"" (expand "subset?" )"" (expand "Intersection" )"" (expand "member" )"" (skosimp*)"" (typepred "a!1" )"" (inst - "x!1" )"" (expand "member" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra" nil )"set" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil subset_algebra_def nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil ) (member const-decl "bool" sets nil )"bool" sets nil ))nil 3426523636"" (skosimp)"" (expand "generated_sigma_algebra" )"" (expand "Intersection" )"" (expand "subset?" 1 1)"" (expand "member" )"" (skosimp)"" (inst - "Y!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra" nil )"bool" sets nil )"setofsets[T]" subset_algebra_def nil )"setofsets[T]" subset_algebra_def nil )set type-eq-decl nil sets nil )"bool" subset_algebra_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil subset_algebra_def nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"set" sets nil ))nil 3426523706"" (skosimp)"" "generated_sigma_algebra_subset2" ("X" "A!1" "Y" "A!1" ))"" (assert )"" (rewrite "subset_reflexive" )"" (lemma "generated_sigma_algebra_subset1" ("X" "A!1" ))"" "subset_antisymmetric" "a" "generated_sigma_algebra(A!1)" "b" "A!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil subset_algebra_def nil )nil nil )nil sets_lemmas nil )set type-eq-decl nil sets nil )nil sets_lemmas nil )"sigma_algebra" nil )nil nil )"(partial_order?[set[T]])" nil ))nil 3426523790"" (skosimp)"" (typepred "A!1" )"" (typepred "B!1" )"" (expand "intersection" )"" (expand "sigma_algebra?" )"" (flatten)"" (expand "member" )"" (split)"1" (expand "subset_algebra_empty?" )"1" (expand "member" ) (("1" (assert ) nil nil ))nil ))nil )"2" (expand "subset_algebra_complement?" )"2" (skosimp)"2" (typepred "x!1" )"2" (inst - "x!1" )"2" (inst - "x!1" )"2" (expand "member" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "sigma_algebra_union?" )"3" (skosimp)"3" (expand "member" )"3" (inst -5 "X!1" )"3" (inst -8 "X!1" )"3" (assert )"3" "1" "1" (assert ) nil nil )"2" "2" "x!1" )"2" (flatten) nil nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"bool" subset_algebra_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" subset_algebra_defnil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" subset_algebra_def nil )"bool" sets nil ))nil 3426524135"" (expand "member" )"" (skosimp)"" (expand "sigma" )"" (expand "extend" )"" (expand "Union" )"" (expand "generated_sigma_algebra" )"" (expand "Intersection" )"" (expand "subset?" )"" (expand "member" )"" (skosimp*)"" (typepred "a!1" )"" (expand "subset?" )"" (expand "member" )"" (inst - "x!1" )"" "1" (propax) nil nil )"2" (inst + "A!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"R" extend nil )"sigma_algebra" nil )"bool" sets nil )"set[sigma_algebra]" subset_algebra_def nil )"sigma_algebra" subset_algebra_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil subset_algebra_def nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil subset_algebra_def nil )"bool" booleans nil )"set" sets nil )"set" sets nil )"sigma_algebra" subset_algebra_def nil )"bool" sets nil ))nil 3449732914"" (lemma "powerset_is_sigma_algebra" )"" (lemma "sigma_algebra_is_subset_algebra" )"" (inst - "powerset(fullset[T])" ) nil nil )) nil ))nil )nil nil )"set" sets nil )"setofsets" sets nil )set type-eq-decl nil sets nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil subset_algebra_def nil )"(nonempty?[set[T]])" nil )nil subset_algebra_defnil ))nil 3449732913"" (subtype-tcc) nil nil )"({Y | AND AND AND (FORALL (x: setof[T]): X!1(x) => Y(x))})" subset_algebra_def nil )"(Intersection[setof[T]] AND AND AND (FORALL (x: setof[T]): X!1(x) => Y(x))}))" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil subset_algebra_def nil )nil defined_types nil )nil sets nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set" sets nil )"set" sets nil )"set" sets nil )"[bool, bool -> bool]" booleans nil )"setofsets[T]" subset_algebra_def nil )"({Y | AND AND AND (FORALL (x: setof[T]): X!1(x) => Y(x))})" subset_algebra_def nil )"(Intersection[setof[T]] AND AND AND (FORALL (x: setof[T]): X!1(x) => Y(x))}))" nil )"(Intersection[setof[T]] AND AND AND (FORALL (x: setof[T]): X!1(x) => Y(x))}))" nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" sets nil )"bool" subset_algebra_def nil )"bool" subset_algebra_defnil )"bool" subset_algebra_def nil )"bool" subset_algebra_def nil )"bool" sets nil )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" ))nil ))nil 3449732987"" (skosimp)"" (expand "subset?" )"" (expand "member" )"" (skosimp)"" (expand "generated_subset_algebra" )"" (expand "Intersection" )"" (skosimp)"" (typepred "a!1" )"" (expand "subset?" )"" (inst - "x!1" )"" (expand "member" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"set" sets nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"subset_algebra" nil )"bool" sets nil ))nil 3449733118"" (skosimp)"" (expand "subset?" +)"" (expand "member" )"" (skosimp)"" (expand "generated_subset_algebra" )"" (expand "Intersection" )"" (inst - "Y!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"set" sets nil )"setofsets[T]" subset_algebra_def nil )"setofsets[T]" subset_algebra_def nil )set type-eq-decl nil sets nil )"bool" subset_algebra_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil subset_algebra_def nil )"(partial_order?[set[T]])" nil )"subset_algebra" nil )"bool" sets nil ))nil 3449733211"" (skosimp)"" (typepred "B!1" )"" (lemma "generated_subset_algebra_subset1" ("X" "B!1" ))"" "generated_subset_algebra_subset2" "X" "B!1" "Y" "B!1" ))"" (assert )"" (rewrite "subset_reflexive" )"" "subset_antisymmetric" "a" "generated_subset_algebra(B!1)" "b" "B!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil nil )set type-eq-decl nil sets nil )nil sets_lemmas nil )"subset_algebra" nil )nil sets_lemmas nil )"(partial_order?[set[T]])" nil )nil nil ))nil 3449733399"" (skosimp)"" (typepred "A!1" )"" (typepred "B!1" )"" (expand "subset_algebra?" )"" (flatten)"" (split)"1" (expand "subset_algebra_empty?" )"1" (expand "member" )"1" (expand "intersection" )"1" (expand "member" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "subset_algebra_complement?" )"2" (skosimp)"2" (expand "complement" )"2" (expand "member" )"2" (expand "intersection" )"2" (expand "member" )"2" (inst - "x!1" )"1" (inst - "x!1" )"1" (assert ) nil nil )"2" "x!1" )"2" expand "intersection" )"2" "2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "x!1" )"2" expand "intersection" )"2" expand "member" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "subset_algebra_union?" )"3" (skosimp)"3" (typepred "x!1" )"3" (typepred "y!1" )"3" (expand "intersection" )"3" (expand "member" )"3" (flatten)"3" (inst - "x!1" "y!1" )"3" "x!1" "y!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"bool" sets nil )"set" sets nil )"bool" subset_algebra_def nil )"subset_algebra" subset_algebra_def nil )set type-eq-decl nil sets nil )"subset_algebra" subset_algebra_def nil )"(intersection(A!1, B!1))" nil )"set" sets nil )"bool" subset_algebra_defnil )"(intersection(A!1, B!1))" nil )"(intersection(A!1, B!1))" nil )"bool" subset_algebra_def nil ))nil 3449733630"" (skosimp)"" (expand "subset?" )"" (skosimp)"" (expand "member" )"" (expand "subset" )"" (expand "generated_subset_algebra" )"" (expand "Intersection" )"" (skosimp)"" (typepred "a!1" )"" (expand "subset?" )"" (expand "member" )"" (inst - "x!1" )"" (assert )"" (hide 2)"" expand "extend" )"" expand "Union" )"" (inst + "B!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"subset_algebra" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil subset_algebra_def nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil ) (Union const-decl "set" sets nil )nil subset_algebra_def nil )"bool" booleans nil )"R" extend nil )"set" sets nil )"subset_algebra" subset_algebra_def nil ))nil 3455341025"" (skosimp)"" (typepred "a!1" )"" (expand "finite_disjoint_union?" )"" (skosimp)"" (expand "nonempty?" )"" (expand "empty?" )"" (inst -4 "n!1" )"" (expand "member" )"" (inst + "E!1" )"" (expand "finite_disjoint_union_of?" )"" (assert )"" (skosimp)"" (inst - "i!1" )"" (flatten)"" assert )"" expand "member" )"" replace -3)"" expand "empty?" )"" expand "member" )"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def nil )set type-eq-decl nil sets nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil )"bool" subset_algebra_defnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" 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" sets nil ))nil ))nil 3450336806"" (skosimp*)"" case "subset?(finite_disjoint_unions(NX!1),generated_subset_algebra(NX!1))" )"1" "generated_subset_algebra_subset2" "X" "NX!1" "Y" "finite_disjoint_unions(NX!1)" ))"1" (split -1)"1" "subset_antisymmetric" "a" "generated_subset_algebra(NX!1)" "b" "finite_disjoint_unions(NX!1)" ))"1" (assert ) nil nil )) nil )"2" (hide-all-but 1)"2" (expand "finite_disjoint_unions" )"2" (expand "fullset" )"2" (expand "extend" )"2" (expand "subset?" )"2" (expand "member" )"2" (skosimp)"2" (assert )"2" (prop)"2" (expand "finite_disjoint_union?" )"2" "lambda n: if n=0 then x!1 else emptyset[T] endif" "1" )"2" "1" expand "disjoint?" )"1" expand "emptyset" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "emptyset" )"2" expand "IUnion" )"2" "x!1(x!2)" )"1" (inst + "0" ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "member" )"3" rewrite "emptyset_is_empty?" )"3" rewrite "emptyset_is_empty?" )"3" "i!1 < 1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (hide -1)"3" case "forall (a,b:(finite_disjoint_unions(NX!1))): finite_disjoint_unions(NX!1)(intersection(a,b))" )"1" (case "finite_disjoint_unions(NX!1)(emptyset)" )"1" case "FORALL (a: (finite_disjoint_unions(NX!1))): ") "1" (expand "subset_algebra?" )"1" (split)"1" (expand "subset_algebra_empty?" )"1" (expand "member" )"1" (propax) nil nil )) nil ))nil )"2" (expand "subset_algebra_complement?" )"2" (skosimp)"2" (expand "member" )"2" (inst - "x!1" ) nil nil )) nil ))nil ))nil )"3" (expand "subset_algebra_union?" )"3" (expand "member" )"3" (skosimp)"3" "y!1" )"3" "x!1" )"3" "complement(x!1)" "complement(y!1)" )"3" rewrite "demorgan1" -5 :dir rl)"3" "complement(union(x!1, y!1))" )"3" rewrite "complement_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (typepred "a!1" )"2" (expand "finite_disjoint_unions" -1)"2" (expand "fullset" )"2" expand "extend" )"2" "2" expand "finite_disjoint_union?" "2" "2" expand "member" )"2" "n!1=0" )"1" assert )"1" "a!1=emptyset" )"1" rewrite "complement_emptyset" "1" "1" "NX!1" )"1" expand "nonempty?" )"1" expand "empty?" "1" "1" expand "member" )"1" "x!1" )"1" expand "finite_disjoint_union?" "1" "1" expand "member" )"1" expand "finite_disjoint_unions" "1" expand "fullset" "1" expand "extend" )"1" "1" expand "finite_disjoint_union?" )"1" "lambda i: if i = 0 then x!1 else E!2(i-1) endif" "n!2+1" )"1" "1" "1" expand "disjoint?" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "member" )"1" expand "empty?" )"1" expand "member" )"1" "1" "i!1=0" )"1" assert )"1" "extensionality_postulate" "f" "complement(x!1)" "g" "IUnion(E!2)" ))"1" "1" "1" "1" "1" "x!2" )"1" expand "complement" )"1" expand "member" )"1" expand "IUnion" )"1" "j!1-1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "j!1=0" )"1" "extensionality_postulate" "f" "complement(x!1)" "g" "IUnion(E!2)" ))"1" "1" "1" "1" "x!2" )"1" expand "complement" )"1" expand "member" )"1" assert )"1" replace "1" assert )"1" expand "IUnion" )"1" "i!1-1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "i!1 - 1" "j!1-1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "fullset" "1" expand "IUnion" )"1" expand "complement" )"1" expand "member" )"1" "extensionality_postulate" "f" "complement(x!1)" "g" "IUnion(E!2)" ))"1" "1" "1" "1" "x!2" )"1" "1" expand "complement" )"1" expand "member" )"1" "x!1(x!2)" )"1" assert )"1" "0" )nil nil ))nil )"2" assert )"2" expand "IUnion" )"2" "2" "i!1+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "IUnion" )"2" expand "complement" )"2" expand "member" )"2" 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" assert )"3" "i!1=0" )"1" assert )nil nil )"2" assert )"2" "i!1-1" )"2" "2" assert )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "emptyset" )"2" replace -4 -1)"2" expand "IUnion" )"2" "2" "i!1" )"2" expand "empty?" )"2" "x!1" )"2" assert )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1>0" )"1" "1" "FF" "IComplement(E!1)" )"1" "F" "lambda n: Intersection(image(FF,{i| i<=n}))" )"1" case "F(0) = complement(E!1(0))" )"1" case "forall n: F(n+1)=intersection(F(n),complement(E!1(n+1)))" )"1" case "FORALL n: n < n!1 => finite_disjoint_unions(NX!1)(F(n))" )"1" replace "1" "IDemorgan1" )"1" "E!1" )"1" replace "1" "1" case "IIntersection(IComplement(E!1))=F(n!1-1)" )"1" replace "1" "n!1-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "2" expand "IComplement" )"2" expand "IIntersection" )"2" "FORALL (i_1: nat): complement(E!1(i_1))(x!1)" )"1" expand "F" "1" expand "FF" )"1" expand "IComplement" )"1" expand "image" )"1" expand "Intersection" )"1" "1" "a!2" )"1" "1" "x!2" )"1" replace "1" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" "i!1" )"2" "2" case "i!1<n!1" )"1" assert )"1" expand "F" "1" expand "Intersection" )"1" "complement(E!1(i!1))" )"1" expand "FF" )"1" expand "image" )"1" expand "IComplement" )"1" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "complement" )"2" expand "member" )"2" expand "empty?" "2" "x!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" "1" replace "1" "0" )"1" assert )"1" "E!1(0)" )"1" expand "finite_disjoint_unions" )"1" expand "fullset" )"1" expand "extend" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "j!1" )"2" replace "2" "1+j!1" )"2" assert )"2" "E!1(1+j!1)" )"2" "F(j!1)" "complement(E!1(1 + j!1))" )"2" "2" expand "finite_disjoint_unions" )"2" expand "fullset" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "F" )"2" expand "FF" )"2" expand "IComplement" )"2" expand "complement" )"2" expand "image" )"2" expand "Intersection" )"2" expand "intersection" )"2" expand "member" )"2" "E!1(1 + n!2)(x!1)" )"1" assert )"1" "complement(E!1(1+n!2))" )"1" expand "complement" )"1" expand "member" )"1" nil nil ))nil ))nil )"2" "1+n!2" )"2" "2" expand "complement" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "FORALL (a: set [T] |NOT member(x, E!1(x_1))})})):") "1" "1" "a!2" )"1" "1" "a!2" )"1" "x!2" )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" "a!2" )"2" "2" "x!2" )"2" expand "<=" "2" "1" "a!2" )"1" "x!2" )"1" expand "member" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "E!1(1+n!2)" )"2" replace "2" assert )"2" expand "member" )"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 )"2" "2" expand "F" )"2" expand "FF" )"2" expand "IComplement" )"2" expand "image" )"2" expand "complement" )"2" expand "member" )"2" "2" expand "Intersection" )"2" "E!1(0)(x!1)" )"1" assert )"1" "complement(E!1(0))" )"1" expand "complement" )"1" expand "member" )"1" nil nil ))nil ))nil )"2" "0" )"2" expand "complement" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "a!2" )"2" "2" replace "2" assert )nil nil ))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 )"2" (hide 2)"2" (expand "finite_disjoint_unions" 1)"2" (expand "fullset" )"2" (expand "extend" )"2" (prop)"2" (expand "finite_disjoint_union?" )"2" "lambda i: emptyset[T]" "0" )"2" "1" "1" (grind) nil nil ))nil )"2" "2" "2" (grind) nil nil ))nil ))nil )"3" "3" assert )"3" rewrite "emptyset_is_empty?" )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 "finite_disjoint_unions" (-1 -2 1))"2" (expand "fullset" )"2" (expand "extend" )"2" "2" expand "finite_disjoint_union?" "2" "AA" "mm" ))"2" "BB" "nn" ))"2" "2" expand "member" )"2" "mm=0" )"1" assert )"1" "lambda i: emptyset" "0" )"1" "1" "1" nil nil ))nil )"2" "2" expand "intersection" )"2" expand "IUnion" )"2" expand "emptyset" )"2" expand "member" )"2" "2" replace "2" assert )"2" "2" "i!1" )"2" expand "empty?" )"2" expand "member" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "mm>0" )"1" "1" "nn=0" )"1" "lambda i: emptyset" "0" )"1" "1" "1" nil nil ))nil )"2" "2" expand "intersection" )"2" expand "member" )"2" expand "IUnion" )"2" expand "emptyset" )"2" "2" replace "2" assert )"2" "2" "i!1" )"2" expand "empty?" )"2" "x!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil )"2" case "nn>0" )"1" "1" "lambda i: let n = ndiv(i,nn) in intersection(AA(n),BB(rem(nn)(i)))" "nn*mm" )"1" "1" expand "disjoint?" )"1" expand "intersection" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "1" "ndiv(i!1, nn)" "ndiv(j!1, nn)" )"1" "rem(nn)(i!1)" "rem(nn)(j!1)" )"1" expand "/=" )"1" case "rem(nn)(i!1) = rem(nn)(j!1)" )"1" assert )"1" "1" "ndiv(i!1, nn)" )"1" "ndiv(j!1, nn)" )"1" replace "1" replace "1" assert )"1" replace "1" assert )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "IUnion" )"1" expand "intersection" )"1" expand "member" )"1" "a!1(x!1) AND b!1(x!1)" )"1" "1" replace "1" replace "1" assert )"1" "1" "i!2*nn+i!1" )"1" "ndiv(i!2 * nn + i!1, nn)" )"1" case "i!1<nn" )"1" case "i!2<mm" )"1" "rem(nn)(i!2 * nn + i!1) = i!1" )"1" replace "1" assert )"1" "ndiv(i!2 * nn + i!1, nn)=i!2" )"1" "1" "both_sides_times1" )"1" "nn" "ndiv(i!2 * nn + i!1, nn)" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "rem_def" "2" "i!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "i!2" )"2" assert )"2" expand "empty?" )"2" expand "member" )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" expand "empty?" )"2" expand "member" )"2" assert )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" replace "2" replace "2" "1" assert )"1" "rem(nn)(i!1)" )nil nil ))nil )"2" assert )"2" "ndiv(i!1,nn)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" case "rem(nn)(i!1)<nn" )"1" case "nn*ndiv(i!1, nn) +rem(nn)(i!1) = i!1" )"1" assert )"1" case "ndiv(i!1, nn)<mm" )"1" "both_sides_times_pos_le1" "pz" "nn" "x" "ndiv(i!1, nn)" "y" "mm-1" ))"1" assert )"1" case "i!1<mm*nn" )"1" "ndiv(i!1, nn)" )"1" "1" assert )"1" "1" "rem(nn)(i!1)" )"1" "1" assert )"1" "1" "AA(ndiv(i!1, nn))" "BB(rem(nn)(i!1))" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "both_sides_times_pos_le1" "pz" "nn" "x" "mm" "y" "ndiv(i!1, nn)" ))"2" assert )"2" "ndiv(i!1, nn)" )"2" assert )"2" "2" expand "empty?" )"2" expand "intersection" )"2" expand "member" )"2" "2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ndiv(i!1, nn)" )"2" assert )nil nil ))nil ))nil ))nil )"2" "rem(nn)(i!1)" )"2" nil nil ))nil )"3" nil nil ))nil ))nil ))nil )"2" "le_times_le_pos" "nnx" "0" "y" "nn-1" "nnz" "0" "w" "mm-1" ))"2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" assert )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 ))nil ))nil )"2" (hide 2)"2" (expand "finite_disjoint_unions" )"2" (expand "fullset" )"2" (expand "extend" )"2" (expand "subset?" )"2" (expand "member" )"2" (skosimp*)"2" (prop)"2" (expand "generated_subset_algebra" )"2" (expand "Intersection" )"2" (skosimp)"2" (typepred "a!1" )"2" expand "finite_disjoint_union?" -3)"2" "2" expand "member" )"2" case "forall i: a!1(E!1(i))" )"1" "F" "lambda n: Union(image[nat,set[T]](E!1,{i | i <= n}))" )"1" case "forall n: F(n+1) = union(F(n),E!1(n+1))" )"1" case "IUnion(E!1) = F(n!1)" )"1" case "forall n: a!1(F(n))" )"1" "n!1" )"1" assert )nil nil ))nil )"2" "2" "n" )"1" "1" "F(0)=E!1(0)" )"1" "0" )nil nil )"2" "2" expand "F" )"2" "2" "E!1(0)(x!2)" )"1" expand "image" )"1" expand "Union" )"1" "E!1(0)" )"1" "0" )nil nil ))nil ))nil ))nil )"2" assert )"2" expand "image" )"2" expand "Union" )"2" "2" "a!2" )"2" "2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" replace -2)"2" "2" expand "subset_algebra?" )"2" "2" expand "subset_algebra_union?" )"2" expand "member" )"2" "j!1+1" )"2" "F(j!1)" "E!1(j!1 + 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "F" )"2" expand "image" )"2" expand "Union" )"2" expand "IUnion" )"2" "EXISTS (i: nat): E!1(i)(x!2)" )"1" "1" "i!1" )"1" "1" rewrite "emptyset_is_empty?" )"1" "trich_lt" "x" "i!1" "y" "n!1" ))"1" "1" assert )"1" "E!1(i!1)" )"1" "i!1" )nil nil ))nil ))nil )"2" assert )"2" replace "2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil )"3" assert )"3" replace "3" expand "emptyset" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" "a!2" )"2" "2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "union" )"2" expand "F" )"2" expand "member" )"2" expand "image" )"2" expand "Union" )"2" "E!1(1 + n!2)(x!2)" )"1" "E!1(1+n!2)" )"1" "1+n!2" )nil nil ))nil )"2" assert )"2" "EXISTS (a: set [T] |") "1" "1" "a!2" )"1" "1" "x!3" )"1" expand "<=" "1" "1" "E!1(x!3)" )"1" assert )nil nil )"2" "x!3" )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" "a!2" )"2" "2" "E!1(x!3)" )"1" assert )nil nil )"2" "x!3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" )"2" "2" expand "subset?" )"2" "E!1(i!1)" )"2" expand "member" )"2" expand "subset_algebra?" )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" rewrite "emptyset_is_empty?" )"2" "i!1 < n!1" )"1" assert )nil nil )"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 )"subset_algebra" nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )"bool" sets nil )"setofsets[T]" nil )nil sets nil )"bool" sets nil )set type-eq-decl nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil subset_algebra_def nil )"(partial_order?[set[T]])" nil )nil sets_lemmas nil )"R" extend nil )"bool" sets nil )"bool" subset_algebra_def nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" indexed_sets_aux "sets_aux/" )"set[T]" indexed_sets nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )nil sets_lemmas nil )"set" sets nil )"[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 )"set" sets nil )nil real_props nil )"nonneg_int" nil )nil modulo_arithmetic nil )nil real_props nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )nil real_types nil )nil real_types nil )"{q: int | x = b * q + rem(b)(x)}" nil )"{r: mod(b) | EXISTS q: x = b * q + r}" nil )"[numfield, numfield -> numfield]" number_fields nil )nil euclidean_division nil )nil integers nil )nil integers nil )"nat" subset_algebra_def nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil application-judgement "upto(n)" modulo_arithmetic nil )"nonneg_int" nil )NOT const-decl "[bool -> bool]" booleans nil )"set[T]" subset_algebra_def nil )"(total_order?[real])" nil )nil functions nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )"int" integers nil )"posint" nil )nil sets_lemmas nil )"set" sets nil )"set[R]" function_image nil )"bool" reals nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"nat" subset_algebra_def nil )"odd_int" integersnil )nil naturalnumbers nil )nil defined_types nil )"[nat -> set[T]]" subset_algebra_def nil )"[nat -> set[T]]" subset_algebra_def nil )"sequence[set[T]]" subset_algebra_def nil )"nat" subset_algebra_def nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" subset_algebra_def nil )"set[T]" indexed_sets nil )nil indexed_sets_aux "sets_aux/" )"nat" subset_algebra_def nil )"({y: set[T] | NOT member(x, E!1(x_1))})})" nil )"({i | i <= 1 + n!2})" subset_algebra_defnil )"({y: set[T] | NOT member(x, E!1(x_1))})})" subset_algebra_def nil) "set[T]" indexed_sets_aux "sets_aux/" )"bool" reals nil )"bool" subset_algebra_def nil )nil sets_lemmas nil )nil sets_lemmas nil )"set" sets nil )"(finite_disjoint_unions(NX!1))" nil )"(finite_disjoint_unions(NX!1))" nil )"(nonempty?[set[T]])" subset_algebra_defnil )"bool" subset_algebra_defnil )"bool" subset_algebra_def nil )"set" sets nil )"boolean" notequal nil )"finite_set[T]" "sets_aux/" )nil nil )"nat" subset_algebra_def nil )"nat" subset_algebra_def nil )nil real_props nil )"[nat -> set[T]]" subset_algebra_def nil )"bool" booleans nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"({Y | subset_algebra?(Y) AND subset?(NX!1, Y)})" nil )"nat" subset_algebra_def nil )"sequence[set[T]]" subset_algebra_def nil )"({i | i <= n!2})" subset_algebra_def nil )"({i | i <= 1 + n!2})" subset_algebra_defnil )"nat" subset_algebra_def nil )"set" sets nil ))nil 3449748022"" (expand "monotone?" )"" (skosimp)"" (split)"1" (flatten)"1" (expand "member" )"1" (expand "trivial_subset_algebra" )"1" (expand "union" )"1" (expand "member" )"1" (flatten)"1" (expand "singleton" )"1" (case "forall n: E!1(n) = emptyset[T]" )"1" (hide 2)"1" (expand "IUnion" )"1" (apply-extensionality :hide? t)"1" expand "emptyset" )"1" "1" "i!1" )"1" replace -2 -1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skosimp)"2" (inst - "n!1" )"2" assert )"2" "2" "2" expand "fullset" )"2" expand "IUnion" )"2" "n!1" )"2" replace -1 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "member" )"2" (expand "trivial_subset_algebra" )"2" (expand "union" )"2" (expand "member" )"2" (expand "singleton" )"2" (flatten)"2" (case "forall n: E!1(n) = fullset[T]" )"1" (hide-all-but (-1 2))"1" (expand "fullset" )"1" (expand "IIntersection" )"1" "1" "1" "i!1" )"1" replace -1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (inst - "n!1" )"2" (assert )"2" "2" "2" expand "emptyset" )"2" expand "IIntersection" )"2" "n!1" )"2" replace -2 -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[T]" indexed_sets nil )"bool" booleans nil )"(subset_algebra?)" nil )"(singleton?)" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )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 subset_algebra_def nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )nil sequences nil )"set" sets nil )"set" sets nil )"bool" sets nil )"bool" subset_algebra_def nil ))nil ))nil 3449818847"" (expand "monotone?" )"" (skosimp)"" (expand "member" )"" (split)"1" (flatten)"1" (expand "fullset" )"1" (expand "powerset" )"1" (expand "subset?" )"1" (expand "member" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "fullset" )"2" (expand "powerset" )"2" (expand "subset?" )"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" sets nil )"setofsets" sets nil )"bool" sets nil )"bool" subset_algebra_def nil ))nil 3449769838"" (skolem + "A!1" )"" (typepred "A!1" )"" (expand "monotone?" )"" (skosimp)"" (split)"1" (expand "member" )"1" (skosimp)"1" (expand "sigma_algebra?" )"1" (flatten)"1" (expand "sigma_algebra_union?" )"1" (inst - "image(E!1,fullset[nat])" )"1" (split -4)"1" (expand "member" )"1" "Union(image(E!1, fullset[nat]))=IUnion(E!1)" )"1" "1" "1" expand "IUnion" )"1" expand "fullset" )"1" expand "image" )"1" expand "Union" )"1" "EXISTS (i: nat): E!1(i)(x!1)" )"1" "1" "E!1(i!1)" )"1" "i!1" )nil nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "a!1" )"2" "2" replace -1 -2)"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "countable_image[nat,set[T]]" )"2" "fullset[nat]" "E!1" )"2" "1" expand "image" -1)"1" (propax) nil nil ))nil )"2" "2" expand "fullset" )"2" expand "is_countable" )"2" "lambda (n:nat): n" )"2" expand "injective?" )"2" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp)"3" "x!1" )"3" expand "member" )"3" expand "fullset" )"3" expand "image" )"3" "3" replace -1)"3" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "member" )"2" (expand "sigma_algebra?" )"2" (flatten)"2" (expand "subset_algebra_complement?" )"2" (expand "member" )"2" "complement(IIntersection(E!1))" )"1" (rewrite "complement_complement" ) nil nil )"2" (hide 2)"2" (rewrite "IDemorgan2" +)"2" expand "sigma_algebra_union?" )"2" "image(IComplement(E!1),fullset[nat])" )"2" expand "member" )"2" "1" "Union(image(IComplement(E!1), fullset[nat]))=IUnion(IComplement(E!1))" )"1" "1" "1" expand "fullset" )"1" expand "IComplement" )"1" expand "complement" )"1" expand "member" )"1" expand "image" )"1" expand "IUnion" )"1" expand "Union" )"1" "(EXISTS (i_1: nat): NOT E!1(i_1)(x!1))" )"1" "1" "complement(E!1(i!1))" )"1" expand "complement" )"1" expand "member" )"1" nil nil ))nil ))nil )"2" expand "complement" )"2" expand "member" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" "a!1" )"2" "2" replace "2" assert )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "countable_image[nat,set[T]]" )"2" "fullset[nat]" "IComplement(E!1)" )"2" "1" expand "image" -1)"1" nil nil ))nil )"2" "2" expand "fullset" )"2" expand "is_countable" )"2" "lambda (n:nat): n" )"2" expand "injective?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "x!1" )"3" expand "fullset" )"3" expand "image" )"3" "3" expand "IComplement" )"3" replace -1)"3" "3" "A!1" )"3" expand "sigma_algebra?" )"3" "3" expand "subset_algebra_complement?" )"3" expand "member" )"3" "E!1(x!2)" )"3" "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 )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" subset_algebra_defnil )"set[T]" indexed_sets nil )"set" sets nil )"sigma_algebra" subset_algebra_def nil )nil sets_lemmas nil )nil indexed_sets_aux "sets_aux/" )"set[T]" indexed_sets_aux "sets_aux/" )"nat" subset_algebra_def nil )"({x | TRUE})" subset_algebra_def nil )"bool" sets nil )"bool" subset_algebra_def nil )"set[T]" indexed_sets nil )"set" sets nil )"[T, T -> boolean]" equalities nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"nat" subset_algebra_def nil )"sequence[set[T]]" subset_algebra_def nil )"bool" booleans nil )nil countable_image "sets_aux/" )"set[R]" function_image nil )"bool" functions nil )"bool" countability "sets_aux/" )"set" sets nil )nil sequences nil )"set[R]" function_image nil )set type-eq-decl nil sets 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 ))nil ))nil 3449799687"" (skosimp)"" (expand "subset_algebra?" )"" (expand "sigma_algebra?" )"" (flatten)"" (split)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (expand "sigma_algebra_union?" )"3" (skolem + "Y!1" )"3" (flatten)"3" (lemma "Union_IUnion[T]" ("XS" "Y!1" ))"3" (assert )"3" (skosimp)"3" (replace -1)"3" (expand "member" )"3" (expand "monotone?" )"3" expand "member" )"3" "increasing_IUnion" "A" "YS!1" ))"3" "3" "B!1" )"3" replace -1)"3" "1" "1" (assert ) nil nil ))nil )"2" "2" "n" )"1" replace -2)"1" "0" )"1" "1" expand "subset_algebra_empty?" )"1" expand "member" )"1" rewrite "emptyset_is_empty?" )"1" assert )nil nil ))nil ))nil ))nil )"2" "YS!1(0)" )nil nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" replace -4)"2" "j!1+1" )"2" "1" rewrite "emptyset_is_empty?" )"1" expand "subset_algebra_empty?" )"1" expand "member" )"1" expand "subset_algebra_union?" )"1" expand "member" )"1" "B!1(j!1)" "YS!1(j!1 + 1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "YS!1(j!1 + 1)" )"1" expand "subset_algebra_union?" )"1" expand "member" )"1" "B!1(j!1)" "YS!1(j!1 + 1)" )"1" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def nil )"bool" subset_algebra_def nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" subset_algebra_def nil )nil sequences nil )set type-eq-decl nil sets 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 nat_indexed_sets "sets_aux/" )nil defined_types nil )nil naturalnumbers nil )"setofsets[T]" subset_algebra_def nil )"sequence[set[T]]" subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets_lemmas nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"nat" subset_algebra_def nil )"sequence[set[T]]" subset_algebra_def nil )"setofsets[T]" subset_algebra_def nil )"bool" subset_algebra_def nil )"odd_int" integersnil )"int" integers nil )"bool" sets nil )nil countable_indexed_sets "sets_aux/" )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil ))nil 3449803550"" (skosimp)"" (expand "extend" )"" (expand "Intersection" )"" (expand "monotone?" 1 1)"" (skosimp*)"" (expand "member" )"" (split)"1" (flatten)"1" (skosimp)"1" (typepred "a!1" )"1" (assert )"1" (expand "monotone?" )"1" (expand "member" )"1" (inst - "E!1" )"1" "1" "1" (assert ) nil nil ))nil )"2" "2" "n!1" )"2" (inst - "a!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp)"2" (typepred "a!1" )"2" (assert )"2" (expand "monotone?" )"2" (inst - "E!1" )"2" (split -2)"1" "1" expand "member" )"1" (propax) nil nil ))nil ))nil )"2" "2" expand "member" )"2" "n!1" )"2" (inst - "a!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"R" extend nil )"bool" subset_algebra_def nil )"bool" sets nil )"bool" booleans nil )set type-eq-decl nil sets nil )nil subset_algebra_def nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sets nil )nil defined_types nil )nil subset_algebra_def nil )"[bool, bool -> bool]" booleans 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 )"set" sets nil ))nil 3449748340"" (skolem + ("A!1" "C!1" ))"" (flatten)"" (typepred "A!1" )"" (typepred "C!1" )"" (name "MM" "{C | subset?(A!1, C)}" )"" (case "nonempty?(MM)" )"1" (lemma "monotone_class_Intersection" ("K" "MM" ))"1" (expand "extend" )"1" "M" "Intersection(LAMBDA (t: setof[setof[T]]): IF monotone?(t) THEN MM(t) ELSE FALSE ENDIF)") "1" (case "subset?(A!1,M)" )"1" (case "subset?(M,C!1)" )"1" case "subset?(M,generated_sigma_algebra(A!1))" )"1" case "subset?(generated_sigma_algebra(A!1), M)" )"1" "subset_antisymmetric" "a" "generated_sigma_algebra(A!1)" "b" "M" ))"1" (assert ) nil nil )) nil )"2" (hide 2)"2" "monotone_algebra_is_sigma" "X" "M" ))"2" replace -5 -6)"2" replace -6 -1)"2" "1" "generated_sigma_algebra_subset2" "X" "A!1" "Y" "M" ))"1" (assert ) nil nil ))nil )"2" "2" expand "subset_algebra?" )"2" "2" "KK" "lambda (a:set[T]): {b:set[T] | M(union(a,b)) & M(difference(a,b)) & M(difference(b,a))}" )"2" case "forall (a,b:set[T]): KK(a)(b) iff KK(b)(a)" )"1" case "FORALL (a, b: (A!1)): KK(b)(a)" )"1" "subset_algebra_empty?(M)" )"1" case "forall (b:set[T]): monotone?(KK(b))" )"1" case "forall (x:(A!1)): subset?(A!1,KK(x))" )"1" case "forall (b:(A!1)): subset?(M,KK(b))" )"1" case "forall (a,b:(M)): M(union(a, b)) & M(difference(a, b)) & M(difference(b, a))" )"1" "1" expand "subset_algebra_complement?" )"1" expand "member" )"1" "1" "x!1" )"1" expand "subset_algebra_empty?" "1" expand "member" )"1" "emptyset[T]" )"1" rewrite "complement_emptyset" )"1" expand "subset?" "1" "fullset[T]" )"1" expand "member" )"1" assert )"1" "fullset[T]" "x!1" )"1" "1" rewrite "difference_fullset2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset_algebra_union?" )"2" "2" "x!1" "y!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a!1" )"2" "b!1" )"2" case "forall (a:(M)): subset?(A!1,KK(a))" )"1" case "FORALL (a: (M)): subset?(M, KK(a))" )"1" "1" expand "subset?" )"1" expand "KK" )"1" expand "member" )"1" "a!1" )"1" "b!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a!2" )"2" "a!2" )"2" expand "subset?" "2" "2" expand "member" )"2" expand "M" "2" expand "Intersection" "2" "KK(a!2)" )"2" "a!2" )"2" assert )"2" expand "MM" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a!2" )"2" expand "subset?" "2" "2" expand "member" )"2" "x!1" )"2" expand "subset?" "2" expand "member" )"2" "a!2" )"2" assert )"2" "a!2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "b!1" )"2" "b!1" )"2" expand "subset?" "2" "2" expand "member" )"2" replace "2" expand "Intersection" "2" "KK(b!1)" )"2" replace "2" "2" expand "MM" "2" "b!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "subset?" "2" "2" expand "member" )"2" "x!1" )"2" "x!2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "monotone?" "2" "2" expand "member" )"2" "2" "1" "1" "1" expand "KK" )"1" expand "monotone?" )"1" expand "member" )"1" "1" "lambda n: union(b!1, E!1(n))" )"1" "1" "1" "1" "1" "IUnion(LAMBDA n: union(b!1, E!1(n))) = union(b!1, IUnion(E!1))" )"1" "1" "1" expand "union" )"1" expand "member" )"1" "b!1(x!1)" )"1" expand "IUnion" )"1" "0" )"1" nil nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "increasing?" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "lambda n: difference(b!1, E!1(n))" )"2" "1" "1" "1" "1" "IIntersection(LAMBDA n: difference(b!1, E!1(n)))=difference(b!1, IUnion(E!1))" )"1" "1" "1" expand "difference" )"1" expand "member" )"1" "b!1(x!1)" )"1" assert )"1" expand "IIntersection" )"1" "IUnion(E!1)(x!1)" )"1" assert )"1" expand "IUnion" )"1" "1" "i!1" )nil nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "IUnion" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IIntersection" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "decreasing?" )"2" expand "increasing?" )"2" expand "difference" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "lambda n: difference(E!1(n),b!1)" )"3" "1" "1" "1" "1" "IUnion(LAMBDA n: difference(E!1(n), b!1))=difference(IUnion(E!1), b!1)" )"1" "1" "1" expand "difference" )"1" expand "member" )"1" expand "IUnion" )"1" "b!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" expand "difference" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "KK" )"2" "2" expand "monotone?" "2" "2" "1" "lambda n: union(b!1,E!1(n))" )"1" expand "member" )"1" "1" "1" "1" "1" "IIntersection(LAMBDA n: union(b!1, E!1(n)))=union(b!1, IIntersection(E!1))" )"1" "1" "1" expand "union" )"1" expand "member" )"1" expand "IIntersection" )"1" "b!1(x!1)" )"1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "decreasing?" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "lambda n: difference(b!1, E!1(n))" )"2" expand "member" )"2" "1" "1" "1" "1" "IUnion(LAMBDA n: difference(b!1, E!1(n)))=difference(b!1, IIntersection(E!1))" )"1" "1" "1" expand "difference" )"1" expand "member" )"1" "b!1(x!1)" )"1" expand "IUnion" )"1" assert )"1" "IIntersection(E!1)(x!1)" )"1" assert )"1" expand "IIntersection" )"1" "1" "i!1" )nil nil ))nil ))nil ))nil )"2" assert )"2" expand "IIntersection" )"2" "2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "decreasing?" )"2" expand "increasing?" )"2" expand "difference" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "member" )"3" "lambda n: difference(E!1(n),b!1)" )"3" "1" "1" "1" "1" "IIntersection(LAMBDA n: difference(E!1(n), b!1))=difference(IIntersection(E!1), b!1)" )"1" "1" "1" expand "difference" )"1" expand "member" )"1" expand "IIntersection" )"1" "b!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "decreasing?" )"2" expand "difference" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" expand "subset?" )"2" "emptyset[T]" )"2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "KK" )"2" expand "M" )"2" rewrite "difference_intersection" )"2" rewrite "difference_intersection" )"2" "1" expand "Intersection" )"1" "1" "a!2" )"1" assert )"1" expand "MM" )"1" expand "subset_algebra_union?" )"1" "b!1" "a!1" )"1" expand "member" )"1" expand "subset?" )"1" "union(b!1, a!1)" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Intersection" )"2" "2" "a!2" )"2" assert )"2" expand "MM" )"2" expand "subset?" )"2" expand "member" )"2" "intersection(b!1, complement(a!1))" )"2" assert )"2" "2" expand "subset_algebra_complement?" )"2" expand "subset_algebra_union?" )"2" expand "member" )"2" "demorgan1" "a" "complement(b!1)" "b" "a!1" ))"2" rewrite "complement_complement" )"2" replace "2" "2" "b!1" )"2" "complement(b!1)" "a!1" )"2" "union(complement(b!1), a!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "Intersection" )"3" "3" "a!2" )"3" assert )"3" expand "MM" )"3" expand "subset?" )"3" expand "member" )"3" "intersection(a!1, complement(b!1))" )"3" assert )"3" "3" "demorgan1" "a" "complement(a!1)" "b" "b!1" ))"3" rewrite "complement_complement" )"3" replace "3" "3" expand "subset_algebra_complement?" )"3" expand "subset_algebra_union?" )"3" expand "member" )"3" "a!1" )"3" "complement(a!1)" "b!1" )"3" "union(complement(a!1), b!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 ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "KK" )"2" "1" "1" assert )"1" rewrite "union_commutative" )nil nil ))nil ))nil )"2" "2" assert )"2" rewrite "union_commutative" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -3 -4)"2" "generated_sigma_algebra(A!1)" )"2" "sigma_algebra_is_monotone_class" "x" "generated_sigma_algebra(A!1)" ))"2" "generated_sigma_algebra_subset1" "X" "A!1" ))"2" "SA" "generated_sigma_algebra(A!1)" )"2" expand "subset?" 1)"2" "2" expand "member" )"2" expand "M" -4)"2" expand "Intersection" )"2" "SA" )"2" assert )"2" expand "MM" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -2)"2" (expand "subset?" 1)"2" (skosimp)"2" expand "member" )"2" expand "M" -1)"2" expand "Intersection" )"2" "C!1" )"2" expand "MM" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "subset?" 1)"2" (skosimp)"2" (expand "member" )"2" replace -2 1 rl)"2" "2" expand "Intersection" )"2" "2" "a!1" )"2" assert )"2" replace -6 -1 rl)"2" assert )"2" expand "subset?" )"2" expand "member" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "powerset_is_monotone" )"2" (hide-all-but (-1 1))"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "powerset(fullset[T])" )"2" (hide-all-but 1)"2" (expand "MM" )"2" expand "fullset" )"2" expand "powerset" )"2" expand "subset?" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )"bool" sets nil )"R" extend nil )"monotone_class" subset_algebra_def nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" nil )nil nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set" sets nil )"set" sets nil )nil sets_lemmas nil )"setof[T]" subset_algebra_def nil )"[monotone_class -> bool]" subset_algebra_defnil )"(M)" subset_algebra_def nil )"set[setof[T]]" subset_algebra_def nil )"[set[T] -> [set[T] -> boolean]]" nil )"setof[T]" subset_algebra_def nil )"bool" sets nil )nil sets_lemmas nil )"set" sets nil )nil sets_lemmas nil )"set" sets nil )"subset_algebra" subset_algebra_def nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"bool" subset_algebra_defnil )"bool" subset_algebra_def nil )"(A!1)" subset_algebra_def nil )"set[T]" indexed_sets nil )"bool" fun_preds_partial "structures/" )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 )"set[T]" indexed_sets nil )"(total_order?[real])" nil )"bool" fun_preds_partial "structures/" )"bool" subset_algebra_def nil )nil sets_lemmas nil )"(A!1)" subset_algebra_def nil )"(A!1)" subset_algebra_def nil )nil sets_lemmas nil )"set" sets nil )"set" sets nil )"[bool, bool -> bool]" booleans nil )nil sets_lemmas nil )"[bool, bool -> bool]" booleans nil )nil subset_algebra_def nil )nil sets_lemmas nil )"(partial_order?[set[T]])" nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil nil )"sigma_algebra" subset_algebra_def nil )nil nil )"bool" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )nil subset_algebra_defnil )"bool" sets nil )"(nonempty?[set[T]])" nil )"setofsets" sets nil )nil subset_algebra_def nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil subset_algebra_def nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.742Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
