|
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
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
