graph_path_conn[T: TYPE]: THEORY

BEGIN

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

   G,G1,G2: VAR graph[T]

   isolated_not_path: LEMMA isolated?(G) AND NOT singleton?(G)
                                IMPLIES NOT path_connected?(G)

   u,v,y: VAR T
   pic_A: LEMMA (EXISTS v: vert(G)(v) AND deg(v,G) = 0)
                    IMPLIES path_connected?(G) IMPLIES connected?(G)


   IMPORTING graph_inductions[T], subtrees[T], path_ops[T]



   thw_A: LEMMA  (FORALL (GG: graph[T]): size(GG) < size(G)
                                              IMPLIES
                     (FORALL (x: T, y: T): tree?(GG) AND vert(GG)(x) 
                                           AND vert(GG)(y) AND x /= y
                     IMPLIES (EXISTS (w: Walk(GG)): walk_from?(GG, w, x, y))))
               AND deg(v, G) = 1 AND tree?(del_vert[T](G, v)) AND
        vert(G)(v) AND vert(G)(y) AND v /= y
  IMPLIES
      (EXISTS (w: Walk(G)): walk_from?(G, w, v, y))

   TR: VAR graph[T]
   x: VAR T
   tree_has_walk: LEMMA tree?(TR) AND vert(TR)(x) AND vert(TR)(y)
                           AND x /= y IMPLIES
                              (EXISTS (w: Walk(TR)):
                                   walk_from?(TR,w,x,y))

   path_implies_conn: THEOREM path_connected?(G) IMPLIES connected?(G)


END graph_path_conn