Quelle k_menger.pvs Sprache: PVS

k_menger[T: TYPE]: THEORY
BEGIN
   %% IMPORTING h_menger[T],

   %% IMPORTING meng_scaff_prelude[T],
      IMPORTING ind_paths[T]

   IMPORTING graph_inductions[T], graph_ops[T], path_ops[T]
   IMPORTING finite_sets@finite_sets_inductions[T]

   G,GG,H,HH,MM: VAR graph[T]
   v,s,t,w,w1,w2,a,b,c,av,ajm,z,x: VAR T
   W,W1,W2: VAR finite_set[T]
   p,p1,p2,q,q1,q2: VAR prewalk
   e: VAR doubleton[T]
   U,U1,V,V1,V2: VAR finite_set[T]
   k,i,j,m,n: VAR nat


   good?(G,s,t):bool = separable?(G,s,t) AND vert(G)(s) AND vert(G)(t)

   green?(V,s,t):bool = NOT V(s) AND NOT V(t)

   B(G,s,t,k): bool = good?(G,s,t) AND (FORALL V: separates(G,V,s,t) IMPLIES card(V)>=k)

   set_of_prewalks: TYPE = finite_set[prewalk]

   ips,ipt,ips1,ips2,ipss,ipst,ipsg: VAR set_of_prewalks

   ind_prewalk_set?(ips): bool =
                   (FORALL (p1,p2):
                             ips(p1) AND ips(p2) AND  p1 /= p2
                                         IMPLIES independent?(p1,p2))
   st_path_set?(G,s,t,ips): bool = (FORALL p1 : ips(p1) IMPLIES path_from?(G,p1,s,t))

   many_ind(G,s,t,j):bool = EXISTS (ips): ind_prewalk_set?(ips)
                                          AND st_path_set?(G,s,t,ips)
                                          AND card[prewalk](ips)=j

   B_many(G,s,t,k): bool = B(G,s,t,k) IMPLIES many_ind(G,s,t,k)

%  Relation to sep_num is mentioned for comparison; minimal separating set or
%  separating number will not be used in the sequel.

   sep_num_B:       LEMMA  B(G,s,t,k) IMPLIES sep_num(G,s,t)>=k

   sep_num_implies: LEMMA  good?(G,s,t) AND sep_num(G,s,t)=k IMPLIES B(G,s,t,k)

% We do not perform a new proof of easy_menger but simply recast it in our
% notation.

  % We use some basic results on card from extension that are originally found
  % in finite_sets module.

  IMPORTING finite_sets_card_from

  card_extension_W   : LEMMA subset?(V,W) IMPLIES
                             card(extend[T,(W),bool,false](V))=card(V)

  card_extension_same: LEMMA card(extend[T,(W),bool,false](W))=card(W)

  % This last result will be used in comparing card for prewalk sets AND vertex
  % sets.

   %% IMPORTING menger

   IMPORTING easy_menger[T], subgraph_paths[T] %% , meng_scaff_defs[T]
   IMPORTING complem

   easy_menger_B: LEMMA good?(G,s,t) AND many_ind(G,s,t,k) IMPLIES B(G,s,t,k)

% No min_sep_set after this point.  Also specifications from "menger.pvs"
% will no longer be used. Lemma "easy_menger" was the basis of "easy_menger_B"
% above.

   C(G,s,t):bool = (FORALL k: B_many(G,s,t,k))

   sep_set_small: LEMMA B(G,s,t,k) AND green?(V,s,t) AND card(V) < k
                        IMPLIES EXISTS p : path_from?(del_verts(G,V),p,s,t)

   B_many_1     : LEMMA B_many(G,s,t,1)

% Here you prove all special cases.

  tight?(G,s,t,W): bool = subset?(W, intersection(path_verts(G,s),path_verts(G,t)))

  sub_tight     : LEMMA subset?(V,W) AND tight?(G,s,t,W) IMPLIES tight?(G,s,t,V)

  smaller_tight : LEMMA separates(G,W,s,t)
                        IMPLIES tight?(G,s,t,W)
                           OR EXISTS V :subset?(V,W) AND NOT V=W AND separates(G,V,s,t)

  small_tight   : LEMMA separates(G,W,s,t) IMPLIES
                        EXISTS V :subset?(V,W) AND separates(G,V,s,t) AND tight?(G,s,t,V)

  exists_tight  : LEMMA good?(G,s,t) IMPLIES
                                   EXISTS V: separates(G,V,s,t) AND tight?(G,s,t,V)

  close?(G,s,t,W): bool = FORALL (w:T) :  W(w)
                          IMPLIES EXISTS p: path_from?(G,p,s,t)
                                    AND intersection(W,internal_verts(p))=singleton[T](w)

  close_tight   : LEMMA close?(G,s,t,W) IMPLIES tight?(G,s,t,W)

  smaller_close : LEMMA separates(G,W,s,t) AND tight?(G,s,t,W) IMPLIES
                       close?(G,s,t,W) OR EXISTS V :subset?(V,W) AND
                              NOT V=W AND separates(G,V,s,t) AND tight?(G,s,t,V)

  small_close   : LEMMA separates(G,W,s,t) IMPLIES
                        EXISTS V :subset?(V,W) AND separates(G,V,s,t) AND close?(G,s,t,V)

  exists_close: LEMMA good?(G,s,t)
                        IMPLIES EXISTS V: separates(G,V,s,t) AND close?(G,s,t,V)

  closed_minimal: LEMMA separates(G,W,s,t) AND close?(G,s,t,W)
                        AND subset?(V,W) AND separates(G,V,s,t) IMPLIES V=W

  closed_verts: LEMMA close?(G,s,t,W) IMPLIES subset?(W,vert(G))

  attached?(G,s,t,W): bool = (FORALL w: W(w) IMPLIES edge?(G)(s,w)) OR
                             (FORALL w: W(w) IMPLIES edge?(G)(t,w))

  attach_edges(W,x): finite_set[doubleton[T]]
                         = {e :doubleton[T]|EXISTS w: W(w) AND e=dbl[T](w,x)}

  %%%%%%%  Definition of special graphs.

  Hverts(G,W,x): finite_set[T] = path_verts(del_verts(G,W),x)

  Kgraph(G,W,x): graph = subgraph(G, difference[T](vert(G),Hverts(G,W,x)))

  Mgraph(G,W,x):graph = (# vert :=  add(x,vert(Kgraph(G,W,x))),
                           edges := union(edges(Kgraph(G,W,x)),
                                          attach_edges(intersection(vert(G),W),x))
                         #)

  %%%%%%%   End of definitions.

  Hst_intersect: LEMMA separates(G,W,s,t)
                       IMPLIES empty?(intersection(Hverts(G,W,s),Hverts(G,W,t)))

  subset_Ws: LEMMA good?(G,s,t) AND separates(G,W,s,t) AND NOT attached?(G,s,t,W)
                   IMPLIES subset?(vert(Mgraph(G,W,s)),vert(G))

  subset_Wt: LEMMA good?(G,s,t) AND separates(G,W,s,t) AND NOT attached?(G,s,t,W)
                   IMPLIES subset?(vert(Mgraph(G,W,t)),vert(G))

  size_Ws: LEMMA good?(G,s,t) AND separates(G,W,s,t)
                 AND close?(G,s,t,W) AND NOT attached?(G,s,t,W)
                 IMPLIES size(Mgraph(G,W,s)) < size(G)

  size_Wt: LEMMA good?(G,s,t) AND separates(G,W,s,t)
                 AND close?(G,s,t,W) AND NOT attached?(G,s,t,W)
                 IMPLIES size(Mgraph(G,W,t)) < size(G)

  C_induct(G,s,t):bool = (FORALL GG: size(GG)<size(G) IMPLIES C(GG,s,t))
                              IMPLIES C(G,s,t)

  Menger_hard: LEMMA (FORALL G:C_induct(G,s,t)) IMPLIES
                           (FORALL G: C(G,s,t))          %Proved from graph inductions.

   % We include some elementary lemmas on paths.  Some were proved
   % earlier in meng_scaff_defs.pvs, and the "greatest" and "least"
   % constructions would follow from meng_scaff.pvs. We give a formulation
   % specific to subsets of vertices in a graph.

  subgraph_walks: LEMMA subgraph?(GG,G) AND walk?(GG,p1) IMPLIES walk?(G,p1)

  subgraph_paths: LEMMA subgraph?(GG,G) AND path_from?(GG,p1,s,t)
                        IMPLIES path_from?(G,p1,s,t)

  greatest?(p,V,i): bool = i<length(p) AND V(seq(p)(i)) AND
                    FORALL j:(j<length(p) AND V(seq(p)(j)) IMPLIES j<=i)

  least?(p,V,i): bool = i<length(p) AND V(seq(p)(i)) AND FORALL j:(j<length(p) AND V(seq(p)(j))
                        IMPLIES j>=i)

  greatest_is: LEMMA i<length(p) AND V(seq(p)(i)) IMPLIES EXISTS k: greatest?(p,V,k)

  least_is: LEMMA i<length(p) AND V(seq(p)(i)) IMPLIES EXISTS k: least?(p,V,k)

  set_small_s: LEMMA B(G,s,t,k) AND good?(G,s,t)
                     AND separates(G,W,s,t) AND green?(V,s,t) AND card(V) < k
                     IMPLIES EXISTS p : path_from?(del_verts(Mgraph(G,W,s),V),p,s,t)

  set_small_t: LEMMA B(G,s,t,k) AND good?(G,s,t) AND separates(G,W,s,t)
                     AND green?(V,s,t) AND card(V) < k
                     IMPLIES EXISTS p : path_from?(del_verts(Mgraph(G,W,t),V),p,s,t)

  separates_Ws: LEMMA B(G,s,t,k) AND separates(G,W,s,t) IMPLIES B(Mgraph(G,W,s),s,t,k)

  separates_Wt: LEMMA B(G,s,t,k) AND separates(G,W,s,t) IMPLIES B(Mgraph(G,W,t),s,t,k)

  separ_sub: LEMMA subgraph?(GG,G) AND separates(G,V,s,t)
                   IMPLIES separates(GG,V,s,t)

  separ_plus: LEMMA separates(del_vert(G,a),V,s,t)
                    IMPLIES separates(G,add(a,V),s,t) or a=s or a=t

  % A main lemma based on graph induction is used only in the version of k_Menger
  % Theorem below called 'Many_indep_paths'.

  super_separ: LEMMA good?(G,s,t) AND subset?(V,W)
                     AND green?(W,s,t) AND separates(G,V,s,t)
                     IMPLIES separates(G,W,s,t)

  % Requires a graph induction.

  intermediate_subgraph: LEMMA (good?(G,s,t) AND subgraph?(H,G) AND green?(vert(H),s,t)
                                AND size(H)<=k AND k< size(G)-1)
                          IMPLIES (EXISTS HH: (green?(vert(HH),s,t) AND
                                               subgraph?(H,HH) AND size(HH)=k AND
                                               subgraph?(HH,G)))

  intermediate_verts: LEMMA good?(G,s,t) AND green?(V,s,t)
                            AND subset?(V,vert(G)) AND card(V)<=k AND k<size(G)-1
                        IMPLIES (EXISTS W: subset?(V,W) AND card(W)=k AND
                                           green?(W,s,t) AND subset?(W,vert(G)))

  % The section necessary for 'Many_indep_paths' is closed.

  one_wedge_s: LEMMA good?(G,s,t)
                     AND path_from?(G,q,s,t) IMPLIES
                             EXISTS k: k<length(q)-1 AND edge?(G)(s,seq(q)(k))
                     AND (FORALL j: j < length(q) AND edge?(G)(s, seq(q)(j)) IMPLIES j <= k)
                     AND path_from?(G,gen_seq1(G,s) o q^(k,length(q)-1),s,t)

  one_edge_s: LEMMA good?(G,s,t)
                    AND path_from?(G,q,s,t) IMPLIES EXISTS p:path_from?(G,p,s,t)
                    AND FORALL (i: below(length(p))):( edge?(G)(s,seq(p)(i)) IMPLIES i=1)
                    AND subset?(verts_of(p),verts_of(q))

  % Auxiliary LEMMA  one_edge_t: LEMMA good?(G,s,t) AND path_from?(G,q,s,t)
  %                  IMPLIES EXISTS p:path_from?(G,p,s,t)
  %                      AND FORALL (i: below(length(p))):( edge?(G)(seq(p)(i),t)
  %                      IMPLIES i=length(p)-2) AND subset?(verts_of(p),verts_of(q))

  IMPORTING sep_set_lems[T]

  short_path_k: LEMMA k>=1 AND B(G,s,t,k) IMPLIES EXISTS p:path_from?(G,p,s,t) AND
                       FORALL (i: below(length(p))): ((edge?(G)(s,seq(p)(i))
                              IMPLIES i=1) AND (edge?(G)(seq(p)(i),t) IMPLIES i=length(p)-2))

  indep_path_sub: LEMMA subgraph?(GG,G)AND many_ind(GG,s,t,j) IMPLIES many_ind(G,s,t,j)

  second: VAR [prewalk -> T]

  %  [{p:prewalk | length(p)>1} -> T]

  ips_lem1: LEMMA (FORALL q,q1:(ips(q) IMPLIES V(second(q))) AND (ips(q) AND ips(q1)
                          AND q /= q1 IMPLIES second(q) /= second(q1)))
               IMPLIES subset?(image(second,ips),V) AND
                       injective?(restrict[prewalk,(ips),T](second))

  ips_lem2: LEMMA (FORALL q,q1:(ips(q) IMPLIES V(second(q))) AND (ips(q)
                          AND ips(q1) AND q /= q1 IMPLIES second(q) /= second(q1)))
                   AND card[prewalk](ips)=card[T](V)
               IMPLIES image(second,ips)=V

  secoo(p:prewalk | length(p)>1): T = p(1)

  secpp(p:prewalk|length(p)>1): T = p(length(p)-2)

   inj_ips: LEMMA (FORALL (q,q1):(ips(q) IMPLIES V(second(q)))
                                  AND (ips(q) AND ips(q1) AND q /= q1 IMPLIES
                                      second(q) /= second(q1)))
                  AND card[prewalk](ips)=card[T](V)
               IMPLIES EXISTS (fq:[(V) -> prewalk]): image(fq,V)=ips AND
                       (FORALL (v:(V)): second(fq(v))=v) AND
                       (FORALL q2:ips(q2) IMPLIES fq(second(q2))=q2)

  long_ipss_paths: LEMMA good?(G,s,t) AND st_path_set?(Mgraph(G,W,s),s,t,ipss)
                         AND ipss(p) IMPLIES length(p)>1

  ipss_W: LEMMA good?(G,s,t) AND st_path_set?(Mgraph(G,W,s),s,t,ipss)
                AND separates(G,W,s,t) AND ipss(p) IMPLIES W(secoo(p))

  long_ipst_paths: LEMMA good?(G,s,t) AND st_path_set?(Mgraph(G,W,t),s,t,ipss)
                         AND ipss(p) IMPLIES length(p)>1

  ipst_W: LEMMA good?(G,s,t) AND st_path_set?(Mgraph(G,W,t),s,t,ipss)
                AND separates(G,W,s,t) AND ipss(p) IMPLIES W(secpp(p))

  long_ipss_2: LEMMA good?(G,s,t) AND st_path_set?(Mgraph(G,W,s),s,t,ipss)
                     AND ipss(p) AND separates(G,W,s,t) IMPLIES length(p)>2

  long_ipst_2: LEMMA good?(G,s,t) AND st_path_set?(Mgraph(G,W,t),s,t,ipss)
                     AND ipss(p) AND separates(G,W,s,t) IMPLIES length(p)>2

  ind_path_set_secoo: LEMMA good?(G,s,t) AND card[T](W)= card[prewalk](ipss)
                            AND separates(G,W,s,t) AND ind_prewalk_set?(ipss)
                            AND st_path_set?(Mgraph(G,W,s),s,t,ipss)
                        IMPLIES image(secoo, ipss)=W AND
                               FORALL (q,q1):(ipss(q) AND ipss(q1) AND q /=q1
                                              IMPLIES secoo(q) /= secoo(q1))

  ind_path_set_secpp: LEMMA good?(G,s,t) AND card[T](W)= card[prewalk](ipst)
                            AND separates(G,W,s,t) AND ind_prewalk_set?(ipst)
                            AND st_path_set?(Mgraph(G,W,t),s,t,ipst)
                        IMPLIES image(secpp, ipst)=W
                                AND FORALL (q,q1):(ipst(q) AND ipst(q1) AND q /=q1
                                                  IMPLIES secpp(q) /= secpp(q1))

  uniq_w_ipss:   LEMMA good?(G,s,t) AND card[T](W)= card[prewalk](ipss)
                       AND ind_prewalk_set?(ipss)
                       AND st_path_set?(Mgraph(G,W,s),s,t,ipss) AND separates(G,W,s,t)
                       AND ipss(p) AND verts_of(p)(w) AND W(w)
                    IMPLIES w=secoo(p)

  uniq_w_ipst:   LEMMA good?(G,s,t) AND card[T](W)= card[prewalk](ipst)
                       AND ind_prewalk_set?(ipst)
                       AND st_path_set?(Mgraph(G,W,t),s,t,ipst) AND separates(G,W,s,t)
                       AND ipst(q) AND verts_of(q)(w) AND W(w)
                   IMPLIES w=secpp(q)

% Instead of calling on minimal separating set, we show by induction that such a set EXISTS.

  low_card_sep: LEMMA B(G,s,t,k) IMPLIES EXISTS W: separates(G,W,s,t)
                         AND card(W)>=k AND FORALL V: (separates(G,V,s,t)
                     IMPLIES card(V)>= card(W))

  smaller_ips : LEMMA j<=card[prewalk](ips)
                      IMPLIES EXISTS ips1: subset?(ips1,ips) AND card[prewalk](ips1)=j

  few_many    : LEMMA i>=j AND many_ind(G,s,t,i)
                      IMPLIES many_ind(G,s,t,j)

  min_B       : LEMMA B(G,s,t,k) IMPLIES
                        EXISTS (i,W): i>=k AND B(G,s,t,i) AND
                                      separates(G,W,s,t) AND card(W)=i

  no_sep_req  : LEMMA (FORALL k,W: B(G,s,t,k) AND separates(G,W,s,t)
                       AND card(W)=k IMPLIES many_ind(G,s,t,k))
                     IMPLIES (FORALL k: B(G,s,t,k) IMPLIES many_ind(G,s,t,k))

  k_sep_close : LEMMA FORALL k,W: B(G,s,t,k) AND separates(G,W,s,t)
                      AND card(W)=k IMPLIES close?(G,s,t,W)

  p_Ht        : LEMMA good?(G,s,t) AND separates(G,W,s,t)
                      AND path_from?(Mgraph(G,W,s),p,s,t) AND length(p)>2
                      AND (FORALL w: W(w) AND verts_of(p)(w) IMPLIES w=secoo(p))
                   IMPLIES subset?(verts_of(p^(2,length(p)-1)),Hverts(G,W,t))

  q_Hs        : LEMMA good?(G,s,t) AND separates(G,W,s,t)
                      AND path_from?(Mgraph(G,W,t),q,s,t) AND length(q)>2
                      AND (FORALL w: W(w) AND verts_of(q)(w) IMPLIES w=secpp(q))
                   IMPLIES subset?(verts_of(q^(0,length(q)-3)),Hverts(G,W,s))

  disjoint_M_paths: LEMMA good?(G,s,t) AND close?(G,s,t,W) AND separates(G,W,s,t)
                          AND card[T](W)= card[prewalk](ipss)
                          AND card[T](W)= card[prewalk](ipst)
                          AND st_path_set?(Mgraph(G,W,s),s,t,ipss)
                          AND st_path_set?(Mgraph(G,W,t),s,t,ipst)
                          AND ind_prewalk_set?(ipss) AND ind_prewalk_set?(ipst)
                          AND ipss(p) AND ipst(q)
                    IMPLIES (secoo(p)=secpp(q) AND
                             intersection(verts_of(p^(1,length(p)-1)),verts_of(q^(0,length(q)-2)))
                                =singleton[T](secoo(p)) AND
                             W(secoo(p)))
                        OR (secoo(p) /= secpp(q) AND
                            empty?(intersection(verts_of(p^(1,length(p)-1)),
                                                verts_of(q^(0,length(q)-2)))))

  % The first two hypotheses of sec_image are mainly to assure a non-empty type for
  % Thence for prewalk. We could have used the lemmas of prelude function_image and
  % function_inverse_def but a brute force approach is serviceable.  Note however
  % that producing an inverse for 'second' mapping involves the possibility of
  % (ipss) that is an empty set of prewalks.  Some of the work in sec_image
  % is to recall how a function defined from an empty set to an empty set
  % has an inverse.

   sec_image: LEMMA good?(G,s,t) AND separates(G,W,s,t) AND image(second, ipss)=W
                    AND injective?(LAMBDA (s: (ipss)): second(s))
                          IMPLIES
                EXISTS (tau:[(W) -> prewalk]): image(tau,W)=ipss
                                             AND FORALL w:(W(w)
                                                    IMPLIES second(tau(w))=w)

   Map_s    : LEMMA good?(G,s,t) AND separates(G,W,s,t)
                    AND card[T](W)= card[prewalk](ipss) AND ind_prewalk_set?(ipss)
                    AND st_path_set?(Mgraph(G,W,s),s,t,ipss)
               IMPLIES EXISTS (tau:[(W) -> prewalk]): image(tau,W)=ipss
                          AND FORALL w: (W(w) IMPLIES secoo(tau(w))=w)

   Map_t    : LEMMA good?(G,s,t) AND separates(G,W,s,t)
                    AND card[T](W)= card[prewalk](ipst) AND ind_prewalk_set?(ipst)
                    AND st_path_set?(Mgraph(G,W,t),s,t,ipst)
             IMPLIES EXISTS (tau:[(W) -> prewalk]): image(tau,W)=ipst
                          AND FORALL w: (W(w) IMPLIES secpp(tau(w))=w)

% The following took twenty days to complete.

   Mapper_ips:  LEMMA good?(G,s,t) AND close?(G,s,t,W) AND separates(G,W,s,t)
                      AND card[T](W)= card[prewalk](ipss)
                      AND card[T](W)= card[prewalk](ipst)
                      AND st_path_set?(Mgraph(G,W,s),s,t,ipss)
                      AND st_path_set?(Mgraph(G,W,t),s,t,ipst)
                      AND ind_prewalk_set?(ipss) AND ind_prewalk_set?(ipst)
                IMPLIES EXISTS (phi:[(W) -> prewalk]):
                             card[prewalk](image(phi,W))=card[T](W) AND
                             st_path_set?(G,s,t,image(phi,W)) AND
                             ind_prewalk_set?(image(phi,W))

   non_attached_induct: LEMMA good?(G,s,t) AND separates(G,W,s,t) AND B(G,s,t,k)
                              AND card[T](W)=k
                              AND (FORALL GG: size(GG)<size(G) IMPLIES C(GG,s,t))
                            IMPLIES many_ind(G,s,t,k) or attached?(G,s,t,W)

   plus_sep_vert : LEMMA good?(G,s,t) AND separates(del_vert(G,a),W,s,t)
                         IMPLIES separates(G,add(a,W),s,t) or a=s or a=t

   separ_del_vert: LEMMA separates(G,W,s,t)
                         IMPLIES separates(G,remove(x,W),s,t) OR vert(G)(x)

   plus_path_set : LEMMA good?(G,s,t) AND path_from?(G,q,s,t)
                         AND st_path_set?(del_verts(G,verts_of(q^(1,length(q)-2))),s,t,ips)
                         AND ind_prewalk_set?(ips)
                   IMPLIES EXISTS ipss: card[prewalk](ipss)= card[prewalk](ips)+1 AND
                                        st_path_set?(G,s,t,ipss) AND
                                        ind_prewalk_set?(ipss)

   short_path_attach: LEMMA B(G,s,t,k) AND separates(G,W,s,t) AND card[T](W)=k
                            AND (FORALL V: separates(G,V,s,t)
                            AND card[T](V)=k  IMPLIES attached?(G,s,t,V))
                            AND (FORALL GG: size(GG)<size(G) IMPLIES C(GG,s,t))
                   IMPLIES many_ind(G,s,t,k)
                           OR EXISTS a: edge?(G)(s,a) AND (edge?(G)(a,t)
                           OR EXISTS c: edge?(G)(a,c) AND edge?(G)(c,t))

   bridge_one  : LEMMA edge?(G)(s,a) AND edge?(G)(a,t)
                       AND (FORALL GG: size(GG)<size(G) IMPLIES C(GG,s,t))
                   IMPLIES B_many(G,s,t,k)

   bridge_two  : LEMMA k>=1 AND edge?(G)(s,a) AND edge?(G)(a,c) AND edge?(G)(c,t)
                       AND  B(del_verts(G,dbl[T](a,c)),s,t,k-1)
                       AND (FORALL GG: size(GG)<size(G) IMPLIES C(GG,s,t))
                   IMPLIES B_many(G,s,t,k)

   bridge_three: LEMMA  k>=1 AND edge?(G)(s,a) AND edge?(G)(a,c) AND edge?(G)(c,t)
                        AND B(G,s,t,k) AND separates(G,W,s,t) AND card[T](W)=k
                        AND (FORALL V: separates(G,V,s,t)
                        AND card[T](V)=k IMPLIES attached?(G,s,t,V))
                  IMPLIES B(del_verts(G,dbl[T](a,c)),s,t,k-1)
                          OR edge?(G)(s,c) OR edge?(G)(a,t)

   C_induct_lemma: LEMMA  C_induct(G,s,t)   % Major lemma to prove.

   Menger_k_hard: THEOREM C(G,s,t)          % Proved from C_induct lemma.

   % Next is a 'constructive' version of hard Menger theorem. We search for separating
   % sets only among suitable subsets of the vertices of G,
   % those not containing the terminals. If all such
   % 'green' subsets of vert(G) of cardinality k (< size(G) -1) fail to separate s
   % from t in G, one concludes that there are k+1 independent paths in G from s to t.

   Many_indep_paths: THEOREM good?(G,s,t) AND k<=size(G)-2
                             AND (FORALL W: card[T](W)=k
                             AND subset?(W,difference(vert(G), dbl(s,t)))
                                    IMPLIES EXISTS q: walk_from?(del_verts(G,W),q,s,t))
                           IMPLIES many_ind(G,s,t,k+1)

   % We proved the general hard k-Menger theorem independently of the
   % proof for case k=2, without using 'sep_num' or
   % 'minimal separating set'. Using the definitions of these
   % terms, we may derive the traditional version directly from Menger_k_hard.

   hard_menger_trad: THEOREM  separable?(G,s,t) AND sep_num(G,s,t) = k
                              AND vert(G)(s) AND vert(G)(t)
                        IMPLIES
                            (EXISTS (ips: set_of_paths(G,s,t)):
                                   card(ips) = k AND ind_path_set?(G,s,t,ips))


END k_menger

quality86%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.