products/sources/formale Sprachen/PVS/algebra/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: commutative_ring_with_one.prf   Sprache: Lisp

Original von: PVS©
(finite_bags_inductions
 (cardinal_induction 0
  (cardinal_induction-1 nil 3306770151 ("" (grind :defs nil) nil nil)
   ((card const-decl "nat" finite_bags 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)
    (T formal-type-decl nil finite_bags_inductions 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (finite_bag_induction 0
  (finite_bag_induction-1 nil 3306770151
   ("" (skolem!)
    (("" (flatten)
      (("" (lemma "cardinal_induction")
        (("" (inst -1 "pb!1")
          (("" (flatten)
            (("" (hide -1)
              (("" (split -1)
                (("1" (propax) nil nil)
                 ("2" (hide 2)
                  (("2" (induct "n")
                    (("1" (skosimp*)
                      (("1" (hide -3)
                        (("1" (use "card_nonempty_bag?")
                          (("1" (assert)
                            (("1" (expand "nonempty_bag?")
                              (("1"
                                (use "emptybag_is_empty?")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp*)
                      (("2" (inst -1 "rest(b!1)")
                        (("2" (inst -4 "choose(b!1)" "rest(b!1)")
                          (("1" (case "b!1 = emptybag[T]")
                            (("1" (assert) nil nil)
                             ("2" (assert)
                              (("2"
                                (case " nonempty_bag?(b!1)")
                                (("1"
                                  (rewrite "insert_choose_rest")
                                  (("1"
                                    (lemma
                                     "finite_bags_aux.card_bag_rest")
                                    (("1"
                                      (inst -1 "b!1")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (use "emptybag_is_empty?")
                                  (("2"
                                    (hide -2 -3 -4 -5 -6 3)
                                    (("2" (grind) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide -1 -3 2)
                            (("2" (lemma "card_bag_empty?")
                              (("2"
                                (inst?)
                                (("2"
                                  (assert)
                                  (("2"
                                    (ground)
                                    (("2"
                                      (hide -1)
                                      (("2"
                                        (expand "nonempty_bag?")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil finite_bags_inductions 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)
    (pred type-eq-decl nil defined_types nil)
    (b!1 skolem-const-decl "finite_bag[T]" finite_bags_inductions nil)
    (choose const-decl "T" bags_aux nil)
    (nil application-judgement "nonempty_finite_bag[T]"
     finite_bags_inductions nil)
    (empty? const-decl "bool" bags nil)
    (insert_choose_rest formula-decl nil bags_aux nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (card_bag_rest formula-decl nil finite_bags_aux nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (emptybag const-decl "bag" bags nil)
    (card_bag_empty? formula-decl nil finite_bags nil)
    (rest const-decl "bag" bags_aux nil)
    (nil application-judgement "finite_bag[T]" finite_bags_inductions
     nil)
    (card_nonempty_bag? formula-decl nil finite_bags nil)
    (nil name-judgement "finite_bag" finite_bags_inductions nil)
    (nonempty_bag? const-decl "bool" bags nil)
    (emptybag_is_empty? formula-decl nil bags nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (card const-decl "nat" finite_bags nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (cardinal_induction formula-decl nil finite_bags_inductions nil))
   nil)))


¤ Dauer der Verarbeitung: 0.18 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff