min_walks[T: TYPE]: THEORY BEGIN IMPORTING digraphs[T] IMPORTING walks[T], abstract_min v1,v2,x,y: VAR T G: VAR digraph[T] gr_walk(v1,v2): TYPE = {G: digraph[T] | vert(G)(v1) AND vert(G)(v2) AND (EXISTS (w: Seq(G)): walk_from?(G,w,v1,v2))} min_walk_from(x,y,(Gw:gr_walk(x,y))): Walk(Gw) = min[Seq(Gw),(LAMBDA (w: Seq(Gw)): l(w)), (LAMBDA (w: Seq(Gw)): walk_from?(Gw,w,x,y))] is_min(G,(w: Seq(G)),x,y): bool = walk?(G,w) AND (FORALL (ww: Seq(G)): walk_from?(G,ww,x,y) IMPLIES l(w) <= l(ww)) min_walk_def: LEMMA FORALL (Gw: gr_walk(x,y)): walk_from?(Gw,min_walk_from(x,y,Gw),x,y) AND is_min(Gw, min_walk_from(x,y,Gw),x,y) min_walk_in : LEMMA FORALL (Gw: gr_walk(x,y)): walk_from?(Gw,min_walk_from(x,y,Gw),x,y) min_walk_is_min: LEMMA FORALL (Gw: gr_walk(x,y), ww: Seq(Gw)): walk_from?(Gw,ww,x,y) IMPLIES l(min_walk_from(x,y,Gw)) <= l(ww) END min_walks