min_walk_reduced[T: TYPE]: THEORY

BEGIN

   IMPORTING min_walks[T], path_ops[T]

   reduced?(G: graph[T], w: Seq(G)): bool = 
          (FORALL (k: nat): k > 0 AND k < length(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 < length(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