h_menger[T: TYPE]: THEORY BEGIN IMPORTING meng_scaff_prelude[T], graph_inductions[T], graph_ops[T], path_ops[T] G,MM: VAR graph[T] v,s,t,w1,w2,av,ajm,z,x: VAR T W: VAR finite_set[T] p,p1,p2: VAR prewalk e: VAR doubleton[T] path_not_thru: LEMMA separable?(G,s,t) AND sep_num(G,s,t) = 2 AND vert(G)(s) AND vert(G)(t) IMPLIES (FORALL (z: T): z /= s AND z /= t IMPLIES (EXISTS (pn: prewalk): path_from?(del_vert(G,z),pn,s,t))) 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: prewalk): path_from?(G,p1,s,t) AND path_from?(G,p2,s,t) AND independent?(p1,p2)) sep_num_del: LEMMA separable?(G,s,t) AND vert(G)(s) AND vert(G)(t) AND v /= t AND v /= s IMPLIES sep_num(del_vert(G, v), s, t) <= sep_num(G, s, t) separates_del: LEMMA separates(del_vert(G,ajm), singleton(z), s,t) AND vert(G)(ajm) AND vert(G)(s) AND vert(G)(t) AND ajm /= s AND ajm /= t IMPLIES separates(G, dbl(ajm,z), s,t) induction_step_comm: LEMMA induction_step(G,s,t) IMPLIES induction_step(G,t,s) separable?_del: LEMMA separable?(G,s,t) AND vert(G)(s) AND vert(G)(t) AND v /= s AND v /= t IMPLIES separable?(del_vert(G, v), s, t) AND vert(del_vert(G, v))(s) AND vert(del_vert(G, v))(t) seq_j: LEMMA (l(p) > 3 AND edge?(G)(seq(p)(l(p)-2),t) AND NOT edge?(G)(seq(p)(0),t)) IMPLIES (EXISTS (j: nat): j > 0 AND j < l(p) AND NOT edge?(G)(seq(p)(j - 1), t) AND edge?(G)(seq(p)(j), t)) short_path_case: LEMMA vert(G)(x) AND vert(G)(s) AND vert(G)(t) AND edge?(G)(s, x) AND edge?(G)(x, t) AND separable?(G, s, t) AND sep_num(G, s, t) = 2 IMPLIES (EXISTS (p1, p2: prewalk): path_from?(G, p1, s, t) AND path_from?(G, p2, s, t) AND independent?(p1, p2)) finale: LEMMA separable?(G,s,t) AND sep_num(G,s,t) = 2 AND vert(G)(s) AND vert(G)(t) AND induction_step(G,s,t) IMPLIES (EXISTS (p1,p2: prewalk): path_from?(G,p1,s,t) AND path_from?(G,p2,s,t) AND independent?(p1,p2)) h_menger: LEMMA separable?(G,s,t) AND sep_num(G,s,t) = 2 AND vert(G)(s) AND vert(G)(t) IMPLIES (EXISTS (p1,p2: prewalk): path_from?(G,p1,s,t) AND path_from?(G,p2,s,t) AND independent?(p1,p2)) hard_menger: LEMMA separable?(G,s,t) AND sep_num(G,s,t) = 2 AND vert(G)(s) AND vert(G)(t) IMPLIES (EXISTS (ips: set_of_paths(G,s,t)): card(ips) = 2 AND ind_path_set?(G,s,t,ips)) END h_menger