FDL > PVS > Graphs > subgraphs > subgraph : const-decl


subgraph(G, V): Subgraph(G) = G WITH [vert := {i | vert(G)(i) AND V(i)}, edges := {e | edges(G)(e) AND (FORALL (x:T) : e(x) IMPLIES V(x))}];