meng_scaff_prelude[T: TYPE]: THEORY BEGIN IMPORTING meng_scaff[T], sep_set_lems[T], meng_scaff_defs[T] G,MM: VAR graph[T] v,s,t,w1,w2: VAR T W: VAR finite_set[T] p,p1,p2: VAR prewalk i,j: VAR nat 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)) line20: LEMMA separable?(G,s,t) AND in?(G,s,t,w1,w2) AND sep_num(G,s,t) = 2 AND separates(G, dbl(w1, w2), s, t) AND disjoint?(s,t,w1,w2) AND MM = meng(G,s,t,w1,w2) AND induction_step(G,s,t) AND NOT (edge?(G)(w1,t) AND edge?(G)(w2,t)) IMPLIES (EXISTS (P1,P2: prewalk): path_from?(MM,P1,s,t) AND l(P1) > 2 AND path_from?(MM,P2,s,t) AND l(P2) > 2 AND seq(P1)(l(P1)-2) = w1 AND NOT verts_of(P1)(w2) AND seq(P2)(l(P2)-2) = w2 AND NOT verts_of(P2)(w1) AND independent?(P1,P2)) Long_walk_from(G,s,v): TYPE = {w: Walk_from(G,s,v) | l(w) > 1} join2(G,s,t,v,(p1: Long_walk_from(G,s,v)),(p2: Walk_from(G,t,v))): Walk_from(G,s,t) = p1^(0,l(p1)-2) o rev(p2) path_meng_t : LEMMA path_from?(G, p, s, t) AND l(p) > 0 IMPLIES (i < l(p) AND seq(p)(i) = t IMPLIES i = l(p) - 1) path_H_def : LEMMA path?(H(G,s,w1,w2),p) AND j < l(p) IMPLIES walk?(del_verts[T](G, dbl[T](w1, w2)), p^(0,j)) path_H_ind : LEMMA l(p1) > 1 AND l(p2) > 1 AND path?(H(G,s,w1,w2),trunc1(p1)) AND path?(H(G,t,w1,w2),trunc1(p2)) AND separates(G, dbl(w1, w2), s, t) AND seq(p1)(0) = s AND seq(p2)(0) = t IMPLIES independent?(p1,p2) path_comps_ind3: LEMMA l(p1) > 2 AND l(p2) > 2 AND path?(H(G,s,w1,w2),trunc1(trunc1(p1))) AND path?(H(G,t,w1,w2),trunc1(trunc1(p2))) AND separates(G, dbl(w1, w2), s, t) AND seq(p1)(0) = s AND seq(p2)(0) = t IMPLIES independent?(trunc1(p1),trunc1(p2)) path_H_trunc: LEMMA l(p) >= 2 AND path?(H(G, s, w1, w2), trunc1(p)) AND from?(p, s, w1) AND edge?(G)(p(l(p)-2),p(l(p)-1)) AND vert(G)(s) AND w1 /= s AND vert(G)(t) AND w2 /= s AND vert(G)(w1) AND vert(G)(w2) IMPLIES path_from?[T](G, p, s, w1) meng_last: LEMMA l(p) > 2 AND vert(G)(s) AND w1 /= s AND w1 /= t AND vert(G)(t) AND w2 /= s AND w2 /= t AND vert(G)(w1) AND vert(G)(w2) AND path_from?(meng(G, s, t, w1, w2), p, s, t) IMPLIES edge?(G)(seq(p)(l(p) - 3), seq(p)(l(p) - 2)) ind_verts_W: LEMMA path_from?(G,p1,s,t) AND path_from?(G,p2,t,s) AND l(p1) > 2 AND seq(p1)(l(p1) - 2) = w1 AND l(p2) > 2 AND seq(p2)(l(p2) - 2) = w2 AND independent?(p1,p2) AND w1 /= s AND w1 /= t AND w2 /= s AND w2 /= t IMPLIES NOT verts_of(p1)(w2) AND NOT verts_of(p2)(w1) ind_verts_w: LEMMA path_from?(G,p1,s,t) AND path_from?(G,p2,s,t) AND l(p1) > 2 AND seq(p1)(l(p1) - 2) = w1 AND l(p2) > 2 AND seq(p2)(l(p2) - 2) = w2 AND independent?(p1,p2) AND w1 /= s AND w1 /= t AND w2 /= s AND w2 /= t IMPLIES NOT verts_of(p1)(w2) AND NOT verts_of(p2)(w1) path_meng_in: LEMMA l(p) > 2 AND vert(G)(s) AND w1 /= s AND w1 /= t AND vert(G)(t) AND w2 /= s AND w2 /= t AND vert(G)(w1) AND vert(G)(w2) AND path?(meng(G, s, t, w1, w2), p) AND from?(p,s,t) AND ((seq(p)(l(p) - 2) = w1 AND NOT verts_of(p)(w2)) OR (seq(p)(l(p) - 2) = w2 AND NOT verts_of(p)(w1)) ) IMPLIES path?(H(G, s, w1, w2), trunc1(trunc1(p))) disjoint?(w1,w2: prewalk): bool = (FORALL (i,j: nat): i < l(w1) AND j < l(w2) IMPLIES seq(w1)(i) /= seq(w2)(j)) join2_lem: LEMMA path_from?(G,p1,s,v) AND path_from?(G,p2,t,v) AND s /= v AND t /= v AND s /= t AND disjoint?(trunc1(p1),trunc1(p2)) IMPLIES path_from?(G,join2(G,s,t,v,p1,p2),s,t) path_from_to_walk_from: LEMMA path_from?(G,p,s,t) IMPLIES walk_from?(G,p,s,t) paths_H_disj: LEMMA path?(H(G, t, w1, w2), p2) AND path?(H(G, s, w1, w2), p1) AND separates(G, dbl(w1, w2), s, t) AND seq(p1)(0) = s AND seq(p2)(0) = t AND s /= t IMPLIES disjoint?(p1,p2) prelude: LEMMA 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)) END meng_scaff_prelude