| products/sources/formale sprachen/PVS/Tarski/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: bounded_orders.prf Sprache: LispOriginal 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.0 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
