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

Quelle  chain_chain.prf   Sprache: Lisp

 
(chain_chain
 (chain_incl_partial_order 0
  (chain_incl_partial_order-1 nil 3314727370
   ("" (lemma "subset_partial_order[T]") (("" (grind) nil nil)) nil)
   ((subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (chain_incl const-decl "bool" chain_chain nil)
    (partial_order? const-decl "bool" orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (y!1 skolem-const-decl "chain[T, <=]" chain_chain nil)
    (x!2 skolem-const-decl "T" chain_chain nil)
    (chain nonempty-type-eq-decl nil chain nil)
    (chain? const-decl "bool" chain nil)
    (<= formal-const-decl "(partial_order?[T])" chain_chain nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (restrict const-decl "R" restrict nil)
    (dichotomous? const-decl "bool" orders nil)
    (total_order? const-decl "bool" orders nil)
    (subset_partial_order formula-decl nil sets_lemmas nil)
    (T formal-type-decl nil chain_chain nil))
   nil))
 (chain_union_TCC1 0
  (chain_union_TCC1-1 nil 3314727370
   ("" (typepred "<=")
    (("" (grind :if-match nil)
      (("" (inst -7 "a!1" "a!2")
        (("" (split)
          (("1" (inst - "x!1")
            (("1" (assert)
              (("1" (inst - "x!1" "y!1") (("1" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (inst - "y!1")
            (("2" (assert)
              (("2" (inst -4 "x!1" "y!1") (("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((reflexive? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (restrict const-decl "R" restrict nil)
    (dichotomous? const-decl "bool" orders nil)
    (total_order? const-decl "bool" orders nil)
    (chain? const-decl "bool" chain nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_props nil)
    (set type-eq-decl nil sets nil)
    (subchain nonempty-type-eq-decl nil chain_chain nil)
    (chain_incl const-decl "bool" chain_chain nil)
    (chain_chain nonempty-type-eq-decl nil chain_chain nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (Union const-decl "set" sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (chain_incl_partial_order name-judgement
     "(partial_order?[subchain])" chain_chain 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 chain_chain nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(partial_order?[T])" chain_chain nil))
   nil))
 (chain_union_upper_bound 0
  (chain_union_upper_bound-1 nil 3314727563 ("" (grind) nil nil)
   ((chain_chain nonempty-type-eq-decl nil chain_chain nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (chain_incl_partial_order name-judgement
     "(partial_order?[subchain])" chain_chain nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (restrict const-decl "R" restrict nil)
    (dichotomous? const-decl "bool" orders nil)
    (total_order? const-decl "bool" orders nil)
    (FALSE const-decl "bool" booleans nil)
    (chain_union const-decl "subchain" chain_chain nil)
    (member const-decl "bool" sets nil)
    (Union const-decl "set" sets nil)
    (subset? const-decl "bool" sets nil)
    (chain_incl const-decl "bool" chain_chain nil)
    (subchain nonempty-type-eq-decl nil chain_chain nil)
    (chain? const-decl "bool" chain nil)
    (<= formal-const-decl "(partial_order?[T])" chain_chain nil)
    (partial_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types 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 chain_chain nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (extend const-decl "R" extend nil))
   shostak)))

100%


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