reduce_walks[T: TYPE]: THEORY BEGIN IMPORTING paths[T] G: VAR digraph[T] Long_walk(G): TYPE = {w: Walk(G) | l(w) > 3} reduce(G: digraph[T], w: Long_walk(G), k: {n: nat | n > 0 AND n < l(w)-1}): Walk(G) = IF w(k-1) = w(k+1) THEN (# l := l(w) - 2, seq := (LAMBDA (i: below(l(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 < l(w)-1}): w(k-1) = w(k+1) AND l(w) > 3 IMPLIES reduce(G,w,k) = w^(0,k-1) o w^(k+2,l(w)-1) END reduce_walks