Quelle circuits.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 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

quality98%

¤ Dauer der Verarbeitung: 0.12 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.