products/sources/formale Sprachen/PVS/sets_aux/  image not shown  

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.21 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff