|
tree_circ[T: TYPE]: THEORY
BEGIN
IMPORTING trees[T], graphs[T], graph_deg[T], graph_ops[T],
circuit_deg[T], subgraphs_from_walk[T]
G,GP,C,GG: VAR graph[T]
GT: VAR Tree
IMPORTING abstract_min
exists_c_tree: LEMMA FORALL (w: Walk(GT)):
EXISTS (t: Tree[T]): subgraph?(G_from(GT, w), t)
c_tree(TR: Tree, C: Subgraph(TR)): Tree =
min[Tree[T],(LAMBDA GT: size(GT)),
(LAMBDA GT: subgraph?(C,GT))]
tree_containing_lem: LEMMA FORALL (w: Walk(GT)):
tree?(c_tree(GT,G_from(GT,w))) AND
subgraph?(G_from(GT,w),c_tree(GT,G_from(GT,w))) AND
(FORALL (GG: Tree): subgraph?(G_from(GT,w),GG) IMPLIES
size(c_tree(GT,G_from(GT,w))) <= size(GG))
tree_deg: LEMMA FORALL (w: Walk(GT), v: T):
vert(c_tree(GT,G_from(GT,w)))(v) AND
deg(v, G_from(GT,w)) >= 2
IMPLIES deg(v, c_tree(GT,G_from(GT,w))) >= 2
small_tree_lem: LEMMA FORALL (w: Walk(G)): tree?(G) =>
size(G) <= 1 IMPLIES NOT circuit?(G,w)
tree_no_circuits: THEOREM (FORALL (w: Walk(G)): tree?(G) =>
NOT circuit?(G,w))
END tree_circ
¤ Dauer der Verarbeitung: 0.14 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.
|
