path_circ[T: TYPE]: THEORY

BEGIN

 IMPORTING walks[T],circuits[T],paths[T]


  x,y,s,t,ss,tt: VAR T
  i: VAR nat
  G,GG: VAR graph[T]
  u,w,p,q: VAR prewalk

  path_reduc       : LEMMA FORALL (p: Path(G)) : reduced?(G,p)

  trunc_long       : LEMMA length(u)>= 2 AND length(w) >= 2 IMPLIES length(trunc1(u) o w) >= 1

  trunc_walk       : LEMMA length(u)>=2 AND walk?(G,u) IMPLIES walk?(G,trunc1(u))

  walks_concat_red : LEMMA walk?(G,u) AND walk?(G,w) AND
                           length(u) >=2 AND length(w) >=2 AND reduced?(G,u) AND 
                           reduced?(G,w) AND u(length(u)-1) = w(0) AND
                           u(length(u)-2) /= w(1) IMPLIES reduced?(G,trunc1(u) o w)

  index_rev        : LEMMA length(q)>=2 IMPLIES length(rev(q)) = length(q) AND 
                                           rev(q)(0) = q(length(q)-1) AND
                                           rev(q)(1) = q(length(q)-2)

  rev_rev          : LEMMA rev(rev(q))=q

  ind_rev_rev      : LEMMA length(q)>=2  IMPLIES rev(q)(length(q)-1) = q(0) AND 
                                            rev(q)(length(q)-2) = q(1)

  second_in_cat    : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t) IMPLIES 
                               p(1) = (trunc1(p) o rev(q))(1)

  sec_from_last    : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t) IMPLIES 
                           q(1) = (trunc1(p) o rev(q))(length(trunc1(p) o rev(q))-2)

  prewalk_same     : LEMMA s=t AND length(p)=1 AND length(q)=1 AND from?(p,s,t) AND 
                           from?(q,s,t) IMPLIES p=q 


  compose_long     : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t) AND 
                           p(length(p)-2) /= q(length(q)-2) IMPLIES length(trunc1(p) o rev(q)) > 2 

  red_compos       : LEMMA s /= t AND path_from?(G,p,s,t) AND 
                           path_from?(G,q,s,t) AND p(length(p)-2) /= q(length(q)-2) 
                              IMPLIES reduced?(G,trunc1(p) o rev(q))

  cycl_red_compos  : LEMMA s /= t AND path_from?(G,p,s,t) AND 
                           path_from?(G,q,s,t) AND p(length(p)-2) /= q(length(q)-2) AND 
                           p(1) /= q(1) 
                              IMPLIES cyclically_reduced?(G,trunc1(p) o rev(q))

  walkers          : LEMMA finseq_appl(p)(0)=finseq_appl(q)(0) AND 
                           finseq_appl(p)(length(p)-1)=finseq_appl(q)(length(q)-1)
                         IMPLIES 
                           from?(p,finseq_appl(p)(0),finseq_appl(p)(length(p)-1)) AND 
                           from?(q,finseq_appl(p)(0),finseq_appl(p)(length(p)-1))

  path_one         : LEMMA s=t and path_from?(G,p,s,t) IMPLIES length(p)=1 OR circuit?(G,p)

  rev_eq           : LEMMA rev(p)=rev(q) IMPLIES p=q

  front_back       : LEMMA from?(p,s,t) AND from?(q,s,t) 
                            IMPLIES p(0)=q(0) AND  p(length(p)-1)=q(length(q)-1)

  walk_from_l      : LEMMA from?(p,s,t) AND s /= t IMPLIES length(p) >= 2

  plus_up          : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t)  IMPLIES 
                (trunc1(p) = trunc1(q) IMPLIES  p=q)


  two_walks        : LEMMA s /=t AND walk?(G,p) AND walk?(G,q) AND 
                           from?(p,s,t) AND from?(q,s,t) IMPLIES 
                                     pre_circuit?(G,trunc1(p) o rev(q))

  back_short       : LEMMA s /= t AND path_from?(G,p,s,t) AND 
                           path_from?(G,q,s,t) 
                        IMPLIES 
                           ( p(length(p)-2)=q(length(q)-2) AND p /= q IMPLIES  
                             (EXISTS (pp,qq: prewalk) : pp /= qq AND 
                                 path_from?(G,pp,s,p(length(p)-2)) AND 
                                 path_from?(G,qq,s,p(length(p)-2)) AND 
                                 length(pp)= length(p)-1 AND length(qq)=length(q)-1)
                           )

  from_rev         : LEMMA from?(p,s,t) IMPLIES from?(rev(p),t,s)

  front_short: LEMMA s /= t AND path_from?(G,p,s,t) AND path_from?(G,q,s,t)
                      IMPLIES 
                        ( p(1)=q(1) AND p /= q  IMPLIES  
                          (EXISTS (pp,qq: prewalk) :
                            pp /= qq AND path_from?(G,pp,t,p(1)) 
                            AND path_from?(G,qq,t,p(1))
                            AND length(pp)= length(p)-1 AND length(qq)=length(q)-1)
                        )

  add1_rev: LEMMA FORALL (w:Seq(G),x:(vert(G))): 
                   length(w)>1 AND x /= seq(w)(length(w)-1) 
                   IMPLIES add1(w,x)=trunc1(w) o rev(gen_seq2(G,x,seq(w)(length(w)-1)))
 

END path_circ