Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: relations_extra.prf Sprache: Lisp

Original von: PVS^©

(relations_extra
(strict_order_is_asymmetric 0
  (strict_order_is_asymmetric-1 nil 3308139199
   ("" (skosimp* t)
    (("" (expand "strict_order?")
      (("" (flatten)
        (("" (expand "asymmetric?")
          (("" (skosimp*)
            (("" (expand "transitive?")
              (("" (inst - "x!2" "y!1" "x!2")
                (("" (assert)
                  (("" (expand "irreflexive?") (("" (inst?) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((asymmetric? const-decl "bool" relations_extra nil)
    (transitive? const-decl "bool" relations nil)
    (irreflexive? const-decl "bool" relations nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (strict_order? const-decl "bool" orders nil))
   shostak))
(asymmetric_is_antisymmetric 0
  (asymmetric_is_antisymmetric-1 nil 3308139286
   ("" (skosimp* t)
    (("" (expand "asymmetric?")
      (("" (expand "antisymmetric?")
        (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((antisymmetric? const-decl "bool" relations nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (asymmetric? const-decl "bool" relations_extra nil))
   shostak))
(asymmetric_is_irreflexive 0
  (asymmetric_is_irreflexive-1 nil 3308139358
   ("" (skosimp* t)
    (("" (expand "irreflexive?")
      (("" (expand "asymmetric?")
        (("" (skosimp*) (("" (inst?) (("" (prop) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((irreflexive? const-decl "bool" relations nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (asymmetric? const-decl "bool" relations_extra nil))
   shostak))
(reflexive 0
  (reflexive-3 nil 3308138472
   ("" (skolem-typepred)
    (("" (expand "reflexive?") (("" (propax) nil nil)) nil)) nil)
   ((reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (reflexive-2 nil 3308137563
   ("" (skosimp* t)
    (("" (auto-rewrite-defs) (("" (assert) (("" (inst?) nil nil)) nil))
      nil))
    nil)
   nil nil)
  (reflexive-1 nil 3308137369 ("" (grind) nil nil) nil shostak))
(irreflexive 0
  (irreflexive-3 nil 3308138470
   ("" (skolem-typepred)
    (("" (expand "irreflexive?") (("" (propax) nil nil)) nil)) nil)
   ((irreflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (irreflexive-2 nil 3308137556
   ("" (skosimp* t)
    (("" (auto-rewrite-defs) (("" (assert) (("" (inst?) nil nil)) nil))
      nil))
    nil)
   nil nil)
  (irreflexive-1 nil 3308137450 ("" (grind) nil nil) nil nil))
(symmetric 0
  (symmetric-2 nil 3308138467
   ("" (skolem-typepred)
    (("" (expand "symmetric?") (("" (propax) nil nil)) nil)) nil)
   ((symmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (symmetric-1 nil 3308137453
   ("" (skosimp* t)
    (("" (auto-rewrite-defs)
      (("" (assert)
        (("" (inst - "x!1" "y!1") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   nil nil))
(antisymmetric 0
  (antisymmetric-2 nil 3308138464
   ("" (skolem-typepred)
    (("" (expand "antisymmetric?") (("" (propax) nil nil)) nil)) nil)
   ((antisymmetric? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (antisymmetric-1 nil 3308137572
   ("" (skosimp* t)
    (("" (auto-rewrite-defs)
      (("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   nil nil))
(asymmetric 0
  (asymmetric-1 nil 3308139089
   ("" (skolem-typepred)
    (("" (expand "asymmetric?") (("" (propax) nil nil)) nil)) nil)
   ((asymmetric? const-decl "bool" relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(transitive 0
  (transitive-2 nil 3308138460
   ("" (skolem-typepred)
    (("" (expand "transitive?") (("" (propax) nil nil)) nil)) nil)
   ((transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (transitive-1 nil 3308137577
   ("" (skosimp* t)
    (("" (auto-rewrite-defs)
      (("" (assert)
        (("" (inst - "x!1" "y!1" "z!1") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   nil nil))
(dichotomous 0
  (dichotomous-2 nil 3308138452
   ("" (skolem-typepred)
    (("" (expand "dichotomous?") (("" (propax) nil nil)) nil)) nil)
   ((dichotomous? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (dichotomous-1 nil 3308137580
   ("" (skosimp* t)
    (("" (auto-rewrite-defs)
      (("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   nil nil))
(trichotomous 0
  (trichotomous-2 nil 3308138441
   ("" (skolem-typepred)
    (("" (expand "trichotomous?") (("" (propax) nil nil)) nil)) nil)
   ((trichotomous? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (trichotomous-1 nil 3308137584
   ("" (skosimp* t)
    (("" (auto-rewrite-defs)
      (("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   nil nil))
(dichotomous_is_trichotomous 0
  (dichotomous_is_trichotomous-1 nil 3308166081
   ("" (skosimp* t)
    (("" (expand* "trichotomous?" "dichotomous?")
      (("" (skosimp*) (("" (inst?) (("" (prop) nil nil)) nil)) nil))
      nil))
    nil)
   ((trichotomous? const-decl "bool" orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (dichotomous? const-decl "bool" orders nil))
   shostak))
(well_founded 0
  (well_founded-1 nil 3308138322
   ("" (skolem-typepred)
    (("" (expand "well_founded?") (("" (propax) nil nil)) nil)) nil)
   ((well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil relations_extra nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(reflexive_closure_TCC1 0
  (reflexive_closure_TCC1-1 nil 3308173829 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (reflexive? const-decl "bool" relations nil))
   shostak))
(irreflexive_kernel_TCC1 0
  (irreflexive_kernel_TCC1-1 nil 3308173829 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (irreflexive? const-decl "bool" relations nil))
   shostak))
(symmetric_closure_TCC1 0
  (symmetric_closure_TCC1-1 nil 3308173829 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (union const-decl "set" sets nil)
    (symmetric? const-decl "bool" relations nil))
   shostak))
(symmetric_kernel_TCC1 0
  (symmetric_kernel_TCC1-1 nil 3308173829 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (intersection const-decl "set" sets nil)
    (symmetric? const-decl "bool" relations nil))
   shostak))
(reflexive_closure_preserves_transitive 0
  (reflexive_closure_preserves_transitive-1 nil 3308174613
   ("" (skosimp* t)
    ((""
      (expand* "preorder?" "transitive?" "reflexive_closure" "union"
       "member")
      (("" (skosimp*)
        (("" (inst - "x!1" "y!1" "z!1")
          (("" (assert) (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure const-decl "(reflexive?)" relations_extra nil)
    (preorder? const-decl "bool" orders nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (PRED type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil))
   shostak))
(strict_order_to_partial_order 0
  (strict_order_to_partial_order-1 nil 3308174139
   ("" (skosimp* t)
    (("" (expand* "partial_order?" "preorder?")
      ((""
        (expand* "antisymmetric?" "reflexive_closure" "union" "member")
        (("" (skosimp*)
          (("" (assert)
            (("" (use "asymmetric") (("" (prop) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((reflexive_closure_preserves_transitive application-judgement
     "(preorder?)" relations_extra nil)
    (partial_order? const-decl "bool" orders nil)
    (asymmetric formula-decl nil relations_extra nil)
    (asymmetric? const-decl "bool" relations_extra nil)
    (antisymmetric? const-decl "bool" relations nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure const-decl "(reflexive?)" relations_extra nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (strict_order? const-decl "bool" orders nil))
   shostak))
(reflexive_closure_dichotomous 0
  (reflexive_closure_dichotomous-1 nil 3308223765
   ("" (skosimp*)
    (("" (expand* "dichotomous?" "reflexive_closure" "union" "member")
      (("" (skosimp*)
        (("" (use "trichotomous") (("" (prop) nil nil)) nil)) nil))
      nil))
    nil)
   ((reflexive_closure const-decl "(reflexive?)" relations_extra nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (dichotomous? const-decl "bool" orders nil)
    (trichotomous formula-decl nil relations_extra nil)
    (trichotomous? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil relations_extra nil))
   nil))
(strict_total_order_to_total_order 0
  (strict_total_order_to_total_order-1 nil 3308223200
   ("" (skosimp*)
    (("" (expand "total_order?") (("" (propax) nil nil)) nil)) nil)
   ((reflexive_closure_dichotomous application-judgement
     "(dichotomous?)" relations_extra nil)
    (strict_order_to_partial_order application-judgement
     "(partial_order?)" relations_extra nil)
    (total_order? const-decl "bool" orders nil))
   shostak))
(partial_order_to_strict_order 0
  (partial_order_to_strict_order-1 nil 3308174139
   ("" (skosimp* t)
    ((""
      (expand* "strict_order?" "transitive?" "irreflexive_kernel"
       "difference" "member")
      (("" (skosimp*)
        (("" (lemma "transitive")
          (("" (assert)
            (("" (inst - "R!1" "x!1" "y!1" "z!1")
              (("" (assert)
                (("" (replace -5 :hide? t)
                  (("" (lemma "antisymmetric")
                    (("" (inst - "R!1" "z!1" "y!1")
                      (("" (prop) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((transitive? const-decl "bool" relations nil)
    (difference const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" relations_extra
     nil)
    (strict_order? const-decl "bool" orders nil)
    (transitive formula-decl nil relations_extra nil)
    (PRED type-eq-decl nil defined_types nil)
    (antisymmetric? const-decl "bool" relations nil)
    (antisymmetric formula-decl nil relations_extra nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil))
   shostak))
(irreflexive_kernel_trichotomous 0
  (irreflexive_kernel_trichotomous-1 nil 3308223871
   ("" (skosimp*)
    ((""
      (expand* "trichotomous?" "irreflexive_kernel" "difference"
       "member")
      (("" (skosimp*)
        (("" (assert)
          (("" (use "dichotomous") (("" (prop) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((irreflexive_kernel const-decl "(irreflexive?)" relations_extra
     nil)
    (member const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (trichotomous? const-decl "bool" orders nil)
    (T formal-type-decl nil relations_extra nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (dichotomous? const-decl "bool" orders nil)
    (dichotomous formula-decl nil relations_extra nil))
   nil))
(total_order_to_strict_total_order 0
  (total_order_to_strict_total_order-1 nil 3308223398
   ("" (skosimp*)
    (("" (expand "strict_total_order?") (("" (propax) nil nil)) nil))
    nil)
   ((irreflexive_kernel_trichotomous application-judgement
     "(trichotomous?)" relations_extra nil)
    (partial_order_to_strict_order application-judgement
     "(strict_order?)" relations_extra nil)
    (strict_total_order? const-decl "bool" orders nil))
   shostak))
(symmetric_kernel_of_preorder 0
  (symmetric_kernel_of_preorder-1 nil 3308174139
   ("" (skosimp* t)
    (("" (expand "equivalence?")
      (("" (prop)
        (("1"
          (expand* "reflexive?" "symmetric_kernel" "intersection"
           "converse" "member")
          (("1" (skosimp*)
            (("1" (use "reflexive") (("1" (prop) nil nil)) nil)) nil))
          nil)
         ("2"
          (expand* "transitive?" "symmetric_kernel" "intersection"
           "converse" "member")
          (("2" (skosimp*)
            (("2" (lemma "transitive")
              (("2" (inst-cp - "R!1" "x!1" "y!1" "z!1")
                (("2" (inst - "R!1" "z!1" "y!1" "x!1")
                  (("2" (prop) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((equivalence? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (transitive formula-decl nil relations_extra nil)
    (symmetric_kernel const-decl "(symmetric?)" relations_extra nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (reflexive? const-decl "bool" relations nil)
    (reflexive formula-decl nil relations_extra nil)
    (PRED type-eq-decl nil defined_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil relations_extra nil)
    (pred type-eq-decl nil defined_types nil)
    (preorder? const-decl "bool" orders nil))
   shostak)))

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