|
(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
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.136 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
