Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: finite_bags_lems.prf Sprache: Lisp

Original von: PVS^©

(finite_bags_lems
(card_bag_plus 0
  (card_bag_plus-1 nil 3288974765
   ("" (induct "A" 1 "finite_bag_induction")
    (("1" (skosimp*)
      (("1" (rewrite "plus_emptybag")
        (("1" (rewrite "card_emptybag") (("1" (assert) nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst -1 "B!1")
        (("2" (rewrite "bag_plus_insert")
          (("2" (rewrite "card_bag_insert")
            (("1" (rewrite "card_bag_insert") (("1" (assert) nil nil))
              nil)
             ("2" (rewrite "finite_bag_plus ") nil nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skosimp*) (("3" (rewrite "finite_bag_plus ") nil nil)) nil))
    nil)
   ((bag_plus_insert formula-decl nil bags nil)
    (nil application-judgement "nonempty_finite_bag[T]"
     finite_bags_lems nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (card_bag_insert formula-decl nil finite_bags nil)
    (card_emptybag formula-decl nil finite_bags nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (plus_emptybag formula-decl nil bags nil)
    (finite_bag_induction formula-decl nil finite_bags_inductions nil)
    (T formal-type-decl nil finite_bags_lems nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (plus const-decl "bag" bags nil)
    (card const-decl "nat" finite_bags nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types 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)
    (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)
    (nil application-judgement "finite_bag[T]" finite_bags_lems nil))
   nil))
(card_bag_union 0
  (card_bag_union-1 nil 3288974765
   ("" (skosimp*)
    (("" (lemma "card_bag_plus")
      (("" (use "bag_plus_union")
        (("" (inst?)
          (("1" (lemma "card_bag_plus")
            (("1" (inst -1 "A!1" "B!1") (("1" (ground) nil nil)) nil))
            nil)
           ("2" (rewrite "finite_bag_intersection ") nil nil)
           ("3" (rewrite "finite_bag_union ") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((card_bag_plus formula-decl nil finite_bags_lems nil)
    (nil application-judgement "finite_bag[T]" finite_bags_lems nil)
    (nil application-judgement "finite_bag[T]" finite_bags_lems nil)
    (intersection const-decl "bag" bags nil)
    (union const-decl "bag" bags nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nil application-judgement "finite_bag[T]" finite_bags_lems 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)
    (T formal-type-decl nil finite_bags_lems nil)
    (bag_plus_union formula-decl nil bags nil))
   nil))
(card_bag_disj_union 0
  (card_bag_disj_union-1 nil 3288974765
   ("" (skosimp*)
    (("" (rewrite "card_bag_union")
      (("" (rewrite "card_disj_intersection") (("" (assert) nil nil))
        nil))
      nil))
    nil)
   ((card_bag_union formula-decl nil finite_bags_lems nil)
    (T formal-type-decl nil finite_bags_lems 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)
    (nil application-judgement "finite_bag[T]" finite_bags_lems nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (card_disj_intersection formula-decl nil finite_bags nil))
   nil))
(card_subbag_strict 0
  (card_subbag_strict-2 nil 3288974785
   ("" (skosimp*)
    (("" (use "card_subbag?")
      (("" (assert)
        (("" (case "subbag?(B!1, A!1)")
          (("1" (hide-all-but (-1 -4 1)) (("1" (grind) nil nil)) nil)
           ("2" (hide -3 2)
            (("2" (expand "subbag?" +)
              (("2" (skosimp*)
                (("2" (case "A!1 = B!1")
                  (("1" (assert) nil nil)
                   ("2" (case "subbag?(insert(x!2, A!1), B!1)")
                    (("1" (lemma "card_subbag?")
                      (("1" (inst - "insert(x!2, A!1)" "B!1")
                        (("1" (assert)
                          (("1" (use "card_bag_insert")
                            (("1" (replace - :hide? t)
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil)
                         ("2" (rewrite "finite_insert") nil nil))
                        nil))
                      nil)
                     ("2" (expand "subbag?")
                      (("2" (skosimp*)
                        (("2" (expand "insert")
                          (("2" (lift-if)
                            (("2" (split)
                              (("1"
                                (flatten)
                                (("1"
                                  (replace -)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (flatten)
                                (("2" (inst?) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_subbag? formula-decl nil finite_bags nil)
    (T formal-type-decl nil finite_bags_lems 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)
    (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)
    (subbag? const-decl "bool" bags nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (member const-decl "bool" bags nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (card_bag_insert formula-decl nil finite_bags nil)
    (insert const-decl "bag" bags nil)
    (nil application-judgement "nonempty_finite_bag[T]"
     finite_bags_lems nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil)
  (card_subbag_strict-1 nil 3288974772
   ("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak))
(card_subbag_strict2 0
  (card_subbag_strict2-1 nil 3289748966
   ("" (skosimp*)
    (("" (use "card_subbag?")
      (("" (assert)
        (("" (case "subbag?(B!1, A!1)")
          (("1" (hide-all-but (-1 -4 1)) (("1" (grind) nil nil)) nil)
           ("2" (hide -3 2)
            (("2" (expand "subbag?" +)
              (("2" (skosimp*)
                (("2" (case "A!1 = B!1")
                  (("1" (assert) nil nil)
                   ("2" (case "subbag?(insert(x!2, A!1), B!1)")
                    (("1" (lemma "card_subbag?")
                      (("1" (inst - "insert(x!2, A!1)" "B!1")
                        (("1" (assert)
                          (("1" (use "card_bag_insert")
                            (("1" (replace - :hide? t)
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil)
                         ("2" (rewrite "finite_insert") nil nil))
                        nil))
                      nil)
                     ("2" (expand "subbag?")
                      (("2" (skosimp*)
                        (("2" (expand "insert")
                          (("2" (lift-if)
                            (("2" (split)
                              (("1"
                                (flatten)
                                (("1"
                                  (replace -)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (flatten)
                                (("2" (inst?) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_subbag? formula-decl nil finite_bags nil)
    (T formal-type-decl nil finite_bags_lems 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)
    (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)
    (subbag? const-decl "bool" bags nil)
    (nil application-judgement "finite_set" finite_bags_lems nil)
    (nil application-judgement "nat" finite_bags_lems nil)
    (nil application-judgement "nonneg_real" finite_bags_lems nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (card const-decl "nat" finite_bags nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (card_bag_insert formula-decl nil finite_bags nil)
    (insert const-decl "bag" bags nil)
    (nil application-judgement "nonempty_finite_bag[T]"
     finite_bags_lems nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.3 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.