|
trees[T: TYPE]: THEORY
BEGIN
IMPORTING graph_deg[T], graph_ops[T], subgraphs[T], graph_inductions[T]
G,GP,C,GG: VAR graph[T]
u,v: VAR T
k,n,m: VAR nat
tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
(EXISTS (v: (vert(G))): deg(v,G) = 1 AND
tree?(del_vert[T](G,v)))
MEASURE size(G)
tree_nonempty: LEMMA tree?(G) IMPLIES NOT empty?(G)
Tree: TYPE = {G: graph[T] | tree?(G)}
tree_edge_card: LEMMA tree?(G) IMPLIES
size(G)= card[doubleton[T]](edges(G))+1
tree_edge_k: LEMMA (FORALL G,v,k: tree?(G) AND size(G) = k+2 AND vert(G)(v)
IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1) IMPLIES
(FORALL G,v: tree?(G) AND vert(G)(v)
IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1)
tree_edge: LEMMA (FORALL G,v,k: tree?(G) AND size(G) = k+2 AND vert(G)(v)
IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1)
tree_edge_all: LEMMA tree?(G) AND vert(G)(v) IMPLIES deg(v,G)>0 OR
card[T](vert(G)) = 1
del_tree_k: LEMMA ( FORALL G,v,k: tree?(G) and size(G) = k+1 AND
vert(G)(v) AND deg(v,G)=1
IMPLIES tree?(del_vert(G,v)))
IMPLIES (FORALL G,v: tree?(G) AND
vert(G)(v) AND
deg(v,G)=1
IMPLIES tree?(del_vert(G,v)))
del_tree: LEMMA ( FORALL G,v,k: tree?(G) AND size(G) = k+1 AND
vert(G)(v) AND deg(v,G)=1
IMPLIES tree?(del_vert(G,v)))
del_tree_all: LEMMA tree?(G) AND vert(G)(v) AND deg(v,G)=1 IMPLIES
tree?(del_vert(G,v))
END trees
¤ Dauer der Verarbeitung: 0.1 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.
|
