Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale sprachen/PVS/measure_integration/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: subset_algebra.prf Sprache: Lisp

Original von: PVS^©

(subset_algebra
(subset_algebra_emptyset 0
  (subset_algebra_emptyset-1 nil 3316499448
   ("" (typepred "S")
    (("" (expand "subset_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?")
          (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (member const-decl "bool" sets 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 subset_algebra nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "subset_algebra[T]" subset_algebra nil))
   shostak))
(subset_algebra_fullset 0
  (subset_algebra_fullset-1 nil 3316499471
   ("" (typepred "S")
    (("" (expand "subset_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?")
          (("" (expand "subset_algebra_complement?")
            (("" (expand "member")
              (("" (inst - "emptyset[T]")
                (("" (rewrite "complement_emptyset") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (member const-decl "bool" sets nil)
    (complement_emptyset formula-decl nil sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (emptyset const-decl "set" sets nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (subset_algebra_emptyset name-judgement "(S)" subset_algebra nil)
    (subset_algebra_complement? const-decl "bool" subset_algebra_def
     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 subset_algebra nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "subset_algebra[T]" subset_algebra nil))
   shostak))
(subset_algebra_complement 0
  (subset_algebra_complement-1 nil 3316499521
   ("" (skosimp)
    (("" (typepred "S")
      (("" (expand "subset_algebra?")
        (("" (flatten)
          (("" (expand "subset_algebra_complement?")
            (("" (inst - "x!1")
              (("" (expand "member") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "subset_algebra[T]" subset_algebra nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil subset_algebra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (subset_algebra_complement? const-decl "bool" subset_algebra_def
     nil))
   shostak))
(subset_algebra_union 0
  (subset_algebra_union-1 nil 3316499547
   ("" (skosimp)
    (("" (typepred "S")
      (("" (expand "subset_algebra?")
        (("" (flatten)
          (("" (expand "subset_algebra_union?")
            (("" (inst - "x!1" "y!1")
              (("" (expand "member") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "subset_algebra[T]" subset_algebra nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil subset_algebra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (subset_algebra_union? const-decl "bool" subset_algebra_def nil))
   shostak))
(subset_algebra_intersection 0
  (subset_algebra_intersection-1 nil 3316499770
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (typepred "y!1")
        (("" (typepred "S")
          (("" (expand "subset_algebra?")
            (("" (flatten)
              (("" (expand "subset_algebra_union?")
                (("" (expand "subset_algebra_complement?")
                  (("" (expand "member")
                    (("" (inst-cp - "x!1")
                      (("" (inst-cp - "y!1")
                        ((""
                          (inst - "complement(x!1)" "complement(y!1)")
                          ((""
                            (inst -
                             "union(complement(x!1), complement(y!1))")
                            (("" (rewrite "demorgan1" -2)
                              ((""
                                (rewrite "complement_complement")
                                ((""
                                  (rewrite "complement_complement")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "subset_algebra[T]" subset_algebra nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil subset_algebra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (subset_algebra_complement? const-decl "bool" subset_algebra_def
     nil)
    (complement const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (demorgan1 formula-decl nil sets_lemmas nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (subset_algebra_union application-judgement "(S)" subset_algebra
     nil)
    (subset_algebra_complement application-judgement "(S)"
     subset_algebra nil)
    (subset_algebra_union? const-decl "bool" subset_algebra_def nil))
   shostak))
(subset_algebra_difference 0
  (subset_algebra_difference-1 nil 3316499965
   ("" (skosimp)
    (("" (rewrite "difference_intersection")
      (("" (typepred "x!1")
        (("" (typepred "y!1")
          (("" (lemma "subset_algebra_complement" ("x" "y!1"))
            (("" (expand "member")
              ((""
                (lemma "subset_algebra_intersection"
                 ("x" "x!1" "y" "complement(y!1)"))
                (("1" (expand "member") (("1" (propax) nil nil)) nil)
                 ("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((difference_intersection 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)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "subset_algebra[T]" subset_algebra nil)
    (T formal-type-decl nil subset_algebra nil)
    (subset_algebra_complement application-judgement "(S)"
     subset_algebra nil)
    (subset_algebra_intersection application-judgement "(S)"
     subset_algebra nil)
    (subset_algebra_intersection judgement-tcc nil subset_algebra nil)
    (complement const-decl "set" sets nil)
    (subset_algebra_complement judgement-tcc nil subset_algebra nil)
    (NOT const-decl "[bool -> bool]" booleans 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.