| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle cycles.pvs Sprache: PVS |
|||||||||
|
cycles[T: TYPE]: THEORY
BEGIN IMPORTING paths[T] G: VAR graph[T] cycle?(G: graph[T], (w: Seq(G))): bool = pre_circuit?(G,w) AND length(w) > 1 AND w(1) /= w(length(w)-2) AND (FORALL (i,j: below(length(w))): w(i) = w(j) IMPLIES (i = j OR (endpoint?(i,w) AND endpoint?(j,w)))) cycle_l_gt_3: LEMMA (FORALL (w: Seq(G)): cycle?(G,w) IMPLIES length(w) > 3) cycle_has_path: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IMPLIES (EXISTS (j: below(length(w))): path?(G,w^(0,j))) %% -- the term "w(1) /= w(length(w)-2)" rules out length(w) = 2 AND length(w) = 3 -- cycle_gt3: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IMPLIES length(w) > 3 cycle_def: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IFF pre_circuit?(G,w) AND length(w) > 3 AND (FORALL (i,j: below(length(w))): w(i) = w(j) IMPLIES (i = j OR (endpoint?(i,w) AND endpoint?(j,w)))) END cycles ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28