di_subgraphs_from_walk[T: TYPE]: THEORY BEGIN IMPORTING digraphs[T], walks[T], di_subgraphs[T] G,GG: VAR digraph[T] t,t1,t2,v: VAR T i: VAR nat e: VAR edgetype[T] G_from(G, (w: Walk(G))): di_subgraph(G) = (# vert := verts_of(w), edges := edges_of(w) #) G_from_vert : LEMMA FORALL (w: Walk(G)): vert(G_from(G,w)) = verts_of(w) vert_G_from : LEMMA FORALL (w: Walk(G), i: below(l(w))): vert(G_from(G, w))(w(i)) edge?_G_from : LEMMA FORALL (w: Walk(G), i: below(l(w)-1)): edge?(G_from(G, w))(w(i), w(i+1)) %%%%%%%%%%%%%%%%%%%%%%%%%% not true for directed graphs %%%%%%%%%%%%%%%%%%%% % % edge?_G_from_rev: LEMMA FORALL (w: Walk(G), i: below(l(w)-1)): % edge?(G_from(G, w))(w(i+1), w(i)) vert_G_from_not : LEMMA FORALL (w: Walk(G)): subset?(vert(G_from(G, w)), vert(GG)) AND NOT verts_of(w)(v) IMPLIES subset?(vert(G_from(G, w)), remove[T](v, vert(GG))) IMPORTING digraph_ops[T] del_vert_di_subgraph: LEMMA FORALL (w: Walk(G), v: (vert(GG))): di_subgraph?(G_from(G, w), GG) AND NOT verts_of(w)(v) IMPLIES di_subgraph?(G_from(G, w), del_vert(GG, v)) END di_subgraphs_from_walk