Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: complementary_orders.prf Sprache: Lisp

Original von: PVS^©

(complementary_orders
(complement_complement 0
  (complement_complement-1 nil 3318701342
   ("" (skolem-typepred)
    (("" (expand* "complement?" "o" "id")
      (("" (flatten)
        (("" (decompose-equality) (("" (inst?) nil nil)) nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (complement? const-decl "bool" complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil complementary_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(image_complement 0
  (image_complement-1 nil 3318701387
   ("" (skosimp* t)
    (("" (decompose-equality)
      (("" (expand "image")
        (("" (iff)
          (("" (prop)
            (("1" (skosimp* t)
              (("1" (use "complement_complement")
                (("1" (assert) nil nil)) nil))
              nil)
             ("2" (inst + "C!1(x!1)")
              (("1" (rewrite "complement_complement") nil nil)
               ("2" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (image const-decl "set[R]" function_image nil)
    (x!1 skolem-const-decl "T" complementary_orders nil)
    (C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
     nil)
    (rel!1 skolem-const-decl "pred[[T, T]]" complementary_orders nil)
    (S!1 skolem-const-decl "set[T]" complementary_orders nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (complement_complement formula-decl nil complementary_orders 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-nonempty-type-decl nil complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (complement? const-decl "bool" complementary_orders nil))
   shostak))
(inverse_complement 0
  (inverse_complement-1 nil 3318701457
   ("" (skolem-typepred)
    (("" (decompose-equality)
      (("" (rewrite "bijective_inverse[T, T]")
        (("1" (rewrite "complement_complement") nil nil)
         ("2" (lemma "left_inj_surj[T, T]")
          (("2" (inst - "C!1" "C!1")
            (("1" (expand "bijective?") (("1" (propax) nil nil)) nil)
             ("2" (expand* "left_inverse?" "complement?" "o" "id")
              (("2" (flatten) (("2" (decompose-equality) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inverse const-decl "D" function_inverse nil)
    (left_inj_surj formula-decl nil function_inverse_def nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (O const-decl "T3" function_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
     nil)
    (rel!1 skolem-const-decl "pred[[T, T]]" complementary_orders nil)
    (left_inverse? const-decl "bool" function_inverse_def nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (bijective? const-decl "bool" functions nil)
    (bijective_inverse formula-decl nil function_inverse nil)
    (complement? const-decl "bool" complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil complementary_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(le_complement 0
  (le_complement-1 nil 3318701551
   ("" (skolem-typepred)
    (("" (prop)
      (("1" (expand* "complement?" "preserves" "converse")
        (("1" (flatten)
          (("1" (inst - "C!1(t1!1)" "C!1(t2!1)")
            (("1" (assert)
              (("1" (rewrite "complement_complement")
                (("1" (rewrite "complement_complement") nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand* "complement?" "preserves" "converse")
        (("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((complement_complement formula-decl nil complementary_orders nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (preserves const-decl "bool" functions nil)
    (complement? const-decl "bool" complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil complementary_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(upper_bound_complement 0
  (upper_bound_complement-1 nil 3318701679
   ("" (skolem!)
    (("" (prop)
      (("1" (expand* "lower_bound?" "upper_bound?")
        (("1" (skolem-typepred)
          (("1" (inst - "C!1(r!1)")
            (("1" (use "le_complement" ("t2" "C!1(t!1)"))
              (("1" (assert)
                (("1" (rewrite "complement_complement") nil nil)) nil))
              nil)
             ("2" (expand "image")
              (("2" (skolem-typepred)
                (("2" (use "complement_complement" ("t" "x!1"))
                  (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand* "lower_bound?" "upper_bound?")
        (("2" (skolem-typepred)
          (("2" (inst - "C!1(r!1)")
            (("1" (rewrite "le_complement") nil nil)
             ("2" (expand "image") (("2" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    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-nonempty-type-decl nil complementary_orders nil)
    (set type-eq-decl nil sets nil)
    (image const-decl "set[R]" function_image nil)
    (pred type-eq-decl nil defined_types nil)
    (complement? const-decl "bool" complementary_orders nil)
    (le_complement formula-decl nil complementary_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (S!1 skolem-const-decl "set[T]" complementary_orders nil)
    (rel!1 skolem-const-decl "pred[[T, T]]" complementary_orders nil)
    (C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
     nil)
    (r!1 skolem-const-decl "(image(C!1, S!1))" complementary_orders
     nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (r!1 skolem-const-decl "(S!1)" complementary_orders nil))
   shostak))
(bounded_above_complement 0
  (bounded_above_complement-1 nil 3318701876
   ("" (skolem!)
    (("" (expand* "bounded_above?" "bounded_below?")
      (("" (prop)
        (("1" (skolem!)
          (("1" (inst + "C!1(t!1)")
            (("1" (use "upper_bound_complement")
              (("1" (assert) nil nil)) nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (inst + "C!1(t!1)")
            (("2" (use "upper_bound_complement")
              (("2" (rewrite "complement_complement")
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bounded_below? const-decl "bool" bounded_orders nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (upper_bound_complement formula-decl nil complementary_orders nil)
    (set type-eq-decl nil sets nil)
    (complement? const-decl "bool" complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil complementary_orders nil))
   shostak))
(least_upper_bound_complement 0
  (least_upper_bound_complement-1 nil 3318701959
   ("" (skolem!)
    (("" (expand* "least_upper_bound?" "greatest_lower_bound?")
      (("" (prop)
        (("1" (use "upper_bound_complement") (("1" (assert) nil nil))
          nil)
         ("2" (skosimp)
          (("2" (hide -2)
            (("2" (inst - "C!1(r!1)")
              (("2" (use "upper_bound_complement")
                (("2" (rewrite "complement_complement")
                  (("2" (assert)
                    (("2"
                      (use "le_complement"
                           ("t1" "C!1(r!1)" "t2" "t!1"))
                      (("2" (assert)
                        (("2" (rewrite "complement_complement") nil
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (use "upper_bound_complement") (("3" (assert) nil nil))
          nil)
         ("4" (skosimp)
          (("4" (hide -2)
            (("4" (inst - "C!1(r!1)")
              (("4" (use "upper_bound_complement")
                (("4" (assert)
                  (("4" (rewrite "le_complement") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (le_complement formula-decl nil complementary_orders nil)
    (upper_bound_complement formula-decl nil complementary_orders nil)
    (complement? const-decl "bool" complementary_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil complementary_orders nil))
   shostak))
(least_bounded_above_complement 0
  (least_bounded_above_complement-1 nil 3318702440
   ("" (skolem!)
    (("" (expand* "least_bounded_above?" "greatest_bounded_below?")
      (("" (prop)
        (("1" (skolem!)
          (("1" (use "least_upper_bound_complement")
            (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
          nil)
         ("2" (skolem!)
          (("2" (inst + "C!1(t!1)")
            (("2" (use "least_upper_bound_complement")
              (("2" (rewrite "complement_complement")
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (complement? const-decl "bool" complementary_orders nil)
    (T formal-nonempty-type-decl nil complementary_orders 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)
    (least_upper_bound_complement formula-decl nil complementary_orders
     nil))
   shostak))
(lub_complement_TCC1 0
  (lub_complement_TCC1-1 nil 3318701312
   ("" (skolem!)
    (("" (use "least_bounded_above_complement") (("" (assert) nil nil))
      nil))
    nil)
   ((least_bounded_above_complement formula-decl nil
     complementary_orders nil)
    (complement? const-decl "bool" complementary_orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil complementary_orders nil))
   nil))
(lub_complement 0
  (lub_complement-1 nil 3318702643
   ("" (skolem!)
    (("" (invoke (name-replace "T" "%1" :hide? nil) (! 1 r 1))
      (("" (use "unique_least_upper_bound")
        (("" (rewrite "glb_def")
          (("" (use "least_upper_bound_complement")
            (("" (rewrite "complement_complement")
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((least_bounded_above? const-decl "bool" bounded_orders nil)
    (complement? const-decl "bool" complementary_orders nil)
    (image const-decl "set[R]" function_image nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil complementary_orders nil)
    (glb_def formula-decl nil bounded_orders nil)
    (complement_complement formula-decl nil complementary_orders nil)
    (least_upper_bound_complement formula-decl nil complementary_orders
     nil)
    (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
     bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (T skolem-const-decl
     "(LAMBDA (t: T): greatest_lower_bound?(t, image(C!1, S!1), rel!1))"
     complementary_orders nil)
    (S!1 skolem-const-decl
     "(LAMBDA (S: set[T]): least_bounded_above?(S, rel!1))"
     complementary_orders nil)
    (C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
     nil)
    (rel!1 skolem-const-decl "(antisymmetric?[T])" complementary_orders
     nil)
    (unique_least_upper_bound formula-decl nil bounded_orders nil))
   shostak))
(glb_complement_TCC1 0
  (glb_complement_TCC1-1 nil 3318701312
   ("" (skolem!)
    ((""
      (use "least_bounded_above_complement"
           ("S" "image[T, T](C!1, S!1)"))
      (("" (rewrite "image_complement") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((least_bounded_above_complement formula-decl nil
     complementary_orders nil)
    (T formal-nonempty-type-decl nil complementary_orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (image const-decl "set[R]" function_image nil)
    (pred type-eq-decl nil defined_types nil)
    (complement? const-decl "bool" complementary_orders nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (image_complement formula-decl nil complementary_orders nil))
   nil))
(glb_complement 0
  (glb_complement-1 nil 3318702699
   ("" (skolem!)
    (("" (invoke (name-replace "T" "%1" :hide? nil) (! 1 r 1))
      (("" (use "unique_greatest_lower_bound")
        (("" (rewrite "lub_def")
          (("" (use "least_upper_bound_complement")
            (("" (rewrite "image_complement") (("" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (complement? const-decl "bool" complementary_orders nil)
    (image const-decl "set[R]" function_image nil)
    (antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
     bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil complementary_orders nil)
    (lub_def formula-decl nil bounded_orders nil)
    (image_complement formula-decl nil complementary_orders nil)
    (least_upper_bound_complement formula-decl nil complementary_orders
     nil)
    (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
     bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (T skolem-const-decl
     "(LAMBDA (t: T): least_upper_bound?(t, image(C!1, S!1), rel!1))"
     complementary_orders nil)
    (S!1 skolem-const-decl
     "(LAMBDA (S: set[T]): greatest_bounded_below?(S, rel!1))"
     complementary_orders nil)
    (C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
     nil)
    (rel!1 skolem-const-decl "(antisymmetric?[T])" complementary_orders
     nil)
    (unique_greatest_lower_bound formula-decl nil bounded_orders nil))
   shostak)))

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