products/sources/formale sprachen/PVS/structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: finite_bags_aux.prf   Sprache: Lisp

Original von: PVS©
(finite_bags_aux
 (finite_bag_rest 0
  (finite_bag_rest-1 nil 3306770024
   ("" (skosimp*)
    (("" (auto-rewrite "nonempty_bag?")
      (("" (expand "rest")
        (("" (rewrite "finite_delete")
          (("" (use "finite_emptybag") (("" (ground) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((rest const-decl "bag" bags_aux nil)
    (nil application-judgement "finite_bag[T]" finite_bags_aux nil))
   nil))
 (rest_TCC1 0
  (rest_TCC1-1 nil 3306769997
   ("" (skosimp*)
    (("" (auto-rewrite "nonempty_bag?")
      (("" (expand "rest")
        (("" (rewrite "finite_delete")
          (("" (use "finite_emptybag") (("" (ground) nil))))))))))
    nil)
   ((rest const-decl "bag" bags_aux nil)
    (nil application-judgement "finite_bag[T]" finite_bags_aux nil))
   nil))
 (card_bag_rest 0
  (card_bag_rest-1 nil 3306769997
   ("" (skosimp*)
    (("" (expand "rest")
      (("" (expand "nonempty_bag?")
        (("" (lift-if)
          (("" (assert)
            (("" (rewrite "card_bag_delete")
              (("1" (assert)
                (("1" (expand "min")
                  (("1" (lift-if)
                    (("1" (ground)
                      (("1" (use "choose_gt_zero")
                        (("1" (expand "nonempty_bag?")
                          (("1" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "nonempty_bag?") (("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rest const-decl "bag" bags_aux nil)
    (card_bag_delete formula-decl nil finite_bags 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)
    (choose const-decl "T" bags_aux nil)
    (T formal-type-decl nil finite_bags_aux nil)
    (nat_min application-judgement "{k: nat | k <= i AND k <= j}"
     real_defs nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (choose_gt_zero formula-decl nil bags_aux nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nil application-judgement "finite_bag[T]" finite_bags_aux nil)
    (nonempty_bag? const-decl "bool" bags nil))
   nil))
 (finite_filter 0
  (finite_filter-1 nil 3306769997
   ("" (skosimp*)
    (("" (expand "is_finite")
      (("" (typepred "b!1")
        (("" (expand "is_finite")
          (("" (expand "is_finite")
            (("" (expand "injective?")
              (("" (skosimp*)
                ((""
                  (inst 1 "N!1" "(LAMBDA (t:{t: T | IF p!1(t)
                              THEN b!1(t)  > 0 
                              ELSE FALSE  ENDIF}): f!1(t))")
                  (("1" (skosimp*)
                    (("1" (inst?)
                      (("1" (grind) nil nil)
                       ("2" (typepred "x2!1")
                        (("2" (typepred "b!1(x2!1)")
                          (("2" (hide -3) (("2" (grind) nil nil)) nil))
                          nil))
                        nil)
                       ("3" (typepred "x1!1")
                        (("3" (hide -2) (("3" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp*) (("2" (grind) nil nil)) nil)
                   ("3" (skosimp*)
                    (("3" (typepred "t!1") (("3" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite const-decl "bool" finite_bags nil)
    (is_finite const-decl "bool" finite_sets nil)
    (injective? const-decl "bool" functions nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (set type-eq-decl nil sets nil)
    (FALSE const-decl "bool" booleans nil)
    (b!1 skolem-const-decl "finite_bag[T]" finite_bags_aux nil)
    (> const-decl "bool" reals nil)
    (p!1 skolem-const-decl "pred[T]" finite_bags_aux nil)
    (pred type-eq-decl nil defined_types nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (filter const-decl "bag" bags_aux nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nil application-judgement "finite_set" finite_bags_aux nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil finite_bags_aux 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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (bag type-eq-decl nil bags nil)
    (finite_bag type-eq-decl nil finite_bags nil))
   nil))
 (filter_TCC1 0
  (filter_TCC1-1 nil 3306769997
   ("" (skosimp*) (("" (rewrite "finite_filter") nil)) nil)
   ((finite_filter formula-decl nil finite_bags_aux nil)
    (T formal-type-decl nil finite_bags_aux 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))
   nil))
 (card_filter_insert 0
  (card_filter_insert-1 nil 3306769997
   ("" (skosimp*)
    (("" (lemma "filter_insert")
      (("" (inst?)
        (("" (replace -1 :hide? t)
          (("" (case "p!1(x!1)")
            (("1" (assert)
              (("1" (use "card_bag_insert") (("1" (assert) nil)))))
             ("2" (assert) nil))))))))))
    nil)
   ((T formal-type-decl nil finite_bags_aux nil)
    (filter_insert formula-decl nil bags_aux nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nil application-judgement "finite_bag" finite_bags_aux nil)
    (nil application-judgement "nonempty_finite_bag[T]" finite_bags_aux
     nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (filter const-decl "bag" bags_aux nil)
    (card_bag_insert formula-decl nil finite_bags 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))
 (card_filter_delete 0
  (card_filter_delete-1 nil 3306769997
   ("" (skosimp*)
    (("" (use "filter_delete")
      (("" (replace -1 :hide? t)
        (("" (lemma "card_bag_delete")
          (("" (inst -1 "filter(b!1, p!1)" "x!1" "n!1")
            (("" (replace -1 :hide? t)
              (("" (expand "filter") (("" (grind) nil))))))))))))))
    nil)
   ((filter_delete formula-decl nil bags_aux nil)
    (T formal-type-decl nil finite_bags_aux 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)
    (card_bag_delete formula-decl nil finite_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)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (filter const-decl "bag" bags_aux nil)
    (nil application-judgement "finite_bag" finite_bags_aux nil))
   nil)))


¤ 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.


Bot Zugriff