|
(max_subtrees
(sing_is_tree 0
(sing_is_tree-1 nil 3251113228
("" (skosimp*)
(("" (expand "tree?")
(("" (prop)
(("" (hide 2)
(("" (expand "singleton_graph")
(("" (rewrite "card_singleton") nil nil)) 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_graph const-decl "(singleton?)" graphs nil))
nil))
(tree_in 0
(tree_in-1 nil 3251113228
("" (skosimp*)
(("" (typepred "G!1")
(("" (hide -1)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (skosimp*)
(("" (expand "member")
(("" (case "isolated?(G!1)")
(("1" (inst 1 "singleton_graph(x!1)")
(("1" (grind) nil nil)
("2" (rewrite "sing_is_tree") nil nil))
nil)
("2" (expand "isolated?")
(("2" (expand "empty?")
(("2" (skosimp*)
(("2" (expand "member")
(("2" (typepred "x!2")
(("2" (skosimp*)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(typepred "G!1")
(("2"
(inst?)
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst
2
"(# vert := edg[T](x!3,y!1), edges := singleton[doubleton](dbl[T](x!3,y!1)) #)")
(("1"
(expand "edg")
(("1"
(expand "subgraph?")
(("1"
(prop)
(("1"
(typepred "G!1")
(("1"
(inst?)
(("1"
(hide -2)
(("1"
(split -1)
(("1"
(inst-cp
-1
"y!1")
(("1"
(inst
-1
"x!3")
(("1"
(hide
-3)
(("1"
(expand
"dbl")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil)
("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"subset?")
(("2"
(skosimp*)
(("2"
(expand
"member")
(("2"
(expand
"singleton")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(inst -1 "x!3")
(("3"
(expand "dbl")
(("3"
(propax)
nil
nil))
nil))
nil)
("4"
(expand
"subset?")
(("4"
(skosimp*)
(("4"
(expand
"member")
(("4"
(typepred
"G!1")
(("4"
(inst?)
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5"
(expand
"subset?")
(("5"
(skosimp*)
(("5"
(expand
"member")
(("5"
(expand
"singleton")
(("5"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("6"
(inst -1 "x!3")
(("6"
(expand "dbl")
(("6"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(split +)
(("1"
(skosimp*)
(("1"
(expand
"singleton")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand
"edg")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1)
(("2"
(expand "tree?")
(("2"
(flatten)
(("2"
(inst 2 "x!3")
(("1"
(prop)
(("1"
(hide
-1
-3
2)
(("1"
(expand
"deg")
(("1"
(expand
"incident_edges")
(("1"
(case-replace
"{e: doubleton[T] |
singleton[doubleton](dbl[T](x!3, y!1))(e) AND e(x!3)} =
singleton[doubleton](dbl[T](x!3, y!1))")
(("1"
(rewrite
"card_singleton[doubleton]")
(("1"
(inst
+
"x!3"
"y!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(apply-extensionality
1
:hide?
t)
(("1"
(grind)
nil
nil)
("2"
(inst?)
(("2"
(assert)
nil
nil))
nil)
("3"
(skosimp*)
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(inst?)
(("3"
(assert)
nil
nil))
nil)
("4"
(skosimp*)
(("4"
(inst?)
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"del_vert[T]((# vert := edg[T](x!3, y!1),
edges :=
singleton[doubleton]
(dbl[T](x!3,
y!1))
#),
x!3) = singleton_graph(y!1)")
(("1"
(hide -1)
(("1"
(rewrite
"sing_is_tree")
nil
nil))
nil)
("2"
(hide
2
3)
(("2"
(hide
-1
-2)
(("2"
(apply-extensionality
:hide?
t)
(("1"
(grind)
(("1"
(apply-extensionality
:hide?
t)
(("1"
(grind)
nil
nil)
("2"
(skosimp*)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"del_vert")
(("2"
(expand
"remove")
(("2"
(expand
"singleton_graph")
(("2"
(expand
"member")
(("2"
(expand
"singleton")
(("2"
(expand
"edg")
(("2"
(expand
"dbl")
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(iff
1)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(expand
"edg")
(("3"
(expand
"singleton")
(("3"
(assert)
nil
nil))
nil))
nil))
nil)
("4"
(inst?)
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(expand
"singleton")
(("3"
(expand
"edg")
(("3"
(assert)
nil
nil))
nil))
nil))
nil)
("4"
(expand
"edg")
(("4"
(inst?)
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"edg")
(("2"
(expand
"dbl")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Graph type-eq-decl nil graphs nil)
(nonempty? const-decl "bool" sets nil)
(graph type-eq-decl nil graphs nil)
(pregraph type-eq-decl nil graphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets 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)
(isolated? const-decl "bool" graphs nil)
(sing_is_tree formula-decl nil max_subtrees nil)
(G!1 skolem-const-decl "Graph[T]" max_subtrees nil)
(singleton const-decl "(singleton?)" sets nil)
(subgraph? const-decl "bool" subgraphs nil)
(emptyset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(Tree type-eq-decl nil trees nil)
(x!1 skolem-const-decl "T" max_subtrees nil)
(singleton_graph const-decl "(singleton?)" graphs nil)
(singleton? const-decl "bool" graphs nil)
(tree? def-decl "bool" trees nil)
(nil application-judgement "finite_set[T]" max_subtrees nil)
(singleton? const-decl "bool" sets nil)
(x!3 skolem-const-decl "T" max_subtrees nil)
(y!1 skolem-const-decl "T" max_subtrees nil)
(edg const-decl "doubleton[T]" graphs nil)
(finite_doubleton formula-decl nil doubletons nil)
(deg const-decl "nat" graph_deg nil)
(card_singleton formula-decl nil finite_sets nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(finite_remove application-judgement "finite_set" finite_sets nil)
(remove const-decl "set" sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil))
nil))
(max_subtree_TCC1 0
(max_subtree_TCC1-1 nil 3251113228
("" (skosimp*)
(("" (lemma "tree_in")
(("" (inst?)
(("" (skosimp*)
(("" (inst?)
(("" (prop)
(("" (expand "extend") (("" (assert) nil))))))))))))))
nil)
((tree_in formula-decl nil max_subtrees nil)
(extend const-decl "R" extend nil)
(tree? def-decl "bool" trees nil) (Tree type-eq-decl nil trees nil)
(Graph type-eq-decl nil graphs nil)
(nonempty? const-decl "bool" sets nil)
(graph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pregraph type-eq-decl nil graphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans 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 max_subtrees nil))
nil))
(max_subtree_TCC2 0
(max_subtree_TCC2-1 nil 3251113228
("" (skosimp*)
(("" (prop)
(("1" (lemma "max_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)
((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)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(pred type-eq-decl nil defined_types nil)
(subgraph? const-decl "bool" subgraphs nil)
(Gpred type-eq-decl nil max_subgraphs nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(tree? def-decl "bool" trees nil)
(max_subgraph_in formula-decl nil max_subgraphs nil)
(T formal-type-decl nil max_subtrees nil))
nil))
(max_subtree_tree 0
(max_subtree_tree-1 nil 3251113228
("" (skosimp*)
(("" (expand "max_subtree")
(("" (lemma "max_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)
(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)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(pred type-eq-decl nil defined_types nil)
(subgraph? const-decl "bool" subgraphs nil)
(Gpred type-eq-decl nil max_subgraphs nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(tree? def-decl "bool" trees nil)
(max_subgraph_in formula-decl nil max_subgraphs nil)
(T formal-type-decl nil max_subtrees nil))
nil))
(max_subtree_subgraph 0
(max_subtree_subgraph-1 nil 3251113228
("" (skosimp*) (("" (assert) nil)) nil) nil nil))
(max_subtree_max 0
(max_subtree_max-1 nil 3251113228
("" (skosimp*)
(("" (expand "max_subtree")
(("" (lemma "max_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)
(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)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(pred type-eq-decl nil defined_types nil)
(subgraph? const-decl "bool" subgraphs nil)
(Gpred type-eq-decl nil max_subgraphs nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(tree? def-decl "bool" trees nil)
(Subgraph type-eq-decl nil subgraphs nil)
(Tree type-eq-decl nil trees nil)
(Subtree type-eq-decl nil max_subtrees nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(tree_nonempty formula-decl nil trees nil)
(empty? const-decl "bool" graphs nil)
(max_subgraph_is_max formula-decl nil max_subgraphs nil)
(T formal-type-decl nil max_subtrees nil))
nil)))
¤ Dauer der Verarbeitung: 0.87 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.
|
