min_walk_reduced[T: TYPE]: THEORY BEGIN IMPORTING min_walks[T], path_ops[T] reduced?(G: digraph[T], w: Seq(G)): bool = (FORALL (k: nat): k > 0 AND k < l(w) - 1 IMPLIES w(k-1) /= w(k+1)) x,y: VAR T i: VAR nat min_walk_vert: LEMMA FORALL (Gw: gr_walk(x,y)): i < l(min_walk_from(x,y,Gw)) IMPLIES vert(Gw)(min_walk_from(x,y,Gw)(i)) min_walk_is_reduced: LEMMA FORALL (Gw: gr_walk(x,y)): reduced?(Gw,min_walk_from(x,y,Gw)) END min_walk_reduced