sep_sets[T: TYPE]: THEORY BEGIN IMPORTING digraphs[T], walks[T] G: VAR digraph[T] v,s,t: VAR T e: VAR edgetype[T] V: VAR finite_set[T] del_verts(G,V): digraph[T] = (# vert := difference[T](vert(G),V), edges := {e | edges(G)(e) AND (FORALL v: V(v) IMPLIES NOT in?(v,e))} #) 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 digraph_deg[T], finite_sets@finite_sets_card_eq adj_verts(G,s): finite_set[T] = {v: T | (EXISTS (e: edgetype[T]): incident_edges[T](s, G)(e) AND in?(v,e) 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