|
%********************************************************************************%
%
% 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
%
%********************************************************************************%
% A circuit is a walk where the end points are the same
circuits[T: TYPE]: THEORY
BEGIN
IMPORTING walks[T],
structures@seq_extras[T]
G: VAR digraph[T]
w, w1, w2: VAR prewalk[T]
% --------------------------------------------------------------------------------
% Definitions
% --------------------------------------------------------------------------------
pre_circuit?(G: digraph[T], w: prewalk): bool =
walk?(G,w) AND w(0) = w(length(w)-1)
circuit?(G: digraph[T], w: prewalk): bool =
pre_circuit?(G,w) AND length(w) > 1
loop?(G: digraph[T], w: prewalk): bool =
pre_circuit?(G, w) AND length(w) = 2
eq_circuit?(G, w, w1): bool =
circuit?(G, w) AND circuit?(G, w1) AND eq_prewalk?(rest(w), rest(w1))
% --------------------------------------------------------------------------------
% Properties
% --------------------------------------------------------------------------------
eq_circuit_length: LEMMA
eq_circuit?(G, w1, w2) IMPLIES length(w1) = length(w2)
eq_circuit_reflexive: LEMMA
circuit?(G, w) IMPLIES eq_circuit?(G, w, w)
eq_circuit_symmetric: LEMMA
eq_circuit?(G, w1, w2) IMPLIES eq_circuit?(G, w2, w1)
loop_is_circuit: LEMMA
loop?(G, w) IMPLIES circuit?(G, w)
equal_rest_equal_circuit: LEMMA
circuit?(G, w1) AND circuit?(G, w2) AND rest(w1) = rest(w2)
IMPLIES w1 = w2
equal_eq_circuit: LEMMA
eq_circuit?(G, w1, w2) AND rest(w1) = rest(w2)
IMPLIES w1 = w2
circuit_equal_fisrt: LEMMA
circuit?(G, w1) AND circuit?(G, w2) AND circuit?(G, w1 o rest(w2))
IMPLIES w1`seq(0) = w2`seq(0)
comp_circuit_inter: LEMMA
circuit?(G, w1 o rest(w2)) AND length(w2) > 1
IMPLIES nonempty?(intersection(verts_of(w1), verts_of(w2)))
eq_circuit_position: LEMMA
eq_circuit?(G, w1, w2) IMPLIES
EXISTS (i: below[length(w1)]): w2 = w1 ^ (i, length(w1) - 2) o w1 ^ (0, i)
eq_circuit_edges: LEMMA
eq_circuit?(G, w1, w2) IMPLIES edges_of(w1) = edges_of(w2)
commuted_circuit: LEMMA
FORALL (i : below[w`length]): circuit?(G, w)
IMPLIES circuit?(G, w ^ (i, w`length-1) o w ^ (1,i))
commuted_circuit_is_eq: LEMMA
FORALL (i : below[w`length]): circuit?(G, w)
IMPLIES eq_circuit?(G, w, w ^ (i, w`length-1) o w ^ (1,i))
END circuits
¤ Dauer der Verarbeitung: 0.17 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.
|
