Quelle cycles.pvs Sprache: 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
%
%********************************************************************************%

% 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

quality83%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.