Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
min_walk_reduced.pvs
Sprache: Unknown
|
min_walk_reduced[T: TYPE]: THEORY
BEGIN
IMPORTING min_walks[T], path_ops[T]
reduced?(G: digraph[T], w: Seq(G)): bool =
(FORALL (k: nat): k > 0 AND k < length(w) - 1 IMPLIES w(k-1) /= w(k+1))
x,y: VAR T
i: VAR nat
min_walk_vert: LEMMA FORALL (Gw: gr_walk(x,y)): i < length(min_walk_from(x,y,Gw))
IMPLIES vert(Gw)(min_walk_from(x,y,Gw)(i))
min_walk_is_reduced: LEMMA FORALL (Gw: gr_walk(x,y)):
reduced?(Gw,min_walk_from(x,y,Gw))
END min_walk_reduced
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
|
