|
path_ops[T: TYPE]: THEORY
BEGIN
IMPORTING paths[T], subgraphs[T], sep_sets[T], graph_ops[T]
G: VAR graph[T]
u,v,s,t,yt: VAR T
e: VAR doubleton[T]
W,V: VAR finite_set[T]
w,w1,p,p1,q,q1: VAR prewalk
walk?_del_vert : LEMMA walk?(del_vert(G, v), w) IMPLIES walk?[T](G, w)
walk?_del_vert_not : LEMMA walk?(G, w) AND NOT verts_of(w)(v)
IMPLIES walk?(del_vert(G, v), w)
path?_del_vert : LEMMA FORALL (w: prewalk): path?(del_vert(G, v), w)
IMPLIES path?[T](G, w)
path?_del_verts : LEMMA FORALL (w: prewalk): path?(del_verts(G, W), w)
IMPLIES path?[T](G, w)
IMPORTING walk_inductions[T],path_circ[T]
walk_to_path : LEMMA (EXISTS (w: prewalk): walk_from?(G,w,s,t)) IMPLIES
(EXISTS (p: prewalk): path?(G,p) AND
walk_from?(G,p,s,t))
walk_to_path_less : LEMMA walk_from?(G,w,s,t) IMPLIES
(EXISTS (p: prewalk): path?(G,p) AND
walk_from?(G,p,s,t)and length(p)<=length(w))
walk_to_path_from : LEMMA walk_from?(G,w,s,t) IMPLIES
(EXISTS (p: prewalk): path_from?(G,p,s,t))
walk_to_path_from_less : LEMMA walk_from?(G,w,s,t) IMPLIES
(EXISTS (p: prewalk): path_from?(G,p,s,t) AND
length(p)<=length(w))
% More lemmas to aid in Menger and other advanced theories.
path_disjoint: LEMMA u /= yt AND path_from?(G, p, u, yt)
AND path_from?(G, q, yt, v)
AND empty?(intersection(verts_of(trunc1(p)),verts_of(q)))
IMPLIES path_from?(G,trunc1(p) o q,u,v)
END path_ops
¤ Dauer der Verarbeitung: 0.0 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.
|
