|
di_subgraphs_from_walk[T: TYPE]: THEORY
BEGIN
IMPORTING digraphs[T], walks[T], di_subgraphs[T]
G,GG: VAR digraph[T]
t,t1,t2,v: VAR T
i: VAR nat
e: VAR edgetype[T]
G_from(G, (w: Walk(G))): di_subgraph(G) = (# vert := verts_of(w),
edges := edges_of(w) #)
G_from_vert : LEMMA FORALL (w: Walk(G)): vert(G_from(G,w)) = verts_of(w)
vert_G_from : LEMMA FORALL (w: Walk(G), i: below(length(w))):
vert(G_from(G, w))(w(i))
edge?_G_from : LEMMA FORALL (w: Walk(G), i: below(length(w)-1)):
edge?(G_from(G, w))(w(i), w(i+1))
%%%%%%%%%%%%%%%%%%%%%%%%%% not true for directed graphs %%%%%%%%%%%%%%%%%%%%
%
% edge?_G_from_rev: LEMMA FORALL (w: Walk(G), i: below(length(w)-1)):
% edge?(G_from(G, w))(w(i+1), w(i))
vert_G_from_not : LEMMA FORALL (w: Walk(G)):
subset?(vert(G_from(G, w)), vert(GG)) AND
NOT verts_of(w)(v)
IMPLIES
subset?(vert(G_from(G, w)), remove[T](v, vert(GG)))
IMPORTING digraph_ops[T]
del_vert_di_subgraph: LEMMA FORALL (w: Walk(G), v: (vert(GG))):
di_subgraph?(G_from(G, w), GG) AND
NOT verts_of(w)(v) IMPLIES
di_subgraph?(G_from(G, w), del_vert(GG, v))
END di_subgraphs_from_walk
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
