SSL class_equation_scaf.prf
Interaktion und
(class_equation_scafnil 3526046475"" (skosimp*)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (assert )"" (lemma "Union_finite[T]" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil finite_sets_of_sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil ))nil ))nil 3526046475"" (skosimp*)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (hide (-1 -2))"" (expand "every" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil ) (set type-eq-decl nil sets nil )"bool" sets nil )"(p)" sets nil ))nil ))nil 3526046475"" (skosimp*)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (lemma "Union_finite[T]" )"" (inst?)"" (assert )"" (hide (-1 2))"" (prop)"1" (rewrite "finite_rest" ) nil nil )"2" (expand "every" )"2" (skosimp*)"2" (inst?)"2" (typepred "x!1" )"2" (lemma "rest_member[setof[T]]" )"2" "FP!1" "x!1" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil ) (rest const-decl "set" sets nil )"bool" sets nil )"finite_partition[T]" class_equation_scafnil )"(rest[setof[T]](FP!1))" class_equation_scafnil )nil sets_lemmas nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil finite_sets_of_sets nil ))nil ))nil 3526047645"" (skosimp*)"" (lemma "card_Union_rest" )"" (inst?)"" (assert )"" (replaces -1)"" (rewrite "card_disj_union" )"" (hide 2)"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (expand "partition?" )"" (expand "disjoint?" )"" (expand "empty?" )"" (skosimp*)"" expand "member" )"" expand "intersection" )"" expand "member" )"" "" expand "Union" )"" "" "a!1" "choose(FP!1)" )"1" "1" "a!1" )"1" "1" "1" "choose_not_member[setof[T]]" )"1" "1" expand "nonempty?" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" "a!1" )"2" "rest_member[setof[T]]" )"2" "FP!1" "a!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil class_equation_scaf nil )nil lagrange_scaf "algebra/" )"nonneg_int" nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil ) (rest const-decl "set" sets nil )"bool" sets nil )"(p)" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"set" sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"(rest(FP!1))" class_equation_scaf nil )"finite_partition[T]" class_equation_scafnil )"bool" sets nil )"bool" sets nil )"bool" lagrange_scaf "algebra/" )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil ))nil 3526042692"" (skosimp*)"" (typepred "A!1" )"" (typepred "FP!1" )"" (expand "finite_partition?" )"" (flatten)"" (expand "every" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil ))nil ))nil 3526042692"" (skosimp*)"" (expand "convergent?" )"" (prop)"1" (typepred "FP!1" )"1" (expand "finite_partition?" )"1" (flatten)"1" (hide -1)"1" (rewrite "finite_countable" )"1" (hide 2)"1" (expand "is_finite" (-1 1))"1" (skosimp)"1" (inst 1 "N!1" "f!1" )"1" (hide (-2 -3))"1" (expand "injective?" )"1" (grind) nil nil )) nil ))nil )"2" (skosimp*)"2" (prop)"1" expand "every" )"1" (inst?) nil nil ))nil )"2" expand "nonzero_elts" )"2" expand "restrict" )"2" assert )"2" (inst?) nil nil ))nil ))nil ))nil )"3" expand "nonzero_elts" )"3" expand "restrict" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "convergent?" )"2" (flatten)"2" (hide 2)"2" (typepred "FP!1" )"2" (expand "finite_partition?" )"2" (flatten)"2" (hide -1)"2" (expand "is_finite" (-1 1))"2" (skosimp)"2" (inst 1 "N!1" "f!1" )"1" (hide (-2 -3))"1" expand "injective?" )"1" (grind) nil nil ))nil ))nil )"2" (skosimp*)"2" "1" expand "every" )"1" (inst?) nil nil ))nil )"2" expand "nonzero_elts" )"2" expand "restrict" )"2" assert )"2" (inst?) nil nil ))nil ))nil ))nil )"3" expand "nonzero_elts" )"3" expand "restrict" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" convergence_set "sigma_set/" )"bool" countable_convergence "sigma_set/" )"setof[T]" class_equation_scaf nil )nil lagrange_scaf "algebra/" )"bool" lagrange_scaf "algebra/" )nil sets nil )nil defined_types nil )nil class_equation_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil countable_props "sets_aux/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"set[T]" convergence_set "sigma_set/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"R" restrict nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"finite_partition[T]" class_equation_scafnil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"bool" reals nil )"bool" functions nil )"boolean" notequal nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"setof[T]" class_equation_scaf nil )"bool" sets nil ))nil ))nil 3526051917"" (measure-induct+ "card(FP)" "FP" )"1" (inst -1 "rest(x!1)" )"1" (prop)"1" (lemma "choose_rest[setof[T]]" )"1" (inst?)"1" (expand "nonempty?" )"1" (assert )"1" (rewrite "add_as_union" )"1" "ZZ" "restrict[setof[T], finite_set[T], boolean](x!1)" )"1" (replace -1 2)"1" (lemma "sigma_set.sigma_disjoint_union" )"1" "rest(x!1)" "singleton(choose(x!1))" "card" )"1" (prop)"1" (replace -4 -1 rl)"1" case "ZZ = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)), ") "1" replace -1 -2 rl)"1" replace -2 2)"1" "card_rest_aux" )"1" "x!1" )"1" expand "nonempty?" )"1" "1" assert )"1" "1" rewrite "sigma_countable" )"1" "sigma_countable.sigma_finite" "F" "singleton(choose(x!1))" ))"1" "1" case "card(singleton(choose(x!1))) = 1" )"1" "1" assert )"1" replace "1" "1" expand "sigma" )"1" expand "o " )"1" "finite_enumeration(singleton(choose(x!1)))(0)" )"1" expand "singleton" )"1" assert )"1" replace "1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "card_def" )"2" rewrite "Card_bijection" )"2" "LAMBDA (y : (singleton(choose(x!1)))) : 0" )"2" "2" "choose(x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "empty?" )"1" "choose[setof[T]](x!1)" )"1" expand "member" )"1" expand "singleton" )"1" nil nil ))nil ))nil )"2" "x!1" )"2" expand "finite_partition?" )"2" "2" expand "every" )"2" "choose[setof[T]](x!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[(x!1)]" )"2" "choose[setof[T]](x!1)" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergent?" )"2" "2" "2" "finite_singleton[(x!1)]" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "finite_countable" )"3" "3" "finite_singleton[(x!1)]" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -2 -1 rl)"2" "2" replace -1 1 rl)"2" "2" "2" "2" "1" expand *"restrict" "union" "member" )"1" "1" "1" nil nil ))nil ))nil ))nil )"2" expand *"restrict" "union" "member" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" expand "disjoint?" )"2" expand "empty?" 1)"2" "2" expand "member" )"2" expand "intersection" )"2" "2" expand "member" )"2" expand "restrict" )"2" expand "singleton" )"2" "choose_not_member[setof[T]]" )"2" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (expand "convergent?" )"2" "1" rewrite "finite_countable" )"1" "1" "finite_union[finite_set[T]]" )"1" case "nonzero_elts[finite_set[T]] ") "1" replace -1)"1" "1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "finite_partition?" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" expand "nonzero_elts" )"1" nil nil ))nil )"2" expand "nonzero_elts" )"2" "2" expand "union" )"2" expand "member" )"2" expand "restrict" )"2" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "convergent?" )"2" "2" "2" case "nonzero_elts(card[T], ") "1" "1" "finite_union[finite_set[T]]" )"1" "1" "1" "finite_singleton[(x!1)]" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "finite_rest[setof[T]]" )"2" "1" expand *"is_finite" "restrict" )"1" "1" "N!1" "f!1" )"1" expand "injective?" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "x!1" )"1" expand "finite_partition?" )"1" "1" "1" "rest_member[setof[T]]" )"1" "x!1" "x!2" )"1" expand "member" )"1" assert )"1" expand "every" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" nil nil ))nil )"3" expand "restrict" )"3" nil quality 100%
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.56Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
2026-03-28
