|
sep_sets[T: TYPE]: THEORY
BEGIN
IMPORTING graphs[T], walks[T]
G: VAR graph[T]
v,s,t: VAR T
e: VAR doubleton[T]
V: VAR finite_set[T]
del_verts(G,V): graph[T] =
(# vert := difference[T](vert(G),V),
edges := {e | edges(G)(e) AND
(FORALL v: V(v) IMPLIES NOT e(v))} #)
separates(G,V,s,t): bool = NOT V(s) AND NOT V(t) AND
NOT (EXISTS (w: prewalk): walk_from?(del_verts(G,V),w,s,t))
seps(G,s,t): TYPE = {V: finite_set[T] | IF s = t OR edge?(G)(s,t) THEN
V = vert(G)
ELSE separates(G,V,s,t)
ENDIF}
IMPORTING abstract_min
sep_set_exists: LEMMA (EXISTS (t: seps(G, s, t)): TRUE)
min_sep_set(G,s,t): finite_set[T] = min[seps(G,s,t),
(LAMBDA (v: seps(G,s,t)): card(v)),
(LAMBDA (v: seps(G,s,t)): true)]
separable?(G,s,t): bool = (s /= t AND NOT edge?(G)(s,t))
min_sep_set_edge: LEMMA NOT separable?(G,s,t) IMPLIES
min_sep_set(G,s,t) = vert(G)
min_sep_set_card: LEMMA FORALL (s,t: (vert(G))): separates(G,V,s,t)
IMPLIES card(min_sep_set(G,s,t)) <= card(V)
min_sep_set_seps: LEMMA separable?(G,s,t) IMPLIES
separates(G,min_sep_set(G,s,t),s,t)
min_sep_set_vert: LEMMA separable?(G,s,t) AND min_sep_set(G,s,t)(v)
IMPLIES vert(G)(v)
ends_not_in_min_sep_set: LEMMA separable?(G,s,t) AND min_sep_set(G, s, t)(v)
IMPLIES v /= s AND v /= t
w: VAR prewalk
walk?_del_verts_not : LEMMA walk?(G, w) AND
empty?(intersection(verts_of(w),V))
IMPLIES walk?(del_verts(G, V), w)
sep_num(G,s,t): nat = card(min_sep_set(G,s,t))
IMPORTING graph_deg[T], finite_sets@finite_sets_card_eq
adj_verts(G,s): finite_set[T] = {v: T | (EXISTS (e: Dbl[T]):
incident_edges[T](s, G)(e)
AND e(v) AND NOT v = s)}
adj_verts_lem: LEMMA card(adj_verts(G,s)) = deg(s,G)
sep_num_min: LEMMA FORALL (s,t: (vert(G))):
separable?(G,s,t) IMPLIES
sep_num(G,s,t) <= min(deg(s,G),deg(t,G))
END sep_sets
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
