Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 5 kB image not shown  

Quelle  sets_lemmas_aux.prf   Sprache: Lisp

 
(sets_lemmas_aux
 (union_complement 0
  (union_complement-1 nil 3313990217
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "complement")
        (("" (expand "union")
          (("" (expand "fullset")
            (("" (flatten)
              (("" (expand "member") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (fullset const-decl "set" sets nil)
    (complement const-decl "set" sets nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (member const-decl "bool" sets nil))
   shostak))
 (intersection_complement 0
  (intersection_complement-1 nil 3313990250
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (complement const-decl "set" sets nil)
    (intersection const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil))
   shostak))
 (disjoint_complement 0
  (disjoint_complement-1 nil 3322194982
   ("" (skosimp)
    (("" (lemma "intersection_complement" ("a" "a!1"))
      (("" (expand "disjoint?")
        (("" (rewrite "emptyset_is_empty?") 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)
    (T formal-type-decl nil sets_lemmas_aux nil)
    (intersection_complement formula-decl nil sets_lemmas_aux nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (intersection const-decl "set" sets nil)
    (complement const-decl "set" sets nil)
    (disjoint? const-decl "bool" sets nil))
   shostak))
 (disjoint_commutative 0
  (disjoint_commutative-1 nil 3314018116
   ("" (expand "disjoint?")
    (("" (skosimp) (("" (rewrite "intersection_commutative") nil nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection_commutative formula-decl nil sets_lemmas nil)
    (disjoint? const-decl "bool" sets nil))
   shostak))
 (disjoint_empty 0
  (disjoint_empty-1 nil 3314018543
   ("" (skosimp)
    (("" (expand "disjoint?")
      (("" (expand "intersection")
        (("" (expand "empty?")
          (("" (skosimp*)
            (("" (expand "member")
              (("" (expand "emptyset") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (intersection const-decl "set" sets nil))
   shostak))
 (powerset_fullset 0
  (powerset_fullset-1 nil 3321769783
   ("" (skosimp)
    (("" (lemma "subset_powerset" ("a" "a!1" "b" "a!1"))
      (("" (rewrite "subset_reflexive") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (subset_powerset formula-decl nil sets_lemmas nil)
    (nonempty_powerset application-judgement "(nonempty?[set[T]])"
     sets_lemmas_aux nil)
    (subset_reflexive formula-decl nil sets_lemmas nil))
   shostak))
 (union_diff_inter 0
  (union_diff_inter-1 nil 3321854850
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "difference")
        (("" (expand "intersection")
          (("" (expand "union")
            (("" (expand "member")
              (("" (case-replace "a!1(x!1)")
                (("1" (flatten) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil sets_lemmas_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection const-decl "set" sets nil)
    (difference const-decl "set" sets nil)
    (union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (member const-decl "bool" sets nil))
   shostak))
 (disjoint_diff_inter 0
  (disjoint_diff_inter-1 nil 3321854884
   ("" (skosimp)
    (("" (expand "disjoint?")
      (("" (expand "intersection")
        (("" (expand "difference")
          (("" (expand "empty?")
            (("" (expand "member") (("" (skosimp*) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((disjoint? const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil))
   shostak))
 (disjoint_member 0
  (disjoint_member-1 nil 3321935681
   ("" (expand "disjoint?")
    (("" (expand "intersection")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (skosimp*)
            (("" (inst - "x!1") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((intersection const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (T formal-type-decl nil sets_lemmas_aux nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.11 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.