Quelle  meng_scaff.pvs

meng_scaff[T: TYPE]: THEORY


BEGIN

   IMPORTING meng_scaff_defs[T], sep_set_lems[T], min_lem

   G,MM: VAR graph[T]
   v,s,t,w1,w2: VAR T
   W: VAR finite_set[T]
   p: VAR prewalk
   i: VAR nat


  P: VAR pred[T]
  
  ps_ptype(P): TYPE = {ps: prewalk | EXISTS (i: below(length(ps))): P(seq(ps)(i))}

  first(P: pred[T],ps: ps_ptype(P)): below(length(ps)) = 
                  min({i: nat | i < length(ps) AND P(seq(ps)(i))})
  
  first_lem: LEMMA FORALL (ps: ps_ptype(P)): P(seq(ps)(first(P,ps)))
  
  first_not: LEMMA FORALL (ps: ps_ptype(P)): i < first(P,ps) IMPLIES
        NOT  P(seq(ps)(i))
  
    
  z: VAR T

  meng_to_G_sep: LEMMA walk_from?(G, p, s, t) AND 
                        in?(G, s, t, w1, w2) AND disjoint?(s, t, w1, w2) AND
                        separates(meng(G, s, t, w1, w2), singleton(z), s, t) AND
                        separable?(G, s, t) AND
                        separates(G, dbl(w1, w2), s, t) AND
                        NOT verts_of(p)(z)
                     IMPLIES sep_num(G, s, t) <= 1

  prep_14: LEMMA  vert(G)(s) AND vert(G)(t) AND
              vert(G)(w1) AND vert(G)(w2) AND 
                   disjoint?(s, t, w1, w2) AND
                   sep_num(meng(G, s, t, w1, w2),s,t) <= 1 AND
                   separates(meng(G, s, t, w1, w2), dbl(w1, w2), s, t) AND
              separable?(G, s, t) AND
              separates(G, dbl(w1, w2), s, t) AND 
                   sep_num(G, s, t) = 2 
                  IMPLIES sep_num(G,s,t) <= 1

   line14: 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)
                   IMPLIES
                        sep_num(meng(G, s, t, w1, w2), s, t) = 2 


   line15ab: 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)
              IMPLIES
                 ((EXISTS (Psw1: prewalk): path_from?(G,Psw1,s,w1)) AND
                  (EXISTS (Psw2: prewalk): path_from?(G,Psw2,s,w2)))


   prep_16: LEMMA separates(G, dbl(w1, w2), s, t) AND
                     disjoint?(s, t, w1, w2) AND
                     (FORALL p: path_from?(G,p,t,w1) IMPLIES verts_of(p)(w2))
                     AND vert(G)(s) AND vert(G)(t)
                     IMPLIES  sep_num(G,s,t) <= 1

   line16: LEMMA NOT edge?(G)(w1, t) AND 
                        disjoint?(s,t,w1,w2) AND
                        separates(G, dbl(w1, w2), s, t) AND
                        sep_num(G,s,t) = 2 AND vert(G)(s) AND vert(G)(t)
                   IMPLIES EXISTS (yt: T): vert(H(G,t,w1,w2))(yt) AND yt /= t

   line19: LEMMA      separable?(G,s,t) AND in?(G,s,t,w1,w2)
                      AND disjoint?(s,t,w1,w2)
                      AND MM = meng(G, s, t, w1, w2)
                      AND separates(G, dbl(w1, w2), s, t)
                      AND path_from?(MM, p, s, t)
                          IMPLIES length(p) > 2 AND (  seq(p)(length(p)-2) = w1
                                               OR seq(p)(length(p)-2) = w2)
 

   yt: VAR T

   line17_prep: LEMMA vert(G)(s) AND vert(G)(t) AND disjoint?(s,t,w1,w2) AND
                      vert(H(G, t, w1, w2))(yt) AND
                      separates(G, dbl(w1, w2), s, t) IMPLIES
                          NOT vert(H(G, s, w1, w2))(yt)


   line17: LEMMA  vert(H(G,t,w1,w2))(yt) AND
                  in?(G, s, t, w1, w2) AND
                  disjoint?(s, t, w1, w2) AND
                  yt /= t AND
                  separates(G, dbl(w1, w2), s, t) 
                       IMPLIES size(meng(G, s, t, w1, w2)) < size(G)

   pre20: 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)
                IMPLIES
               ( separable?(meng(G, s, t, w1, w2),s,t) AND
                     sep_num(meng(G, s, t, w1, w2), s, t) = 2 AND
                     vert(meng(G, s, t, w1, w2))(s) AND 
                     vert(meng(G, s, t, w1, w2))(t)                 ) 


END meng_scaff