| 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 trees.pvs Sprache: PVS |
|||||||||
|
trees[T: TYPE]: THEORY
BEGIN IMPORTING graph_deg[T], graph_ops[T], subgraphs[T], graph_inductions[T] G,GP,C,GG: VAR graph[T] u,v: VAR T k,n,m: VAR nat tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR (EXISTS (v: (vert(G))): deg(v,G) = 1 AND tree?(del_vert[T](G,v))) MEASURE size(G) tree_nonempty: LEMMA tree?(G) IMPLIES NOT empty?(G) Tree: TYPE = {G: graph[T] | tree?(G)} tree_edge_card: LEMMA tree?(G) IMPLIES size(G)= card[doubleton[T]](edges(G))+1 tree_edge_k: LEMMA (FORALL G,v,k: tree?(G) AND size(G) = k+2 AND vert(G)(v) IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1) IMPLIES (FORALL G,v: tree?(G) AND vert(G)(v) IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1) tree_edge: LEMMA (FORALL G,v,k: tree?(G) AND size(G) = k+2 AND vert(G)(v) IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1) tree_edge_all: LEMMA tree?(G) AND vert(G)(v) IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1 del_tree_k: LEMMA ( FORALL G,v,k: tree?(G) and size(G) = k+1 AND vert(G)(v) AND deg(v,G)=1 IMPLIES tree?(del_vert(G,v))) IMPLIES (FORALL G,v: tree?(G) AND vert(G)(v) AND deg(v,G)=1 IMPLIES tree?(del_vert(G,v))) del_tree: LEMMA ( FORALL G,v,k: tree?(G) AND size(G) = k+1 AND vert(G)(v) AND deg(v,G)=1 IMPLIES tree?(del_vert(G,v))) del_tree_all: LEMMA tree?(G) AND vert(G)(v) AND deg(v,G)=1 IMPLIES tree?(del_vert(G,v)) END trees ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28