digraph_deg[T: TYPE ]: THEORY %------------------------------------------------------------------------ % % Defines degree of a vertex % ------------------------------------------------ % % Authors: Ricky W. Butler NASA Langley Research Center % Kristin Y. Rozier NASA Langley Research Center % % Defines: % % incident_edges(v,G) -- returns set of edges attached to vertex v % % in_deg(v,G), out_deg(v,G) -- number of edges attached to vertex v % %------------------------------------------------------------------------ BEGIN IMPORTING digraphs[T], digraph_ops[T]VAR TVAR digraph[T]AND e`2 = v}AND e`1 = v}AND in ?(v,e)}LEMMA subset?(incoming_edges(v,G),edges(G))LEMMA subset?(outgoing_edges(v,G),edges(G))LEMMA subset?(incident_edges(v,G),edges(G))%This definition of degree doesn't work for digraphs %deg(v,G): nat = card(incident_edges(v,G)) VAR pred[digraph[T]]VAR natVAR edgetype[T]VAR T%possible alternate: self_loop?(e,G): bool = edges(G)(e) AND (e`1 = e`2) LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES %Define incident edges independently from in & out so self-loops aren't %counted twice (i.e. incident edges /= in_edges + out_edges) LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES LEMMA e = (x,y) AND edges(G)(e) IMPLIES LEMMA e = (x,y) AND edges(G)(e) IMPLIES LEMMA NOT in ?(y,e) IMPLIES LEMMA NOT y = e`2 IMPLIES LEMMA NOT y = e`1 IMPLIES LEMMA in ?(y,e) AND edges(G)(e) AND NOT self_loop?(e) IMPLIES deg(y, G) = deg(y, del_edge(G, e)) + 1LEMMA in ?(y,e) AND edges(G)(e) AND self_loop?(e) IMPLIES deg(y, G) = deg(y, del_edge(G, e)) + 2LEMMA in_deg(y, G) >= in_deg(y, del_edge(G, e))LEMMA out_deg(y, G) >= out_deg(y, del_edge(G, e))LEMMA deg(y, G) >= deg(y, del_edge(G, e))LEMMA in_deg(y, G) - 1 <= in_deg(y, del_edge(G, e))LEMMA out_deg(y, G) - 1 LEMMA deg(y, G) - 2 <= deg(y, del_edge(G, e))LEMMA in_deg(v,G) > 0 IMPLIES EXISTS e: (e`2 = v) AND edges(G)(e))LEMMA out_deg(v,G) > 0 IMPLIES EXISTS e: (e`1 = v) AND edges(G)(e))LEMMA deg(v,G) > 0 IMPLIES EXISTS e: in ?(v,e) AND edges(G)(e))LEMMA FORALL (SG: simple_digraph):IMPLIES size(SG) >= 2LEMMA deg(v,G) = 0 IMPLIES LEMMA FORALL (SG: simple_digraph): singleton?(SG) IMPLIES FORALL (e | edges(SG)(e)): self_loop?(e)LEMMA FORALL (SG: simple_digraph): singleton?(SG) IMPLIES LEMMA FORALL (SG: simple_digraph):IMPLIES in_deg(v, SG) = out_deg(v, SG)LEMMA in_deg(v, G) = 1 IMPLIES EXISTS e: incoming_edges(v, G) = singleton(e) AND AND edges(G)(e))LEMMA out_deg(v, G) = 1 IMPLIES EXISTS e: outgoing_edges(v, G) = singleton(e) AND AND edges(G)(e))LEMMA deg(v, G) = 1 IMPLIES EXISTS e: incident_edges(v, G) = singleton(e) AND in ?(v,e) AND edges(G)(e))LEMMA deg(v, G) = 1 IMPLIES AND out_deg(v, G) = 0)OR (in_deg(v, G) = 0 AND out_deg(v, G) = 1)LEMMA deg(v,G) = 1 IMPLIES EXISTS (e:{e:edgetype | edges(G)(e)}, u:{u:T | vert(G)(u)}):OR e = (u,v))AND v /= uEND digraph_degquality 94%
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
