| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle subtrees.pvs Sprache: PVS |
|||||||||
|
subtrees[T: TYPE]: THEORY
%------------------------------------------------------------------------------- % Authors: % % Ricky W. Butler, NASA Langley % Kristin Y. Rozier, NASA Langley % % Last modified 07/30/04 % % Maintained by: % % Rick Butler NASA Langley Research Center % R.W.Butler@larc.nasa.gov %------------------------------------------------------------------------------- BEGIN IMPORTING max_subtrees[T], digraph_conn_defs[T] G: VAR Digraph[T] % not empty?(G) S: VAR digraph[T] n: VAR nat walk_acr: LEMMA FORALL (w: Walk(G)): n < length(w) AND vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n)) IMPLIES (EXISTS (j: posnat): (j <= n AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j))))) walk_acr2: LEMMA FORALL (w: Walk(G)): n < length(w) AND vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n)) IMPLIES (EXISTS (j: posnat): (j <= n AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j))))) e: VAR edgetype[T] v,w: VAR T add_pair: LEMMA vert(G)(v) AND v /= w AND add((v, w), edges(G))(e) IMPLIES LET (x,y) = e IN add(w, vert(G))(x) AND add(w, vert(G))(y) no_self_loops?(G): bool = FORALL (e: (edges(G))): e`1 /= e`2 max_tree_all_verts: LEMMA connected?(G) AND no_self_loops?(G) IMPLIES vert(max_subtree(G)) = vert(G) %Another possible lemma: (after a definition for root exists) % Starting from the root, there exists a walk from the root to % any other vertex in G END subtrees ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28