|
graph_deg[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% Defines degree of a vertex
% ------------------------------------------------
%
% Author: Ricky W. Butler NASA Langley Research Center
%
% Defines:
%
% incident_edges(v,G) -- returns set of edges attached to vertex v
%
% deg(v,G) -- number of edges attached to vertex v
%
%------------------------------------------------------------------------
BEGIN
IMPORTING graphs[T], graph_ops[T]
v: VAR T
G,GS: VAR graph[T]
incident_edges(v,G) : finite_set[doubleton[T]]
= {e: doubleton[T] | edges(G)(e) AND e(v)}
incident_edges_subset: LEMMA subset?(incident_edges(v,G),edges(G))
deg(v,G): nat = card(incident_edges(v,G))
P : VAR pred[graph[T]]
n : VAR nat
e: VAR doubleton[T]
x,y: VAR T
incident_edges_emptyset: LEMMA edges(G) = emptyset[doubleton[T]] IMPLIES
incident_edges(v,G) = emptyset[doubleton[T]]
deg_del_edge : LEMMA e = dbl(x,y) AND edges(G)(e) IMPLIES
deg(y, G) = deg(y, del_edge(G, e)) + 1
deg_del_edge2 : LEMMA e(y) AND edges(G)(e) IMPLIES
deg(y, G) = deg(y, del_edge(G, e)) + 1
deg_del_edge3 : LEMMA NOT e(y) IMPLIES
deg(y, G) = deg(y, del_edge(G, e))
deg_del_edge_ge : LEMMA deg(y, G) >= deg(y, del_edge(G, e))
deg_del_edge_le : LEMMA deg(y, G) - 1 <= deg(y, del_edge(G, e))
deg_edge_exists : LEMMA deg(v,G) > 0 IMPLIES
(EXISTS e: e(v) AND edges(G)(e))
deg_to_card : LEMMA deg(v,G) > 0 IMPLIES size(G) >= 2
del_vert_deg_0 : LEMMA deg(v,G) = 0 IMPLIES
edges(del_vert(G,v)) = edges(G)
deg_del_vert: LEMMA x /= v AND edges(G)(dbl[T](x, v))
IMPLIES deg(v, del_vert(G, x)) =
deg(v, G) - 1
del_vert_not_incident: LEMMA x /= v AND NOT edges(G)(dbl[T](x, v)) IMPLIES
deg(x, del_vert(G, v)) = deg(x, G)
singleton_deg: LEMMA singleton?(G) IMPLIES deg(v, G) = 0
deg_1_sing : LEMMA deg(v, G) = 1 IMPLIES
(EXISTS e: incident_edges(v, G) = singleton(e) AND
e(v) AND edges(G)(e))
END graph_deg
¤ Dauer der Verarbeitung: 0.23 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.
|
