Quelle finite_bags.prf
Sprache: Lisp
(finite_bagsnil 3249305393 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_bags nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )"bool" functions nil )"bool" finite_sets nil ))nil ))nil 3289826684"" (skosimp*)"" (expand "is_finite" )"" (expand "is_finite" )"" (skolem -1 ("n!1" "f!1" ))"" (inst + "n!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?)"1" (assert ) nil nil ) ("2" (grind) nil nil )"3" (expand "bag_to_set" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" finite_sets nil )"bool" finite_bags nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set" finite_bags nil )"bool" functions nil )nil nat_types nil )"bool" reals nil )nil finite_bags nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil ) (set type-eq-decl nil sets nil )"set[T]" bags_to_sets nil )nil finite_bags nil )"finite_bag" finite_bags nil )"bool" reals nil ))nil 3249305393"" (expand "emptybag" )"" (lemma "finite_emptyset" )"" (expand "emptyset" )"" (expand "is_finite" 1)"" (expand "bag_to_set" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil finite_bags nil )nil finite_sets nil )"bool" finite_bags nil )"set[T]" bags_to_sets nil )"set" sets nil )"bag" bags nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "singleton_bag" )"" (expand "is_finite" )"" (expand "bag_to_set" )"" (expand "is_finite" )"" "1" "(LAMBDA (t: {t: T | IF t = t!1 THEN 1 ELSE 0 ENDIF > 0}): 0)" )"" (expand "injective?" )"" (skosimp*)"" (typepred "x1!1" )"" (typepred "x2!1" )"" (ground)"" (lift-if)"" (prop)"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bag" bags nil )"set[T]" bags_to_sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil finite_bags nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil nat_types nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"bool" finite_sets nil )"bool" finite_bags nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "is_finite" )"" (rewrite "insert_bag_lem" )"" (rewrite "finite_add" ) nil nil )) nil ))nil ))nil )"bool" finite_bags nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[T]" bags_to_sets nil )"non_empty_finite_set[T]" finite_bags nil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )nil finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bags_to_sets nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "is_finite" )"" (rewrite "purge_bag_lem" )"" (rewrite "finite_remove" ) nil nil )) nil ))nil ))nil )"bool" finite_bags nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[T]" bags_to_sets nil )"finite_set[T]" finite_bagsnil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )nil finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bags_to_sets nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "delete" )"" (typepred "B!1" )"" (expand "is_finite" )"" (expand "bag_to_set" )"" (expand "is_finite" )"" (skosimp*)"" "N!1" "(LAMBDA (t:{t: T | IF t!1 = t THEN IF B!1(t) >= n!1 THEN B!1(t) - n!1") "1" (expand "injective?" )"1" (skosimp*)"1" (inst?)"1" (assert ) nil nil )"2" (assert )"2" (assert )"2" (typepred "x2!1" )"2" "2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "x1!1" )"3" (lift-if) (("3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "t!2" )"2" (lift-if) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bag" bags nil )"bool" finite_sets nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" finite_bags nil )"finite_bag" finite_bags nil )"T" finite_bags nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil nat_types nil )"bool" functions nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"set[T]" bags_to_sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_bags nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "is_finite" )"" (rewrite "bag_union_lem" )"" (rewrite "finite_union" ) nil nil )) nil ))nil ))nil )"bool" finite_bags nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[T]" bags_to_sets nil )"finite_set[T]" finite_bagsnil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )nil finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bags_to_sets nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "is_finite" )"" (rewrite "bag_intersection_lem" )"" (lemma "finite_intersection" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil )"bool" finite_bags nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[T]" bags_to_sets nil )"finite_set[T]" nil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )nil finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bags_to_sets nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "is_finite" )"" (rewrite "bag_plus_lem" )"" (rewrite "finite_union" ) nil nil )) nil ))nil ))nil )"bool" finite_bags nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[T]" bags_to_sets nil )"finite_set[T]" finite_bagsnil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )nil finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bags_to_sets nil ))nil ))nil 3249305393"" (skosimp*)"" (typepred "B!1" )"" (expand "is_finite" )"" (case "B!1(x!1) = 0" )"1" (case "xn!1 = 0 " )"1" (replace -1)"1" (hide -1)"1" (case-replace "B!1 WITH [x!1 := 0] = B!1" )"1" (assert )"1" (apply-extensionality :hide? t)"1" (lift-if) (("1" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" "bag_to_set(B!1 WITH [x!1 := xn!1]) = add(x!1, bag_to_set(B!1))" )"1" (hide -1) (("1" (rewrite "finite_add" ) nil nil ))nil )"2" (hide -1 -2 3)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (case "xn!1 = 0 " )"1" (replace -1)"1" (hide -1)"1" (lemma "finite_subset" )"1" "bag_to_set(B!1)" "bag_to_set(B!1 WITH [x!1 := 0])" )"1" (assert )"1" (hide -1 3) (("1" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" "bag_to_set(B!1 WITH [x!1 := xn!1]) = bag_to_set(B!1)" )"2" (apply-extensionality :hide? t)"2" (hide -1 4) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_bags nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"non_empty_finite_set[T]" finite_bags nil )set type-eq-decl nil sets nil )"set[T]" bags_to_sets nil )"bool" sets nil )"(nonempty?)" sets nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )nil application-judgement "finite_set" finite_bags nil )nil finite_sets nil )"(partial_order?[set[T]])" nil )"(partial_order?[set[T]])" nil )"bool" sets nil ))nil ))nil 3286293268 ("" (grind) nil nil )nil application-judgement "finite_set" finite_bags nil )) nil ))nil 3286293280"" (skosimp*)"" (expand "is_finite" )"" (expand "extract" )"" (lemma "finite_subset" )"" (inst?)"" (inst - "bag_to_set(B!1)" )"" (assert )"" (expand "subset?" )"" (skosimp*)"" (expand "member" )"" (expand "bag_to_set" )"" (lift-if)"" (assert ) nil ))))))))))))))))))))))))nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_sets nil )nil application-judgement "finite_set" finite_bags nil )nil finite_sets nil )"bool" finite_sets nil )"bool" sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(partial_order?[set[T]])" nil )"(partial_order?[set[T]])" nil )nil finite_bags nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set[T]" bags_to_sets nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )"bag" bags nil ))nil ))nil 3249305418"" (skosimp*) (("" (typepred "x!1" ) (("" (grind) nil nil )) nil ))nil )nil finite_bags nil )"bool" bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_bags nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil application-judgement "finite_set" finite_bags nil )"bool" bags nil ))nil 3249305393"" (skosimp*) (("" (rewrite "finite_singleton_bag" ) nil nil )) nil )nil finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*) (("" (rewrite "finite_bag_union" ) nil nil )) nil )nil finite_bags nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*) (("" (rewrite "finite_bag_intersection" ) nil nil ))nil )nil finite_bags nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*) (("" (rewrite "finite_bag_plus" ) nil nil )) nil )nil finite_bags nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*)"" (typepred "NB!1" ) (("" (hide -1) (("" (grind) nil nil )) nil ))nil ))nil )nil finite_bags nil )"bool" bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_bags nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil application-judgement "finite_bag" finite_bags nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bag" bags nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3249305393 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_bags nil )"nonneg_int" nil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )"bag" bags nil )"bool" bags nil )nil application-judgement "finite_bag" finite_bags nil ))nil ))nil 3249305393 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_bags nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )"bag" bags nil )"bool" bags nil )nil application-judgement "finite_bag" finite_bags nil ))nil ))nil 3249305393 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_bags nil )"nonneg_int" nil )nil application-judgement "finite_set" finite_bags nil )nil finite_bags nil )"bag" bags nil )"bool" bags nil )nil application-judgement "finite_bag" finite_bags nil ))nil ))nil 3249305393"" (skosimp*)"" (rewrite "finite_insert" )"" (assert ) (("" (grind) nil nil )) nil )) nil ))nil )nil finite_bags nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )"bag" bags nil )"bool" bags nil )"posint" nil )"even_int" integersnil )"int" integers nil )"odd_int" integersnil ))nil ))nil 3249305393"" (skosimp*) (("" (rewrite "finite_purge" ) nil nil )) nil )nil finite_bags nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*) (("" (rewrite "finite_delete" ) nil nil )) nil )nil finite_bags nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (rewrite "finite_emptybag" ) nil nil )nil finite_bags nil )) nil ))nil 3286293715"" (skosimp*) (("" (rewrite "finite_extract" ) nil nil )) nil )nil finite_bags nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil ))nil )nil 3286293634 ("" (postpone) nil nil ) nil shostak))nil 3249305393"" (expand "emptybag" )"" (expand "card" )"" (expand "bag_to_set" )"" (lemma "sum_emptyset" )"" (inst?)"" (expand "emptyset" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"nat" finite_bags nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_bags nil )nil finite_sets_sum "finite_sets/" )"set" sets nil )"set[T]" bags_to_sets nil )"bag" bags nil ))nil ))nil 3249305393"" (skosimp*)"" (rewrite "emptybag_is_empty?" )"" (iff)"" (split)"1" (flatten)"1" (expand "card" )"1" (expand "emptybag" )"1" (use "sum_is_null" )"1" (assert )"1" (case "EXISTS x: B!1(x) > 0" )"1" (skosimp*)"1" (inst -2 "x!1" )"1" (assert )"1" (expand "bag_to_set" )"1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (grind)"2" (use "emptybag_is_empty?" )"2" (expand "emptybag" )"2" (expand "empty?" )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "card_emptybag" )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_bags nil )nil name-judgement "finite_bag" finite_bags nil )"nat" finite_bags nil )nil finite_sets_sum_real "finite_sets/" )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[T]" bags_to_sets nil )nil application-judgement "finite_set" finite_bags nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"bool" bags nil )"bool" sets nil )"bool" sets nil )nil application-judgement "int" finite_bags nil )nil application-judgement "nat" finite_bags nil )"bag" bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (expand "singleton_bag" )"" (expand "card" )"" (expand "bag_to_set" )"" (skosimp*)"" case "{t_3: T | IF t_3 = t!1 THEN 1 ELSE 0 ENDIF > 0} = ") "1" (replace -1)"1" (hide -1)"1" (lemma "sum_singleton" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" finite_bags nil )"(strict_total_order?[real])" real_props nil )nil finite_sets_sum "finite_sets/" )nil number_fields nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integers nil )"posint" nil )nil application-judgement "nat" finite_bags nil )nil application-judgement "int" finite_bags nil )"odd_int" integersnil )"non_empty_finite_set[T]" finite_bags nil )nil finite_bags nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )set type-eq-decl nil sets nil )"bool" sets nil )"(singleton?)" sets nil )"set[T]" bags_to_sets nil )"bag" bags nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "subbag?" )"" (expand "card" )"" (lemma "sum_order_sub" )"" (inst?)"" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (expand "subset?" )"2" (expand "member" )"2" (expand "bag_to_set" )"2" (skosimp*)"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bags nil )nil finite_bags nil )nil finite_sets_sum_real"finite_sets/" )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" sets nil )nil real_types nil )nil finite_bags nil )"bool" finite_bags nil )"set[T]" bags_to_sets nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil application-judgement "finite_set" finite_bags nil )"nat" finite_bags nil ))nil ))nil 3249305393"" (skosimp*) (("" (use "finite_update" ) nil nil )) nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_bags nil )nil finite_bags nil ))nil ))nil 3495462629"" (skosimp*)"" (case "B!1(x!1) = 0" )"1" (expand "card" )"1" (case "xn!1 = 0" )"1" (replace * -1 -2)"1" (assert )"1" (case "B!1 WITH [x!1 := 0] = B!1" )"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (apply-extensionality 1)"2" (lift-if) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" case "bag_to_set(B!1 WITH [x!1 := xn!1]) = add(x!1,bag_to_set(B!1))" )"1" (replace -1)"1" (rewrite "sum_add" )"1" (case "NOT member(x!1, bag_to_set(B!1))" )"1" (replace 1)"1" (assert )"1" (replace -2)"1" (apply-eta "B!1" )"1" (replace -1 :hide? t)"1" (apply-eta "B!1 WITH [x!1 := xn!1]" )"1" replace -1 :hide? t)"1" "sum_particular_gen" )"1" replace -1)"1" assert )"1" "1" expand "member" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bag_to_set" )"2" (expand "member" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (apply-extensionality 1 :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "card" )"2" (apply-eta " B!1 WITH [x!1 := xn!1]" )"2" (replace -1 :hide? t)"2" (apply-eta " B!1" )"2" (replace -1 :hide? t)"2" (case "xn!1 = 0" )"1" case "bag_to_set(B!1) = add(x!1,bag_to_set(B!1 WITH [x!1 := xn!1]))" )"1" (replace -1 :hide? t)"1" case "is_finite[T](bag_to_set[T](B!1 WITH [x!1 := xn!1]))" )"1" (rewrite "sum_add" )"1" (expand "member" )"1" (lift-if)"1" "1" "1" assert )"1" expand "bag_to_set" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "sum_particular_gen" )"2" replace -1 :hide? t)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (rewrite "bag_to_set_TCC1" )"2" (hide 2)"2" (rewrite "finite_update" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bag_to_set" )"2" (expand "add" )"2" (expand "member" )"2" (apply-extensionality 1 :hide? t)"2" (case "x!1 = x!2" )"1" (ground) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "bag_to_set(B!1 WITH [x!1 := xn!1]) = bag_to_set(B!1)" )"1" (replace -1 :hide? t)"1" (use "sum_particular_gen" )"1" (replace -1 :hide? t)"1" (lift-if)"1" (expand "bag_to_set" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "bag_to_set" )"2" (apply-extensionality 1 :hide? t)"2" (lift-if) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil finite_bags nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil application-judgement "finite_set" finite_bags nil )"int" integers nil )nil application-judgement "int" finite_bags nil )nil application-judgement "nat" finite_bags nil )"int" integers nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets_sum_real"finite_sets/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )nil number_fields nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets_sum "finite_sets/" )"non_empty_finite_set[T]" finite_bags nil )set type-eq-decl nil sets nil )"set[T]" bags_to_sets nil )"bool" sets nil )"(nonempty?)" sets nil )"nat" finite_bags nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil finite_bags nil )nil finite_bags nil )"real" reals nil ))nil )nil 3249305393"" (skosimp*)"" (case "B!1(x!1) = 0" )"1" (expand "card" )"1" (case "xn!1 = 0" )"1" (replace * -1 -2)"1" (assert )"1" (case "B!1 WITH [x!1 := 0] = B!1" )"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (apply-extensionality 1)"2" (lift-if) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" case "bag_to_set(B!1 WITH [x!1 := xn!1]) = add(x!1,bag_to_set(B!1))" )"1" (replace -1)"1" (rewrite "sum_add" )"1" (case "NOT member(x!1, bag_to_set(B!1))" )"1" (replace 1)"1" (assert )"1" (replace -2)"1" (apply-eta "B!1" )"1" (replace -1 :hide? t)"1" (apply-eta "B!1 WITH [x!1 := xn!1]" )"1" replace -1 :hide? t)"1" "sum_particular_gen" )"1" replace -1)"1" assert )"1" "1" expand "member" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bag_to_set" )"2" (expand "member" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (apply-extensionality 1 :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "card" )"2" (apply-eta " B!1 WITH [x!1 := xn!1]" )"2" (replace -1 :hide? t)"2" (apply-eta " B!1" )"2" (replace -1 :hide? t)"2" (case "xn!1 = 0" )"1" case "bag_to_set(B!1) = add(x!1,bag_to_set(B!1 WITH [x!1 := xn!1]))" )"1" (replace -1 :hide? t)"1" case "is_finite[T](bag_to_set[T](B!1 WITH [x!1 := xn!1]))" )"1" (rewrite "sum_add" )"1" (expand "member" )"1" (lift-if)"1" "1" "1" assert )"1" expand "bag_to_set" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "sum_particular_gen" )"2" replace -1 :hide? t)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (rewrite "bag_to_set_TCC1" )"2" (hide 2)"2" (rewrite "finite_update" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bag_to_set" )"2" (expand "add" )"2" (expand "member" )"2" (apply-extensionality 1 :hide? t)"2" (case-old-lift-if 1)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "bag_to_set(B!1 WITH [x!1 := xn!1]) = bag_to_set(B!1)" )"1" (replace -1 :hide? t)"1" (use "sum_particular_gen" )"1" (replace -1 :hide? t)"1" (lift-if)"1" (expand "bag_to_set" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "bag_to_set" )"2" (apply-extensionality 1 :hide? t)"2" (lift-if) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[T]" bags_to_sets nil )nil finite_sets_sum "finite_sets/" )nil finite_sets_sum_real"finite_sets/" )nil bags nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "delete" )"" (lemma "card_bag_particular" )"" "B!1" "e!1" "IF B!1(e!1) > n!1 THEN B!1(e!1) - n!1 ELSE 0 ENDIF" )"1" (expand "min" )"1" (lift-if)"1" (case "B!1(e!1) > n!1" )"1" (assert )"1" case "B!1 WITH [e!1 := B!1(e!1) - n!1] = (LAMBDA (t: T): IF e!1 = t THEN B!1(t) - n!1 ELSE B!1(t) ENDIF)" )"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (apply-extensionality 1 :hide? t)"1" (lift-if) (("1" (assert ) nil nil )) nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert )"2" "(LAMBDA (t: T): IF e!1 = t THEN IF B!1(t) >= n!1 THEN B!1(t) - n!1") "2" (apply-extensionality 1)"2" (lift-if) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"{k: nat | k <= i AND k <= j}" nil )"bag" bags nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" finite_bags nil )"T" finite_bags nil )"finite_bag" finite_bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil finite_bags nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"int" integers nil )"[T, T -> boolean]" equalities nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "insert" )"" (lemma "card_bag_particular" )"" (inst -1 "B!1" "x!1" "B!1(x!1) + 1" )"" (assert )"" (replace -1 :dir rl)"" (hide -1)"" "(LAMBDA (t: T): IF x!1 = t THEN 1 + B!1(t) ELSE B!1(t) ENDIF) = B!1 WITH [x!1 := 1 + B!1(x!1)]" )"" (hide 2)"" (apply-extensionality :hide? t)"" (lift-if) (("" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bag" bags nil )"posint" nil )nil finite_bags nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"int" integers nil )"posint" nil )nil finite_bags nil ))nil ))nil 3249305393"" (use "card_bag_empty?" )"" (skosimp*)"" (inst?)"" (expand "nonempty_bag?" ) (("" (ground) nil nil )) nil ))nil ))nil ))nil )"bool" bags nil )"(strict_total_order?[real])" real_props nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_bags nil )nil finite_bags nil ))nil ))nil 3249305393"" (skosimp*)"" (expand "disjoint?" )"" (rewrite "card_bag_empty?" ) nil nil )) nil ))nil )"bool" bags nil )"bag" bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_bags nil )nil finite_bags nil )nil application-judgement "finite_bag" finite_bags nil ))nil ))nil 3249305393"" (skosimp*)"" case "(FORALL (S: finite_set[T]): subset?(S,bag_to_set(A!1)) IMPLIES sum(S, (LAMBDA (t: T): union(A!1, B!1)(t))) LAMBDA (t: T): A!1(t))))") "1" (inst?)"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (expand "subset?" ) (("2" (skosimp*) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "S" 1 "finite_set_induction_rest" )"1" (skosimp*)"1" (rewrite "sum_emptyset" )"1" (rewrite "sum_emptyset" ) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "sum" 1)"2" (split -1)"1" (replace -1)"1" (hide -1)"1" case "union(A!1, B!1)(choose(SS!1)) = A!1(choose(SS!1))" )"1" (assert ) nil nil )"2" (hide 2)"2" (expand "subset?" )"2" (expand "member" )"2" (case "A!1(choose(SS!1)) = 0" )"1" case "NOT bag_to_set(A!1)(choose(SS!1))" )"1" "choose(SS!1)" )"1" (assert ) nil nil ))nil )"2" expand "bag_to_set" -1)"2" (assert ) nil nil ))nil ))nil )"2" "B!1(choose(SS!1)) = 0" )"1" expand "union" )"1" expand "max" )"1" (assert ) nil nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" "choose(SS!1)" )"2" expand "min" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "rest_subset" )"2" (inst?)"2" (lemma "subset_transitive[T]" )"2" "rest(SS!1)" "SS!1" "bag_to_set(A!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bag" bags nil )"R" finite_sets_sum "finite_sets/" )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_bags nil )"bool" finite_bags nil )"set[T]" bags_to_sets nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" sets nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_bags nil )"real" reals nil )nil application-judgement "nat" finite_bags nil )nil application-judgement "int" finite_bags nil )nil application-judgement "finite_set" finite_bags nil )nil defined_types nil )nil finite_sets_inductions"finite_sets/" )nil finite_sets_sum "finite_sets/" )"set" sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"bool" sets nil )"(p)" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )nil application-judgement "finite_bag" finite_bags nil )"(partial_order?[set[T]])" nil )"(partial_order?[set[T]])" nil )"nonneg_int" nil )"finite_set[T]" finite_bags nil )"(strict_total_order?[real])" real_props nil )"bag" bags nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" bags nil )"bool" bags nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" sets nil ))nil ))nil 3286293750"" (skosimp*)"" (use "extract_subbag" ) (("" (rewrite "card_subbag?" ) nil nil ))nil ))nil )nil bags nil )nil finite_bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bag" bags nil )nil finite_bags nil )nil application-judgement "finite_bag" finite_bags nil ))nil )nil 3286293506"" (skosimp*)"" (use "subbag_extract" ) (("" (rewrite "card_subbag?" ) nil ))))nil )nil nil ))nil 3286293528"" (skosimp*)"" (expand "card" )"" (use "extract_empty_or_singlton_set" )"" (split)"1" (use "extract_singleton" )"1" (assert )"1" (replace -1 :dir rl)"1" (use "sum_singleton" )"1" (replace -1)"1" (assert )"1" (expand "extract" +)"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "emptyset_is_empty?" )"2" (assert )"2" (replace -1)"2" (use "sum_emptyset" )"2" (replace -1)"2" (hide -1 -3)"2" (expand "bag_to_set" )"2" (expand "extract" )"2" (decompose-equality)"2" (inst?)"2" expand "emptyset" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" finite_bags nil )nil application-judgement "nat" finite_bags nil )nil application-judgement "int" finite_bags nil )nil application-judgement "finite_bag" finite_bags nil )nil application-judgement "finite_set" finite_bags nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )nil number_fields nil )nil finite_sets_sum "finite_sets/" )"bag" bags nil )"int" integers nil )"non_empty_finite_set[T]" finite_bags nil )"real" reals nil )"even_int" integersnil )"real" reals nil )"nonneg_int" nil )nil bags_to_sets nil )"finite_set[T]" finite_bags nil )"finite_set" finite_sets nil )nil finite_sets_sum "finite_sets/" )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )set type-eq-decl nil sets nil )"set[T]" bags_to_sets nil )nil sets_lemmas nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_bags nil )nil bags_to_sets nil ))nil ))nil 3286297464"" (skosimp*)"" (use "bag_disj_set" )"" (assert )"" (hide -2)"" (expand "card" )"" (lemma "sum_disj_union" )"" "bag_to_set(A!1)" "bag_to_set(B!1)" "LAMBDA (t: T): union(A!1, B!1)(t)" )"" (assert )"" (use "bag_set_dist_union" )"" (replace -1)"" (replace -2)"" (reveal -3)"" (forward-chain "sum_bag_disj_union" )"" (rewrite "bag_disj_comm" )"" "sum_bag_disj_union" )"" "B!1" "A!1" )"" assert )"" replace -2)"" rewrite "bag_union_comm" )"" replace -1)"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil bags_to_sets nil )nil finite_bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_sets_sum "finite_sets/" )nil number_fields nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil application-judgement "nat" finite_bags nil )nil application-judgement "int" finite_bags nil )nil bags nil )nil bags nil )"finite_set[T]" finite_bagsnil )nil finite_bags nil )nil bags_to_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set[T]" bags_to_sets nil )"bag" bags nil )nil application-judgement "finite_set" finite_bags nil )"nat" finite_bags nil )nil application-judgement "finite_bag" finite_bags nil )"nonneg_int" nil ))nil )nil 3286295983"" (skosimp*)"" (use "disj_bag_set" )"" (assert )"" (hide -2)"" (expand "card" )"" (lemma "sum_bag_disj_union" )"" "bag_to_set(A!1)" "bag_to_set(B!1)" "LAMBDA (t: T): union(A!1, B!1)(t)" )"" (assert )"" (use "bag_set_dist_union" )"" (replace -1)"" (replace -2)"" (reveal -3)"" (forward-chain "sum_bag_disj_union" )"" (rewrite "bag_disj_comm" )"" "sum_bag_disj_union" )"" "B!1" "A!1" )"" assert )"" replace -2)"" rewrite "bag_union_comm" )"" replace -1)"" nil ))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3286294959"" (skosimp*)"" (use "disj_bag_set" )"" (assert )"" (hide -2)"" (expand "card" )"" (lemma "sum_disj_union" )"" "bag_to_set(A!1)" "bag_to_set(B!1)" "LAMBDA (t: T): union(A!1, B!1)(t)" )"" (assert )"" (use "bag_set_dist_union" )"" (replace -1)"" (replace -2)"" (reveal -3)"" (forward-chain "sum_bag_disj_union" )"" (rewrite "bag_disj_comm" )"" "sum_bag_disj_union" )"" "B!1" "A!1" )"" assert )"" replace -2)"" rewrite "union_comm" )"" replace -1)"" nil ))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3286293554"" (skosimp*)"" (use "disj_bag_set" )"" (assert )"" (hide -2)"" (expand "card" )"" (lemma "sum_disj_union" )"" "bag_to_set(A!1)" "bag_to_set(B!1)" "LAMBDA (t: T): union(A!1, B!1)(t)" )"" (assert )"" (use "bag_set_dist_union" )"" (replace -1)"" (replace -2)"" (reveal -3)"" (forward-chain "sum_bag_disj_union" )"" (rewrite "disj_comm" )"" "sum_bag_disj_union" )"" "B!1" "A!1" )"" assert )"" replace -2)"" rewrite "union_comm" )"" replace -1)"" nil ))))))))))))))))))))))))))))))))))))))))nil )nil nil ))nil 3286293569"" (skosimp*)"" (use "bag_purge_extract" )"" (use "bag_disj_extract_perge" )"" (use "card_disjoint_add" )"" (assert )"" (use "bag_disj_comm" )"" (replace -) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil bags nil )nil finite_bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_bags nil )"bag" bags nil )"bag" bags nil )nil application-judgement "finite_bag" finite_bags nil )nil application-judgement "finite_bag" finite_bags nil )nil bags nil )nil application-judgement "finite_bag" finite_bags nil )"int" integers nil )nil bags nil ))nil ))nil 3286295105"" (skosimp*)"" (case "x!1 /= y!1" )"1" (lemma "extract_disj" )"1" (inst - "A!1" "x!1" "y!1" )"1" (assert )"1" (use "card_disjoint_add" )"1" (assert )"1" (replace -1)"1" (rewrite "card_extract_bag" )"1" (rewrite "card_extract_bag" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "/=" ) (("2" (propax) nil nil )) nil ))nil ))nil )"boolean" notequal nil )nil booleans nil )nil finite_bags nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_bags nil )"bag" bags nil )nil finite_bags nil )nil application-judgement "finite_bag" finite_bags nil )nil application-judgement "finite_bag" finite_bags nil )"nonneg_int" nil )nil bags nil ))nil )nil 3286293584"" (skosimp*)"" (case "x!1 /= y!1" )"1" (lemma "extract_disj" )"1" (inst - "A!1" "x!1" "y!1" )"1" (assert )"1" (use "disjoint_add" )"1" (assert )"1" (replace -1)"1" (rewrite "card_extract_bag" )"1" (rewrite "card_extract_bag" )nil )))))))))))))))"2" (expand "/=" ) (("2" (propax) nil ))))))nil )nil nil ))nil 3286293598"" (skosimp*)"" (use "bag_extract_union_subbag" )"" (assert ) (("" (rewrite "card_subbag?" ) nil nil )) nil )) nil ))nil )nil bags nil )nil finite_bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bag" bags nil )"bag" bags nil )nil finite_bags nil )"(total_order?[real])" nil )nil application-judgement "finite_bag" finite_bags nil )nil application-judgement "finite_bag" finite_bags nil ))nil ))nil 3286293610"" (skosimp*)"" (use "card_extract_bag" )"" (replace - :dir rl) (("" (use "card_extract" ) nil ))))))nil )nil finite_bags nil )nil finite_bags nil )"bool" finite_bags nil )nil bags nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_bags nil )nil finite_bags nil ))nil ))nil 3286295232"" (skosimp*)"" (case "x!1 = y!1" )"1" (propax) nil nil )"2" (use "card_union_extract_add" )"2" (assert )"2" (replace - :dir rl)"2" (rewrite "card_union_extract" ) nil nil )) nil ))nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil finite_bags nil )"nonneg_int" nil )"(total_order?[real])" nil )nil finite_bags nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil bags nil )"bool" finite_bags nil )nil finite_bags nil )nil finite_bags nil ))nil )nil 3286295175"" (skosimp*)"" (case "x!1 = y!1" )"1" (propax) nil )"2" (use "extract_union_add" )"2" (assert )"2" (replace - :dir rl)"2" (rewrite "extract_union_card" ) nil ))))))))))nil )nil nil )nil 3286293626"" (skosimp*)"" (case "x!1 = y!1" )"1" (propax) nil )"2" (use "union_extract_add" )"2" (assert )"2" (replace - :dir rl)"2" (rewrite "union_extract_card" ) nil ))))))))))nil )nil nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.43 Sekunden
(vorverarbeitet am 2026-05-02)
¤ *© Formatika GbR, Deutschland
2026-05-26
