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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: product_orders.pvs   Sprache: Isabelle

Original von: PVS©

(total_lattices
 (singleton_has_greatest 0
  (singleton_has_greatest-1 nil 3316873516
   ("" (skolem!) (("" (use "non_empty_finite_has_greatest"nil nil))
    nil)
   ((<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (non_empty_finite_has_greatest formula-decl nil minmax_orders nil)
    (T formal-type-decl nil total_lattices nil))
   nil))
 (union_preserves_has_greatest 0
  (union_preserves_has_greatest-1 nil 3316872843
   ("" (skolem-typepred)
    ((""
      (expand"has_greatest?" "greatest?" "upper_bound?" "union"
       "member")
      (("" (skosimp*)
        (("" (case "t!1 <= t!2")
          (("1" (inst + "t!2")
            (("1" (assert)
              (("1" (skolem-typepred)
                (("1" (expand"union" "member")
                  (("1" (split)
                    (("1" (inst - "r!1")
                      (("1" (typepred "<=")
                        (("1"
                          (expand"total_order?" "partial_order?"
                           "preorder?" "transitive?")
                          (("1" (flatten)
                            (("1" (inst - "r!1" "t!1" "t!2")
                              (("1" (assertnil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (inst -6 "r!1"nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (typepred "<=")
            (("2"
              (expand"total_order?" "dichotomous?" "partial_order?"
               "preorder?" "transitive?")
              (("2" (flatten)
                (("2" (inst - "t!1" "t!2")
                  (("2" (inst + "t!1")
                    (("2" (assert)
                      (("2" (skolem-typepred)
                        (("2" (expand"union" "member")
                          (("2" (split)
                            (("1" (inst - "r!1"nil nil)
                             ("2" (inst -9 "r!1")
                              (("2"
                                (inst - "r!1" "t!2" "t!1")
                                (("2" (assertnil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest? const-decl "bool" minmax_orders nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (G1!1 skolem-const-decl
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (G2!1 skolem-const-decl
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (r!1 skolem-const-decl "(union[T](G1!1, G2!1))" total_lattices nil)
    (partial_order? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (dichotomous? const-decl "bool" orders nil)
    (r!1 skolem-const-decl "(union[T](G1!1, G2!1))" total_lattices nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (total_order? const-decl "bool" orders nil)
    (has_greatest? const-decl "bool" minmax_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil total_lattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (add_preserves_has_greatest 0
  (add_preserves_has_greatest-1 nil 3316872843
   ("" (skolem!)
    (("" (rewrite "add_as_union[T]") (("" (assertnil nil)) nil)) nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (has_greatest? const-decl "bool" minmax_orders nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (T formal-type-decl nil total_lattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (singleton_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (nonempty_union2 application-judgement "(nonempty?)" total_lattices
     nil)
    (union_preserves_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil))
   nil))
 (greatest_singleton 0
  (greatest_singleton-1 nil 3316873630
   ("" (skolem!)
    (("" (rewrite "greatest_def")
      (("" (grind)
        (("" (typepred "<=")
          ((""
            (expand"total_order?" "partial_order?" "preorder?"
             "reflexive?")
            (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((singleton_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (greatest_def formula-decl nil minmax_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (set type-eq-decl nil sets nil)
    (has_greatest? const-decl "bool" minmax_orders nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (T formal-type-decl nil total_lattices nil)
    (preorder? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (greatest? const-decl "bool" minmax_orders nil))
   shostak))
 (greatest_union 0
  (greatest_union-1 nil 3316873738
   ("" (skolem!)
    (("" (lift-if)
      (("" (ground)
        (("1" (rewrite "greatest_def")
          (("1" (typepred "greatest(<=)(G2!1)")
            (("1" (typepred "greatest(<=)(G1!1)")
              (("1" (typepred "<=")
                (("1" (grind :if-match nil)
                  (("1" (inst -7 "r!1")
                    (("1"
                      (inst - "r!1" "greatest(<=)(G1!1)"
                       "greatest(<=)(G2!1)")
                      (("1" (assertnil nil)) nil))
                    nil)
                   ("2" (inst -9 "r!1"nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (typepred "<=")
          (("2" (expand"total_order?" "dichotomous?")
            (("2" (flatten)
              (("2" (inst - "greatest(<=)(G1!1)" "greatest(<=)(G2!1)")
                (("2" (assert)
                  (("2" (typepred "greatest(<=)(G2!1)")
                    (("2" (typepred "greatest(<=)(G1!1)")
                      (("2" (rewrite "greatest_def")
                        (("2" (grind :if-match nil)
                          (("1" (inst - "r!1"nil nil)
                           ("2" (inst -5 "r!1")
                            (("2"
                              (inst - "r!1" "greatest(<=)(G2!1)"
                               "greatest(<=)(G1!1)")
                              (("2" (assertnil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest_def formula-decl nil minmax_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (set type-eq-decl nil sets nil)
    (has_greatest? const-decl "bool" minmax_orders nil)
    (greatest? const-decl "bool" minmax_orders nil)
    (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
     nil)
    (union const-decl "set" sets nil)
    (T formal-type-decl nil total_lattices nil)
    (member const-decl "bool" sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (dichotomous? const-decl "bool" orders nil)
    (partial_order? const-decl "bool" orders nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (union_preserves_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil))
   shostak))
 (greatest_add 0
  (greatest_add-1 nil 3316873976
   ("" (skolem!)
    (("" (rewrite "add_as_union[T]")
      (("" (use "greatest_union")
        (("" (rewrite "greatest_singleton"nil nil)) nil))
      nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (has_greatest? const-decl "bool" minmax_orders nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (T formal-type-decl nil total_lattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (singleton_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (nonempty_union2 application-judgement "(nonempty?)" total_lattices
     nil)
    (union_preserves_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (greatest_singleton formula-decl nil total_lattices nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (greatest_union formula-decl nil total_lattices nil))
   shostak))
 (singleton_has_least 0
  (singleton_has_least-1 nil 3316873516
   ("" (skolem!) (("" (use "non_empty_finite_has_least"nil nil)) nil)
   ((<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (singleton_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (non_empty_finite_has_least formula-decl nil minmax_orders nil)
    (T formal-type-decl nil total_lattices nil))
   nil))
 (union_preserves_has_least 0
  (union_preserves_has_least-1 nil 3316872843
   ("" (skolem-typepred)
    ((""
      (expand"has_least?" "least?" "lower_bound?" "union" "member")
      (("" (skosimp*)
        (("" (case "t!1 <= t!2")
          (("1" (inst + "t!1")
            (("1" (assert)
              (("1" (skolem-typepred)
                (("1" (expand"union" "member")
                  (("1" (split)
                    (("1" (inst - "r!1"nil nil)
                     ("2" (inst -6 "r!1")
                      (("2" (typepred "<=")
                        (("2"
                          (expand"total_order?" "partial_order?"
                           "preorder?" "transitive?")
                          (("2" (flatten)
                            (("2" (inst - "t!1" "t!2" "r!1")
                              (("2" (assertnil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (typepred "<=")
            (("2"
              (expand"total_order?" "dichotomous?" "partial_order?"
               "preorder?" "transitive?")
              (("2" (flatten)
                (("2" (inst - "t!1" "t!2")
                  (("2" (inst + "t!2")
                    (("2" (assert)
                      (("2" (skolem-typepred)
                        (("2" (expand"union" "member")
                          (("2" (split)
                            (("1" (inst - "r!1")
                              (("1"
                                (inst - "t!2" "t!1" "r!1")
                                (("1" (assertnil nil))
                                nil))
                              nil)
                             ("2" (inst -9 "r!1"nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((least? const-decl "bool" minmax_orders nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (partial_order? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (L1!1 skolem-const-decl "(LAMBDA (S: set[T]): has_least?(S, <=))"
     total_lattices nil)
    (L2!1 skolem-const-decl "(LAMBDA (S: set[T]): has_least?(S, <=))"
     total_lattices nil)
    (r!1 skolem-const-decl "(union[T](L1!1, L2!1))" total_lattices nil)
    (dichotomous? const-decl "bool" orders nil)
    (r!1 skolem-const-decl "(union[T](L1!1, L2!1))" total_lattices nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (total_order? const-decl "bool" orders nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil total_lattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (add_preserves_has_least 0
  (add_preserves_has_least-1 nil 3316872843
   ("" (skolem!)
    (("" (rewrite "add_as_union[T]") (("" (assertnil nil)) nil)) nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (T formal-type-decl nil total_lattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (singleton_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (singleton_has_least application-judgement
     "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil)
    (nonempty_union2 application-judgement "(nonempty?)" total_lattices
     nil)
    (union_preserves_has_least application-judgement
     "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil))
   nil))
 (least_singleton 0
  (least_singleton-1 nil 3316874553
   ("" (skolem!)
    (("" (rewrite "least_def")
      (("" (grind)
        (("" (typepred "<=")
          ((""
            (expand"total_order?" "partial_order?" "preorder?"
             "reflexive?")
            (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((singleton_has_least application-judgement
     "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil)
    (singleton_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (least_def formula-decl nil minmax_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (set type-eq-decl nil sets nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (T formal-type-decl nil total_lattices nil)
    (preorder? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (least? const-decl "bool" minmax_orders nil))
   shostak))
 (least_union 0
  (least_union-1 nil 3316874582
   ("" (skolem!)
    (("" (lift-if)
      (("" (ground)
        (("1" (rewrite "least_def")
          (("1" (typepred "least(<=)(L2!1)")
            (("1" (typepred "least(<=)(L1!1)")
              (("1" (typepred "<=")
                (("1" (grind :if-match nil)
                  (("1" (inst -7 "r!1"nil nil)
                   ("2" (inst -9 "r!1")
                    (("2"
                      (inst - "least(<=)(L1!1)" "least(<=)(L2!1)"
                       "r!1")
                      (("2" (assertnil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (typepred "<=")
          (("2" (expand"total_order?" "dichotomous?")
            (("2" (flatten)
              (("2" (inst - "least(<=)(L1!1)" "least(<=)(L2!1)")
                (("2" (assert)
                  (("2" (typepred "least(<=)(L2!1)")
                    (("2" (typepred "least(<=)(L1!1)")
                      (("2" (rewrite "least_def")
                        (("2" (grind :if-match nil)
                          (("1" (inst - "r!1")
                            (("1"
                              (inst - "least(<=)(L2!1)"
                               "least(<=)(L1!1)" "r!1")
                              (("1" (assertnil nil)) nil))
                            nil)
                           ("2" (inst -5 "r!1"nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((least_def formula-decl nil minmax_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (set type-eq-decl nil sets nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
    (union const-decl "set" sets nil)
    (T formal-type-decl nil total_lattices nil)
    (member const-decl "bool" sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (dichotomous? const-decl "bool" orders nil)
    (partial_order? const-decl "bool" orders nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (union_preserves_has_least application-judgement
     "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil))
   shostak))
 (least_add 0
  (least_add-1 nil 3316874740
   ("" (skolem!)
    (("" (rewrite "add_as_union[T]")
      (("" (use "least_union")
        (("" (rewrite "least_singleton"nil nil)) nil))
      nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" total_lattices nil)
    (T formal-type-decl nil total_lattices nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" total_lattices nil)
    (singleton_has_greatest application-judgement
     "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)
    (singleton_has_least application-judgement
     "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil)
    (nonempty_union2 application-judgement "(nonempty?)" total_lattices
     nil)
    (union_preserves_has_least application-judgement
     "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil)
    (least_singleton formula-decl nil total_lattices nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (least_union formula-decl nil total_lattices nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.47 Sekunden  (vorverarbeitet)  ¤





Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff