Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: card_single.prf Sprache: Lisp

Original von: PVS^©

(card_single
(card_lt_is_irreflexive 0
  (card_lt_is_irreflexive-1 nil 3316968557
   ("" (expand* "irreflexive?" "card_lt")
    (("" (skolem!)
      (("" (inst + "identity[(x!1)]") (("" (judgement-tcc) nil nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (identity const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions 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 card_single nil)
    (irreflexive? const-decl "bool" relations nil)
    (card_lt const-decl "bool" card_comp_set nil))
   nil))
(card_le_is_reflexive 0
  (card_le_is_reflexive-1 nil 3316968557
   ("" (expand* "reflexive?" "card_le")
    (("" (skolem!)
      (("" (inst + "identity[(x!1)]") (("" (judgement-tcc) nil nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (identity const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions 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 card_single nil)
    (reflexive? const-decl "bool" relations nil)
    (card_le const-decl "bool" card_comp_set nil))
   nil))
(card_eq_is_reflexive 0
  (card_eq_is_reflexive-1 nil 3316968557
   ("" (expand* "reflexive?" "card_eq")
    (("" (skolem!)
      (("" (inst + "identity[(x!1)]") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((identity const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions 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 card_single nil)
    (reflexive? const-decl "bool" relations nil)
    (card_eq const-decl "bool" card_comp_set nil))
   nil))
(card_ge_is_reflexive 0
  (card_ge_is_reflexive-1 nil 3316968557
   ("" (expand* "reflexive?" "card_ge")
    (("" (skolem!)
      (("" (inst + "identity[(x!1)]") (("" (judgement-tcc) nil nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (identity const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions 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 card_single nil)
    (reflexive? const-decl "bool" relations nil)
    (card_ge const-decl "bool" card_comp_set nil))
   nil))
(card_gt_is_irreflexive 0
  (card_gt_is_irreflexive-1 nil 3316968557
   ("" (expand* "irreflexive?" "card_gt")
    (("" (skolem!)
      (("" (inst + "identity[(x!1)]") (("" (judgement-tcc) nil nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (identity const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions 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 card_single nil)
    (irreflexive? const-decl "bool" relations nil)
    (card_gt const-decl "bool" card_comp_set nil))
   nil))
(card_lt_is_antisymmetric 0
  (card_lt_is_antisymmetric-1 nil 3316968557
   ("" (expand "antisymmetric?")
    (("" (skosimp)
      (("" (forward-chain "card_lt_anticommutative") nil nil)) nil))
    nil)
   ((T formal-type-decl 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)
    (card_lt_anticommutative formula-decl nil card_comp_set_props nil)
    (antisymmetric? const-decl "bool" relations nil))
   nil))
(card_eq_is_symmetric 0
  (card_eq_is_symmetric-1 nil 3316968557
   ("" (expand "symmetric?")
    (("" (skosimp) (("" (rewrite "card_eq_symmetric") nil nil)) nil))
    nil)
   ((T formal-type-decl 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)
    (card_eq_symmetric formula-decl nil card_comp_set_props nil)
    (card_eq_is_reflexive name-judgement "(reflexive?[set[T]])"
     card_single nil)
    (symmetric? const-decl "bool" relations nil))
   nil))
(card_gt_is_antisymmetric 0
  (card_gt_is_antisymmetric-1 nil 3316968557
   ("" (expand "antisymmetric?")
    (("" (skosimp)
      (("" (forward-chain "card_gt_anticommutative") nil nil)) nil))
    nil)
   ((T formal-type-decl 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)
    (card_gt_anticommutative formula-decl nil card_comp_set_props nil)
    (antisymmetric? const-decl "bool" relations nil))
   nil))
(card_lt_is_transitive 0
  (card_lt_is_transitive-1 nil 3316968557
   ("" (expand "transitive?")
    (("" (skosimp) (("" (forward-chain "card_lt_transitive") nil nil))
      nil))
    nil)
   ((T formal-type-decl 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)
    (card_lt_transitive formula-decl nil card_comp_set_transitive nil)
    (transitive? const-decl "bool" relations nil))
   nil))
(card_le_is_transitive 0
  (card_le_is_transitive-1 nil 3316968557
   ("" (expand "transitive?")
    (("" (skosimp) (("" (forward-chain "card_le_transitive") nil nil))
      nil))
    nil)
   ((T formal-type-decl 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)
    (card_le_transitive formula-decl nil card_comp_set_transitive nil)
    (transitive? const-decl "bool" relations nil))
   nil))
(card_eq_is_transitive 0
  (card_eq_is_transitive-1 nil 3316968557
   ("" (expand "transitive?")
    (("" (skosimp) (("" (forward-chain "card_eq_transitive") nil nil))
      nil))
    nil)
   ((T formal-type-decl 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)
    (card_eq_transitive formula-decl nil card_comp_set_transitive nil)
    (transitive? const-decl "bool" relations nil))
   nil))
(card_ge_is_transitive 0
  (card_ge_is_transitive-1 nil 3316968557
   ("" (expand "transitive?")
    (("" (skosimp) (("" (forward-chain "card_ge_transitive") nil nil))
      nil))
    nil)
   ((T formal-type-decl 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)
    (card_ge_transitive formula-decl nil card_comp_set_transitive nil)
    (transitive? const-decl "bool" relations nil))
   nil))
(card_gt_is_transitive 0
  (card_gt_is_transitive-1 nil 3316968557
   ("" (expand "transitive?")
    (("" (skosimp) (("" (forward-chain "card_gt_transitive") nil nil))
      nil))
    nil)
   ((T formal-type-decl 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)
    (card_gt_transitive formula-decl nil card_comp_set_transitive nil)
    (transitive? const-decl "bool" relations nil))
   nil))
(card_le_is_dichotomous 0
  (card_le_is_dichotomous-1 nil 3316968557
   ("" (expand "dichotomous?")
    (("" (skolem!) (("" (use "card_le_dichotomous") nil nil)) nil))
    nil)
   ((T formal-type-decl nil card_single nil)
    (card_le_dichotomous formula-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (dichotomous? const-decl "bool" orders nil))
   nil))
(card_ge_is_dichotomous 0
  (card_ge_is_dichotomous-1 nil 3316968557
   ("" (expand "dichotomous?")
    (("" (skolem!) (("" (use "card_ge_dichotomous") nil nil)) nil))
    nil)
   ((T formal-type-decl nil card_single nil)
    (card_ge_dichotomous formula-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (dichotomous? const-decl "bool" orders nil))
   nil))
(card_eq_is_equivalence 0
  (card_eq_is_equivalence-1 nil 3316968557 ("" (judgement-tcc) nil nil)
   ((card_eq_is_transitive name-judgement "(transitive?[set[T]])"
     card_single nil)
    (card_eq_is_symmetric name-judgement "(symmetric?[set[T]])"
     card_single nil)
    (card_eq_is_reflexive name-judgement "(reflexive?[set[T]])"
     card_single nil)
    (equivalence? const-decl "bool" relations nil))
   nil)))

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.