| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Bernstein/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 44 kB |
|
Quellcode-Bibliothek di_subgraphs.pvs Sprache: PVS |
|||||||||
|
di_subgraphs[T: TYPE]: THEORY
BEGIN IMPORTING digraphs[T] V: VAR set[T] G,G1,G2,SS: VAR digraph[T] i: VAR T e: VAR edgetype[T] di_subgraph?(G1,G2): bool = subset?(vert(G1),vert(G2)) AND subset?(edges(G1),edges(G2)) equal?(G1,G2): bool = di_subgraph?(G1,G2) AND di_subgraph?(G2,G1) di_subgraph(G): TYPE = {S: digraph[T] | di_subgraph?(S,G)} finite_vert_subset: LEMMA is_finite(LAMBDA (i:T): vert(G)(i) AND V(i)) finite_edge_subset: LEMMA is_finite[edgetype[T]] ({e | G`edges(e) AND (LET (x, y) = e IN V(x) AND V(y))}) % di_subgraph(G, V): di_subgraph(G) = % (G WITH [vert := {i | vert(G)(i) AND V(i)}, % edges := {e | edges(G)(e) AND % (FORALL (x: T): in?(x,e) IMPLIES V(x))}]) x,y: VAR T di_subgraph(G, V): di_subgraph(G) = (G WITH [vert := {i | vert(G)(i) AND V(i)}, edges := {e | edges(G)(e) AND (Let (x,y) = e IN V(x) AND V(y))}]) di_subgraph_vert_sub: LEMMA subset?(V,vert(G)) IMPLIES vert(di_subgraph(G,V)) = V di_subgraph_lem : LEMMA di_subgraph?(di_subgraph(G,V),G) di_subgraph_smaller: LEMMA di_subgraph?(SS, G) IMPLIES size(SS) <= size(G) END di_subgraphs ¤ 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.12Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
