|
(finite_bags_aux
(finite_bag_rest 0
(finite_bag_rest-1 nil 3306770024
("" (skosimp*)
(("" (auto-rewrite "nonempty_bag?")
(("" (expand "rest")
(("" (rewrite "finite_delete")
(("" (use "finite_emptybag") (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
((rest const-decl "bag" bags_aux nil)
(nil application-judgement "finite_bag[T]" finite_bags_aux nil))
nil))
(rest_TCC1 0
(rest_TCC1-1 nil 3306769997
("" (skosimp*)
(("" (auto-rewrite "nonempty_bag?")
(("" (expand "rest")
(("" (rewrite "finite_delete")
(("" (use "finite_emptybag") (("" (ground) nil))))))))))
nil)
((rest const-decl "bag" bags_aux nil)
(nil application-judgement "finite_bag[T]" finite_bags_aux nil))
nil))
(card_bag_rest 0
(card_bag_rest-1 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)
((rest const-decl "bag" bags_aux nil)
(card_bag_delete formula-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)
(choose const-decl "T" bags_aux nil)
(T formal-type-decl nil finite_bags_aux nil)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(choose_gt_zero formula-decl nil bags_aux nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nil application-judgement "finite_bag[T]" finite_bags_aux nil)
(nonempty_bag? const-decl "bool" bags nil))
nil))
(finite_filter 0
(finite_filter-1 nil 3306769997
("" (skosimp*)
(("" (expand "is_finite")
(("" (typepred "b!1")
(("" (expand "is_finite")
(("" (expand "is_finite")
(("" (expand "injective?")
(("" (skosimp*)
((""
(inst 1 "N!1" "(LAMBDA (t:{t: T | IF p!1(t)
THEN b!1(t) > 0
ELSE FALSE ENDIF}): f!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)
((is_finite const-decl "bool" finite_bags nil)
(is_finite const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(set type-eq-decl nil sets nil)
(FALSE const-decl "bool" booleans nil)
(b!1 skolem-const-decl "finite_bag[T]" finite_bags_aux nil)
(> const-decl "bool" reals nil)
(p!1 skolem-const-decl "pred[T]" finite_bags_aux nil)
(pred type-eq-decl nil defined_types nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(filter const-decl "bag" bags_aux nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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)
(nil application-judgement "finite_set" finite_bags_aux nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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_aux 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)
(finite_bag type-eq-decl nil finite_bags nil))
nil))
(filter_TCC1 0
(filter_TCC1-1 nil 3306769997
("" (skosimp*) (("" (rewrite "finite_filter") nil)) nil)
((finite_filter formula-decl nil finite_bags_aux nil)
(T formal-type-decl nil finite_bags_aux 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)
(pred type-eq-decl nil defined_types nil))
nil))
(card_filter_insert 0
(card_filter_insert-1 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)
((T formal-type-decl nil finite_bags_aux nil)
(filter_insert formula-decl nil bags_aux nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nil application-judgement "finite_bag" finite_bags_aux nil)
(nil application-judgement "nonempty_finite_bag[T]" finite_bags_aux
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(filter const-decl "bag" bags_aux nil)
(card_bag_insert formula-decl nil finite_bags nil)
(pred type-eq-decl nil defined_types 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))
nil))
(card_filter_delete 0
(card_filter_delete-1 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)
((filter_delete formula-decl nil bags_aux nil)
(T formal-type-decl nil finite_bags_aux nil)
(pred type-eq-decl nil defined_types 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)
(card_bag_delete formula-decl nil finite_bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(real_times_real_is_real application-judgement "real" reals nil)
(filter const-decl "bag" bags_aux nil)
(nil application-judgement "finite_bag" finite_bags_aux nil))
nil)))
¤ Dauer der Verarbeitung: 0.16 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.
|
