paths[T: TYPE]: THEORY

BEGIN

   IMPORTING graphs[T], walks[T] 

   G: VAR graph[T]
   x,y,s,t: VAR T
   i,j: VAR nat
   p,ps: VAR prewalk

   path?(G,ps): bool = walk?(G,ps) AND (FORALL (i,j: below(length(ps))):
                                          i /= j IMPLIES ps(i) /= ps(j))

   Path(G): TYPE = {p: prewalk | path?(G,p)}

   path_from?(G,ps,s,t): bool = path?(G,ps) AND from?(ps,s,t)

   Path_from(G,s,t): TYPE = {p: prewalk | path_from?(G,p,s,t)}

   endpoint?(i: nat, w: prewalk): bool = (i = 0) OR (i = length(w)-1)

   path_verts(G,(x:T)): set[T] = {v: T | EXISTS (w: prewalk): walk_from?(G,w,x,v)}


   path?_verts     : LEMMA path?(G,ps) IMPLIES verts_in?(G,ps)

   path_from_l     : LEMMA path_from?(G,ps,s,t) AND s /= t IMPLIES length(ps) >= 2

   path_from_in    : LEMMA path_from?(G, ps, s, t) IMPLIES 
                          vert(G)(s) AND vert(G)(t)


   path?_caret     : LEMMA i <= j AND j < length(ps) AND path?(G,ps) 
                            IMPLIES path?(G,ps^(i,j))

   path_from?_caret: LEMMA  i <= j AND j < length(ps) AND path_from?(G, ps, s, t)
                         IMPLIES path_from?(G, ps^(i, j),seq(ps)(i),seq(ps)(j))

   path?_rev       : LEMMA path?(G,ps) IMPLIES path?(G,rev(ps))


   path?_gen_seq2  : LEMMA vert(G)(x) AND vert(G)(y) AND
                            edge?(G)(x,y) IMPLIES path?(G,gen_seq2(G,x,y))

   path?_add1      : LEMMA path?(G,p) AND vert(G)(x)
                            AND edge?(G)(seq(p)(length(p)-1),x)
                            AND NOT verts_of(p)(x)
                            IMPLIES path?(G,add1(p,x))                      

   path?_trunc1      : LEMMA path?(G,p) AND length(p) > 1 IMPLIES
                            path_from?(G,trunc1(p),seq(p)(0),seq(p)(length(p)-2)) 


END paths