SSL meng_scaff_prelude.pvs   Interaktion und
PortierbarkeitPVS

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 length(P1) > 2 AND
                              path_from?(MM,P2,s,t) AND length(P2) > 2 AND
                              seq(P1)(length(P1)-2) = w1 AND NOT verts_of(P1)(w2) AND
                              seq(P2)(length(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) | length(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,length(p1)-2) o rev(p2)
   
   path_meng_t  : LEMMA path_from?(G, p, s, t) AND length(p) > 0 
                           IMPLIES (i < length(p) AND seq(p)(i) = t
                                      IMPLIES i = length(p) - 1)

   path_H_def   : LEMMA path?(H(G,s,w1,w2),p) AND j < length(p) IMPLIES 
                           walk?(del_verts[T](G, dbl[T](w1, w2)), p^(0,j))


   path_H_ind   : LEMMA length(p1) > 1 AND length(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 length(p1) > 2 AND length(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 length(p) >= 2 AND
                    path?(H(G, s, w1, w2), trunc1(p)) AND
                    from?(p, s, w1) AND 
                    edge?(G)(p(length(p)-2),p(length(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 length(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)(length(p) - 3), seq(p)(length(p) - 2))

   ind_verts_W: LEMMA path_from?(G,p1,s,t) AND
                      path_from?(G,p2,t,s) AND
                      length(p1) > 2 AND seq(p1)(length(p1) - 2) = w1 AND
                      length(p2) > 2 AND seq(p2)(length(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
                         length(p1) > 2 AND seq(p1)(length(p1) - 2) = w1 AND
                         length(p2) > 2 AND seq(p2)(length(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 length(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)(length(p) - 2) = w1 AND NOT verts_of(p)(w2)) OR
                        (seq(p)(length(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 < length(w1)  AND j < length(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