digraph_conn_defs[T: TYPE]: THEORY BEGIN IMPORTING digraph_deg[T] G,G1,G2: VAR digraph[T] connected?(G): RECURSIVE bool = singleton?(G) OR (EXISTS (v: (vert(G))): deg(v,G) > 0 AND connected?(del_vert(G,v))) MEASURE size(G) IMPORTING walks[T] path_connected?(G): bool = NOT empty?(G) AND (FORALL (x,y: (vert(G))): % x /= y IMPLIES (EXISTS (w: Walk(G)): seq(w)(0) = x AND seq(w)(l(w)-1) = y)) H1,H2: VAR digraph[T] piece_connected?(G): bool = NOT empty?(G) AND (FORALL H1,H2: G = union(H1,H2) AND NOT empty?(H1) AND NOT empty?(H2) IMPLIES NOT empty?(intersection(vert(H1), vert(H2)))) complected?(G): bool = IF isolated?(G) THEN singleton?(G) ELSIF (EXISTS (v: (vert(G))): deg(v,G) = 1) THEN (EXISTS (x: (vert(G))): deg(x,G) = 1 AND connected?(del_vert(G,x))) ELSE (EXISTS (e: (edges(G))): connected?(del_edge(G,e))) ENDIF END digraph_conn_defs