Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: product_sections.prf Sprache: Lisp

Original von: PVS^©

(product_sections
(x_section_emptyset 0
  (x_section_emptyset-1 nil 3455512524
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T1 formal-type-decl nil product_sections nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   shostak))
(x_section_complement 0
  (x_section_complement-1 nil 3455512530
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (complement const-decl "set" sets nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T1 formal-type-decl nil product_sections nil)
    (member const-decl "bool" sets nil))
   shostak))
(x_section_union 0
  (x_section_union-1 nil 3455512540
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (union const-decl "set" sets nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T1 formal-type-decl nil product_sections nil)
    (member const-decl "bool" sets nil))
   shostak))
(x_section_intersection 0
  (x_section_intersection-1 nil 3455512548
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection const-decl "set" sets nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T1 formal-type-decl nil product_sections nil)
    (member const-decl "bool" sets nil))
   shostak))
(x_section_disjoint 0
  (x_section_disjoint-1 nil 3455512555
   ("" (skosimp)
    (("" (expand "disjoint?")
      (("" (expand "intersection")
        (("" (expand "empty?")
          (("" (expand "member")
            (("" (skosimp)
              (("" (expand "x_section")
                (("" (inst - "(a!1,x!1)") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (T2 formal-type-decl nil product_sections nil)
    (T1 formal-type-decl nil product_sections nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil))
   shostak))
(y_section_emptyset 0
  (y_section_emptyset-1 nil 3455512611
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T1 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-type-decl nil product_sections nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   shostak))
(y_section_complement 0
  (y_section_complement-1 nil 3455512620
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T1 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (complement const-decl "set" sets nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-type-decl nil product_sections nil)
    (member const-decl "bool" sets nil))
   shostak))
(y_section_union 0
  (y_section_union-1 nil 3455512630
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T1 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (union const-decl "set" sets nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-type-decl nil product_sections nil)
    (member const-decl "bool" sets nil))
   shostak))
(y_section_intersection 0
  (y_section_intersection-1 nil 3455512637
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T1 formal-type-decl nil product_sections nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection const-decl "set" sets nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-type-decl nil product_sections nil)
    (member const-decl "bool" sets nil))
   shostak))
(y_section_disjoint 0
  (y_section_disjoint-1 nil 3455512644
   ("" (skosimp)
    (("" (expand "disjoint?")
      (("" (expand "empty?")
        (("" (skosimp)
          (("" (inst - "(x!1,b!1)") (("" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((disjoint? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (T2 formal-type-decl nil product_sections nil)
    (T1 formal-type-decl nil product_sections nil)
    (empty? const-decl "bool" sets nil))
   shostak)))

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