Quelle  reduce_walks.pvs

reduce_walks[T: TYPE]: THEORY

BEGIN

   IMPORTING paths[T]

   G: VAR graph[T]

   Long_walk(G): TYPE = {w: Walk(G) | length(w) > 3}

   reduce(G: graph[T], w: Long_walk(G), 
          k: {n: nat | n > 0 AND n < length(w)-1}): Walk(G) =
                      IF w(k-1) = w(k+1) THEN
                          (# length := length(w) - 2,
                          seq := (LAMBDA (i: below(length(w)-2)):
                                     IF i < k THEN w(i)
                                     ELSE w(i+2)
                                     ENDIF) #) 
                      ELSE
                          w
                      ENDIF

   reduce_lem: LEMMA FORALL (w: Walk(G), 
                            k: {n: nat | n > 0 AND n < length(w)-1}):
       w(k-1) = w(k+1) AND length(w) > 3 IMPLIES
          reduce(G,w,k) = w^(0,k-1) o w^(k+2,length(w)-1)
            

END reduce_walks