|
(finite_bags
(bag_to_set_TCC1 0
(bag_to_set_TCC1-1 nil 3249305393 ("" (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 finite_bags 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)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil))
nil))
(finite_bag 0
(finite_bag-1 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)
((is_finite const-decl "bool" finite_sets nil)
(is_finite const-decl "bool" finite_bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "finite_set" finite_bags nil)
(injective? const-decl "bool" functions nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(T formal-type-decl nil finite_bags nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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)
(bag type-eq-decl nil bags nil) (set type-eq-decl nil sets nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(finite_bag type-eq-decl nil finite_bags nil)
(B!1 skolem-const-decl "finite_bag" finite_bags nil)
(> const-decl "bool" reals nil))
shostak))
(finite_emptybag 0
(finite_emptybag-1 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)
((T formal-type-decl nil finite_bags nil)
(finite_emptyset judgement-tcc nil finite_sets nil)
(is_finite const-decl "bool" finite_bags nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(emptyset const-decl "set" sets nil)
(emptybag const-decl "bag" bags nil))
nil))
(finite_singleton_bag 0
(finite_singleton_bag-1 nil 3249305393
("" (skosimp*)
(("" (expand "singleton_bag")
(("" (expand "is_finite")
(("" (expand "bag_to_set")
(("" (expand "is_finite")
((""
(inst 1 "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)
((singleton_bag const-decl "bag" bags nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil finite_bags nil)
(> const-decl "bool" reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil)
(is_finite const-decl "bool" finite_bags nil))
nil))
(finite_insert 0
(finite_insert-1 nil 3249305393
("" (skosimp*)
(("" (expand "is_finite")
(("" (rewrite "insert_bag_lem")
(("" (rewrite "finite_add") nil nil)) nil))
nil))
nil)
((is_finite const-decl "bool" finite_bags nil)
(finite_add 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)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" finite_bags nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(insert_bag_lem formula-decl nil bags_to_sets nil))
nil))
(finite_purge 0
(finite_purge-1 nil 3249305393
("" (skosimp*)
(("" (expand "is_finite")
(("" (rewrite "purge_bag_lem")
(("" (rewrite "finite_remove") nil nil)) nil))
nil))
nil)
((is_finite const-decl "bool" finite_bags nil)
(finite_remove judgement-tcc 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)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(finite_remove application-judgement "finite_set[T]" finite_bags
nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(purge_bag_lem formula-decl nil bags_to_sets nil))
nil))
(finite_delete 0
(finite_delete-1 nil 3249305393
("" (skosimp*)
(("" (expand "delete")
(("" (typepred "B!1")
(("" (expand "is_finite")
(("" (expand "bag_to_set")
(("" (expand "is_finite")
(("" (skosimp*)
((""
(inst 1 "N!1" "(LAMBDA (t:{t: T |
IF t!1 = t THEN IF B!1(t) >= n!1 THEN B!1(t) - n!1
ELSE 0
ENDIF
ELSE B!1(t)
ENDIF
> 0}): f!1(t))")
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert) nil nil)
("2" (assert)
(("2" (assert)
(("2" (typepred "x2!1")
(("2"
(ground)
(("2"
(lift-if)
(("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)
((delete const-decl "bag" bags nil)
(is_finite const-decl "bool" finite_sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(n!1 skolem-const-decl "nat" finite_bags nil)
(B!1 skolem-const-decl "finite_bag" finite_bags nil)
(t!1 skolem-const-decl "T" finite_bags nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(> const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(injective? const-decl "bool" functions nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bag_to_set const-decl "set[T]" bags_to_sets 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 finite_bags 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)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil))
nil))
(finite_bag_union 0
(finite_bag_union-1 nil 3249305393
("" (skosimp*)
(("" (expand "is_finite")
(("" (rewrite "bag_union_lem")
(("" (rewrite "finite_union") nil nil)) nil))
nil))
nil)
((is_finite const-decl "bool" finite_bags nil)
(finite_union judgement-tcc 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)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(finite_union application-judgement "finite_set[T]" finite_bags
nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(bag_union_lem formula-decl nil bags_to_sets nil))
nil))
(finite_bag_intersection 0
(finite_bag_intersection-1 nil 3249305393
("" (skosimp*)
(("" (expand "is_finite")
(("" (rewrite "bag_intersection_lem")
(("" (lemma "finite_intersection") (("" (inst?) nil nil)) nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_bags nil)
(finite_intersection 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)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(finite_intersection1 application-judgement "finite_set[T]"
finite_bags nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(bag_intersection_lem formula-decl nil bags_to_sets nil))
nil))
(finite_bag_plus 0
(finite_bag_plus-1 nil 3249305393
("" (skosimp*)
(("" (expand "is_finite")
(("" (rewrite "bag_plus_lem")
(("" (rewrite "finite_union") nil nil)) nil))
nil))
nil)
((is_finite const-decl "bool" finite_bags nil)
(finite_union judgement-tcc 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)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(finite_union application-judgement "finite_set[T]" finite_bags
nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(bag_plus_lem formula-decl nil bags_to_sets nil))
nil))
(finite_update 0
(finite_update-1 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"
(case-replace
"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"
(inst -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"
(case-replace
"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)
((finite_bag type-eq-decl nil finite_bags nil)
(is_finite const-decl "bool" finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil finite_bags nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" finite_bags nil)
(set type-eq-decl nil sets nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_add formula-decl nil finite_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(member const-decl "bool" sets nil)
(nil application-judgement "finite_set" finite_bags nil)
(finite_subset formula-decl nil finite_sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
finite_bags nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil))
nil))
(finite_set 0
(finite_set-1 nil 3286293268 ("" (grind) nil nil)
((nil application-judgement "finite_set" finite_bags nil)) nil))
(finite_extract 0
(finite_extract-1 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)
((is_finite const-decl "bool" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(finite_subset formula-decl nil finite_sets nil)
(nil application-judgement "finite_set" finite_bags nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(extract const-decl "bag" bags nil))
nil))
(subtype_TCC1 0
(subtype_TCC1-1 nil 3249305418
("" (skosimp*) (("" (typepred "x!1") (("" (grind) nil nil)) nil))
nil)
((nonempty_finite_bag type-eq-decl nil finite_bags nil)
(empty? const-decl "bool" bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(is_finite const-decl "bool" finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil finite_bags nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nil application-judgement "finite_set" finite_bags nil)
(nonempty_bag? const-decl "bool" bags nil))
shostak))
(singleton_bag_TCC1 0
(singleton_bag_TCC1-1 nil 3249305393
("" (skosimp*) (("" (rewrite "finite_singleton_bag") nil nil)) nil)
((finite_singleton_bag formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil))
nil))
(union_TCC1 0
(union_TCC1-1 nil 3249305393
("" (skosimp*) (("" (rewrite "finite_bag_union") nil nil)) nil)
((finite_bag_union formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil))
nil))
(intersection_TCC1 0
(intersection_TCC1-1 nil 3249305393
("" (skosimp*) (("" (rewrite "finite_bag_intersection") nil nil))
nil)
((finite_bag_intersection formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil))
nil))
(plus_TCC1 0
(plus_TCC1-1 nil 3249305393
("" (skosimp*) (("" (rewrite "finite_bag_plus") nil nil)) nil)
((finite_bag_plus formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil))
nil))
(union_TCC2 0
(union_TCC2-1 nil 3249305393
("" (skosimp*)
(("" (typepred "NB!1") (("" (hide -1) (("" (grind) nil nil)) nil))
nil))
nil)
((nonempty_finite_bag type-eq-decl nil finite_bags nil)
(empty? const-decl "bool" bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(is_finite const-decl "bool" finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil finite_bags nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nil application-judgement "finite_bag" finite_bags nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(union const-decl "bag" bags nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(plus_TCC2 0
(plus_TCC2-1 nil 3249305393 ("" (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)
(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)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(nonempty_finite_bag type-eq-decl nil finite_bags nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(plus const-decl "bag" bags nil)
(empty? const-decl "bool" bags nil)
(nil application-judgement "finite_bag" finite_bags nil))
nil))
(union_TCC3 0
(union_TCC3-1 nil 3249305393 ("" (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)
(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)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(nonempty_finite_bag type-eq-decl nil finite_bags nil)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs nil)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(union const-decl "bag" bags nil)
(empty? const-decl "bool" bags nil)
(nil application-judgement "finite_bag" finite_bags nil))
nil))
(plus_TCC3 0
(plus_TCC3-1 nil 3249305393 ("" (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)
(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)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(nonempty_finite_bag type-eq-decl nil finite_bags nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nil application-judgement "finite_set" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(plus const-decl "bag" bags nil)
(empty? const-decl "bool" bags nil)
(nil application-judgement "finite_bag" finite_bags nil))
nil))
(insert_TCC1 0
(insert_TCC1-1 nil 3249305393
("" (skosimp*)
(("" (rewrite "finite_insert")
(("" (assert) (("" (grind) nil nil)) nil)) nil))
nil)
((finite_insert formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(insert const-decl "bag" bags nil)
(empty? const-decl "bool" bags nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil))
nil))
(purge_TCC1 0
(purge_TCC1-1 nil 3249305393
("" (skosimp*) (("" (rewrite "finite_purge") nil nil)) nil)
((finite_purge formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil))
nil))
(delete_TCC1 0
(delete_TCC1-1 nil 3249305393
("" (skosimp*) (("" (rewrite "finite_delete") nil nil)) nil)
((finite_delete formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil))
nil))
(emptybag_TCC1 0
(emptybag_TCC1-1 nil 3249305393
("" (rewrite "finite_emptybag") nil nil)
((finite_emptybag formula-decl nil finite_bags nil)) nil))
(extract_TCC1 0
(extract_TCC1-2 nil 3286293715
("" (skosimp*) (("" (rewrite "finite_extract") nil nil)) nil)
((finite_extract formula-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil))
nil)
(extract_TCC1-1 nil 3286293634 ("" (postpone) nil nil) nil shostak))
(card_emptybag 0
(card_emptybag-1 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)
((card const-decl "nat" finite_bags nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(restrict const-decl "R" restrict nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil finite_bags nil)
(sum_emptyset formula-decl nil finite_sets_sum "finite_sets/")
(emptyset const-decl "set" sets nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(emptybag const-decl "bag" bags nil))
nil))
(card_bag_empty? 0
(card_bag_empty?-1 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"
(skosimp*)
(("2"
(inst?)
(("2"
(inst?)
(("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)
((emptybag_is_empty? formula-decl nil bags nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bag type-eq-decl nil bags nil)
(is_finite const-decl "bool" finite_bags nil)
(finite_bag type-eq-decl nil finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(nil name-judgement "finite_bag" finite_bags nil)
(card const-decl "nat" finite_bags nil)
(sum_is_null formula-decl nil finite_sets_sum_real "finite_sets/")
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(nil application-judgement "finite_set" finite_bags nil)
(> const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty? const-decl "bool" bags nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nil application-judgement "int" finite_bags nil)
(nil application-judgement "nat" finite_bags nil)
(emptybag const-decl "bag" bags nil)
(card_emptybag formula-decl nil finite_bags nil))
nil))
(card_singleton_bag 0
(card_singleton_bag-1 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} =
singleton(t!1)")
(("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)
((card const-decl "nat" finite_bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sum_singleton formula-decl nil finite_sets_sum "finite_sets/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(restrict const-decl "R" restrict nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nil application-judgement "nat" finite_bags nil)
(nil application-judgement "int" finite_bags nil)
(odd_minus_even_is_odd application-judgement "odd_int" integers
nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" finite_bags nil)
(T formal-type-decl nil finite_bags nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(set type-eq-decl nil sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(singleton_bag const-decl "bag" bags nil))
nil))
(card_subbag? 0
(card_subbag?-1 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)
((subbag? const-decl "bool" bags nil)
(T formal-type-decl nil finite_bags nil)
(sum_order_sub formula-decl nil finite_sets_sum_real
"finite_sets/")
(subset? const-decl "bool" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(finite_bag type-eq-decl nil finite_bags nil)
(is_finite const-decl "bool" finite_bags nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nil application-judgement "finite_set" finite_bags nil)
(card const-decl "nat" finite_bags nil))
nil))
(card_bag_particular_TCC1 0
(card_bag_particular_TCC1-1 nil 3249305393
("" (skosimp*) (("" (use "finite_update") nil nil)) nil)
((finite_bag type-eq-decl nil finite_bags nil)
(is_finite const-decl "bool" finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil finite_bags nil)
(finite_update formula-decl nil finite_bags nil))
nil))
(card_bag_particular 0
(card_bag_particular-2 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"
(use "sum_particular_gen")
(("1"
(replace -1)
(("1"
(assert)
(("1"
(lift-if)
(("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"
(split)
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand "bag_to_set")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(use "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)
((finite_bag type-eq-decl nil finite_bags nil)
(is_finite const-decl "bool" finite_bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(T formal-type-decl nil finite_bags nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nil application-judgement "finite_set" finite_bags nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nil application-judgement "int" finite_bags nil)
(nil application-judgement "nat" finite_bags nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(sum_particular_gen formula-decl nil finite_sets_sum_real
"finite_sets/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(restrict const-decl "R" restrict nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(sum_add formula-decl nil finite_sets_sum "finite_sets/")
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" finite_bags nil)
(set type-eq-decl nil sets nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(card const-decl "nat" finite_bags nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(finite_update formula-decl nil finite_bags nil)
(bag_to_set_TCC1 judgement-tcc nil finite_bags nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(card_bag_particular-1 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"
(use "sum_particular_gen")
(("1"
(replace -1)
(("1"
(assert)
(("1"
(lift-if)
(("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"
(split)
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand "bag_to_set")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(use "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)")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.70 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.
|
