Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bags_to_sets.prf Sprache: Lisp

Original von: PVS^©

(bags_to_sets
(insert_bag_lem 0
  (insert_bag_lem-1 nil 3286292907
   ("" (skosimp*) (("" (apply-extensionality 1) (("" (grind) nil))))
    nil)
   ((T formal-type-decl nil bags_to_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (add const-decl "(nonempty?)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (insert const-decl "bag" bags nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (set type-eq-decl nil sets 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)
    (number nonempty-type-decl nil numbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (member const-decl "bool" sets nil))
   nil))
(purge_bag_lem 0
  (purge_bag_lem-1 nil 3286292907
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t) (("" (grind) nil)))) nil)
   ((T formal-type-decl nil bags_to_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (remove const-decl "set" sets nil)
    (purge const-decl "bag" bags nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (set type-eq-decl nil sets 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)
    (number nonempty-type-decl nil numbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (member const-decl "bool" sets nil))
   nil))
(bag_union_lem 0
  (bag_union_lem-1 nil 3286292907
   ("" (skosimp*)
    (("" (expand "bag_to_set")
      (("" (expand "union")
        (("" (expand "member")
          (("" (apply-extensionality 1 :hide? t)
            (("" (expand "max")
              (("" (lift-if)
                (("" (case "A!1(x!1) > 0")
                  (("1" (assert) nil) ("2" (assert) nil))))))))))))))))
    nil)
   ((bag_to_set const-decl "set[T]" bags_to_sets nil)
    (member const-decl "bool" sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (>= const-decl "bool" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (bag type-eq-decl nil bags nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil bags_to_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (union const-decl "bag" bags nil)
    (union const-decl "set" sets nil))
   nil))
(bag_intersection_lem 0
  (bag_intersection_lem-1 nil 3286292907
   ("" (skosimp*)
    (("" (expand "intersection")
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "member")
          (("" (expand "bag_to_set")
            (("" (expand "min")
              (("" (lift-if)
                (("" (case "A!1(x!1) > 0")
                  (("1" (ground) nil) ("2" (ground) nil))))))))))))))))
    nil)
   ((intersection const-decl "set" sets nil)
    (intersection const-decl "bag" bags nil)
    (> const-decl "bool" reals 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)
    (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)
    (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) (set type-eq-decl nil sets nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil bags_to_sets nil))
   nil))
(subbag_lem 0
  (subbag_lem-1 nil 3286292907
   ("" (skosimp*)
    (("" (expand "subbag?")
      (("" (expand "bag_to_set")
        (("" (expand "subset?")
          (("" (skosimp*)
            (("" (expand "member")
              (("" (inst?) (("" (assert) nil))))))))))))))
    nil)
   ((subbag? const-decl "bool" bags nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T formal-type-decl nil bags_to_sets nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil))
   nil))
(bag_to_set_emptybag 0
  (bag_to_set_emptybag-1 nil 3286292907
   ("" (expand "bag_to_set")
    (("" (expand "emptybag")
      (("" (expand "emptyset") (("" (propax) nil))))))
    nil)
   ((emptybag const-decl "bag" bags nil)
    (emptyset const-decl "set" sets nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil))
   nil))
(empty_bts_bag 0
  (empty_bts_bag-1 nil 3286292907
   ("" (skosimp*)
    (("" (expand "bag_to_set")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (skosimp*)
            (("" (inst?)
              (("" (typepred "b!1(x!1)")
                (("" (ground) nil))))))))))))))
    nil)
   ((bag_to_set const-decl "set[T]" bags_to_sets nil)
    (member const-decl "bool" sets nil)
    (T formal-type-decl nil bags_to_sets nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (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)
    (bag type-eq-decl nil bags nil) (empty? const-decl "bool" sets nil)
    (empty? const-decl "bool" bags nil))
   nil))
(bag_intersection_commutative 0
  (bag_intersection_commutative-1 nil 3286292907
   ("" (skosimp*)
    (("" (expand "intersection")
      (("" (apply-extensionality 1 :hide? t)
        (("1" (grind) nil) ("2" (skosimp*) (("2" (grind) nil))))))))
    nil)
   ((intersection const-decl "bag" 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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (T formal-type-decl nil bags_to_sets nil))
   nil))
(bag_union_commutative 0
  (bag_union_commutative-1 nil 3286292907
   ("" (skosimp*)
    (("" (expand "union")
      (("" (apply-extensionality 1 :hide? t)
        (("1" (grind) nil) ("2" (skosimp*) (("2" (grind) nil))))))))
    nil)
   ((union const-decl "bag" bags nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (bag type-eq-decl nil bags nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (>= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (T formal-type-decl nil bags_to_sets nil))
   nil))
(bag_plus_lem 0
  (bag_plus_lem-1 nil 3286292907
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("" (expand "bag_to_set")
        (("" (expand "union")
          (("" (expand "member")
            (("" (typepred "A!1(x!1)")
              (("" (typepred "B!1(x!1)") (("" (grind) nil))))))))))))))
    nil)
   ((T formal-type-decl nil bags_to_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (union const-decl "set" sets nil) (plus const-decl "bag" bags nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (set type-eq-decl nil sets 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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (member const-decl "bool" sets nil))
   nil))
(extract_empty_or_singlton_set 0
  (extract_empty_or_singlton_set-1 nil 3286292927
   ("" (skosimp*) (("" (grind) nil)) nil)
   ((T formal-type-decl nil bags_to_sets nil)
    (extract const-decl "bag" bags nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (singleton? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets 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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (bag type-eq-decl nil bags nil)
    (A!1 skolem-const-decl "bag[T]" bags_to_sets nil)
    (t!1 skolem-const-decl "T" bags_to_sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(extract_singleton 0
  (extract_singleton-1 nil 3286292940
   ("" (skosimp*)
    (("" (grind) (("" (decompose-equality) (("" (grind) nil)))))) nil)
   ((T formal-type-decl nil bags_to_sets nil)
    (extract const-decl "bag" bags nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (singleton? const-decl "bool" sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (set type-eq-decl nil 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (t!1 skolem-const-decl "T" bags_to_sets nil)
    (A!1 skolem-const-decl "bag[T]" bags_to_sets nil)
    (> const-decl "bool" reals nil)
    (singleton const-decl "(singleton?)" sets nil))
   nil))
(bag_disj_set 0
  (bag_disj_set-1 nil 3286292964 ("" (grind) nil nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (T formal-type-decl nil bags_to_sets nil)
    (intersection const-decl "bag" bags nil)
    (empty? const-decl "bool" bags nil)
    (disjoint? const-decl "bool" bags nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil))
   nil))
(bag_set_dist_union 0
  (bag_set_dist_union-1 nil 3286293066
   ("" (skosimp*)
    (("" (decompose-equality +)
      (("" (expand "bag_to_set") (("" (grind) nil))))))
    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)
    (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) (set type-eq-decl nil sets nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (union const-decl "bag" bags nil) (union const-decl "set" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil bags_to_sets nil)
    (member const-decl "bool" sets nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(bag_non_empty 0
  (bag_non_empty-1 nil 3286292999 ("" (grind) nil nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T formal-type-decl nil bags_to_sets nil)
    (empty? const-decl "bool" bags 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)))

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.