meng_scaff_defs.pvs

meng_scaff_defs[T: TYPE]: THEORY
BEGIN

   IMPORTING paths[T], subgraphs[T], sep_sets[T],
             path_ops[T], subgraph_paths[T]

   G,HH: VAR graph[T]
   w1,w2,v,s,t,z: VAR T
   e: VAR doubleton[T]
   V: VAR finite_set[T]
   p: VAR prewalk

   IMPORTING ind_paths[T]

   path_comp(G,(x:T)): Subgraph(G) = subgraph(G,path_verts(G,x))

   IMPORTING graph_deg[T]

   H(G,(x,w1,w2:T)): Subgraph(G) = path_comp(del_vert(del_vert(G,w1),w2),x)
   

   incident(v,G,(x,w1,w2:T)): finite_set[doubleton[T]] 
              = {e: doubleton[T] | (EXISTS z: edges(G)(e) AND e = dbl(v,z) 
                                              AND vert(H(G,x,w1,w2))(z))}

   meng(G,(x,y: (vert(G))),(w1,w2: {t | vert(G)(t) AND t /= y})): graph[T] =
                   (# vert  := add(y,add(w1,add(w2,vert(H(G,x,w1,w2))))),
                      edges := add(dbl(w1,y), add(dbl(w2,y),
                                 union(edges(H(G,x,w1,w2)),
                                       union(incident(w1,G,x,w1,w2),
                                             incident(w2,G,x,w1,w2)))))
                   #)


   in?(G,s,t,w1,w2): bool = vert(G)(s) AND vert(G)(t) AND vert(G)(w1)
                                AND vert(G)(w2) 
   
   disjoint?(s,t,w1,w2): bool = (s /= t AND w1 /= w2 AND w1 /= s AND w2 /= s 
                                     AND w1 /= t AND w2 /= t) 

   vert_H_s: LEMMA vert(G)(s) AND s /= w1 AND s /= w2
                     IMPLIES vert(H(G, s, w1, w2))(s)


   path_H_W        : LEMMA path?(H(G,s,w1,w2),p) IMPLIES
                              NOT verts_of(p)(w1) AND NOT verts_of(p)(w2)

%  MOVED TO theory subgraph_paths
%
%  walk?_subgraph  : LEMMA subgraph?(HH,G) AND walk?(HH, p)
%                               IMPLIES walk?(G, p)
%
%  path?_subgraph  : LEMMA subgraph?(HH,G) AND path?(HH, p)
%                                  IMPLIES path?(G, p)

   path_comp_in    : LEMMA path?(H(G,s,w1,w2),p) IMPLIES path?(G,p)

   walk?_H         : LEMMA walk?(G, p) AND seq(p)(0) = s AND
                           NOT verts_of(p)(w1) AND NOT verts_of(p)(w2) 
                         IMPLIES walk?(H(G, s, w1, w2), p)

   vert_meng_sub   : LEMMA in?(G, s, t, w1, w2) AND disjoint?(s, t, w1, w2)
                           IMPLIES subset?(vert(meng(G, s, t, w1, w2)), vert(G))

   del_vert_comm   : LEMMA del_vert(del_vert(G,w2),w1) = 
                                    del_vert(del_vert(G,w1),w2)

   H_comm          : LEMMA H(G, t, w2, w1) = H(G, t, w1, w2)

   incident_comm   : LEMMA incident(v, G, t, w2, w1) = incident(v, G, t, w1, w2)

   meng_comm       : LEMMA vert(G)(s)  AND vert(G)(t) AND
                              vert(G)(w1) AND w1 /= s    AND
                              vert(G)(w2) AND w2 /= s 
                            IMPLIES meng(G, t, s, w1, w2) = meng(G, t, s, w2, w1)


END meng_scaff_defs