| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
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 ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28