products/Sources/formale Sprachen/PVS/topology/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: cross_product.prf   Sprache: Lisp

Original von: PVS©
(cross_product
 (cross_product_empty1 0
  (cross_product_empty1-1 nil 3346222769
   ("" (skosimp)
    (("" (expand "cross_product")
      (("" (expand "empty?")
        (("" (skosimp)
          (("" (expand "member")
            (("" (flatten) (("" (inst - "x!1`1") nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (T1 formal-type-decl nil cross_product nil)
    (T2 formal-type-decl nil cross_product nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil))
   shostak))
 (cross_product_empty2 0
  (cross_product_empty2-1 nil 3346222805
   ("" (skosimp)
    (("" (expand "cross_product")
      (("" (expand "empty?")
        (("" (skosimp)
          (("" (expand "member")
            (("" (flatten) (("" (inst - "x!1`2") nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (T2 formal-type-decl nil cross_product nil)
    (T1 formal-type-decl nil cross_product nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil))
   shostak))
 (cross_product_emptyset1 0
  (cross_product_emptyset1-1 nil 3346223889
   ("" (skosimp)
    (("" (lemma "cross_product_empty1" ("A" "emptyset[T1]" "B" "B!1"))
      (("" (lemma "emptyset_is_empty?" ("a" "emptyset[T1]"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((T2 formal-type-decl nil cross_product nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil cross_product nil)
    (cross_product_empty1 formula-decl nil cross_product nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil))
   shostak))
 (cross_product_emptyset2 0
  (cross_product_emptyset2-1 nil 3346223969
   ("" (skosimp)
    (("" (lemma "emptyset_is_empty?" ("a" "emptyset[T2]"))
      ((""
        (lemma "cross_product_empty2" ("B" "emptyset[T2]" "A" "A!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((T2 formal-type-decl nil cross_product nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (cross_product_empty2 formula-decl nil cross_product nil)
    (T1 formal-type-decl nil cross_product nil))
   shostak))
 (cross_product_fullset 0
  (cross_product_fullset-1 nil 3346228173
   ("" (expand "fullset")
    (("" (expand "cross_product")
      (("" (expand "full?")
        (("" (skosimp)
          (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (member const-decl "bool" sets nil)
    (full? const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil))
   shostak))
 (projection_product1 0
  (projection_product1-1 nil 3346221058
   ("" (skosimp)
    (("" (typepred "NB!1")
      (("" (expand "nonempty?")
        (("" (expand "empty?")
          (("" (skosimp)
            (("" (expand "member")
              (("" (expand "cross_product")
                (("" (expand "projection_1")
                  (("" (apply-extensionality :hide? t)
                    (("" (case-replace "A!1(x!2)")
                      (("1" (inst + "(x!2,x!1)")
                        (("1" (assert) nil nil)) nil)
                       ("2" (assert)
                        (("2" (skosimp) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil cross_product nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (projection_1 const-decl "set[T1]" cross_product nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T1 formal-type-decl nil cross_product nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product nil))
   shostak))
 (projection_product2 0
  (projection_product2-1 nil 3346222475
   ("" (skosimp)
    (("" (typepred "NA!1")
      (("" (expand "nonempty?")
        (("" (expand "empty?")
          (("" (skosimp)
            (("" (expand "cross_product")
              (("" (expand "projection_2")
                (("" (expand "member")
                  (("" (apply-extensionality :hide? t)
                    (("" (case-replace "B!1(x!2)")
                      (("1" (inst + "(x!1,x!2)")
                        (("1" (assert) nil nil)) nil)
                       ("2" (assert)
                        (("2" (skosimp) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil cross_product nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (empty? const-decl "bool" sets nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (member const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T2 formal-type-decl nil cross_product nil)
    (projection_2 const-decl "set[T2]" cross_product nil))
   shostak))
 (projection_1_emptyset 0
  (projection_1_emptyset-1 nil 3346223533
   ("" (expand "emptyset")
    (("" (apply-extensionality :hide? t)
      (("" (expand "projection_1") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((T1 formal-type-decl nil cross_product nil)
    (boolean nonempty-type-decl nil booleans nil)
    (FALSE const-decl "bool" booleans nil)
    (projection_1 const-decl "set[T1]" cross_product nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-type-decl nil cross_product nil)
    (emptyset const-decl "set" sets nil))
   shostak))
 (projection_2_emptyset 0
  (projection_2_emptyset-1 nil 3346223560
   ("" (expand "emptyset")
    (("" (apply-extensionality :hide? t)
      (("" (expand "projection_2") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((T2 formal-type-decl nil cross_product nil)
    (boolean nonempty-type-decl nil booleans nil)
    (FALSE const-decl "bool" booleans nil)
    (projection_2 const-decl "set[T2]" cross_product nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T1 formal-type-decl nil cross_product nil)
    (emptyset const-decl "set" sets nil))
   shostak))
 (projection_1_fullset 0
  (projection_1_fullset-1 nil 3346228390
   ("" (skosimp*)
    (("" (apply-extensionality :hide? t)
      (("" (expand "fullset")
        (("" (expand "projection_1")
          (("" (inst + "(x!1,b!1)") nil nil)) nil))
        nil))
      nil))
    nil)
   ((T1 formal-type-decl nil cross_product nil)
    (boolean nonempty-type-decl nil booleans nil)
    (fullset const-decl "set" sets nil)
    (projection_1 const-decl "set[T1]" cross_product nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-type-decl nil cross_product nil))
   shostak))
 (projection_2_fullset 0
  (projection_2_fullset-1 nil 3346229607
   ("" (skosimp*)
    (("" (apply-extensionality :hide? t)
      (("" (expand "fullset")
        (("" (expand "projection_2")
          (("" (inst + "(a!1,x!1)") nil nil)) nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil cross_product nil)
    (boolean nonempty-type-decl nil booleans nil)
    (fullset const-decl "set" sets nil)
    (projection_2 const-decl "set[T2]" cross_product nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T1 formal-type-decl nil cross_product nil))
   shostak))
 (cross_product_empty1_rew 0
  (cross_product_empty1_rew-1 nil 3346229731
   ("" (skosimp)
    (("" (lemma "cross_product_emptyset1" ("B" "B!1"))
      ((""
        (lemma "emptyset_is_empty?"
         ("a" "cross_product(emptyset[T1], B!1)"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil cross_product nil)
    (cross_product_emptyset1 formula-decl nil cross_product nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (emptyset const-decl "set" sets nil)
    (T1 formal-type-decl nil cross_product nil))
   shostak))
 (cross_product_empty2_rew 0
  (cross_product_empty2_rew-1 nil 3346229792
   ("" (skosimp)
    (("" (lemma "cross_product_emptyset2" ("A" "A!1"))
      ((""
        (lemma "emptyset_is_empty?"
         ("a" "cross_product(A!1,emptyset[T2])"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil cross_product nil)
    (cross_product_emptyset2 formula-decl nil cross_product nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (emptyset const-decl "set" sets nil)
    (T2 formal-type-decl nil cross_product nil))
   shostak))
 (cross_product_full_rew 0
  (cross_product_full_rew-1 nil 3346245659
   ("" (apply-extensionality :hide? t)
    (("" (expand "fullset")
      (("" (expand "cross_product") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (fullset const-decl "set" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil cross_product nil)
    (T1 formal-type-decl nil cross_product nil))
   shostak))
 (cross_product_TCC1 0
  (cross_product_TCC1-1 nil 3346225743
   ("" (inst + "emptyset[[T1,T2]]")
    (("" (inst + "emptyset[T1]" "emptyset[T2]")
      (("" (apply-extensionality :hide? t)
        (("" (expand "emptyset")
          (("" (expand "cross_product") (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((emptyset const-decl "set" sets nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil cross_product nil)
    (T1 formal-type-decl nil cross_product nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   nil))
 (product_projection 0
  (product_projection-1 nil 3346221206
   ("" (skosimp)
    (("" (typepred "Y!1")
      (("" (skosimp)
        (("" (replace -1)
          (("" (hide -1)
            (("" (case "nonempty?(A!1)")
              (("1" (rewrite "projection_product2" 1)
                (("1" (case "nonempty?(B!1)")
                  (("1" (rewrite "projection_product1") nil nil)
                   ("2" (expand "nonempty?" 1)
                    (("2"
                      (lemma "cross_product_empty2"
                       ("A" "A!1" "B" "B!1"))
                      (("2" (assert)
                        (("2"
                          (lemma "emptyset_is_empty?"
                           ("a" "cross_product(A!1, B!1)"))
                          (("2" (assert)
                            (("2" (replace -1)
                              (("2"
                                (lemma "projection_1_emptyset")
                                (("2"
                                  (replace -1 1)
                                  (("2"
                                    (lemma
                                     "cross_product_emptyset1"
                                     ("B" "B!1"))
                                    (("2"
                                      (rewrite "emptyset_is_empty?" -1)
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "nonempty?" 1)
                (("2"
                  (lemma "cross_product_empty1" ("A" "A!1" "B" "B!1"))
                  (("2" (assert)
                    (("2"
                      (lemma "emptyset_is_empty?"
                       ("a" "cross_product(A!1, B!1)"))
                      (("2" (lemma "emptyset_is_empty?" ("a" "A!1"))
                        (("2" (assert)
                          (("2" (replace -2)
                            (("2" (lemma "projection_1_emptyset")
                              (("2"
                                (lemma "projection_2_emptyset")
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (replace -2)
                                    (("2"
                                      (lemma
                                       "cross_product_emptyset1"
                                       ("B" "emptyset[T2]"))
                                      (("2"
                                        (lemma
                                         "emptyset_is_empty?"
                                         ("a"
                                          "cross_product(emptyset[T1], emptyset[T2])"))
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cross_product nonempty-type-eq-decl nil cross_product nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T2 formal-type-decl nil cross_product nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil cross_product nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (projection_product1 formula-decl nil cross_product nil)
    (cross_product_empty2 formula-decl nil cross_product nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (emptyset const-decl "set" sets nil)
    (cross_product_emptyset1 formula-decl nil cross_product nil)
    (projection_1_emptyset formula-decl nil cross_product nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (projection_product2 formula-decl nil cross_product nil)
    (cross_product_empty1 formula-decl nil cross_product nil)
    (projection_2_emptyset formula-decl nil cross_product nil))
   shostak)))


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