graph_conn_defs[T: TYPE]: THEORY

BEGIN

   IMPORTING graph_deg[T]

   G,G1,G2: VAR graph[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)(length(w)-1) = y))


   H1,H2: VAR graph[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 graph_conn_defs