graph_conn_piece[T: TYPE]: THEORY

BEGIN

   IMPORTING graph_conn_defs[T]

   G,H1,H2: VAR graph[T]
   x,y,v: VAR 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))))

   singleton_piece: LEMMA singleton?(G) IMPLIES 
                              piece_connected?(G)

   not_piece_has_2: LEMMA NOT piece_connected?(G) IMPLIES empty?(G) OR
                            size(G) > 1
  
   e: VAR doubleton[T] 
   vo: VAR T
   
   edge_not_across: LEMMA e(vo) AND vert(H1)(vo) AND
                          edges(union(H1, H2))(e) AND
                          empty?(intersection(vert(H1), vert(H2)))
                          IMPLIES  edges(H1)(e)
   
   lem1: LEMMA vert(H1)(vo) AND  empty?(intersection(vert(H1), vert(H2))) AND
           NOT empty?(H1) AND NOT empty?(H2)
          IMPLIES del_vert(union(H1, H2), vo) = union(del_vert(H1, vo), H2)
   
   
   
   H1P_not_empty: LEMMA vert(H1)(vo) AND
                         deg(vo, union(H1, H2)) > 0 AND
                         del_vert(G, vo) = union(del_vert(H1, vo), H2) AND
                         empty?(intersection(vert(H1), vert(H2))) AND
                         NOT empty?(H1) AND NOT empty?(H2) AND 
                         NOT empty?(del_vert(G, vo))
                 IMPLIES NOT empty?(del_vert(H1, vo))

   cip0: LEMMA (FORALL (GG: graph[T]): size(GG) < size(G)
                       IMPLIES connected?(GG) IMPLIES piece_connected?(GG)) AND
               vert(H1)(vo) AND  
               deg(vo, G) > 0 AND
               connected?(del_vert(G, vo)) AND
               G = union(H1, H2) AND
               empty?(intersection(vert(H1), vert(H2))) AND
              NOT empty?(H1) AND NOT empty?(H2) 
             IMPLIES NOT empty?(intersection(vert(H1), vert(H2)))


   cip3: LEMMA (FORALL (GG: graph[T]): size(GG) < size(G)
                       IMPLIES connected?(GG) IMPLIES piece_connected?(GG)) AND
               deg(vo, G) > 0 AND
              connected?(del_vert(G, vo)) AND
              G = union(H1, H2) AND
              NOT empty?(H1) AND NOT empty?(H2) AND vert(G)(vo)
             IMPLIES NOT empty?(intersection(vert(H1), vert(H2)))

   connected_not_empty: LEMMA connected?(G) IMPLIES NOT empty?(G)


   IMPORTING graph_inductions[T]

   conn_implies_piece: LEMMA connected?(G) IMPLIES piece_connected?(G)


END graph_conn_piece