|
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
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
