%********************************************************************************% % % Contributions from: % % Andréia Borges Avelar -- Universidade de Brasília - Brasil % Mauricio Ayala-Rincon -- Universidade de Brasília - Brasil % Cesar Muñoz -- NASA Langley Research Center - US % %********************************************************************************%
Eulerian[T:TYPE] : THEORY BEGIN
IMPORTING cycles[T],
walk_inductions[T]
G : VAR digraph
w : VAR prewalk
%%% For walks it means that we don't have repeated edges
no_repeat_subseq?(w) : bool = FORALL (i,j:below(length(w) - 1)) :
i < j AND w`seq(i) = w`seq(j) IMPLIES w`seq(i+1) /= w`seq(j+1)
pre_Eulerian_walk?(G,w) : bool =
walk?(G,w) AND no_repeat_subseq?(w)
Eulerian_walk?(G,w) : bool =
pre_Eulerian_walk?(G,w) AND
edges_of(w) = edges(G)
pre_Eulerian_circuit?(G,w) : bool =
pre_Eulerian_walk?(G,w) AND circuit?(G, w) % w(0) = w(length(w)-1) AND % length(w) > 1
Eulerian_circuit?(G,w) : bool =
pre_Eulerian_circuit?(G,w) AND
edges_of(w) = edges(G)
pre_Eulerian_circuit_prefix: LEMMA
circuit?(G,w) IMPLIES (pre_Eulerian_circuit?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o w2) AND
pre_Eulerian_circuit?(G,w1))
pre_Eulerian_circuit_o_circuit: LEMMA
circuit?(G,w) IMPLIES (pre_Eulerian_circuit?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o rest(w2)) AND
pre_Eulerian_circuit?(G,w1) AND circuit?(G,w2))
END Eulerian
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
