|
(bags_aux
(choose_TCC1 0
(choose_TCC1-1 nil 3506271674 ("" (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)
(nonempty_bag? const-decl "bool" bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty? const-decl "bool" bags nil)
(T formal-type-decl nil bags_aux nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(rest_TCC1 0
(rest_TCC1-1 nil 3506271674 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil bags_aux nil)
(empty? const-decl "bool" bags nil)
(nonempty_bag? const-decl "bool" bags nil))
nil))
(choose_gt_zero 0
(choose_gt_zero-1 nil 3506271674
("" (skosimp*)
(("" (expand "nonempty_bag?")
(("" (lemma "choose_member[T]")
(("" (expand "choose")
(("" (inst?)
(("" (use "bag_to_set_emptybag")
(("" (use "emptybag_is_empty?")
(("" (ground)
(("1" (expand "member")
(("1" (expand "bag_to_set")
(("1" (expand "choose") (("1" (propax) nil)))))))
("2" (rewrite "empty_bts_bag") nil))))))))))))))))
nil)
((nonempty_bag? const-decl "bool" bags nil)
(choose const-decl "T" bags_aux nil)
(bag_to_set_emptybag formula-decl nil bags_to_sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(member const-decl "bool" sets nil)
(empty_bts_bag formula-decl nil bags_to_sets nil)
(emptybag_is_empty? formula-decl nil 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)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(choose_member formula-decl nil sets_lemmas nil)
(T formal-type-decl nil bags_aux nil))
nil))
(insert_choose_rest 0
(insert_choose_rest-1 nil 3506271674
("" (skosimp*)
(("" (expand "rest")
(("" (expand "nonempty_bag?")
(("" (assert)
(("" (rewrite "insert_delete")
(("1" (use "choose_gt_zero")
(("1" (expand "nonempty_bag?") (("1" (propax) nil)))))
("2" (expand "nonempty_bag?")
(("2" (propax) nil))))))))))))
nil)
((rest const-decl "bag" bags_aux nil)
(choose_gt_zero formula-decl nil bags_aux nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(T formal-type-decl nil bags_aux nil)
(choose const-decl "T" bags_aux 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_delete formula-decl nil bags nil)
(nonempty_bag? const-decl "bool" bags nil))
nil))
(filter_emptybag 0
(filter_emptybag-1 nil 3506271674
("" (skosimp*)
(("" (expand "filter")
(("" (expand "emptybag") (("" (propax) nil))))))
nil)
((filter const-decl "bag" bags_aux nil)
(emptybag const-decl "bag" bags nil))
nil))
(filter_insert 0
(filter_insert-1 nil 3506271674
("" (skosimp*)
(("" (expand "filter")
(("" (expand "insert")
(("" (apply-extensionality 1 :hide? t)
(("" (lift-if) (("" (assert) nil))))))))))
nil)
((filter const-decl "bag" bags_aux nil)
(T formal-type-decl nil 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)
(bag type-eq-decl nil bags nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(insert const-decl "bag" bags nil))
nil))
(filter_delete 0
(filter_delete-1 nil 3506271674
("" (skosimp*)
(("" (expand "filter")
(("" (expand "delete")
(("" (apply-extensionality 1 :hide? t) (("" (grind) nil))))))))
nil)
((filter const-decl "bag" bags_aux nil)
(T formal-type-decl nil 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(delete const-decl "bag" bags nil))
nil))
(filter_prop 0
(filter_prop-1 nil 3506271674
("" (expand "subbag?")
(("" (skosimp*)
(("" (expand "filter") (("" (lift-if) (("" (grind) nil))))))))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T formal-type-decl nil bags_aux nil)
(filter const-decl "bag" bags_aux nil)
(subbag? const-decl "bool" bags nil))
nil)))
¤ Dauer der Verarbeitung: 0.19 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.
|
