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