|
sep_set_lems[T: TYPE]: THEORY
BEGIN
IMPORTING paths[T], sep_sets[T], path_ops[T]
G,MM: VAR graph[T]
v,s,t,w1,w2: VAR T
e: VAR doubleton[T]
W: VAR finite_set[T]
p: VAR prewalk
sep_num_0: LEMMA separable?(G,s,t) AND sep_num(G, s, t) = 0 IMPLIES
separates(G, emptyset[T], s, t)
sep_num_gt_0: LEMMA vert(G)(s) AND vert(G)(t) AND separable?(G,s,t)
AND sep_num(G,s,t) > 0 IMPLIES
(EXISTS (w: prewalk): walk_from?(G,w,s,t))
sep_num_is_1: LEMMA vert(G)(s) AND vert(G)(t) AND v /= s AND v /= t AND
(FORALL (p: prewalk): walk_from?(G,p,s,t) IMPLIES
(EXISTS (i: below(length(p))): seq(p)(i) = v))
IMPLIES sep_num(G,s,t) <= 1
av: VAR T
sep_num_le1: LEMMA vert(G)(s) AND vert(G)(t) AND vert(G)(av) AND
av /= s AND av /= t AND
separable?(G, s, t) AND
sep_num(G,s,t) <= 1 IMPLIES
(EXISTS (z: T): vert(G)(z) AND z /= s AND z /= t AND
separates(G,singleton(z),s,t))
separable?_comm: LEMMA separable?(G,s,t) IMPLIES separable?(G,t,s)
separates_comm: LEMMA separates(G, W, s, t) = separates(G, W, t, s)
sep_num_comm: LEMMA vert(G)(s) AND vert(G)(t) IMPLIES
sep_num(G,s,t) = sep_num(G,t,s)
v_not_in: LEMMA walk_from?(del_verts(G, remove(v, W)), p,s,t)
AND W(v) AND NOT verts_of(p)(v)
IMPLIES walk_from?(del_verts(G, W), p, s, t)
k: VAR nat
path_thru_each: LEMMA sep_num(G,s,t) = k
AND separates(G, W, s, t)
AND card(W) = k AND W(v)
AND vert(G)(s) AND vert(G)(t)
IMPLIES
(EXISTS (pv: prewalk): verts_of(pv)(v) AND path_from?(G,pv,s,t))
one_to_each: LEMMA sep_num(G,s,t) = 2
AND separates(G, dbl(w1, w2), s, t)
AND vert(G)(s) AND vert(G)(t)
IMPLIES
( (EXISTS (Psw1: prewalk): path_from?(G, Psw1, s, w1)) AND
(EXISTS (Psw2: prewalk): path_from?(G, Psw2, s, w2)))
walk?_del_verts : LEMMA walk?(del_verts(G, W), p) IMPLIES walk?[T](G, p)
del_verts_eq: LEMMA del_vert(del_vert(G, w1), w2) = del_verts(G, dbl(w1, w2))
END sep_set_lems
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
