Quelle class_equation_scaf.prf
Sprache: Lisp
(class_equation_scafnil 3526046475"" (skosimp*)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (assert )"" (lemma "Union_finite[T]" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil finite_sets_of_sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil ))nil ))nil 3526046475"" (skosimp*)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (hide (-1 -2))"" (expand "every" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil ) (set type-eq-decl nil sets nil )"bool" sets nil )"(p)" sets nil ))nil ))nil 3526046475"" (skosimp*)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (lemma "Union_finite[T]" )"" (inst?)"" (assert )"" (hide (-1 2))"" (prop)"1" (rewrite "finite_rest" ) nil nil )"2" (expand "every" )"2" (skosimp*)"2" (inst?)"2" (typepred "x!1" )"2" (lemma "rest_member[setof[T]]" )"2" "FP!1" "x!1" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil ) (rest const-decl "set" sets nil )"bool" sets nil )"finite_partition[T]" class_equation_scafnil )"(rest[setof[T]](FP!1))" class_equation_scafnil )nil sets_lemmas nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil finite_sets_of_sets nil ))nil ))nil 3526047645"" (skosimp*)"" (lemma "card_Union_rest" )"" (inst?)"" (assert )"" (replaces -1)"" (rewrite "card_disj_union" )"" (hide 2)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (expand "partition?" )"" (expand "disjoint?" )"" (expand "empty?" )"" (skosimp*)"" expand "member" )"" expand "intersection" )"" expand "member" )"" "" expand "Union" )"" "" "a!1" "choose(FP!1)" )"1" "1" "a!1" )"1" "1" "1" "choose_not_member[setof[T]]" )"1" "1" expand "nonempty?" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" "a!1" )"2" "rest_member[setof[T]]" )"2" "FP!1" "a!1" )"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 ))nil ))nil ))nil ))nil ))nil )nil class_equation_scaf nil )nil lagrange_scaf "algebra/" )"nonneg_int" nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil ) (rest const-decl "set" sets nil )"bool" sets nil )"(p)" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"set" sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"(rest(FP!1))" class_equation_scaf nil )"finite_partition[T]" class_equation_scafnil )"bool" sets nil )"bool" sets nil )"bool" lagrange_scaf "algebra/" )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil ))nil 3526042692"" (skosimp*)"" (typepred "A!1" )"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (expand "every" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil ))nil ))nil 3526042692"" (skosimp*)"" (expand "convergent?" )"" (prop)"1" (typepred "FP!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" (hide -1)"1" (rewrite "finite_countable" )"1" (hide 2)"1" (expand "is_finite" (-1 1))"1" (skosimp)"1" (inst 1 "N!1" "f!1" )"1" (hide (-2 -3))"1" (expand "injective?" )"1" (grind) nil nil )) nil ))nil )"2" (skosimp*)"2" (prop)"1" expand "every" )"1" (inst?) nil nil ))nil )"2" expand "nonzero_elts" )"2" expand "restrict" )"2" assert )"2" (inst?) nil nil ))nil ))nil ))nil )"3" expand "nonzero_elts" )"3" expand "restrict" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "convergent?" )"2" (flatten)"2" (hide 2)"2" (typepred "FP!1" )"2" (expand "finite_partition?" )"2" (flatten)"2" (hide -1)"2" (expand "is_finite" (-1 1))"2" (skosimp)"2" (inst 1 "N!1" "f!1" )"1" (hide (-2 -3))"1" expand "injective?" )"1" (grind) nil nil ))nil ))nil )"2" (skosimp*)"2" "1" expand "every" )"1" (inst?) nil nil ))nil )"2" expand "nonzero_elts" )"2" expand "restrict" )"2" assert )"2" (inst?) nil nil ))nil ))nil ))nil )"3" expand "nonzero_elts" )"3" expand "restrict" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" convergence_set "sigma_set/" )"bool" countable_convergence "sigma_set/" )"setof[T]" class_equation_scaf nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil countable_props "sets_aux/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"set[T]" convergence_set "sigma_set/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"R" restrict nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"finite_partition[T]" class_equation_scafnil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"bool" reals nil )"bool" functions nil )"boolean" notequal nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"setof[T]" class_equation_scaf nil )"bool" sets nil ))nil ))nil 3526051917"" (measure-induct+ "card(FP)" "FP" )"1" (inst -1 "rest(x!1)" )"1" (prop)"1" (lemma "choose_rest[setof[T]]" )"1" (inst?)"1" (expand "nonempty?" )"1" (assert )"1" (rewrite "add_as_union" )"1" "ZZ" "restrict[setof[T], finite_set[T], boolean](x!1)" )"1" (replace -1 2)"1" (lemma "sigma_set.sigma_disjoint_union" )"1" "rest(x!1)" "singleton(choose(x!1))" "card" )"1" (prop)"1" (replace -4 -1 rl)"1" case "ZZ = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), ") "1" replace -1 -2 rl)"1" replace -2 2)"1" "card_rest_aux" )"1" "x!1" )"1" expand "nonempty?" )"1" "1" assert )"1" "1" rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace "1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace "1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" "2" "choose(x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -2 -1 rl)"2" "2" replace -1 1 rl)"2" "2" "2" "2" "1" expand *"restrict" "union" "member" )"1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand *"restrict" "union" "member" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" expand "disjoint?" )"2" expand "empty?" 1)"2" "2" expand "member" )"2" expand "intersection" )"2" "2" expand "member" )"2" expand "restrict" )"2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (expand "convergent?" )"2" "1" rewrite "finite_countable" )"1" "1" "finite_union[finite_set[T]]" )"1" case "nonzero_elts[finite_set[T]] ") "1" replace -1)"1" "1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "convergent?" )"2" "2" "2" case "nonzero_elts(card[T], ") "1" "1" "finite_union[finite_set[T]]" )"1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-2 -3 3))"3" (skosimp*)"3" "1" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (lemma "rest_empty_lem[setof[T]]" )"2" (inst -1 "x!1" )"2" (assert )"2" (lemma "card_Union_rest" )"2" (inst -1 "x!1" )"2" (expand "nonempty?" )"2" "Union(rest(x!1)) = emptyset" )"1" (rewrite "union_commutative" )"1" (rewrite "union_empty" )"1" (replaces -2)"1" "1" "CC" "card(choose(x!1))" )"1" "1" expand "CC" )"1" "restrict[setof[T], finite_set[T], boolean] " "1" rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace -1)"1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace "1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" "2" "choose(x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "nonempty?" )"3" nil nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand *"restrict" "extend" )"1" nil nil ))nil )"2" expand *"restrict" "extend" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "1" expand "singleton" )"1" "x!1" )"1" expand "finite_partition?" )"1" "1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" (decompose-equality 1)"2" (iff)"2" "1" expand "Union" )"1" "1" "a!1" )"1" (grind) nil nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (inst?)"1" (assert ) nil nil )"2" (typepred "A!1" )"2" (lemma "rest_member[setof[T]]" )"2" (inst -1 "x!1" "A!1" )"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" "ZZ" "restrict[setof[T], finite_set[T], boolean](x!1)" :hide?nil )"4" "ZZ = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), ") "1" (lemma "card_disj_union[finite_set[T]]" )"1" "restrict[setof[T], finite_set[T], boolean](rest(x!1))" "singleton(choose(x!1))" )"1" (prop)"1" (replaces -1)"1" (lemma "nonempty_card[finite_set[T]]" )"1" (inst -1 "singleton(choose(x!1))" )"1" (prop)"1" (assert ) nil nil )"2" (hide-all-but (-3 2))"2" expand "nonempty?" 1)"2" expand "empty?" )"2" "choose(x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" (expand "disjoint?" )"2" (expand "empty?" )"2" (skosimp*)"2" (expand "member" )"2" expand "intersection" )"2" expand "member" )"2" expand "restrict" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" (lemma "finite_singleton[(x!1)]" )"2" (inst?)"2" (expand "is_finite" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 1 rl)"2" (hide (-1 -3 2))"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (expand * "union" "member" "restrict" )"1" (prop)"1" (expand "singleton" )"1" expand "rest" )"1" "1" expand "remove" )"1" "1" (assert ) nil nil )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "union" "member" "restrict" )"2" (prop)"1" (lemma "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" expand "nonempty?" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -3 2))"3" (skosimp*)"3" (prop)"1" (hide (-2 -3))"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" (expand "every" )"1" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3))"2" (expand "singleton" )"2" (lemma "choose_member[setof[T]]" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "x!1" )"2" (expand "finite_partition?" )"2" (prop)"1" (expand "partition?" )"1" (skosimp*)"1" (typepred "a!1" "b!1" )"1" (lemma "rest_member[setof[T]]" )"1" (copy -1)"1" (inst -1 "x!1" "a!1" )"1" (inst -2 "x!1" "b!1" )"1" (expand "member" )"1" "a!1" "b!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "finite_rest" ) nil nil )"3" (expand "every" )"3" (skosimp*)"3" (lemma "rest_member[setof[T]]" )"3" (inst -1 "x!1" "x!2" )"3" (expand "member" )"3" (inst -4 "x!2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "card_partition_TCC2" ) nil nil )) nil )"3" (hide 2) (("3" (rewrite "card_rest_aux_TCC1" ) nil nil )) nil )"4" (hide 2)"4" (skosimp*)"4" (lemma "card_partition_TCC1" )"4" (inst?) (("4" (assert ) (("4" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"5" (hide 2)"5" (typepred "FP!1" )"5" (expand "finite_partition?" )"5" (flatten)"5" (hide (-1 -3))"5" (expand * "is_finite" "restrict" )"5" (skosimp)"5" (inst 1 "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (prop)"1" (typepred "FP!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (propax) nil nil )) nil )"3" (expand "restrict" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setof[T]" class_equation_scaf nil )"finite_partition[T]" class_equation_scafnil )nil class_equation_scaf nil )nil class_equation_scaf nil )nil class_equation_scaf nil )"set" sets nil )"finite_partition[T]" class_equation_scafnil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )nil finite_sets nil )"setof[T]" class_equation_scaf nil )"(rest(x!1))" class_equation_scaf nil )nil lagrange_scaf "algebra/" )"set" sets nil )nil sets_lemmas nil )"{n: nat | n = Card(choose(x!1))}" nil )"(nonempty?[T])" nil )"finite_set[T]" nil )"finite_set[S]" nil )"bool" booleans nil )"R" extend nil )nil sets_lemmas nil )"finite_set" finite_sets nil )"finite_set[T]" "finite_sets/" )"finite_set[T]" countable_props"sets_aux/" )"set" sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"(p)" sets nil )nil sets_lemmas nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"(nonempty?)" sets nil )"bool" sets nil )"(singleton?)" sets nil )"[bool, bool -> bool]" booleans nil )"set" sets nil )nil sets_lemmas nil )"set" sets nil )"bool" sets nil )nil class_equation_scaf nil )"nonneg_int" nil )"real" reals nil )"bool" countable_convergence "sigma_set/" )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil sigma_set "sigma_set/" )nil finite_sets nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )"real" sigma "reals/" )nil nat_types nil )"[below[card(X)] -> (X)]" "sigma_set/" )"nat" sigma "reals/" )"T3" function_props nil )"even_int" integersnil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma_countable "sigma_set/" )nil countable_props "sets_aux/" )"set[T]" convergence_set "sigma_set/" )nil finite_sets nil )nil finite_sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"setof[T]" class_equation_scaf nil )nil sigma_set "sigma_set/" )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(rest[setof[T]](x!1))" class_equation_scafnil )"(rest[setof[T]](x!1))" class_equation_scafnil )"bool" lagrange_scaf "algebra/" )"(rest[setof[T]](x!1))" class_equation_scafnil )"real" sigma_set "sigma_set/" )"bool" convergence_set "sigma_set/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"set" sets nil )"bool" sets nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"R" restrict nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets 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 lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil class_equation_scaf nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3527412900"" (skosimp*)"" (lemma "card_partition_TCC2" )"" (inst?)"" (assert )"" (skosimp*) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil class_equation_scaf nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil class_equation_scaf nil ))nil ))nil 3527412900"" (measure-induct+ "card(FP)" "FP" )"1" (skosimp*)"1" (inst -1 "rest(x!1)" )"1" (inst -1 "n!1" )"1" (prop)"1" (hide (-2 -3))"1" (lemma "sigma_set.sigma_disjoint_union" )"1" "rest(x!1)" "singleton(choose(x!1))" "card" )"1" (prop)"1" "restrict[setof[T], finite_set[T], boolean](x!1) = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), singleton(choose(x!1)))" "1" (replace -1 1)"1" (hide -1)"1" "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1))" "1" (rewrite "card_def" )"1" "Card(choose(x!1))" )"1" (rewrite "closed_plus" ) nil nil ))nil ))nil )"2" (hide (-1 2))"2" rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace -1)"1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace -2)"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" expand "bijective?" )"2" "1" expand "injective?" )"1" "1" "x1!1" "x2!1" )"1" expand "singleton" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "choose(x!1)" )"1" expand "singleton" )"1" nil nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" "x!1" )"3" expand "finite_partition?" )"3" "3" expand "every" )"3" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 2))"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" expand * "restrict" "union" "member" )"1" "1" (grind) nil nil ))nil ))nil )"2" expand * "restrict" "union" "member" )"2" "1" (grind) nil nil )"2" expand "singleton" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (expand "nonempty?" )"2" (expand "disjoint?" )"2" (expand "empty?" 1)"2" (skosimp*)"2" expand "member" )"2" expand "intersection" )"2" "2" expand "member" )"2" expand "restrict" )"2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (expand "convergent?" )"2" (prop)"1" (rewrite "finite_countable" )"1" (hide 2)"1" (lemma "finite_union[finite_set[T]]" )"1" case "nonzero_elts[finite_set[T]] ") "1" replace -1)"1" "1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" (prop) nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "convergent?" )"2" (flatten)"2" (hide 2)"2" case "nonzero_elts(card[T], ") "1" "1" "finite_union[finite_set[T]]" )"1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" (prop) nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" (skosimp*)"3" (prop)"1" (hide (-2 -3))"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" "1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3))"2" (expand "singleton" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3)"2" (lemma "sigma_set.sigma_disjoint_union" )"2" "rest(x!1)" "singleton(choose(x!1))" "card" )"1" (prop)"1" "restrict[setof[T], finite_set[T], boolean](x!1) = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), singleton(choose(x!1)))" "1" (replace -1 1)"1" (hide -1)"1" "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1))" "1" (rewrite "card_def" )"1" "Card(choose(x!1))" )"1" (rewrite "closed_plus" ) nil nil ))nil ))nil )"2" (hide (-1 -2 2))"2" rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace -1)"1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace -2)"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" expand "bijective?" )"2" "1" expand "injective?" )"1" "1" "x1!1" "x2!1" )"1" expand "singleton" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "choose(x!1)" )"1" expand "singleton" )"1" nil nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -2 2))"3" "x!1" )"3" expand "finite_partition?" )"3" "3" expand "every" )"3" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 -3 2))"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" expand * "restrict" "union" "member" )"1" "1" (grind) nil nil ))nil ))nil )"2" expand * "restrict" "union" "member" )"2" "1" (grind) nil nil )"2" expand "singleton" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 2))"2" (expand "nonempty?" )"2" (expand "disjoint?" )"2" (expand "empty?" 1)"2" (skosimp*)"2" expand "member" )"2" expand "intersection" )"2" "2" expand "member" )"2" expand "restrict" )"2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 2))"2" (expand "convergent?" )"2" (prop)"1" (rewrite "finite_countable" )"1" (hide 2)"1" (lemma "finite_union[finite_set[T]]" )"1" case "nonzero_elts[finite_set[T]] ") "1" replace -1)"1" "1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" (prop) nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "convergent?" )"2" (flatten)"2" (hide 2)"2" case "nonzero_elts(card[T], ") "1" "1" "finite_union[finite_set[T]]" )"1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" (prop) nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -2 2))"3" (skosimp*)"3" (prop)"1" (hide (-2 -3))"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" "1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3))"2" (expand "singleton" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 1)"3" (skosimp*)"3" (inst -1 "A!1" )"3" (hide 2)"3" (typepred "A!1" )"3" (lemma "rest_member[setof[T]]" )"3" (inst -1 "x!1" "A!1" )"3" (expand "member" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 1)"4" (skosimp*)"4" (inst -1 "A!1" )"4" (hide 2)"4" (typepred "A!1" )"4" (lemma "rest_member[setof[T]]" )"4" (inst -1 "x!1" "A!1" )"4" (expand "member" )"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide -1)"5" (expand "nonempty?" )"5" (lemma "rest_empty_lem[setof[T]]" )"5" (inst -1 "x!1" )"5" (assert )"5" (replace -1 1)"5" "restrict[setof[T], finite_set[T], boolean] " "1" "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1))" "1" (typepred "card(choose(x!1))" )"1" "1" "Card(choose(x!1))" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 2 3))"2" rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace -1)"1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace -2)"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" "2" "choose(x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "nonempty?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" "x!1" )"3" expand "finite_partition?" )"3" "3" expand "every" )"3" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (decompose-equality 1)"2" "2" "1" expand * "restrict" "extend" )"1" (prop) nil nil ))nil )"2" expand * "restrict" "extend" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" "1" expand "singleton" )"1" "x!1" )"1" expand "finite_partition?" )"1" "1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide -1)"6" (expand "nonempty?" )"6" (lemma "rest_empty_lem[setof[T]]" )"6" (inst -1 "x!1" )"6" (assert )"6" (replace -1 1)"6" "restrict[setof[T], finite_set[T], boolean] " "1" "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1))" "1" (typepred "card(choose(x!1))" )"1" "1" "Card(choose(x!1))" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 2 3))"2" rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace -1)"1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace -2)"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" "2" "choose(x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "nonempty?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" "x!1" )"3" expand "finite_partition?" )"3" "3" expand "every" )"3" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (decompose-equality 1)"2" "2" "1" expand * "restrict" "extend" )"1" (prop) nil nil ))nil )"2" expand * "restrict" "extend" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" "1" expand "singleton" )"1" "x!1" )"1" expand "finite_partition?" )"1" "1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide (-1 1))"7" "restrict[setof[T], finite_set[T], boolean](x!1)= union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), singleton(choose(x!1)))" "1" (lemma "card_disj_union[finite_set[T]]" )"1" "restrict[setof[T], finite_set[T], boolean](rest(x!1))" "singleton(choose(x!1))" )"1" (prop)"1" (replaces -1)"1" (lemma "nonempty_card[finite_set[T]]" )"1" (inst -1 "singleton(choose(x!1))" )"1" (prop)"1" (assert ) nil nil )"2" "2" expand "nonempty?" 1)"2" expand "empty?" )"2" "choose(x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "disjoint?" )"2" (expand "empty?" )"2" (skosimp*)"2" expand "member" )"2" expand "intersection" )"2" expand "member" )"2" expand "restrict" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "finite_singleton[(x!1)]" )"2" (inst?)"2" (expand "is_finite" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (expand * "union" "member" "restrict" )"1" (prop)"1" (expand "singleton" )"1" expand "rest" )"1" "1" expand "remove" )"1" "1" (assert ) nil nil )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "union" "member" "restrict" )"2" (prop)"1" (lemma "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" expand "nonempty?" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" (skosimp*)"3" (prop)"1" (hide -2)"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "singleton" )"2" (lemma "choose_member[setof[T]]" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" (hide (-1 1))"8" "restrict[setof[T], finite_set[T], boolean](x!1)= union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), singleton(choose(x!1)))" "1" (lemma "card_disj_union[finite_set[T]]" )"1" "restrict[setof[T], finite_set[T], boolean](rest(x!1))" "singleton(choose(x!1))" )"1" (prop)"1" (replaces -1)"1" (lemma "nonempty_card[finite_set[T]]" )"1" (inst -1 "singleton(choose(x!1))" )"1" (prop)"1" (assert ) nil nil )"2" "2" expand "nonempty?" 1)"2" expand "empty?" )"2" "choose(x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "disjoint?" )"2" (expand "empty?" )"2" (skosimp*)"2" expand "member" )"2" expand "intersection" )"2" expand "member" )"2" expand "restrict" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "finite_singleton[(x!1)]" )"2" (inst?)"2" (expand "is_finite" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (expand * "union" "member" "restrict" )"1" (prop)"1" (expand "singleton" )"1" expand "rest" )"1" "1" expand "remove" )"1" "1" (assert ) nil nil )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "union" "member" "restrict" )"2" (prop)"1" (lemma "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" expand "nonempty?" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" (skosimp*)"3" (prop)"1" (hide -2)"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "singleton" )"2" (lemma "choose_member[setof[T]]" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (typepred "x!1" )"2" (expand "finite_partition?" )"2" (prop)"1" (expand "partition?" )"1" (skosimp*)"1" (typepred "a!1" "b!1" )"1" (lemma "rest_member[setof[T]]" )"1" (copy -1)"1" (inst -1 "x!1" "a!1" )"1" (inst -2 "x!1" "b!1" )"1" expand "member" )"1" "a!1" "b!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "finite_rest" ) nil nil )"3" (expand "every" )"3" (skosimp*)"3" (lemma "rest_member[setof[T]]" )"3" (inst -1 "x!1" "x!2" )"3" (expand "member" )"3" (inst -4 "x!2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-2 -3 1))"2" (lemma "divide_sigma_TCC1" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (hide-all-but (-1 -2 1))"3" (lemma "divide_sigma_TCC1" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil )"4" (hide (-1 -2 2))"4" (skosimp*)"4" (typepred "y!1" )"4" (expand "finite_partition?" )"4" (flatten)"4" (expand "every" ) (("4" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"5" (hide (-1 -2 2))"5" (skosimp*)"5" (typepred "y!1" )"5" (expand "finite_partition?" )"5" (flatten)"5" (expand "every" ) (("5" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"6" (hide (-1 2))"6" (typepred "x!1" )"6" (expand "finite_partition?" )"6" (flatten)"6" (hide (-1 -3))"6" (expand * "is_finite" "restrict" )"6" (skosimp)"6" (inst 1 "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (prop)"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (propax) nil nil )) nil )"3" (expand "restrict" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide (1 3))"7" (typepred "x!1" )"7" (expand "finite_partition?" )"7" (flatten)"7" (hide (-1 -3))"7" (expand * "is_finite" "restrict" )"7" (skosimp)"7" (inst 1 "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (prop)"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (propax) nil nil )) nil )"3" (expand "restrict" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" (hide (-1 2))"8" (lemma "divide_sigma_TCC1" )"8" (inst?) (("8" (assert ) nil nil )) nil )) nil ))nil )"9" (hide 2)"9" (lemma "divide_sigma_TCC1" )"9" (inst?) (("9" (assert ) nil nil )) nil )) nil ))nil )"10" (hide (1 3))"10" (typepred "FP!1" )"10" (expand "finite_partition?" )"10" (flatten)"10" (expand "every" ) (("10" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"11" (hide 2)"11" (typepred "FP!1" )"11" (expand "finite_partition?" )"11" (flatten)"11" (expand "every" ) (("11" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"12" (hide 2)"12" (typepred "FP!1" )"12" (expand "finite_partition?" )"12" (flatten)"12" (hide (-1 -3))"12" (expand * "is_finite" "restrict" )"12" (skosimp)"12" (inst 1 "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (prop)"1" (typepred "FP!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (propax) nil nil )) nil )"3" (expand "restrict" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setof[T]" class_equation_scaf nil )"finite_partition[T]" class_equation_scafnil )"setof[T]" class_equation_scaf nil )"setof[T]" class_equation_scaf nil )nil class_equation_scaf nil )"(rest[setof[T]](x!1))" class_equation_scafnil )"bool" lagrange_scaf "algebra/" )"(rest[setof[T]](x!1))" class_equation_scafnil )"(rest[setof[T]](x!1))" class_equation_scafnil )"setof[T]" class_equation_scaf nil )"setof[T]" class_equation_scaf nil )nil finite_sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )nil sets_lemmas nil )"R" extend nil )"bool" booleans nil )"finite_set[S]" nil )"(strict_total_order?[real])" real_props nil )"finite_set[T]" nil )"(nonempty?[T])" nil )nil sets_lemmas nil )"(rest(x!1))" class_equation_scaf nil )"(rest(x!1))" class_equation_scaf nil )"(total_order?[real])" nil )"real" reals nil )nil integers nil )"setof[T]" class_equation_scaf nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"bool" sets nil )"(singleton?)" sets nil )"(p)" sets nil )"[bool, bool -> bool]" booleans nil )"set" sets nil )"bool" sets nil )"set" sets nil )nil sets_lemmas nil )nil countable_props "sets_aux/" )nil sigma_countable "sigma_set/" )"bool" sets nil )nil finite_sets nil )"even_int" integersnil )"T3" function_props nil )"nonneg_int" nil )"nat" sigma "reals/" )"[below[card(X)] -> (X)]" "sigma_set/" )nil nat_types nil )"real" sigma "reals/" )nil finite_sets nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )nil sigma_set "sigma_set/" )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"bool" countable_convergence "sigma_set/" )nil finite_sets nil )nil rationals nil )nil rationals nil )NOT const-decl "[bool -> bool]" booleans nil )"set" sets nil )"set[T]" convergence_set "sigma_set/" )nil finite_sets nil )nil finite_sets nil )nil sets_lemmas nil )"setof[T]" class_equation_scaf nil )nil sigma_set "sigma_set/" )"finite_partition[T]" class_equation_scafnil )"set" sets nil )"real" sigma_set "sigma_set/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" divides nil )"bool" sets nil )"bool" convergence_set "sigma_set/" )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"R" restrict nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets 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 lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil class_equation_scaf nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil ))nil 3527554283"" (measure-induct+ "card(FP)" "FP" )"1" (skosimp*)"1" (inst -1 "rest(x!1)" )"1" (inst -1 "n!1" )"1" (prop)"1" (lemma "sigma_set.sigma_disjoint_union" )"1" "rest(x!1)" "singleton(choose(x!1))" "card" )"1" (prop)"1" "restrict[setof[T], finite_set[T], boolean](x!1) = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), singleton(choose(x!1)))" "1" (replace -1 1)"1" (hide -1)"1" "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1))" "1" (lemma "divides_sum" )"1" (inst?)"1" assert )"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "divide_sigma_TCC2" )"2" "rest[setof[T]](x!1)" "n!1" )"1" "1" "1" "1" "A!1" )"1" "1" "A!1" )"1" "rest_member[setof[T]]" )"1" "x!1" "A!1" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "A!1" )"2" "2" "A!1" )"2" "rest_member[setof[T]]" )"2" "x!1" "A!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "nonempty?" )"3" rewrite "sigma_countable" )"1" expand "sigma" )"1" "1" (assert ) nil nil )"2" "2" expand "empty?" )"2" "2" expand *"member" "restrict" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "empty?" )"3" "3" expand *"member" "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_rest[setof[T]]" )"3" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "nonempty?" )"4" rewrite "sigma_countable" )"1" expand "sigma" )"1" "1" (assert ) nil nil )"2" "2" expand "empty?" )"2" "2" expand *"member" "restrict" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "empty?" )"3" "3" expand *"member" "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" rewrite "finite_countable" )"3" "3" "finite_rest[setof[T]]" )"3" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" "x!1" )"2" expand "finite_partition?" )"2" "1" expand "partition?" )"1" "1" "a!1" "b!1" )"1" "rest_member[setof[T]]" )"1" "1" "x!1" "a!1" )"1" "x!1" "b!1" )"1" expand "member" )"1" "a!1" "b!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "finite_rest" )nil nil )"3" expand "every" )"3" "3" "rest_member[setof[T]]" )"3" "x!1" "x!2" )"3" expand "member" )"3" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3 2))"2" (rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace -1)"1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace -2)"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" expand "bijective?" )"2" "1" expand "injective?" )"1" "1" "x1!1" "x2!1" )"1" expand "singleton" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "choose(x!1)" )"1" expand "singleton" )"1" nil nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -3 2))"3" (hide (-1 2))"3" "x!1" )"3" expand "finite_partition?" )"3" "3" expand "every" )"3" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 -4 2))"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (expand * "restrict" "union" "member" )"1" "1" (grind) nil nil ))nil ))nil )"2" (expand * "restrict" "union" "member" )"2" "1" (grind) nil nil )"2" expand "singleton" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3 2))"2" (expand "nonempty?" )"2" (expand "disjoint?" )"2" (expand "empty?" 1)"2" (skosimp*)"2" (expand "member" )"2" expand "intersection" )"2" "2" expand "member" )"2" expand "restrict" )"2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3 2))"2" (expand "convergent?" )"2" (prop)"1" (rewrite "finite_countable" )"1" (hide 2)"1" (lemma "finite_union[finite_set[T]]" )"1" case "nonzero_elts[finite_set[T]] ") "1" replace -1)"1" "1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" (prop) nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "convergent?" )"2" (flatten)"2" (hide 2)"2" case "nonzero_elts(card[T], ") "1" "1" "finite_union[finite_set[T]]" )"1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" (prop) nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -3 2))"3" (skosimp*)"3" (prop)"1" (hide (-2 -3))"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3))"2" (expand "singleton" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (lemma "rest_empty_lem[setof[T]]" )"2" (inst -1 "x!1" )"2" (assert )"2" (replace -1 2)"2" "restrict[setof[T], finite_set[T], boolean] " "1" "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1))" "1" (inst?) (("1" (assert ) nil nil )) nil )"2" (hide (-1 -3 2 3))"2" (rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace -1)"1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace -2)"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" "2" "choose(x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "nonempty?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -3 3))"3" (typepred "x!1" )"3" expand "finite_partition?" )"3" "3" expand "every" )"3" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -3 3))"2" (decompose-equality 1)"2" (iff)"2" "1" expand * "restrict" "extend" )"1" (prop) nil nil ))nil )"2" expand * "restrict" "extend" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 -3 3))"3" (skosimp*)"3" (prop)"1" expand "singleton" )"1" "x!1" )"1" expand "finite_partition?" )"1" "1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (lemma "rest_member[setof[T]]" )"3" (inst -1 "x!1" "A!1" )"3" (expand "member" ) (("3" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (hide (-2 2))"4" "restrict[setof[T], finite_set[T], boolean](x!1)= union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), singleton(choose(x!1)))" "1" (lemma "card_disj_union[finite_set[T]]" )"1" "restrict[setof[T], finite_set[T], boolean](rest(x!1))" "singleton(choose(x!1))" )"1" (prop)"1" (replaces -1)"1" (lemma "nonempty_card[finite_set[T]]" )"1" (inst -1 "singleton(choose(x!1))" )"1" (prop)"1" (assert ) nil nil )"2" "2" expand "nonempty?" 1)"2" expand "empty?" )"2" "choose(x!1)" )"1" expand "member" )"1" expand "singleton" )"1" (propax) nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "disjoint?" )"2" (expand "empty?" )"2" (skosimp*)"2" expand "member" )"2" expand "intersection" )"2" expand "member" )"2" expand "restrict" )"2" "2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "finite_singleton[(x!1)]" )"2" (inst?)"2" (expand "is_finite" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (expand * "union" "member" "restrict" )"1" (prop)"1" (expand "singleton" )"1" expand "rest" )"1" "1" expand "remove" )"1" "1" (assert ) nil nil )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "union" "member" "restrict" )"2" (prop)"1" (lemma "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "singleton" )"2" "choose_member[setof[T]]" )"2" "2" expand "nonempty?" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" (skosimp*)"3" (prop)"1" (hide -2)"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "singleton" )"2" (lemma "choose_member[setof[T]]" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-2 2))"2" (typepred "x!1" )"2" (expand "finite_partition?" )"2" (prop)"1" (expand "partition?" )"1" (skosimp*)"1" (typepred "a!1" "b!1" )"1" (lemma "rest_member[setof[T]]" )"1" (copy -1)"1" (inst -1 "x!1" "a!1" )"1" (inst -2 "x!1" "b!1" )"1" expand "member" )"1" "a!1" "b!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "finite_rest" ) nil nil )"3" (expand "every" )"3" (skosimp*)"3" (lemma "rest_member[setof[T]]" )"3" (inst -1 "x!1" "x!2" )"3" (expand "member" )"3" (inst -4 "x!2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-3 -4 2))"2" (lemma "divide_sigma_TCC2" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (hide (-3 -4 2))"3" (lemma "divide_sigma_TCC2" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil )"4" (hide (-3 -4 2))"4" (lemma "divide_sigma_TCC1" )"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil )"5" (hide (-1 -3 2))"5" (skosimp*)"5" (typepred "y!1" )"5" (expand "finite_partition?" )"5" (flatten)"5" (expand "every" ) (("5" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"6" (hide (-1 -3 2))"6" (skosimp*)"6" (typepred "y!1" )"6" (expand "finite_partition?" )"6" (flatten)"6" (expand "every" ) (("6" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"7" (hide (-1 2))"7" (typepred "x!1" )"7" (expand "finite_partition?" )"7" (flatten)"7" (hide (-1 -3))"7" (expand * "is_finite" "restrict" )"7" (skosimp)"7" (inst 1 "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (prop)"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (propax) nil nil )) nil )"3" (expand "restrict" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" (hide (1 3))"8" (typepred "x!1" )"8" (expand "finite_partition?" )"8" (flatten)"8" (hide (-1 -3))"8" (expand * "is_finite" "restrict" )"8" (skosimp)"8" (inst 1 "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (prop)"1" (typepred "x!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (propax) nil nil )) nil )"3" (expand "restrict" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" (hide 2)"9" (lemma "divide_sigma_TCC2" )"9" (inst?) (("9" (assert ) (("9" (prop) nil nil )) nil )) nil ))nil ))nil )"10" (hide 2)"10" (rewrite "card_partition_TCC2" )"10" (skosimp*)"10" (inst?) (("10" (assert ) nil nil )) nil )) nil ))nil ))nil )"11" (hide 2)"11" (skosimp*)"11" (typepred "FP!1" )"11" (expand "finite_partition?" )"11" (flatten)"11" (expand "every" ) (("11" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"12" (hide 2)"12" (typepred "FP!1" )"12" (expand "finite_partition?" )"12" (flatten)"12" (expand "every" ) (("12" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"13" (hide 2)"13" (typepred "FP!1" )"13" (expand "finite_partition?" )"13" (flatten)"13" (hide (-1 -3))"13" (expand * "is_finite" "restrict" )"13" (skosimp)"13" (inst 1 "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (prop)"1" (typepred "FP!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" expand "every" )"1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (propax) nil nil )) nil )"3" (expand "restrict" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setof[T]" class_equation_scaf nil )"finite_partition[T]" class_equation_scafnil )nil class_equation_scaf nil )"setof[T]" class_equation_scaf nil )"setof[T]" class_equation_scaf nil )nil class_equation_scaf nil )"(rest[setof[T]](x!1))" class_equation_scafnil )"(rest[setof[T]](x!1))" class_equation_scafnil )"(rest[setof[T]](x!1))" class_equation_scafnil )"setof[T]" class_equation_scaf nil )nil finite_sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"(rest(x!1))" class_equation_scaf nil )nil sets_lemmas nil )"finite_set[T]" nil )"(nonempty?[T])" nil )"(strict_total_order?[real])" real_props nil )"finite_set[S]" nil )"bool" booleans nil )"R" extend nil )nil sets_lemmas nil )nil sigma_set "sigma_set/" )"setof[T]" class_equation_scaf nil )nil finite_sets nil )"set[T]" convergence_set "sigma_set/" )"set" sets nil )"real" reals nil )nil class_equation_scaf nil )"(rest[setof[T]](x!1))" class_equation_scafnil )"(rest[setof[T]](x!1))" class_equation_scafnil )"bool" lagrange_scaf "algebra/" )"(rest[setof[T]](x!1))" class_equation_scafnil )nil sets_lemmas nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"(rest[setof[T]](x!1))" class_equation_scafnil )"(rest[setof[T]](x!1))" class_equation_scafnil )nil countable_props "sets_aux/" )nil finite_sets nil )nil nat_types nil )"bool" functions nil )"bool" sets nil )"real" sigma_countable "sigma_set/" )"bool" sets nil )nil sigma_set "sigma_set/" )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"bool" countable_convergence "sigma_set/" )nil divides nil )nil finite_sets nil )nil finite_sets nil )"bool" functions nil )"bool" functions nil )nil finite_sets nil )"real" sigma "reals/" )"[below[card(X)] -> (X)]" "sigma_set/" )"nat" sigma "reals/" )"nonneg_int" nil )"T3" function_props nil )"even_int" integersnil )nil finite_sets nil )nil sigma_countable "sigma_set/" )nil sets_lemmas nil )"set" sets nil )"bool" sets nil )"set" sets nil )"[bool, bool -> bool]" booleans nil )"(p)" sets nil )"(singleton?)" sets nil )"bool" sets nil )"non_empty_finite_set[T]" countable_props "sets_aux/" )"finite_partition[T]" class_equation_scafnil )"set" sets nil )"real" sigma_set "sigma_set/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" divides nil )"bool" convergence_set "sigma_set/" )"boolean" notequal nil )"bool" sets nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"R" restrict nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets 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 lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil class_equation_scaf nil )nil measure_induction nil )"bool" orders nil )nil defined_types 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.831Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
