Quelle subset_algebra.prf Sprache: Lisp

(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)))

quality100%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.