|
cycle_deg[T: TYPE]: THEORY
BEGIN
IMPORTING cycles[T], trees[T], graph_conn_defs[T], graph_connected[T],
graph_deg_sum[T], tree_circ[T], graph_complected[T],
tree_paths[T], subgraph_paths[T]
G,H: VAR graph[T]
n: VAR nat
x,y,s,t: VAR T
w,p,q: VAR prewalk
reachable(G: graph[T],x:T): finite_set[T] =
{y: T | vert(G)(y) AND
(EXISTS (w: Seq(G)): walk_from?(G,w,x,y))}
reachable_subset: LEMMA subset?(reachable(G,x),vert(G))
reachable_conn: LEMMA FORALL (x:(vert(G))):
connected?(subgraph(G,reachable(G,x)))
conn_compon: LEMMA FORALL (G: graph[T], x: (vert(G))): EXISTS H:
(subgraph?(H,G) AND
connected?(H) and vert(H)(x) and
FORALL (y:(vert(H))): (deg(y,G)=deg(y,H)))
sub_cycle: LEMMA FORALL (G,H: graph[T], w: Seq(H)): subgraph?(H,G)
and cycle?(H,w) IMPLIES cycle?(G,w)
uniq_paths?(G):bool = FORALL (s,t,p,q): path_from?(G,p,s,t) AND
path_from?(G,q,s,t) IMPLIES p=q
uniq_del_vert: LEMMA FORALL (G:graph[T], v:(vert(G))): uniq_paths?(G)
IMPLIES uniq_paths?(del_vert(G,v))
del_edge_uniq: LEMMA FORALL (G:graph[T], e:(edges(G))):
connected?(del_edge(G,e)) IMPLIES NOT uniq_paths?(G)
charact_tree: LEMMA connected?(G) AND uniq_paths?(G) IMPLIES tree?(G)
exclus_cycl: THEOREM connected?(G) IMPLIES
tree?(G) XOR (EXISTS (w:Seq(G)): cycle?(G,w))
num_edge_tree: LEMMA connected?(G) and num_edges(G)<size(G)
IMPLIES tree?(G)
iff_tree: LEMMA tree?(G) IFF connected?(G) AND uniq_paths?(G)
tree_num_iff: LEMMA connected?(G) and num_edges(G)=size(G)-1 IFF tree?(G)
deg_gt_1_cycle: LEMMA (FORALL (v: T): vert(G)(v) IMPLIES deg(v,G) > 1)
IMPLIES (EXISTS (w: Seq(G)): cycle?(G,w)) OR
empty?(G)
END cycle_deg
¤ Dauer der Verarbeitung: 0.13 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.
|
