|
%********************************************************************************%
%
% 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 cycle is a simple circuit; i.e., a walk without repetions except for the end points
cycles[T: TYPE]: THEORY
BEGIN
IMPORTING circuits[T]
G: VAR digraph[T]
w: VAR prewalk
% --------------------------------------------------------------------------------
% Definitions
% --------------------------------------------------------------------------------
cycle?(G: digraph[T], w: prewalk): bool =
circuit?(G,w) AND
(FORALL (i,j: below(length(w)-1)): i /= j IMPLIES w(i) /= w(j))
% --------------------------------------------------------------------------------
% Properties
% --------------------------------------------------------------------------------
cycle_is_circuit : LEMMA
FORALL (G: digraph[T], w: prewalk) : cycle?(G,w) IMPLIES circuit?(G,w)
% cycle_has_path: LEMMA FORALL (w: prewalk): cycle?(G,w) IMPLIES
% (EXISTS (j: below(length(w))): path?(G,w^(0,j)))
circuit_subwalk_cycle: LEMMA
circuit?(G, w) IMPLIES
EXISTS (w1: prewalk): sub_walk?(G, w, w1) AND cycle?(G,w1)
cycle_prefix: LEMMA
circuit?(G,w) IMPLIES
(cycle?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o w2)
AND cycle?(G,w1))
cycle_o_circuit: LEMMA
circuit?(G,w) IMPLIES
(cycle?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o rest(w2))
AND cycle?(G,w1) AND circuit?(G,w2))
%--------------------------------------------------------------------------------
IMPORTING digraphs, finite_sets@finite_sets_card_eq, structures@seq_pigeon
GF: VAR Digraph[T]
Pigeon_hole: THEOREM FORALL (w: Walk(GF)): length(w) > card(vert(GF)) IMPLIES
(EXISTS (i,j: below(length(w))): i /= j AND w(i) = w(j))
END cycles
¤ Dauer der Verarbeitung: 0.1 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.
|
