| 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 max_subgraphs.pvs Sprache: PVS |
|||||||||
|
max_subgraphs[T: TYPE]: THEORY
BEGIN IMPORTING subgraphs[T], max_upto G: VAR graph[T] Gpred(G): TYPE = {P: pred[graph[T]] | (EXISTS (S: graph[T]): subgraph?(S,G) AND P(S))} n: VAR nat is_one_of_size(G: graph[T], P: Gpred(G),n: nat): bool = (EXISTS (S: Subgraph(G)): P(S) AND size(S) = n) prep0: LEMMA FORALL (G: graph[T], P: Gpred(G)): nonempty?[upto[size(G)]]({n: upto[size(G)] | is_one_of_size(G,P,n)}) max_size(G: graph[T], P: Gpred(G)): upto[size(G)] = max({n: upto[size(G)] | is_one_of_size(G,P,n)}) prep : LEMMA FORALL (G: graph[T], P: Gpred(G)): nonempty?[Subgraph(G)]({S: Subgraph(G) | size[T](S) = max_size(G,P) AND P(S)}) maximal?(G: graph[T], S: Subgraph(G),P: Gpred(G)): bool = P(S) AND (FORALL (SS: Subgraph(G)): P(SS) IMPLIES size(SS) <= size(S)) % Existence TCC satisfied by % choose({S: Subgraph(G) | size(S) = max_size AND P(S)}) max_subgraph(G: graph[T], P: Gpred(G)): {S: Subgraph(G) | maximal?(G,S,P)} max_subgraph_def : LEMMA FORALL (P: Gpred(G)): maximal?(G,max_subgraph(G,P),P) max_subgraph_in : LEMMA FORALL (P: Gpred(G)): P(max_subgraph(G,P)) max_subgraph_is_max : LEMMA FORALL (P: Gpred(G)): (FORALL (SS: Subgraph(G)): P(SS) IMPLIES size(SS) <= size(max_subgraph(G,P))) END max_subgraphs ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28