(finite_bags_auxnil 3306770024"" (skosimp*)"" (auto-rewrite "nonempty_bag?" )"" (expand "rest" )"" (rewrite "finite_delete" )"" (use "finite_emptybag" ) (("" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"bag" bags_aux nil )nil application-judgement "finite_bag[T]" finite_bags_aux nil ))nil ))nil 3306769997"" (skosimp*)"" (auto-rewrite "nonempty_bag?" )"" (expand "rest" )"" (rewrite "finite_delete" )"" (use "finite_emptybag" ) (("" (ground) nil ))))))))))nil )"bag" bags_aux nil )nil application-judgement "finite_bag[T]" finite_bags_aux nil ))nil ))nil 3306769997"" (skosimp*)"" (expand "rest" )"" (expand "nonempty_bag?" )"" (lift-if)"" (assert )"" (rewrite "card_bag_delete" )"1" (assert )"1" (expand "min" )"1" (lift-if)"1" (ground)"1" (use "choose_gt_zero" )"1" (expand "nonempty_bag?" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty_bag?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bag" bags_aux 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 )"T" bags_aux nil )nil finite_bags_aux nil )"{k: nat | k <= i AND k <= j}" nil )"int" integers nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"even_int" integersnil )"(strict_total_order?[real])" real_props nil )nil bags_aux nil )"int" integers nil )"posint" nil )nil application-judgement "finite_bag[T]" finite_bags_aux nil )"bool" bags nil ))nil ))nil 3306769997"" (skosimp*)"" (expand "is_finite" )"" (typepred "b!1" )"" (expand "is_finite" )"" (expand "is_finite" )"" (expand "injective?" )"" (skosimp*)"" "N!1" "(LAMBDA (t:{t: T | IF p!1(t) ") "1" (skosimp*)"1" (inst?)"1" (grind) nil nil )"2" (typepred "x2!1" )"2" (typepred "b!1(x2!1)" )"2" (hide -3) (("2" (grind) nil nil )) nil ))nil ))nil )"3" (typepred "x1!1" )"3" (hide -2) (("3" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (grind) nil nil )) nil )"3" (skosimp*)"3" (typepred "t!1" ) (("3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" finite_bags nil )"bool" finite_sets nil )"bool" functions nil )"set[T]" bags_to_sets nil )set type-eq-decl nil sets nil )"bool" booleans nil )"finite_bag[T]" finite_bags_aux nil )"bool" reals nil )"pred[T]" finite_bags_aux nil )nil defined_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bag" bags_aux nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil nat_types nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set" finite_bags_aux nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_bags_aux 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 )nil finite_bags nil ))nil ))nil 3306769997"" (skosimp*) (("" (rewrite "finite_filter" ) nil )) nil )nil finite_bags_aux nil )nil finite_bags_aux 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 defined_types nil ))nil ))nil 3306769997"" (skosimp*)"" (lemma "filter_insert" )"" (inst?)"" (replace -1 :hide? t)"" (case "p!1(x!1)" )"1" (assert )"1" (use "card_bag_insert" ) (("1" (assert ) nil )))))"2" (assert ) nil ))))))))))nil )nil finite_bags_aux nil )nil bags_aux nil )"nonneg_int" nil )nil application-judgement "finite_bag" finite_bags_aux nil )nil application-judgement "nonempty_finite_bag[T]" finite_bags_auxnil )"posint" nil )"posint" nil )"int" integers nil )"bag" bags_aux nil )nil finite_bags nil )nil defined_types 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 ))nil 3306769997"" (skosimp*)"" (use "filter_delete" )"" (replace -1 :hide? t)"" (lemma "card_bag_delete" )"" (inst -1 "filter(b!1, p!1)" "x!1" "n!1" )"" (replace -1 :hide? t)"" (expand "filter" ) (("" (grind) nil ))))))))))))))nil )nil bags_aux nil )nil finite_bags_aux nil )nil defined_types 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 )"(strict_total_order?[real])" real_props nil )"{k: nat | k <= i AND k <= j}" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" reals nil )"bag" bags_aux nil )nil application-judgement "finite_bag" finite_bags_aux nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
