Quelle  min_walks.pvs

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)): length(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 
                                                        length(w) <= length(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 
                                        length(min_walk_from(x,y,Gw)) <= length(ww)


END min_walks