| products/sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: trees.pvs Sprache: PVSOriginal von: 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.16 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
