|
%trees, defined for directed graphs
%
% Authors:
%
% Ricky W. Butler NASA Langley Research Center
% Kristin Y. Rozier NASA Langley Research Center
%
% Last updated: 7/28/2004
trees[T: TYPE]: THEORY
BEGIN
IMPORTING digraph_deg[T], digraph_ops[T], di_subgraphs[T]
G,GP,C,GG: VAR digraph[T]
v: VAR T
leaf?(v,G): MACRO bool = in_deg(v,G) = 1 AND out_deg(v,G) = 0
leaf?(G)(v): bool = leaf?(v,G)
root?(v,G): MACRO bool = in_deg(v,G) = 0 AND out_deg(v,G) > 0
root?(G)(v): bool = root?(v,G)
% tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
% (EXISTS (v: (vert(G))): root?(G)(v)
% AND tree?(del_vert[T](G,v)))
% MEASURE size(G)
tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
(EXISTS (v: (vert(G))): leaf?(G)(v)
AND tree?(del_vert[T](G,v)))
MEASURE size(G)
tree_nonempty: LEMMA tree?(G) IMPLIES NOT empty?(G)
Tree: TYPE = {G: digraph[T] | tree?(G)}
END trees
¤ Dauer der Verarbeitung: 0.19 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.
|
