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

Quelle  card_sets_lemmas.prf   Sprache: Lisp

 
(card_sets_lemmas
 (empty_card_le 0
  (empty_card_le-1 nil 3316968940
   ("" (grind)
    (("" (inst + "LAMBDA (x: (emptyset[T])): choose(S!1)")
      (("1" (skolem-typepred)
        (("1" (expand "emptyset") (("1" (propax) nil nil)) nil)) nil)
       ("2" (skolem-typepred)
        (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((S!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (nonempty? const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (choose const-decl "(p)" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (nonempty_card_lt 0
  (nonempty_card_lt-1 nil 3316968979
   ("" (grind)
    (("1" (typepred "f!1(x!1)")
      (("1" (expand "emptyset") (("1" (propax) nil nil)) nil)) nil)
     ("2" (lemma "fun_exists[(S!1), (emptyset[T])]")
      (("2" (reduce)
        (("2" (inst + "f!1")
          (("2" (skosimp :preds? t) (("2" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((fun_exists formula-decl nil function_image nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (full_card_le 0
  (full_card_le-1 nil 3316969028
   ("" (grind)
    (("" (inst + "LAMBDA (x: (S!1)): x") (("" (skosimp) nil nil)) nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (add_card_le 0
  (add_card_le-1 nil 3316969061
   ("" (grind)
    (("" (inst + "LAMBDA (x: (S!1)): x") (("" (skosimp) nil nil)) nil))
    nil)
   ((member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (remove_card_ge 0
  (remove_card_ge-1 nil 3316969072
   ("" (grind)
    (("" (inst + "LAMBDA (x: (remove(t!1, S!1))): x")
      (("1" (skosimp) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((S!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (t!1 skolem-const-decl "T" card_sets_lemmas nil)
    (remove const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (/= const-decl "boolean" notequal nil)
    (card_ge const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (subset_card_le 0
  (subset_card_le-1 nil 3316969103
   ("" (grind)
    (("" (inst + "LAMBDA (x: (S!1)): x")
      (("1" (skosimp) nil nil) ("2" (reduce) nil nil)) nil))
    nil)
   ((R!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (S!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   shostak))
 (strict_subset_card_lt 0
  (strict_subset_card_lt-1 nil 3316969137
   ("" (expand "strict_subset?")
    (("" (skosimp)
      (("" (assert)
        (("" (use "card_lt_is_irreflexive")
          (("" (expand "irreflexive?")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil card_sets_lemmas nil)
    (card_lt_is_irreflexive judgement-tcc nil card_single nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (irreflexive? const-decl "bool" relations nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (card_lt_is_irreflexive name-judgement "(irreflexive?[set[T]])"
     card_sets_lemmas nil)
    (card_lt_is_antisymmetric name-judgement "(antisymmetric?[set[T]])"
     card_sets_lemmas nil)
    (card_lt_is_transitive name-judgement "(transitive?[set[T]])"
     card_sets_lemmas nil)
    (strict_subset? const-decl "bool" sets nil))
   shostak))
 (union_card_le1 0
  (union_card_le1-1 nil 3316969188
   ("" (grind)
    (("" (inst + "LAMBDA (x: (S!1)): x") (("" (skosimp) nil nil)) nil))
    nil)
   ((member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (union_card_le2 0
  (union_card_le2-1 nil 3316969197
   ("" (grind)
    (("" (inst + "LAMBDA (x: (R!1)): x") (("" (skosimp) nil nil)) nil))
    nil)
   ((member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (intersection_card_le1 0
  (intersection_card_le1-1 nil 3316969225
   ("" (grind)
    (("" (inst + "LAMBDA (x: (intersection(S!1, R!1))): x")
      (("1" (skosimp) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((R!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (S!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (intersection const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (intersection_card_le2 0
  (intersection_card_le2-1 nil 3316969249
   ("" (grind)
    (("" (inst + "LAMBDA (x: (intersection(S!1, R!1))): x")
      (("1" (skosimp) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((R!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (S!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (intersection const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak))
 (difference_card_le 0
  (difference_card_le-1 nil 3316969260
   ("" (grind)
    (("" (inst + "LAMBDA (x: (difference(S!1, R!1))): x")
      (("1" (skosimp) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((R!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (S!1 skolem-const-decl "set[T]" card_sets_lemmas nil)
    (difference const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (card_le const-decl "bool" card_comp_set nil)
    (T formal-type-decl nil card_sets_lemmas nil)
    (injective? const-decl "bool" functions nil))
   shostak)))

100%


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