|
%********************************************************************************%
%
% 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)
% ---------------------------------------------------------------
% Properties
% ---------------------------------------------------------------
cycle_is_pre_Eulerian_circuit: LEMMA
cycle?(G, w) IMPLIES pre_Eulerian_circuit?(G,w)
pre_Eulerian_circuit_is_a_circuit: LEMMA
pre_Eulerian_circuit?(G,w) IMPLIES
circuit?(G,w)
Eulerian_circuit_is_circuit: LEMMA
Eulerian_circuit?(G,w) IMPLIES
circuit?(G,w)
Eulerian_walk_is_Eulerian_circuit: LEMMA
Eulerian_circuit?(G,w) IMPLIES
Eulerian_walk?(G,w)
circuit_subwalk_pre_Eulerian: LEMMA
circuit?(G, w) IMPLIES
EXISTS (w1: prewalk): sub_walk?(G, w, w1) AND
pre_Eulerian_circuit?(G,w1)
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.3 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.
|
