|
ind_paths[T: TYPE]: THEORY
BEGIN
IMPORTING paths[T]
G: VAR digraph[T]
u,v,s,t: VAR T
e: VAR edgetype[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
¤ Dauer der Verarbeitung: 0.16 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.
|
