|
(finite_bags_inductions
(cardinal_induction 0
(cardinal_induction-1 nil 3306770151 ("" (grind :defs nil) nil nil)
((card const-decl "nat" finite_bags 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)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil finite_bags_inductions 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(finite_bag_induction 0
(finite_bag_induction-1 nil 3306770151
("" (skolem!)
(("" (flatten)
(("" (lemma "cardinal_induction")
(("" (inst -1 "pb!1")
(("" (flatten)
(("" (hide -1)
(("" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skosimp*)
(("1" (hide -3)
(("1" (use "card_nonempty_bag?")
(("1" (assert)
(("1" (expand "nonempty_bag?")
(("1"
(use "emptybag_is_empty?")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst -1 "rest(b!1)")
(("2" (inst -4 "choose(b!1)" "rest(b!1)")
(("1" (case "b!1 = emptybag[T]")
(("1" (assert) nil nil)
("2" (assert)
(("2"
(case " nonempty_bag?(b!1)")
(("1"
(rewrite "insert_choose_rest")
(("1"
(lemma
"finite_bags_aux.card_bag_rest")
(("1"
(inst -1 "b!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(use "emptybag_is_empty?")
(("2"
(hide -2 -3 -4 -5 -6 3)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -3 2)
(("2" (lemma "card_bag_empty?")
(("2"
(inst?)
(("2"
(assert)
(("2"
(ground)
(("2"
(hide -1)
(("2"
(expand "nonempty_bag?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil finite_bags_inductions 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)
(b!1 skolem-const-decl "finite_bag[T]" finite_bags_inductions nil)
(choose const-decl "T" bags_aux nil)
(nil application-judgement "nonempty_finite_bag[T]"
finite_bags_inductions nil)
(empty? const-decl "bool" bags nil)
(insert_choose_rest formula-decl nil bags_aux nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(card_bag_rest formula-decl nil finite_bags_aux nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(emptybag const-decl "bag" bags nil)
(card_bag_empty? formula-decl nil finite_bags nil)
(rest const-decl "bag" bags_aux nil)
(nil application-judgement "finite_bag[T]" finite_bags_inductions
nil)
(card_nonempty_bag? formula-decl nil finite_bags nil)
(nil name-judgement "finite_bag" finite_bags_inductions nil)
(nonempty_bag? const-decl "bool" bags nil)
(emptybag_is_empty? formula-decl nil bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(card const-decl "nat" finite_bags nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(cardinal_induction formula-decl nil finite_bags_inductions nil))
nil)))
¤ Dauer der Verarbeitung: 0.18 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.
|
