| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/C/Lyx/src/ (Beweissystem Isabelle Version 2025-1©) Datei vom 26.9.1998 mit Größe 15 kB |
|
Quellcode-Bibliothek max_subtrees.pvs Sprache: PVS |
|||||||||
|
max_subtrees[T: TYPE]: THEORY
BEGIN IMPORTING trees[T] G: VAR Digraph[T] % not empty?(G) IMPORTING max_di_subgraphs[T], doubletons[T] v: VAR T sing_is_tree: LEMMA tree?[T](singleton_digraph(v)) tree_in: LEMMA (EXISTS (Tr: Tree[T]): di_subgraph?(Tr,G) AND %% UNPROVED %% nonempty?[T](vert(Tr))) Tr,S: VAR Tree[T] Subtree(G: digraph[T]): TYPE = {Tr: Tree | di_subgraph?(Tr,G)} max_subtree(G: Digraph[T]): Subtree(G) = max_di_subgraph(G,tree?) max_subtree_tree : LEMMA tree?(max_subtree(G)) max_subtree_di_subgraph: LEMMA di_subgraph?(max_subtree(G),G) max_subtree_max : LEMMA FORALL (SS: Subtree(G)): size(SS) <= size(max_subtree(G)) END max_subtrees ¤ 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.0.2Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
