| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 5 kB |
|
Quelle finite_bags_minmax.prf Sprache: Lisp |
|||||||||
|
(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.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28