digraph_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 digraphs[T], digraph_ops[T] v: VAR T G,GS: VAR digraph[T] incident_edges(v,G) : finite_set[edgetype[T]] = {e: edgetype[T] | edges(G)(e) AND in?(v,e)} incident_edges_subset: LEMMA subset?(incident_edges(v,G),edges(G)) deg(v,G): nat = card(incident_edges(v,G)) P : VAR pred[digraph[T]] n : VAR nat e: VAR edgetype[T] x,y: VAR T incident_edges_emptyset: LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES incident_edges(v,G) = emptyset[edgetype[T]] deg_del_edge : LEMMA e = (x,y) AND edges(G)(e) IMPLIES deg(y, G) = deg(y, del_edge(G, e)) + 1 deg_del_edge1 : LEMMA e = (x,y) AND edges(G)(e) IMPLIES deg(x, G) = deg(x, del_edge(G, e)) + 1 deg_del_edge2 : LEMMA in?(y,e) AND edges(G)(e) IMPLIES deg(y, G) = deg(y, del_edge(G, e)) + 1 deg_del_edge3 : LEMMA NOT in?(y,e) 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: in?(v,e) AND edges(G)(e)) deg_to_card : LEMMA FORALL (SG: simple_digraph): deg(v,SG) > 0 IMPLIES size(SG) >= 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)((x, v)) % IMPLIES deg(v, del_vert(G, x)) = % deg(v, G) - 1 % % del_vert_not_incident: LEMMA x /= v AND NOT edges(G)((x, v)) % IMPLIES % deg(x, del_vert(G, v)) = deg(x, G) singleton_deg: LEMMA FORALL (SG: simple_digraph): singleton?(SG) IMPLIES deg(v, SG) = 0 deg_1_sing : LEMMA deg(v, G) = 1 IMPLIES (EXISTS e: incident_edges(v, G) = singleton(e) AND in?(v,e) AND edges(G)(e)) END digraph_deg