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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: Lisp

Original von: PVS©
(max_di_subgraphs
 (prep0 0
  (prep0-1 nil 3507100930
   ("" (skosimp*)
    (("" (expand "nonempty?")
      (("" (expand "empty?")
        (("" (typepred "P!1")
          (("" (skosimp*)
            (("" (inst -3 "size(S!1)")
              (("1" (expand "member")
                (("1" (expand "is_one_of_size")
                  (("1" (inst?) (("1" (assert) nil)))))))
               ("2" (rewrite "di_subgraph_smaller") nil))))))))))))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (Gpred type-eq-decl nil max_di_subgraphs nil)
    (pred type-eq-decl nil defined_types nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil max_di_subgraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (G!1 skolem-const-decl "digraph[T]" max_di_subgraphs nil)
    (S!1 skolem-const-decl "digraph[T]" max_di_subgraphs nil)
    (size const-decl "nat" digraphs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (<= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (upto nonempty-type-eq-decl nil nat_types nil)
    (is_one_of_size const-decl "bool" max_di_subgraphs nil)
    (di_subgraph type-eq-decl nil di_subgraphs nil)
    (member const-decl "bool" sets nil)
    (di_subgraph_smaller formula-decl nil di_subgraphs nil)
    (empty? const-decl "bool" sets nil))
   nil))
 (max_size_TCC1 0
  (max_size_TCC1-1 nil 3507100930
   ("" (expand "nonempty?")
    (("" (expand "empty?")
      (("" (expand "member")
        (("" (skosimp*)
          (("" (lemma "prep0")
            (("" (inst?)
              (("" (inst?)
                (("" (expand "nonempty?")
                  (("" (expand "empty?")
                    (("" (skosimp*)
                      (("" (expand "member")
                        (("" (inst?) nil))))))))))))))))))))))
    nil)
   ((empty? const-decl "bool" sets nil)
    (T formal-type-decl nil max_di_subgraphs nil)
    (edgetype type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (upto nonempty-type-eq-decl nil nat_types nil)
    (size const-decl "nat" digraphs nil)
    (<= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (pred type-eq-decl nil defined_types nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (Gpred type-eq-decl nil max_di_subgraphs nil)
    (prep0 formula-decl nil max_di_subgraphs nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   nil))
 (prep 0
  (prep-1 nil 3507100930
   ("" (skosimp*)
    (("" (expand "nonempty?")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (expand "max_size")
            ((""
              (typepred
               "max({n: upto[size(G!1)] | is_one_of_size(G!1,P!1,n)})")
              (("1" (hide -1 -3)
                (("1" (expand "is_one_of_size")
                  (("1" (skosimp*)
                    (("1" (inst -3 "S!1") (("1" (assert) nil)))))))))
               ("2" (rewrite "prep0") nil))))))))))))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (is_one_of_size const-decl "bool" max_di_subgraphs nil)
    (Gpred type-eq-decl nil max_di_subgraphs nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (pred type-eq-decl nil defined_types nil)
    (max const-decl
         "{a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}"
         max_upto nil)
    (set type-eq-decl nil sets nil)
    (upto nonempty-type-eq-decl nil nat_types nil)
    (size const-decl "nat" digraphs nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil max_di_subgraphs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (<= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (di_subgraph type-eq-decl nil di_subgraphs nil)
    (prep0 formula-decl nil max_di_subgraphs nil)
    (max_size const-decl "upto[size(G)]" max_di_subgraphs nil)
    (empty? const-decl "bool" sets nil))
   nil))
 (max_di_subgraph_TCC1 0
  (max_di_subgraph_TCC1-1 nil 3507100930
   (""
    (inst 1
     "(LAMBDA (G: digraph[T], P: Gpred(G)): choose({S: di_subgraph(G) | size(S) = max_size(G,P) AND P(S)}))")
    (("1" (skosimp*)
      (("1" (expand "maximal?")
        (("1" (skosimp*)
          (("1" (typepred "max_size(G!1,P!1)")
            (("1" (hide -1)
              (("1" (expand "max_size")
                (("1"
                  (typepred
                   "max({n: upto[size(G!1)] | is_one_of_size(G!1,P!1,n)})")
                  (("1" (hide -1 -2)
                    (("1" (inst -1 "size(SS!1)")
                      (("1" (assert)
                        (("1" (hide -1 2)
                          (("1" (expand "is_one_of_size")
                            (("1" (inst?) (("1" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -1 2)
                        (("2" (typepred "SS!1")
                          (("2" (hide -2 -2)
                            (("2" (rewrite "di_subgraph_smaller") nil
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -1 2)
                    (("2" (lemma "prep")
                      (("2" (rewrite "prep0") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (assert)
      (("2" (skosimp*)
        (("2" (lemma "prep") (("2" (inst?) nil nil)) nil)) nil))
      nil))
    nil)
   ((max const-decl
         "{a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}"
         max_upto nil)
    (is_one_of_size const-decl "bool" max_di_subgraphs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (G!1 skolem-const-decl "digraph[T]" max_di_subgraphs nil)
    (SS!1 skolem-const-decl "di_subgraph[T](G!1)" max_di_subgraphs nil)
    (di_subgraph_smaller formula-decl nil di_subgraphs nil)
    (prep formula-decl nil max_di_subgraphs nil)
    (prep0 formula-decl nil max_di_subgraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (max_size const-decl "upto[size(G)]" max_di_subgraphs nil)
    (upto nonempty-type-eq-decl nil nat_types nil)
    (<= const-decl "bool" reals nil)
    (size const-decl "nat" digraphs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (maximal? const-decl "bool" max_di_subgraphs nil)
    (di_subgraph type-eq-decl nil di_subgraphs nil)
    (Gpred type-eq-decl nil max_di_subgraphs nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (pred type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (digraph type-eq-decl nil digraphs nil)
    (T formal-type-decl nil max_di_subgraphs nil))
   nil))
 (max_di_subgraph_def 0
  (max_di_subgraph_def-1 nil 3507100930
   ("" (skosimp*)
    (("" (typepred "max_di_subgraph(G!1, P!1)") (("" (propax) nil nil))
      nil))
    nil)
   ((max_di_subgraph const-decl
     "{S: di_subgraph(G) | maximal?(G, S, P)}" max_di_subgraphs nil)
    (maximal? const-decl "bool" max_di_subgraphs nil)
    (di_subgraph type-eq-decl nil di_subgraphs nil)
    (Gpred type-eq-decl nil max_di_subgraphs nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (pred type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (digraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil max_di_subgraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (max_di_subgraph_in 0
  (max_di_subgraph_in-1 nil 3507100930
   ("" (skosimp*)
    (("" (typepred "max_di_subgraph(G!1, P!1)")
      (("" (hide -1 -2)
        (("" (expand "maximal?") (("" (flatten) nil nil)) nil)) nil))
      nil))
    nil)
   ((max_di_subgraph const-decl
     "{S: di_subgraph(G) | maximal?(G, S, P)}" max_di_subgraphs nil)
    (maximal? const-decl "bool" max_di_subgraphs nil)
    (di_subgraph type-eq-decl nil di_subgraphs nil)
    (Gpred type-eq-decl nil max_di_subgraphs nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (pred type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (digraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil max_di_subgraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (max_di_subgraph_is_max 0
  (max_di_subgraph_is_max-1 nil 3507100930
   ("" (skosimp*)
    (("" (typepred "max_di_subgraph(G!1, P!1)")
      (("" (hide -1 -2)
        (("" (expand "maximal?")
          (("" (flatten)
            (("" (hide -1) (("" (inst?) (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max_di_subgraph const-decl
     "{S: di_subgraph(G) | maximal?(G, S, P)}" max_di_subgraphs nil)
    (maximal? const-decl "bool" max_di_subgraphs nil)
    (di_subgraph type-eq-decl nil di_subgraphs nil)
    (Gpred type-eq-decl nil max_di_subgraphs nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (pred type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (digraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil max_di_subgraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil)))


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