| products/sources/formale Sprachen/Isabelle/HOL/Proofs/Extraction/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 8 kB |
|
Quelle tree_circ.pvs Sprache: PVS |
|||||||||
|
tree_circ[T: TYPE]: THEORY
BEGIN IMPORTING trees[T], graphs[T], graph_deg[T], graph_ops[T], circuit_deg[T], subgraphs_from_walk[T] G,GP,C,GG: VAR graph[T] GT: VAR Tree IMPORTING abstract_min exists_c_tree: LEMMA FORALL (w: Walk(GT)): EXISTS (t: Tree[T]): subgraph?(G_from(GT, w), t) c_tree(TR: Tree, C: Subgraph(TR)): Tree = min[Tree[T],(LAMBDA GT: size(GT)), (LAMBDA GT: subgraph?(C,GT))] tree_containing_lem: LEMMA FORALL (w: Walk(GT)): tree?(c_tree(GT,G_from(GT,w))) AND subgraph?(G_from(GT,w),c_tree(GT,G_from(GT,w))) AND (FORALL (GG: Tree): subgraph?(G_from(GT,w),GG) IMPLIES size(c_tree(GT,G_from(GT,w))) <= size(GG)) tree_deg: LEMMA FORALL (w: Walk(GT), v: T): vert(c_tree(GT,G_from(GT,w)))(v) AND deg(v, G_from(GT,w)) >= 2 IMPLIES deg(v, c_tree(GT,G_from(GT,w))) >= 2 small_tree_lem: LEMMA FORALL (w: Walk(G)): tree?(G) => size(G) <= 1 IMPLIES NOT circuit?(G,w) tree_no_circuits: THEOREM (FORALL (w: Walk(G)): tree?(G) => NOT circuit?(G,w)) END tree_circ ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28