SSL ind_paths.pvs

ind_paths[T: TYPE]: THEORY


BEGIN

   IMPORTING paths[T]

   G: VAR graph[T]
   u,v,s,t: VAR T
   e: VAR doubleton[T]
   V: VAR finite_set[T]
   n: VAR nat

   independent?(w1,w2: prewalk): bool = 
                       (FORALL (i,j: nat): i > 0 AND i < length(w1) - 1 AND
                                           j > 0 AND j < length(w2) - 1 IMPLIES
                                    seq(w1)(i) /= seq(w2)(j))

   p1,p2: VAR prewalk
   independent?_comm: LEMMA independent?(p1,p2) IMPLIES
                                    independent?(p2,p1)

   independent_ne: LEMMA length(p1) > 2 AND independent?(p1,p2) IMPLIES p1 /= p2

   ps: VAR prewalk

%   IMPORTING finite_sets

   set_of_paths(G,s,t): TYPE = finite_set[Path_from(G,s,t)]

   ind_path_set?(G,s,t,(pset: set_of_paths(G,s,t))): bool = 
                   (FORALL (p1,p2: Path_from(G,s,t)): 
                             pset(p1) AND pset(p2) AND  p1 /= p2
                                         IMPLIES independent?(p1,p2))

   ind_path_set_2: LEMMA FORALL (ips: set_of_paths(G,s,t)): 
                                    card(ips) = 2 AND
                                    ind_path_set?(G, s, t, ips)
                              IMPLIES
                         (EXISTS (P_1,P_2: prewalk): path_from?(G, P_1, s, t) AND
                                                    path_from?(G, P_2, s, t) AND
                                                      independent?(P_1,P_2) )

   internal_verts(w: prewalk): finite_set[T] = 
               {t: T | (EXISTS (i: nat): i > 0 AND i < length(w) - 1 AND w(i) = t)}


   indep?(w1,w2: prewalk): bool = empty?(intersection(internal_verts(w1),
                                                      internal_verts(w2)))

   w1,w2: VAR prewalk
   indep?_lem: LEMMA indep?(w1,w2) IFF independent?(w1,w2) 

END ind_paths