graph_piece_path.pvs

graph_piece_path[T: TYPE]: THEORY

BEGIN

   IMPORTING graph_conn_defs[T], walks[T], subgraphs[T]

   G,H1,H2: VAR graph[T]


   VV: VAR set[T]
   union_edge_disj: LEMMA NOT (EXISTS (u, w: T): vert(H1)(u) AND vert(H2)(w) 
                                           AND u /= w
                                           AND edges(G)(edg[T](u, w)))
                              AND H1 = subgraph(G,VV) 
                              AND H2 = subgraph(G,difference(vert(G),VV))
                           IMPLIES 
                              G = union(H1,H2)

   piece_implies_path: THEOREM piece_connected?(G) IMPLIES path_connected?(G)


END graph_piece_path