LEMMA [Prelude] separates(G, dbl(w1, w2), s, t) AND
separable?(G,s,t) AND
sep_num(G,s,t) = 2 AND
induction_step(G,s,t) AND
in?(G,s,t,w1,w2) AND
disjoint?(s,t,w1,w2) AND
NOT (edge?(G)(w1,s) AND edge?(G)(w2,s)) AND
NOT (edge?(G)(w1,t) AND edge?(G)(w2,t))
IMPLIES
(EXISTS (p1,p2: prewalk): path_from?(G,p1,s,t) AND
path_from?(G,p2,s,t) AND
independent?(p1,p2))
where
induction_step(G,s,t): bool = FORALL (GG: graph[T]): size(GG) < size(G)
IMPLIES FORALL (s: T, t: T):
separable?(GG,s,t) AND
sep_num(GG, s, t) = 2 AND
vert(GG)(s) AND vert(GG)(t)
IMPLIES (EXISTS (p1,p2: prewalk):
path_from?(GG,p1,s,t) AND
path_from?(GG,p2,s,t) AND
independent?(p1,p2))
Proof: **** We assume that smaller graphs than G satisfy Menger's theorem
conclusion, that G needs exactly
2 vertices to separate s from t, and that
NOT (edge?(G)(w1,s) AND edge?(G)(w2,s))
AND NOT (edge?(G)(w1,t) AND edge?(G)(w2,t))
[1] induction_step ABOVE
[2] sep_num(G,s,t) = 2 (hypothesis)
[4] Let W = min_sep_set(G,s,t) (definition)
[5] card(W) = 2 (conclusion)
(proof: From [2] [4])
[6] {w1 , w2} = W (conclusion, definition)
from [5]
[7] L = del_verts(G,W) (definition)
[8] Hs = path_comp(L,s) (definition)
where
path_verts(G,(x:T)): set[T] =
{v: T | EXISTS (w: preseq): walk_from?(G,w,x,v)}
path_comp(G,(x:T)): Subgraph(G) = subgraph(G,path_verts(G,x))
[9] Ht = path_comp(L,t) (definition)
[10] subgraph?(Hs,G) conclusion
subgraph?(Ht,G)
[11] ***Construction of Ms ***
vert(Ms) = vert(Hs) union W union {t}
edges(Ms) = { {w1,t}, {w2,t} } union
edges(Hs) union
{ {z,w1} | edge?(G){z,w1} AND vert(Hs)(z) } union
{ {z,w2} | edge?(G){z,w2 AND vert(Hs)(z) } }
[12] *Construct Mt *
vert(Mt) = vert(Ht) union W union {s}
edges(Mt) = { {w1,s}, {w2,s} } union
edges(Ht) union
{ {z,w1} | edge?(G){z,w1} AND vert(Ht)(z) } union
{ {z,w2} | edge?(G){z,w2} AND vert(Ht)(z) }
[14] sep_num(Ms,s,t) = 2
Proof. By hypothesis we have:
separable?(G, s, t) AND
sep_num(G, s, t) = 2 AND
separates(G, dbl(w1, w2), s, t)
Since the only edges incident to t in Ms are
{w1,t} and {w2,t}, clearly {w1,w2} separates Ms.
Thus sep_num(Ms,s,t) <= 2. If sep_num(Ms,s,t) <= 1,
then exists z:
separates(Ms, {z}, s, t)
IF {z} separates s and t in G, then sep_num(G,s,t) <= 1
a contradiction, so let p be a walk from s to t in G
that does not encounter z.
case 1: exists i: seq(p)(i) = w1 OR seq(p)(i) = w2. Then
let ipf be the first vertex equal to w1 or w2
walk?(G,p^(0,ipf))
CASE a: NOT verts(p^(0,ipf))(t)
walk?(Hs,p^(0,ipf-1))
walk?(Ms,p^(0,ipf) o t)
and we have a walk from s to t in Ms
that does not encounter z. This
contradicts separates(Ms, {z}, s, t) above.
CASE b: verts(p^(0,ipf))(t)
let ii be the index < ipf s.t. p(ii) = t.
Then p^(0,ii) is a walk from s to t that
does not encounter w1 or w2. This contradicts
the hypothesis:
separates(G, dbl(w1, w2), s, t)
case 2: FORALL i: seq(p)(i) /= w1 AND seq(p)(i) /= w2.
Then we have a walk from s to t that does not
encounter w1 or w2. This contradicts the hypothesis:
separates(G, dbl(w1, w2), s, t)
[15] NOT (edge?(G,w1,t) AND edge?(G,w2,t)) (hypothesis)
[15.a] LEMMA Exist P in path_from(G,s,w1) ****see list of similar
lemmas at the end ****
Proof. Exist w: walk_from s -> t in G else sep_num(G,s,t) =0,
contradiction with [2]. By the walk to path theorem there
is a path from s -> t, call it P. Now if for all
such P: s -> t, we have that w2 is in P, THEN
separates(G,{w2},s,t) so sep_num(G,s,t) =1, which contradicts [2].
But for all P: s -> t, P meets w1 OR w2, since W = {w1,w2} is a
separating set in G for s,t. Hence there exists P in
path_from(G,s,t) which meets w1, since we showed that not all
of them meet w1.
[15.b] Lemma Exist P in path_from(G,s,w2)
[15.c] Lemma Exist P in path_from(G,t,w1)
[15.d] Lemma Exist P in path_from(G,t,w2)
Proofs identical up to changing names of w1,w2,s,t .
[16] Exists y in vert(Ht), y /= t .
Proof. By lemmas [15.cd] there are paths Rw1 and Rw2 from t to w1 and
to w2 respectively. By [15] there is q = w1 OR w2 such that
NOT edge?(G,q,t). Hence Rq is not a single edge.
The possibility that
Rw1: t ... -> w2 -> w1
Rw2: t ... -> w1 -> w2
is ruled out by another lemma (prep_16):
separates(G, dbl(w1, w2), s, t) AND
disjoint?(s, t, w1, w2) AND
(FORALL p: path_from?(G,p,t,w1) IMPLIES verts(p)(w2))
AND vert(G)(s) AND vert(G)(t)
IMPLIES sep_num(G,s,t) <= 1
Then we have the existence of a path RR from t to w1 that does not
go through w2 and there is y such that R(0)=t R(1)=y /=q .
Clearly y is in the connected path component of t,that is, Ht.
[17] size(Ms) < size (G)
Proof. Every vertex of Ms is a vertex of G. But y in G is not in Ms,
since it is not in Hs and is not =t. NOTE: vert(Hs) and vert(Ht)
are disjoint: Proof: assume contrary: vert(Hs)(z) and vert(Ht)(z).
then there exists psz,ptz: walk_from?(G,psz,s,z) AND
walk_from?(G,psz,t,z)
Thus trunc1(psz) o rev(ptz) is a walk from s to t that does
not go through w1 or w2 contradicting the fact that {w1,w2}
separates s and t.
[18] Exist ips: set[Path_from(Ms,s,t)], card(ips)=2
AND ind_path-set?(Ms,s,t,ips)
Proof. [17] [17b] and [1], the induction hypothesis.
[19] Exist Pw1 and Pw2 in Path_from(Ms,s,t), with w1 in Pw1 and w2 in Pw2.
Proof. The only edges incident to t in Ms are (t,w1) and (t,w2) Thus each
path s -> t must contain either w1 or w2. There are two independent
paths s->t by [18]; they cannot both contain w1 and cannot both
contain w2. Choose the one that goes through w1 and call it Pw1;
choose the one of the two that goes through w2 and call it Pw2.
[20] Pw1 and Pw2 are in Path_from(Ms,s,t) and are independent
containing w1 and w2 respectively (but not containing the other).
Proof. Restatement of [19].
[21] There are Qw1 and Qw2 in Path_from(Mt,t,s) containing w1 and w2
respectively (but not containing the other).
Proof. Take the above proof of [20] starting with [13] and repeat it,
exchanging s and t throughout (even on the subscripts like
Mt and Hs) .
[22] Exist Rw1 and Rw2 in path_from(G,s,t) which are distinct and independent.
Proof. trunc1(Pw1) is a path from s to w1 and trunc1(trunc1(Pw1)) is in Hs.
trunc1(Qw1) is a path from t to w1 and trunc1(trunc1(Qw1)) is in Ht.
Pw1 cannot go thru w2 before reaching w1 (thus making
it not in Hs) is ruled out by the fact that Pw1 and
Pw2 are independent and Pw2 goes thru w2. Similarly Qw1 cannot
go thru w1 before reaching w2.
Hs and Ht are subgraphs of G by [10], hence Pw1 o rev(Qw1) is a
Path_from(G,s,t) and similarly Pw2 o rev(Qw2) is one too. Call
these two paths Rw1 and Rw2 respectively. They are independent
since they do not intersect in Hs, do not intersect in Ht and do
not intersect at w1 or w2.
[23] Q.E.D (We have constructed two independent paths!)
===============================================================================
Adjacent_fact: LEMMA separates(G, dbl(w1, w2), s, t) AND
separable?(G,s,t) AND
sep_num(G,s,t) = 2 AND
in?(G,s,t,w1,w2) AND
disjoint?(s,t,w1,w2) AND
edge?(G)(w1,s) AND
edge?(G)(w2,s) AND
(edge?(G)(w1,s) AND edge?(G)(w1,t))
IMPLIES
(EXISTS (p1,p2: preseq): path_from?(G,p1,s,t) AND
path_from?(G,p2,s,t) AND
independent?(p1,p2))
Proof: (FORALL z: (EXISTS pn: path_from?(del_vert(G,z),pn,s,t)))
Thus EXISTS pn: path_from?(del_vert(G,w1),pn,s,t)))
Let path2 = s -> w1 -> t
independent?(pn,path2)
Q.E.D
===============================================================================
finale: LEMMA separable?(G,s,t) AND sep_num(G,s,t) = 2 AND
vert(G)(s) AND vert(G)(t) AND
IMPLIES
(EXISTS (p1,p2: preseq): path_from?(G,p1,s,t) AND
path_from?(G,p2,s,t) AND
independent?(p1,p2))
Proof: Let p: s -> a1 -> a2 ... an -> t
IF l(p) <= 3 THEN
p: s -> t ruled out by separable?
p: s -> aj -> t, Then aj must be in any separating
set and Adjacent_fact takes care of it.
EXISTS aj: edge?(aj,t) AND NOT edge?(aj-1,t)
Case I: NOT edge?(aj-1,s)
CASE A "(FORALL (v:T): vert(G)(v) AND v /= s AND v /= t
IMPLIES sep_num(del_vert(G,v),s,t) <= 1)")
EXISTS z: separates(del_vert(G,aj-1),{z},s,t)
Thus: separates(G,{aj-1,z},s,t)
By prelude we are done
CASE NOT A
del_vert(G,v) is smaller than G so by induction, we have two
independent paths in del_vert(G,v) and hence in G. DONE.
Case II: edge?(aj-1,s)
CASE A: separates(G,{aj-1,aj},s,t)
Case i: edge?(aj,s)
by Adjacent_fact done
Case ii: NOT edge?(aj,s)
by prelude done
CASE NOT A:
EXISTS p2: path_from?(del_verts(G,{aj-1,aj}),s,t)
NAME Pscat = s -> aj-1 -> aj -> t
independent?(p2,Pscat)
DONE
QED