Quelle  sep_set_lems.pvs

sep_set_lems[T: TYPE]: THEORY
BEGIN

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

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


   sep_num_0: LEMMA separable?(G,s,t) AND sep_num(G, s, t) = 0 IMPLIES
                          separates(G, emptyset[T], s, t)
  
   sep_num_gt_0: LEMMA vert(G)(s) AND vert(G)(t) AND separable?(G,s,t) 
                       AND sep_num(G,s,t) > 0 IMPLIES
                              (EXISTS (w: prewalk): walk_from?(G,w,s,t))

  
   sep_num_is_1: LEMMA vert(G)(s) AND vert(G)(t) AND v /= s AND v /= t AND
                          (FORALL (p: prewalk): walk_from?(G,p,s,t) IMPLIES
                                  (EXISTS (i: below(length(p))): seq(p)(i) = v))
                             IMPLIES sep_num(G,s,t) <= 1

   av: VAR T
   sep_num_le1: LEMMA vert(G)(s) AND vert(G)(t) AND vert(G)(av) AND
                          av /= s AND av /= t AND
                          separable?(G, s, t) AND 
                          sep_num(G,s,t) <= 1 IMPLIES
                             (EXISTS (z: T): vert(G)(z) AND z /= s AND z /= t AND
                                               separates(G,singleton(z),s,t))

   separable?_comm: LEMMA separable?(G,s,t) IMPLIES separable?(G,t,s)

   separates_comm:  LEMMA separates(G, W, s, t) = separates(G, W, t, s)


   sep_num_comm:    LEMMA vert(G)(s) AND vert(G)(t) IMPLIES
                            sep_num(G,s,t) = sep_num(G,t,s)


   v_not_in: LEMMA  walk_from?(del_verts(G, remove(v, W)), p,s,t)
               AND W(v) AND NOT verts_of(p)(v)
               IMPLIES walk_from?(del_verts(G, W), p, s, t)

   k: VAR nat
   path_thru_each: LEMMA     sep_num(G,s,t) = k 
                         AND separates(G, W, s, t)
                         AND card(W) = k AND W(v)
                         AND vert(G)(s) AND vert(G)(t)
              IMPLIES
                 (EXISTS (pv: prewalk): verts_of(pv)(v) AND path_from?(G,pv,s,t))
                 


   one_to_each: LEMMA     sep_num(G,s,t) = 2 
                      AND separates(G, dbl(w1, w2), s, t)
                      AND vert(G)(s) AND vert(G)(t)
              IMPLIES
             ( (EXISTS (Psw1: prewalk): path_from?(G, Psw1, s, w1)) AND
        (EXISTS (Psw2: prewalk): path_from?(G, Psw2, s, w2)))



   walk?_del_verts  : LEMMA walk?(del_verts(G, W), p) IMPLIES walk?[T](G, p)

   del_verts_eq: LEMMA del_vert(del_vert(G, w1), w2) = del_verts(G, dbl(w1, w2))

END sep_set_lems