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

Quellcode-Bibliothek subgraph_paths.prf   Sprache: Lisp

 
(subgraph_paths
 (walk?_subgraph 0
  (walk?_subgraph-1 nil 3507100599
   ("" (skosimp*)
    (("" (expand "walk?")
      (("" (split 1)
        (("1" (flatten)
          (("1" (expand "verts_in?")
            (("1" (skosimp*)
              (("1" (inst?)
                (("1" (expand "subgraph?")
                  (("1" (hide -3)
                    (("1" (expand "subset?")
                      (("1" (flatten)
                        (("1" (hide -2)
                          (("1" (expand "member")
                            (("1" (inst?)
                              (("1" (assert) nil)))))))))))))))))))))))
         ("2" (flatten)
          (("2" (skosimp*)
            (("2" (hide -3)
              (("2" (inst?)
                (("2" (assert)
                  (("2" (expand "subgraph?")
                    (("2" (expand "subset?")
                      (("2" (flatten)
                        (("2" (hide -2)
                          (("2" (expand "member")
                            (("2" (expand "edge?")
                              (("2"
                                (expand "finseq_appl")
                                (("2"
                                  (flatten)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (inst?)
                                      (("1" (assert) nil)
                                       ("2"
                                        (inst?)
                                        (("2"
                                          (assert)
                                          nil))))))))))))))))))))))))))))))))))))))
    nil)
   ((walk? const-decl "bool" walks nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nil application-judgement "finite_set[T]" subgraph_paths nil)
    (edge? const-decl "bool" graphs nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (below type-eq-decl nil naturalnumbers nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (T formal-type-decl nil subgraph_paths nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (verts_in? const-decl "bool" walks nil))
   nil))
 (path?_subgraph 0
  (path?_subgraph-1 nil 3507100599
   ("" (skosimp*)
    (("" (expand "path?")
      (("" (flatten)
        (("" (split 1)
          (("1" (lemma "walk?_subgraph")
            (("1" (inst?) (("1" (inst?) (("1" (assert) nil)))))))
           ("2" (propax) nil))))))))
    nil)
   ((path? const-decl "bool" paths nil)
    (T formal-type-decl nil subgraph_paths nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (walk?_subgraph formula-decl nil subgraph_paths nil))
   nil)))

96%


¤ 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.0.1Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff




Wurzel

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders