|
(finite_bags_minmax
(max_TCC1 0
(max_TCC1-1 nil 3288716520
("" (skosimp*)
(("" (typepred! "D!1") (("" (assert) (("" (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-nonempty-type-decl nil finite_bags_minmax nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "finite_set" finite_bags_minmax nil))
shostak))
(max_member 0
(max_member-1 nil 3288828586
("" (skosimp*)
(("" (expand "member")
(("" (expand "max")
(("" (expand "bag_to_set")
(("" (typepred! "max({t: T | D!1(t) > 0})")
(("1" (propax) nil nil)
("2" (typepred! "D!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" bags nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(T formal-nonempty-type-decl nil finite_bags_minmax 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)
(empty? const-decl "bool" bags nil)
(nonempty_finite_bag type-eq-decl nil finite_bags 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)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(leq formal-const-decl "(total_order?[T])" finite_bags_minmax nil)
(max const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
finite_sets_minmax "finite_sets/")
(max const-decl "T" finite_bags_minmax nil))
shostak))
(min_member 0
(min_member-1 nil 3288828659
("" (skosimp*)
(("" (expand "member")
(("" (expand "min")
(("" (expand "bag_to_set")
(("" (typepred! "min({t: T | D!1(t) > 0})")
(("1" (propax) nil nil)
("2" (typepred! "D!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" bags nil)
(bag_to_set const-decl "set[T]" bags_to_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(T formal-nonempty-type-decl nil finite_bags_minmax 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)
(empty? const-decl "bool" bags nil)
(nonempty_finite_bag type-eq-decl nil finite_bags 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)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(leq formal-const-decl "(total_order?[T])" finite_bags_minmax nil)
(min const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
finite_sets_minmax "finite_sets/")
(min const-decl "T" finite_bags_minmax nil))
nil)))
¤ Dauer der Verarbeitung: 0.29 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.
|
