| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 397 kB |
|
Impressum class_equation_scaf.prfSprache: Lisp |
|||||||||||||||
|
(class_equation_scaf (card_rest_aux_TCC1 0 (card_rest_aux_TCC1-1 nil 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) ((finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil class_equation_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Union_finite formula-decl nil finite_sets_of_sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)) nil)) (card_rest_aux_TCC2 0 (card_rest_aux_TCC2-1 nil 3526046475 ("" (skosimp*) (("" (typepred "FP!1") (("" (expand "finite_partition?") (("" (flatten) (("" (hide (-1 -2)) (("" (expand "every") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil class_equation_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (every const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil)) nil)) (card_rest_aux_TCC3 0 (card_rest_aux_TCC3-1 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" (inst -1 "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) ((finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil class_equation_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (set type-eq-decl nil sets nil) (rest const-decl "set" sets nil) (every const-decl "bool" sets nil) (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (x!1 skolem-const-decl "(rest[setof[T]](FP!1))" class_equation_scaf nil) (rest_member formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_rest judgement-tcc nil finite_sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union_finite formula-decl nil finite_sets_of_sets nil)) nil)) (card_rest_aux 0 (card_rest_aux-1 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") (("" (flatten) (("" (expand "Union") (("" (skosimp*) (("" (inst -1 "a!1" "choose(FP!1)") (("1" (prop) (("1" (typepred "a!1") (("1" (replaces -2) (("1" (hide (-2 -3 -4 -5)) (("1" (lemma "choose_not_member[setof[T]]") (("1" (inst?) (("1" (expand "nonempty?") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a!1") (("2" (lemma "rest_member[setof[T]]") (("2" (inst -1 "FP!1" "a!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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil class_equation_scaf nil) (card_Union_rest formula-decl nil lagrange_scaf "algebra/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (card_disj_union formula-decl nil finite_sets nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (Union const-decl "set" sets nil) (rest const-decl "set" sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (disjoint? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (rest_member formula-decl nil sets_lemmas nil) (choose_not_member formula-decl nil sets_lemmas nil) (a!1 skolem-const-decl "(rest(FP!1))" class_equation_scaf nil) (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (partition? const-decl "bool" lagrange_scaf "algebra/") (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (card_partition_TCC1 0 (card_partition_TCC1-1 nil 3526042692 ("" (skosimp*) (("" (typepred "A!1") (("" (typepred "FP!1") (("" (expand "finite_partition?") (("" (flatten) (("" (expand "every") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil class_equation_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (every const-decl "bool" sets nil)) nil)) (card_partition_TCC2 0 (card_partition_TCC2-1 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" (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)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_set "sigma_set/") (convergent? const-decl "bool" countable_convergence "sigma_set/") (x!1 skolem-const-decl "setof[T]" class_equation_scaf nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil class_equation_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (nonzero_elts const-decl "set[T]" convergence_set "sigma_set/") (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (restrict const-decl "R" restrict nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (injective? const-decl "bool" functions nil) (/= const-decl "boolean" notequal nil) (nonempty? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (x!1 skolem-const-decl "setof[T]" class_equation_scaf nil) (every const-decl "bool" sets nil)) nil)) (card_partition 0 (card_partition-1 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" (name "ZZ" "restrict[setof[T], finite_set[T], boolean](x!1)") (("1" (replace -1 2) (("1" (lemma "sigma_set.sigma_disjoint_union") (("1" (inst -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)), singleton(choose(x!1)))") (("1" (replace -1 -2 rl) (("1" (replace -2 2) (("1" (lemma "card_rest_aux") (("1" (inst -1 "x!1") (("1" (expand "nonempty?") (("1" (replaces -1) (("1" (assert) (("1" (hide-all-but 2) (("1" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (grind) (("2" (inst 1 "choose(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -4 -5 3)) (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand* "restrict" "union" "member") (("1" (prop) (("1" (hide (1 3)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand* "restrict" "union" "member") (("2" (prop) (("2" (hide (1 3)) (("2" (grind) 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" (skosimp*) (("2" (expand "member") (("2" (expand "intersection") (("2" (flatten) (("2" (expand "member") (("2" (expand "restrict") (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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" (prop) (("1" (rewrite "finite_countable") (("1" (hide 2) (("1" (lemma "finite_union[finite_set[T]]") (("1" (case "nonzero_elts[finite_set[T]] (card[T], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replace -1) (("1" (hide -1) (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5 2)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide (2 3)) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -7) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -6) (("2" (inst?) (("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], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replaces -1) (("1" (lemma "finite_union[finite_set[T]]") (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5 2)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide (2 3)) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -6) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -5) (("2" (inst?) (("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" (prop) (("1" (hide (-2 -3 -4)) (("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 -4)) (("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)) 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" (case-replace "Union(rest(x!1)) = emptyset") (("1" (rewrite "union_commutative") (("1" (rewrite "union_empty") (("1" (replaces -2) (("1" (hide (-1 -3 -4 1)) (("1" (name-replace "CC" "card(choose(x!1))") (("1" (replaces -1) (("1" (expand "CC") (("1" (case-replace "restrict[setof[T], finite_set[T], boolean] (extend[setof[T], (x!1), bool, FALSE] (singleton(choose(x!1)))) = singleton(choose(x!1))" :hide? T) (("1" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (grind) (("2" (inst 1 "choose(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil) ("3" (reveal 2) (("3" (expand "nonempty?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand* "restrict" "extend") (("1" (prop) nil nil)) nil) ("2" (expand* "restrict" "extend") (("2" (prop) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (prop) (("1" (expand "singleton") (("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)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "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" (name-replace "ZZ" "restrict[setof[T], finite_set[T], boolean](x!1)" :hide? nil) (("4" (case-replace "ZZ = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), singleton(choose(x!1)))") (("1" (lemma "card_disj_union[finite_set[T]]") (("1" (inst -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" (inst -1 "choose(x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "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" (flatten) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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" (prop) (("1" (expand "remove") (("1" (prop) (("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" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (lemma "choose_member[setof[T]]") (("2" (inst?) (("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" (inst -5 "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) ((x!1 skolem-const-decl "setof[T]" class_equation_scaf nil) (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (card_partition_TCC1 subtype-tcc nil class_equation_scaf nil) (card_rest_aux_TCC1 subtype-tcc nil class_equation_scaf nil) (card_partition_TCC2 subtype-tcc nil class_equation_scaf nil) (rest const-decl "set" sets nil) (x!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty_card formula-decl nil finite_sets nil) (card_disj_union formula-decl nil finite_sets nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (A!1 skolem-const-decl "(rest(x!1))" class_equation_scaf nil) (card_Union_rest formula-decl nil lagrange_scaf "algebra/") (remove const-decl "set" sets nil) (union_commutative formula-decl nil sets_lemmas nil) (CC skolem-const-decl "{n: nat | n = Card(choose(x!1))}" class_equation_scaf nil) (nonempty_extend application-judgement "(nonempty?[T])" extend_set_props nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (union_empty formula-decl nil sets_lemmas nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" finite_sets_inductions "finite_sets/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (emptyset const-decl "set" sets nil) (rest_empty_lem formula-decl nil sets_lemmas nil) (choose_rest formula-decl nil sets_lemmas nil) (choose const-decl "(p)" sets nil) (add_as_union formula-decl nil sets_lemmas nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_props "sets_aux/") (nonempty_union2 application-judgement "(nonempty?)" sets nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (union const-decl "set" sets nil) (choose_not_member formula-decl nil sets_lemmas nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (card_rest_aux formula-decl nil class_equation_scaf nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (convergent? const-decl "bool" countable_convergence "sigma_set/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (sigma_countable formula-decl nil sigma_set "sigma_set/") (finite_singleton judgement-tcc nil finite_sets nil) (every const-decl "bool" sets nil) (member const-decl "bool" sets nil) (Card_bijection formula-decl nil finite_sets nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (card_def formula-decl nil finite_sets nil) (sigma def-decl "real" sigma "reals/") (below type-eq-decl nil nat_types nil) (finite_enumeration const-decl "[below[card(X)] -> (X)]" finite_enumeration "sigma_set/") (sigma_nat application-judgement "nat" sigma "reals/") (O const-decl "T3" function_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_finite formula-decl nil sigma_countable "sigma_set/") (finite_countable judgement-tcc nil countable_props "sets_aux/") (nonzero_elts const-decl "set[T]" convergence_set "sigma_set/") (finite_union judgement-tcc nil finite_sets nil) (finite_rest judgement-tcc nil finite_sets nil) (rest_member formula-decl nil sets_lemmas nil) (choose_member formula-decl nil sets_lemmas nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (sigma_disjoint_union formula-decl nil sigma_set "sigma_set/") (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (b!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (a!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (partition? const-decl "bool" lagrange_scaf "algebra/") (x!2 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (sigma const-decl "real" sigma_set "sigma_set/") (convergent? const-decl "bool" convergence_set "sigma_set/") (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (Union const-decl "set" sets nil) (nonempty? const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil class_equation_scaf nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (divide_sigma_TCC1 0 (divide_sigma_TCC1-1 nil 3527412900 ("" (skosimp*) (("" (lemma "card_partition_TCC2") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((card_partition_TCC2 subtype-tcc nil class_equation_scaf nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil class_equation_scaf nil)) nil)) (divide_sigma_TCC2 0 (divide_sigma_TCC2-1 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" (inst -1 "rest(x!1)" "singleton(choose(x!1))" "card") (("1" (prop) (("1" (case-replace "restrict[setof[T], finite_set[T], boolean](x!1) = union(restrict[setof[T], finite_se :hide? T) (("1" (replace -1 1) (("1" (hide -1) (("1" (case-replace "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1) :hide? T) (("1" (rewrite "card_def") (("1" (typepred "Card(choose(x!1))") (("1" (rewrite "closed_plus") nil nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (expand "nonempty?") (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (expand "bijective?") (("2" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1" "x2!1") (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (inst 1 "choose(x!1)") (("1" (expand "singleton") (("1" (propax) nil nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2)) (("3" (typepred "x!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (expand "every") (("3" (inst -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" (prop) (("1" (grind) nil nil)) nil)) nil) ("2" (expand* "restrict" "union" "member") (("2" (prop) (("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" (flatten) (("2" (expand "member") (("2" (expand "restrict") (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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]] (card[T], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replace -1) (("1" (hide -1) (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil 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 "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -8) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -7) (("2" (inst?) (("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], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replaces -1) (("1" (lemma "finite_union[finite_set[T]]") (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -7) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -6) (("2" (inst?) (("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" (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)) nil) ("2" (hide -3) (("2" (lemma "sigma_set.sigma_disjoint_union") (("2" (inst -1 "rest(x!1)" "singleton(choose(x!1))" "card") (("1" (prop) (("1" (case-replace "restrict[setof[T], finite_set[T], boolean](x!1) = union(restrict[setof[T], finite_se :hide? T) (("1" (replace -1 1) (("1" (hide -1) (("1" (case-replace "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1) :hide? T) (("1" (rewrite "card_def") (("1" (typepred "Card(choose(x!1))") (("1" (rewrite "closed_plus") nil nil)) nil)) nil) ("2" (hide (-1 -2 2)) (("2" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (expand "nonempty?") (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (expand "bijective?") (("2" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1" "x2!1") (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (inst 1 "choose(x!1)") (("1" (expand "singleton") (("1" (propax) nil nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 -2 2)) (("3" (typepred "x!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (expand "every") (("3" (inst -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" (prop) (("1" (grind) nil nil)) nil)) nil) ("2" (expand* "restrict" "union" "member") (("2" (prop) (("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" (flatten) (("2" (expand "member") (("2" (expand "restrict") (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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]] (card[T], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replace -1) (("1" (hide -1) (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil 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 "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -8) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -7) (("2" (inst?) (("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], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replaces -1) (("1" (lemma "finite_union[finite_set[T]]") (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -7) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -6) (("2" (inst?) (("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" (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)) 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" (case-replace "restrict[setof[T], finite_set[T], boolean] (extend[setof[T], (x!1), bool, FALSE] (singleton(choose(x!1)))) = singleton(choose(x!1))" :hide? T) (("1" (case-replace "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1) :hide? T) (("1" (typepred "card(choose(x!1))") (("1" (replaces -1) (("1" (typepred "Card(choose(x!1))") (("1" (hide (-2 -3 2)) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 2 3)) (("2" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (grind) (("2" (inst 1 "choose(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil) ("3" (reveal 3) (("3" (expand "nonempty?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2)) (("3" (typepred "x!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (expand "every") (("3" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand* "restrict" "extend") (("1" (prop) nil nil)) nil) ("2" (expand* "restrict" "extend") (("2" (prop) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (prop) (("1" (expand "singleton") (("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)) 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" (case-replace "restrict[setof[T], finite_set[T], boolean] (extend[setof[T], (x!1), bool, FALSE] (singleton(choose(x!1)))) = singleton(choose(x!1))" :hide? T) (("1" (case-replace "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1) :hide? T) (("1" (typepred "card(choose(x!1))") (("1" (replaces -1) (("1" (typepred "Card(choose(x!1))") (("1" (hide (-2 -3 2)) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 2 3)) (("2" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (grind) (("2" (inst 1 "choose(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil) ("3" (reveal 3) (("3" (expand "nonempty?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2)) (("3" (typepred "x!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (expand "every") (("3" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand* "restrict" "extend") (("1" (prop) nil nil)) nil) ("2" (expand* "restrict" "extend") (("2" (prop) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (prop) (("1" (expand "singleton") (("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)) nil)) nil)) nil) ("7" (hide (-1 1)) (("7" (case-replace "restrict[setof[T], finite_set[T], boolean](x!1)= union(restrict[setof[T], finite_se :hide? T) (("1" (lemma "card_disj_union[finite_set[T]]") (("1" (inst -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 (-1 2)) (("2" (expand "nonempty?" 1) (("2" (expand "empty?") (("2" (inst -1 "choose(x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "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" (flatten) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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" (prop) (("1" (expand "remove") (("1" (prop) (("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" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (lemma "choose_member[setof[T]]") (("2" (inst?) (("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" (case-replace "restrict[setof[T], finite_set[T], boolean](x!1)= union(restrict[setof[T], finite_se :hide? T) (("1" (lemma "card_disj_union[finite_set[T]]") (("1" (inst -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 (-1 2)) (("2" (expand "nonempty?" 1) (("2" (expand "empty?") (("2" (inst -1 "choose(x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "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" (flatten) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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" (prop) (("1" (expand "remove") (("1" (prop) (("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" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (lemma "choose_member[setof[T]]") (("2" (inst?) (("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" (inst -5 "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) ((x!1 skolem-const-decl "setof[T]" class_equation_scaf nil) (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (divide_sigma_TCC1 subtype-tcc nil class_equation_scaf nil) (x!2 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (partition? const-decl "bool" lagrange_scaf "algebra/") (a!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (b!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (card_disj_union formula-decl nil finite_sets nil) (nonempty_card formula-decl nil finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rest_empty_lem formula-decl nil sets_lemmas nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (nonempty_extend application-judgement "(nonempty?[T])" extend_set_props nil) (choose_member formula-decl nil sets_lemmas nil) (A!1 skolem-const-decl "(rest(x!1))" class_equation_scaf nil) (A!1 skolem-const-decl "(rest(x!1))" class_equation_scaf nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (closed_plus formula-decl nil integers nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_props "sets_aux/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (choose const-decl "(p)" sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (union const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (choose_not_member formula-decl nil sets_lemmas nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (sigma_finite formula-decl nil sigma_countable "sigma_set/") (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (O const-decl "T3" function_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma "reals/") (finite_enumeration const-decl "[below[card(X)] -> (X)]" finite_enumeration "sigma_set/") (below type-eq-decl nil nat_types nil) (sigma def-decl "real" sigma "reals/") (Card_bijection formula-decl nil finite_sets nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (every const-decl "bool" sets nil) (finite_singleton judgement-tcc nil finite_sets nil) (sigma_countable formula-decl nil sigma_set "sigma_set/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (convergent? const-decl "bool" countable_convergence "sigma_set/") (card_def formula-decl nil finite_sets nil) (rat nonempty-type-eq-decl nil rationals nil) (closed_plus formula-decl nil rationals nil) (NOT const-decl "[bool -> bool]" booleans nil) (remove const-decl "set" sets nil) (nonzero_elts const-decl "set[T]" convergence_set "sigma_set/") (finite_union judgement-tcc nil finite_sets nil) (finite_rest judgement-tcc nil finite_sets nil) (rest_member formula-decl nil sets_lemmas nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (sigma_disjoint_union formula-decl nil sigma_set "sigma_set/") (x!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (rest const-decl "set" sets nil) (sigma const-decl "real" sigma_set "sigma_set/") (AND const-decl "[bool, bool -> bool]" booleans nil) (divides const-decl "bool" divides nil) (nonempty? const-decl "bool" sets nil) (convergent? const-decl "bool" convergence_set "sigma_set/") (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil class_equation_scaf nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) nil)) (divide_sigma 0 (divide_sigma-1 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" (inst -1 "rest(x!1)" "singleton(choose(x!1))" "card") (("1" (prop) (("1" (case-replace "restrict[setof[T], finite_set[T], boolean](x!1) = union(restrict[setof[T], finite_se :hide? T) (("1" (replace -1 1) (("1" (hide -1) (("1" (case-replace "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1) :hide? T) (("1" (lemma "divides_sum") (("1" (inst?) (("1" (assert) (("1" (hide (-1 2)) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (lemma "divide_sigma_TCC2") (("2" (inst -1 "rest[setof[T]](x!1)" "n!1") (("1" (prop) (("1" (hide 1) (("1" (skosimp*) (("1" (inst -2 "A!1") (("1" (hide 2) (("1" (typepred "A!1") (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "A!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (skosimp*) (("2" (inst -2 "A!1") (("2" (hide 2) (("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)) nil) ("3" (hide -2) (("3" (expand "nonempty?") (("3" (rewrite "sigma_countable") (("1" (expand "sigma") (("1" (prop) (("1" (assert) nil nil) ("2" (hide (-1 1 3)) (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand* "member" "restrict") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (hide (1 2 4)) (("3" (expand "empty?") (("3" (skosimp*) (("3" (expand* "member" "restrict") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5 -6 2)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_rest[setof[T]]") (("3" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5 -6 2)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -2) (("4" (expand "nonempty?") (("4" (rewrite "sigma_countable") (("1" (expand "sigma") (("1" (prop) (("1" (assert) nil nil) ("2" (hide (-1 1 3)) (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand* "member" "restrict") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (hide (1 2 4)) (("3" (expand "empty?") (("3" (skosimp*) (("3" (expand* "member" "restrict") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5 -6 2)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_rest[setof[T]]") (("3" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5 -6 2)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 2)) (("2" (typepred "x!1") (("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" (inst -5 "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)) nil)) nil)) nil)) nil) ("2" (hide (-1 -3 2)) (("2" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (expand "nonempty?") (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (expand "bijective?") (("2" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1" "x2!1") (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (inst 1 "choose(x!1)") (("1" (expand "singleton") (("1" (propax) nil nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 -3 2)) (("3" (hide (-1 2)) (("3" (typepred "x!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (expand "every") (("3" (inst -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" (prop) (("1" (grind) nil nil)) nil)) nil) ("2" (expand* "restrict" "union" "member") (("2" (prop) (("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" (flatten) (("2" (expand "member") (("2" (expand "restrict") (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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]] (card[T], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replace -1) (("1" (hide -1) (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -5) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -4) (("2" (inst?) (("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], union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]] (restrict[setof[T], finite_set[T], boolean] (rest[setof[T]](x!1)), singleton[(x!1)](choose[setof[T]](x!1)))") (("1" (replaces -1) (("1" (lemma "finite_union[finite_set[T]]") (("1" (inst?) (("1" (hide 2) (("1" (lemma "finite_singleton[(x!1)]") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_rest[setof[T]]") (("2" (inst?) (("1" (expand* "is_finite" "restrict") (("1" (skosimp) (("1" (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" (hide (-1 -2 -5)) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (expand "every") (("1" (inst?) nil nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "nonzero_elts") (("1" (prop) nil nil)) nil) ("2" (expand "nonzero_elts") (("2" (prop) (("2" (expand "union") (("2" (expand "member") (("2" (expand "restrict") (("2" (prop) (("1" (lemma "rest_member[setof[T]]") (("1" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) (("1" (reveal -4) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (reveal -3) (("2" (inst?) (("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" (case-replace "restrict[setof[T], finite_set[T], boolean] (extend[setof[T], (x!1), bool, FALSE] (singleton(choose(x!1)))) = singleton(choose(x!1))" :hide? T) (("1" (case-replace "sigma_set[finite_set[T]].sigma(singleton(choose(x!1)), card[T]) = card(choose(x!1) :hide? T) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide (-1 -3 2 3)) (("2" (rewrite "sigma_countable") (("1" (lemma "sigma_countable.sigma_finite" ("F" "singleton(choose(x!1))")) (("1" (inst?) (("1" (case "card(singleton(choose(x!1))) = 1") (("1" (replaces -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "o ") (("1" (typepred "finite_enumeration(singleton(choose(x!1)))(0)") (("1" (expand "singleton") (("1" (assert) (("1" (replace -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (rewrite "card_def") (("2" (rewrite "Card_bijection") (("2" (inst 1 "LAMBDA (y : (singleton(choose(x!1)))) : 0") (("2" (grind) (("2" (inst 1 "choose(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "empty?") (("1" (inst -1 "choose[setof[T]](x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "choose[setof[T]](x!1)") nil nil)) nil)) nil)) nil)) nil) ("3" (reveal 2) (("3" (expand "nonempty?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[(x!1)]") (("2" (inst -1 "choose[setof[T]](x!1)") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (prop) (("2" (hide 2) (("2" (lemma "finite_singleton[(x!1)]") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "finite_countable") (("3" (hide 2) (("3" (lemma "finite_singleton[(x!1)]") (("3" (inst?) (("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" (flatten) (("3" (expand "every") (("3" (inst -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" (prop) (("1" (expand* "restrict" "extend") (("1" (prop) nil nil)) nil) ("2" (expand* "restrict" "extend") (("2" (prop) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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" (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)) 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" (case-replace "restrict[setof[T], finite_set[T], boolean](x!1)= union(restrict[setof[T], finite_se :hide? T) (("1" (lemma "card_disj_union[finite_set[T]]") (("1" (inst -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 (-1 2)) (("2" (expand "nonempty?" 1) (("2" (expand "empty?") (("2" (inst -1 "choose(x!1)") (("1" (expand "member") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst -3 "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" (flatten) (("2" (expand "singleton") (("2" (lemma "choose_not_member[setof[T]]") (("2" (inst?) (("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" (prop) (("1" (expand "remove") (("1" (prop) (("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" (inst -1 "x!1" "x!2") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (lemma "choose_member[setof[T]]") (("2" (inst?) (("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" (inst -5 "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) ((x!1 skolem-const-decl "setof[T]" class_equation_scaf nil) (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (card_partition_TCC2 subtype-tcc nil class_equation_scaf nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (divide_sigma_TCC1 subtype-tcc nil class_equation_scaf nil) (x!2 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (a!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (b!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (card_disj_union formula-decl nil finite_sets nil) (nonempty_card formula-decl nil finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (A!1 skolem-const-decl "(rest(x!1))" class_equation_scaf nil) (choose_member formula-decl nil sets_lemmas nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (nonempty_extend application-judgement "(nonempty?[T])" extend_set_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (rest_empty_lem formula-decl nil sets_lemmas nil) (sigma_disjoint_union formula-decl nil sigma_set "sigma_set/") (x!2 skolem-const-decl "setof[T]" class_equation_scaf nil) (finite_union judgement-tcc nil finite_sets nil) (nonzero_elts const-decl "set[T]" convergence_set "sigma_set/") (remove const-decl "set" sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (divide_sigma_TCC2 subtype-tcc nil class_equation_scaf nil) (b!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (a!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (partition? const-decl "bool" lagrange_scaf "algebra/") (x!2 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (rest_member formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (A!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (A!1 skolem-const-decl "(rest[setof[T]](x!1))" class_equation_scaf nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (finite_rest judgement-tcc nil finite_sets nil) (below type-eq-decl nil nat_types nil) (injective? const-decl "bool" functions nil) (every const-decl "bool" sets nil) (sigma const-decl "real" sigma_countable "sigma_set/") (empty? const-decl "bool" sets nil) (sigma_countable formula-decl nil sigma_set "sigma_set/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (convergent? const-decl "bool" countable_convergence "sigma_set/") (divides_sum formula-decl nil divides nil) (finite_singleton judgement-tcc nil finite_sets nil) (card_def formula-decl nil finite_sets nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (Card_bijection formula-decl nil finite_sets nil) (sigma def-decl "real" sigma "reals/") (finite_enumeration const-decl "[below[card(X)] -> (X)]" finite_enumeration "sigma_set/") (sigma_nat application-judgement "nat" sigma "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (O const-decl "T3" function_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (sigma_finite formula-decl nil sigma_countable "sigma_set/") (choose_not_member formula-decl nil sets_lemmas nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (union const-decl "set" sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_props "sets_aux/") (x!1 skolem-const-decl "finite_partition[T]" class_equation_scaf nil) (rest const-decl "set" sets nil) (sigma const-decl "real" sigma_set "sigma_set/") (AND const-decl "[bool, bool -> bool]" booleans nil) (divides const-decl "bool" divides nil) (convergent? const-decl "bool" convergence_set "sigma_set/") (/= const-decl "boolean" notequal nil) (nonempty? const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil class_equation_scaf nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)))
¤ 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.796Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26