|
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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
