path_ops[T: TYPE]: THEORY BEGIN IMPORTING paths[T], di_subgraphs[T], sep_sets[T], digraph_ops[T] G: VAR digraph[T] v,s,t: VAR T e: VAR edgetype[T] W,V: VAR finite_set[T] w: VAR prewalk walk?_del_vert : LEMMA walk?(del_vert(G, v), w) IMPLIES walk?[T](G, w) walk?_del_vert_not : LEMMA walk?(G, w) AND NOT verts_of(w)(v) IMPLIES walk?(del_vert(G, v), w) path?_del_vert : LEMMA FORALL (w: prewalk): path?(del_vert(G, v), w) IMPLIES path?[T](G, w) path?_del_verts : LEMMA FORALL (w: prewalk): path?(del_verts(G, W), w) IMPLIES path?[T](G, w) IMPORTING walk_inductions[T] walk_to_path : LEMMA (EXISTS (w: prewalk): walk_from?(G,w,s,t)) IMPLIES (EXISTS (p: prewalk): path?(G,p) and walk_from?(G,p,s,t)) walk_to_path_from : LEMMA walk_from?(G,w,s,t) IMPLIES (EXISTS (p: prewalk): path_from?(G,p,s,t)) END path_ops