Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Eulerian.pvs Sprache: PVS

Original von: PVS^©

%********************************************************************************%
%
%   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.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.