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/sets_aux/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: card_sets_lemmas.prf Sprache: Lisp

Original von: PVS^©

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

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