| products/Sources/formale Sprachen/PVS/lebesgue/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(lagrange_scaf
(partition_TCC1 0 (partition_TCC1-1 nil 3292976024 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil lagrange_scaf nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (emptyset const-decl "set" sets nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (partition? const-decl "bool" lagrange_scaf nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (finite_partition_TCC1 0 (finite_partition_TCC1-1 nil 3293027840 ("" (expand "finite_partition?") (("" (expand "partition?") (("" (split) (("1" (skosimp*) (("1" (grind) (("1" (typepred "a!1") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "every") (("2" (skosimp*) (("2" (typepred "x!1") (("2" (expand "extend") (("2" (case-replace "(nonempty?[T])(x!1)") (("1" (expand "emptyset") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition? const-decl "bool" lagrange_scaf nil) (every const-decl "bool" sets nil) (emptyset const-decl "set" sets nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (setof type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil lagrange_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_emptyset name-judgement "finite_set" finite_sets nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil)) shostak)) (finite_partition_is_partition 0 (finite_partition_is_partition-1 nil 3293368458 ("" (skosimp*) (("" (typepred "x!1") (("" (expand "finite_partition?") (("" (flatten) nil nil)) nil)) nil)) nil) ((finite_partition type-eq-decl nil lagrange_scaf nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil lagrange_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (card_Union_rest 0 (dfgdfgf "" 3406374714 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (iff 1) (("" (expand "Union") (("" (expand "union") (("" (expand "member") (("" (prop) (("1" (skosimp*) (("1" (lemma "choose_rest_or[set[T]]") (("1" (assert) (("1" (inst - "PP!1" "a!1") (("1" (assert) (("1" (inst + "a!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "a!1") (("2" (inst + "a!1") (("2" (lemma "rest_member[set[T]]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst + "choose(PP!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil lagrange_scaf nil) (boolean nonempty-type-decl nil booleans nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (rest const-decl "set" sets nil) (union const-decl "set" sets nil) (finite_partition type-eq-decl nil lagrange_scaf nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (Union const-decl "set" sets nil) (set type-eq-decl nil sets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (PP!1 skolem-const-decl "finite_partition" lagrange_scaf nil) (a!1 skolem-const-decl "(rest(PP!1))" lagrange_scaf nil) (rest_member formula-decl nil sets_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (choose_rest_or formula-decl nil sets_lemmas nil)) shostak) (card_Union_rest-1 nil 3406373769 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "Union") (("" (expand "union") (("" (expand "member") (("" (iff 1) (("" (prop) (("1" (skosimp*) (("1" (inst + "a!1") (("1" (typepred "a!1") (("1" (lemma "rest_member[set[T]]") (("1" (inst?) (("1" (expand "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (postpone) nil nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (card_equal_partition_TCC1 0 (card_equal_partition_TCC1-1 nil 3406369425 ("" (skosimp*) (("" (typepred "PP!1") (("" (expand "finite_partition?") (("" (flatten) nil nil)) nil)) nil)) nil) ((finite_partition type-eq-decl nil lagrange_scaf nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil lagrange_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (card_equal_partition_TCC2 0 (card_equal_partition_TCC2-1 nil 3406369425 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil lagrange_scaf nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (finite_partition type-eq-decl nil lagrange_scaf nil) (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) (>= const-decl "bool" reals nil) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (partition? const-decl "bool" lagrange_scaf nil) (every const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil)) nil)) (card_equal_partition_TCC3 0 (card_equal_partition_TCC3-1 nil 3406374244 ("" (skosimp*) (("" (typepred "PP!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 nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil lagrange_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_equal_partition 0 (card_equal_partition-3 nil 3426246039 ("" (induct "n" 1) (("1" (skosimp*) (("1" (assert) (("1" (lemma "card_empty?[set[T]]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?") (("1" (assert) (("1" (lemma "card_empty?[T]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?") (("1" (assert) (("1" (skosimp*) (("1" (expand "Union") (("1" (skosimp*) (("1" (typepred "a!1") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "card_Union_rest") (("1" (case "empty?(rest(PP!1))") (("1" (lemma "emptyset_is_empty?[set[T]]") (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "Union_emptyset_rew") (("1" (rewrite "union_commutative") (("1" (rewrite "union_empty") (("1" (inst? -4) (("1" (assert) (("1" (reveal -2) (("1" (lemma "card_rest[set[T]]") (("1" (inst?) (("1" (split -1) (("1" (assert) (("1" (replace -2) (("1" (rewrite "card_emptyset[set[T]]") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2 -3 -4 1) (("2" (lemma "card_empty?[set[T]]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "rest(PP!1)" "m!1") (("1" (split -1) (("1" (rewrite "card_union") (("1" (case-replace "card(intersection(Union(rest(PP!1)), choose(PP!1))) = 0") (("1" (assert) (("1" (replace -2) (("1" (inst - "choose(PP!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "card_is_0[T]") (("2" (inst?) (("2" (assert) (("2" (assert) (("2" (hide 2) (("2" (hide -1 -2 -3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "intersection") (("2" (expand "Union") (("2" (expand "emptyset") (("2" (assert) (("2" (flatten) (("2" (skosimp*) (("2" (typepred "a!1") (("2" (inst - "a!1" "choose(PP!1)") (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (expand "intersection") (("1" (assert) (("1" (split -5) (("1" (lemma "choose_not_member[set[T]]") (("1" (inst?) (("1" (assert) (("1" (reveal -6) (("1" (inst?) (("1" (lemma "card_empty?[set[T]]") (("1" (inst?) (("1" (assert) nil nil) ("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "rest_member[set[T]]") (("2" (inst?) (("2" (assert) (("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)) nil) ("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "card_rest") (("1" (assert) nil nil) ("2" (lemma "card_empty?[set[T]]") (("2" (inst - "PP!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (reveal -1) (("3" (typepred "A!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "disjoint?") (("4" (hide -2) (("4" (hide 3) (("4" (typepred "A!1") (("4" (typepred "B!1") (("4" (inst?) (("1" (lemma "rest_member[set[T]]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "rest_member[set[T]]") (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "rest_member[set[T]]") (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (prop) (("1" (expand "partition?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil) ("2" (typepred "b!1") (("2" (lemma "rest_member[set[T]]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "a!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_rest[set[T]]") (("2" (inst?) nil nil)) nil) ("3" (expand "every") (("3" (skosimp*) (("3" (inst?) (("3" (typepred "x!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -4 2) (("2" (lemma "card_empty?[set[T]]") (("2" (inst?) (("2" (expand "nonempty?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (lemma "finite_Union_finite[T]") (("3" (inst?) (("3" (assert) (("3" (hide 2) (("3" (typepred "PP!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (typepred "A!1") (("4" (typepred "PP!1") (("4" (expand "finite_partition?") (("4" (flatten) (("4" (expand "every") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (typepred "PP!1") (("5" (expand "finite_partition?") (("5" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((finite_Union_finite formula-decl nil finite_sets_of_sets nil) (rest const-decl "set" sets nil) (Union_emptyset_rew formula-decl nil sets_lemmas nil) (union_empty formula-decl nil sets_lemmas nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (card_rest formula-decl nil finite_sets nil) (card_emptyset formula-decl nil finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (union_commutative formula-decl nil sets_lemmas nil) (emptyset const-decl "set" sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" finite_sets_inductions "finite_sets/") (emptyset_is_empty? formula-decl nil sets_lemmas nil) (x!1 skolem-const-decl "(rest[setof[T]](PP!1))" lagrange_scaf nil) (finite_rest judgement-tcc nil finite_sets nil) (partition? const-decl "bool" lagrange_scaf nil) (a!1 skolem-const-decl "(rest[setof[T]](PP!1))" lagrange_scaf nil) (b!1 skolem-const-decl "(rest[setof[T]](PP!1))" lagrange_scaf nil) (every const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (card_is_0 formula-decl nil finite_sets nil) (a!1 skolem-const-decl "(rest(PP!1))" lagrange_scaf nil) (choose_not_member formula-decl nil sets_lemmas nil) (rest_member formula-decl nil sets_lemmas nil) (card_union formula-decl nil finite_sets nil) (B!1 skolem-const-decl "(rest(PP!1))" lagrange_scaf nil) (A!1 skolem-const-decl "(rest(PP!1))" lagrange_scaf nil) (PP!1 skolem-const-decl "finite_partition" lagrange_scaf nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (card_Union_rest formula-decl nil lagrange_scaf nil) (card_empty? formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (disjoint? const-decl "bool" sets nil) (Union const-decl "set" sets nil) (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) (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_set type-eq-decl nil finite_sets nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (T formal-type-decl nil lagrange_scaf nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (finite_partition type-eq-decl nil lagrange_scaf nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil)) nil) (card_equal_partition-2 nil 3406380188 ("" (induct "n" 1) (("1" (skosimp*) (("1" (assert) (("1" (lemma "card_empty?[set[T]]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?") (("1" (assert) (("1" (lemma "card_empty?[T]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?") (("1" (assert) (("1" (skosimp*) (("1" (expand "Union") (("1" (skosimp*) (("1" (typepred "a!1") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "card_Union_rest") (("1" (case "empty?(rest(PP!1))") (("1" (lemma "emptyset_is_empty?[set[T]]") (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "Union_emptyset_rew") (("1" (rewrite "union_commutative") (("1" (rewrite "union_empty") (("1" (inst? -4) (("1" (assert) (("1" (reveal -2) (("1" (lemma "card_rest[set[T]]") (("1" (inst?) (("1" (split -1) (("1" (assert) (("1" (replace -2) (("1" (rewrite "card_emptyset[set[T]]") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2 -3 -4 1) (("2" (lemma "card_empty?[set[T]]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "rest(PP!1)" "m!1") (("1" (split -1) (("1" (rewrite "card_union") (("1" (case-replace "card(intersection(Union(rest(PP!1)), choose(PP!1))) = 0") (("1" (assert) (("1" (replace -2) (("1" (inst - "choose(PP!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "card_is_0[T]") (("2" (inst?) (("2" (assert) (("2" (assert) (("2" (hide 2) (("2" (hide -1 -2 -3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "intersection") (("2" (expand "Union") (("2" (expand "emptyset") (("2" (assert) (("2" (flatten) (("2" (skosimp*) (("2" (typepred "a!1") (("2" (inst - "a!1" "choose(PP!1)") (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (expand "intersection") (("1" (assert) (("1" (split -5) (("1" (lemma "choose_not_member[set[T]]") (("1" (inst?) (("1" (assert) (("1" (reveal -6) (("1" (inst?) (("1" (lemma "card_empty?[set[T]]") (("1" (inst?) (("1" (assert) nil nil) ("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "rest_member[set[T]]") (("2" (inst?) (("2" (assert) (("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)) nil) ("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "card_rest") (("1" (assert) nil nil) ("2" (lemma "card_empty?[set[T]]") (("2" (inst - "PP!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (reveal -1) (("3" (typepred "A!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "disjoint?") (("4" (hide -2) (("4" (hide 3) (("4" (typepred "A!1") (("4" (typepred "B!1") (("4" (inst?) (("1" (lemma "rest_member[set[T]]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "rest_member[set[T]]") (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "rest_member[set[T]]") (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (prop) (("1" (expand "partition?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil) ("2" (typepred "b!1") (("2" (lemma "rest_member[set[T]]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "a!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_rest[set[T]]") (("2" (inst?) nil nil)) nil) ("3" (expand "every") (("3" (skosimp*) (("3" (inst?) (("3" (typepred "x!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -4 2) (("2" (lemma "card_empty?[set[T]]") (("2" (inst?) (("2" (expand "nonempty?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (lemma "finite_Union_finite") (("3" (inst?) (("3" (assert) (("3" (hide 2) (("3" (typepred "PP!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (typepred "A!1") (("4" (typepred "PP!1") (("4" (expand "finite_partition?") (("4" (flatten) (("4" (expand "every") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (typepred "PP!1") (("5" (expand "finite_partition?") (("5" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((finite_emptyset name-judgement "finite_set[T]" finite_sets_inductions "finite_sets/")) nil) (card_equal_partition-1 nil 3406369430 ("" (induct "n" 1) (("1" (skosimp*) (("1" (assert) (("1" (lemma "card_empty?[set[T]]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?") (("1" (assert) (("1" (lemma "card_empty?[T]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?") (("1" (assert) (("1" (skosimp*) (("1" (expand "Union") (("1" (skosimp*) (("1" (typepred "a!1") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "card_Union_rest") (("2" (inst - "rest(PP!1)") (("1" (inst - "rest(PP!1)" "m!1") (("1" (split -1) (("1" (rewrite "card_union") (("1" (case-replace "card(intersection(Union(rest(PP!1)), choose(PP!1))) = 0") (("1" (assert) (("1" (replace -2) (("1" (reveal -2) (("1" (inst - "choose(PP!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "every") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "card_rest") (("1" (assert) nil nil) ("2" (lemma "card_empty?[set[T]]") (("2" (inst - "PP!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (reveal -2) (("3" (inst?) (("3" (typepred "A!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "PP!1") (("2" (expand "finite_partition?") (("2" (flatten) (("2" (prop) (("1" (expand "partition?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil) ("2" (typepred "b!1") (("2" (lemma "rest_member[set[T]]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "a!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_rest[set[T]]") (("2" (inst?) nil nil)) nil) ("3" (expand "every") (("3" (skosimp*) (("3" (inst?) (("3" (typepred "x!1") (("3" (lemma "rest_member[set[T]]") (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "rest_member[set[T]]") (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (hide -1 -2) (("2" (expand "singleton_elt") (("2" (expand "the") (("2" (lemma "epsilon_ax[set[T]]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (lemma "finite_Union_finite") (("3" (inst?) (("3" (assert) (("3" (hide 2) (("3" (typepred "PP!1") (("3" (expand "finite_partition?") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (typepred "A!1") (("4" (typepred "PP!1") (("4" (expand "finite_partition?") (("4" (flatten) (("4" (expand "every") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (typepred "PP!1") (("5" (expand "finite_partition?") (("5" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (card_eq_part_TCC1 0 (card_eq_part_TCC1-1 nil 3406381416 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil lagrange_scaf nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (finite_partition type-eq-decl nil lagrange_scaf nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (>= const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (every const-decl "bool" sets nil) (partition? const-decl "bool" lagrange_scaf nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil)) nil)) (card_eq_part_TCC2 0 (card_eq_part_TCC2-1 nil 3406381416 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil lagrange_scaf nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (finite_partition type-eq-decl nil lagrange_scaf nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (>= const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (every const-decl "bool" sets nil) (partition? const-decl "bool" lagrange_scaf nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil)) nil)) (card_eq_part_TCC3 0 (card_eq_part_TCC3-1 nil 3406386104 ("" (skosimp*) (("" (typepred "PP!1") (("" (expand "finite_partition?") (("" (flatten) (("" (lemma "Union_finite[T]") --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.604 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.Bot Zugriff |
