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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: dml160.cob   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.1 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
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