reduce(G: digraph[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: LEMMAFORALL (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
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
