paths[T: TYPE]: THEORY BEGIN IMPORTING digraphs[T], walks[T], seq_def G: VAR digraph[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(l(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 = l(w)-1) 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 l(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 < l(ps) AND path?(G,ps) IMPLIES path?(G,ps^(i,j)) path_from?_caret: LEMMA i <= j AND j < l(ps) AND path_from?(G, ps, s, t) IMPLIES path_from?(G, ps^(i, j),seq(ps)(i),seq(ps)(j)) %%%%%%%%%%%%%%%%%%%% NOT TRUE fpr directed graphs %%%%%%%%%%%%%%%%%%% % % path?_rev : LEMMA path?(G,ps) IMPLIES path?(G,rev(ps)) path?_gen_seq2 : LEMMA vert(G)(x) AND vert(G)(y) AND x /= 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)(l(p)-1),x) AND NOT verts_of(p)(x) IMPLIES path?(G,add1(p,x)) path?_trunc1 : LEMMA path?(G,p) AND l(p) > 1 IMPLIES path_from?(G,trunc1(p),seq(p)(0),seq(p)(l(p)-2)) END paths