Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: max_subtrees.prf Sprache: Lisp

Original von: PVS^©

(max_subtrees
(sing_is_tree 0
  (sing_is_tree-1 nil 3301744077
   ("" (skosimp*)
    (("" (expand "tree?")
      (("" (expand "singleton_digraph")
        (("" (rewrite "card_singleton") nil nil)) nil))
      nil))
    nil)
   ((tree? def-decl "bool" trees nil)
    (card_singleton formula-decl nil finite_sets nil)
    (T formal-type-decl nil max_subtrees nil)
    (singleton_digraph const-decl "digraph" digraphs nil))
   nil))
(tree_in 0
  (tree_in-1 nil 3301744077
   ("" (skosimp*)
    (("" (typepred "G!1")
      (("" (hide -1)
        (("" (expand "nonempty?")
          (("" (expand "empty?")
            (("" (skosimp*)
              (("" (expand "member")
                (("" (inst 1 "singleton_digraph(x!1)")
                  (("1" (grind) nil nil)
                   ("2" (rewrite "sing_is_tree") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Digraph type-eq-decl nil digraphs nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (digraph type-eq-decl nil digraphs 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil max_subtrees nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (tree? def-decl "bool" trees nil)
    (singleton_digraph const-decl "digraph" digraphs nil)
    (x!1 skolem-const-decl "T" max_subtrees nil)
    (Tree type-eq-decl nil trees nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (di_subgraph? const-decl "bool" di_subgraphs nil)
    (singleton const-decl "(singleton?)" sets nil)
    (sing_is_tree formula-decl nil max_subtrees nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil))
   nil))
(max_subtree_TCC1 0
  (max_subtree_TCC1-1 nil 3301744077
   ("" (skosimp*)
    (("" (lemma "tree_in")
      (("" (inst?)
        (("" (skosimp*)
          (("" (inst?)
            (("" (prop)
              (("" (expand "extend") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tree_in formula-decl nil max_subtrees nil)
    (tree? def-decl "bool" trees nil) (Tree type-eq-decl nil trees nil)
    (Digraph type-eq-decl nil digraphs nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (digraph type-eq-decl nil digraphs 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)
    (T formal-type-decl nil max_subtrees nil))
   nil))
(max_subtree_TCC2 0
  (max_subtree_TCC2-1 nil 3301744077
   ("" (skosimp*)
    (("" (prop)
      (("1" (lemma "max_di_subgraph_in")
        (("1" (inst?)
          (("1" (expand "extend") (("1" (assert) nil)))
           ("2" (hide 2)
            (("2" (lemma "tree_in")
              (("2" (inst?)
                (("2" (skosimp*)
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (expand "extend")
                        (("2" (propax) nil)))))))))))))))))))
       ("2" (expand "extend") (("2" (assert) nil))))))
    nil)
   ((tree? def-decl "bool" trees 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)
    (Digraph type-eq-decl nil digraphs nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (digraph type-eq-decl nil digraphs 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)
    (max_di_subgraph_in formula-decl nil max_di_subgraphs nil)
    (T formal-type-decl nil max_subtrees nil))
   nil))
(max_subtree_tree 0
  (max_subtree_tree-1 nil 3301744077
   ("" (skosimp*)
    (("" (expand "max_subtree")
      (("" (lemma "max_di_subgraph_in")
        (("" (inst?)
          (("1" (expand "extend") (("1" (assert) nil)))
           ("2" (hide 2)
            (("2" (lemma "tree_in")
              (("2" (inst?)
                (("2" (skosimp*)
                  (("2" (inst?)
                    (("2" (expand "extend")
                      (("2" (assert) nil))))))))))))))))))))
    nil)
   ((max_subtree const-decl "Subtree(G)" max_subtrees nil)
    (tree? def-decl "bool" trees 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)
    (Digraph type-eq-decl nil digraphs nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (digraph type-eq-decl nil digraphs 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)
    (max_di_subgraph_in formula-decl nil max_di_subgraphs nil)
    (T formal-type-decl nil max_subtrees nil))
   nil))
(max_subtree_di_subgraph 0
  (max_subtree_di_subgraph-1 nil 3301744077
   ("" (skosimp*) (("" (assert) nil)) nil) nil nil))
(max_subtree_max 0
  (max_subtree_max-1 nil 3301744077
   ("" (skosimp*)
    (("" (expand "max_subtree")
      (("" (lemma "max_di_subgraph_is_max")
        (("" (inst?)
          (("1" (expand "extend")
            (("1" (ground)
              (("1" (hide 2)
                (("1" (typepred "SS!1")
                  (("1" (hide -1 -3)
                    (("1" (lemma "tree_nonempty")
                      (("1" (inst?)
                        (("1" (expand "empty?")
                          (("1" (expand "nonempty?")
                            (("1" (propax) nil)))))))))))))))))))
           ("2" (hide 2)
            (("2" (lemma "tree_in")
              (("2" (inst?)
                (("2" (skosimp*)
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (expand "extend")
                        (("2" (propax) nil))))))))))))))))))))))
    nil)
   ((max_subtree const-decl "Subtree(G)" max_subtrees 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)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (Digraph type-eq-decl nil digraphs 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)
    (tree? def-decl "bool" trees nil)
    (di_subgraph type-eq-decl nil di_subgraphs nil)
    (Tree type-eq-decl nil trees nil)
    (Subtree type-eq-decl nil max_subtrees nil)
    (max_di_subgraph_is_max formula-decl nil max_di_subgraphs nil)
    (T formal-type-decl nil max_subtrees nil))
   nil)))

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