|
old_menger[T: TYPE]: THEORY
BEGIN
IMPORTING sep_sets[T], ind_paths[T]
G: VAR graph[T]
v,s,t: VAR T
e: VAR doubleton[T]
V: VAR finite_set[T]
m: VAR nat
easy_menger: LEMMA FORALL (ips: set_of_paths(G,s,t)):
separable?(G,s,t) AND
ind_path_set?(G,s,t,ips) IMPLIES
card(ips) <= sep_num(G,s,t)
IMPORTING h_menger[T] % FOR PROOF ONLY
hard_menger: LEMMA separable?(G,s,t) AND sep_num(G,s,t) = 2 AND
vert(G)(s) AND vert(G)(t)
IMPLIES
(EXISTS (ips: set_of_paths(G,s,t)):
card(ips) = 2 AND ind_path_set?(G,s,t,ips))
% --------------------------- PLAY STUFF ------------------------------ %
easy_meng_1: LEMMA FORALL (ips: set_of_paths(G,s,t)):
separable?(G,s,t) AND
ind_path_set?(G,s,t,ips) IMPLIES
card(ips) <= sep_num(G,s,t)
END old_menger
¤ Dauer der Verarbeitung: 0.13 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.
|
