|
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]
k,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 k_menger[T] % FOR PROOF ONLY
hard_menger: THEOREM separable?(G,s,t) AND sep_num(G,s,t) = k
AND vert(G)(s) AND vert(G)(t)
IMPLIES
(EXISTS (ips: set_of_paths(G,s,t)):
card(ips) = k AND ind_path_set?(G,s,t,ips))
% menger: THEOREM separable?(G,s,t) AND vert(G)(s) AND vert(G)(t)
% IMPLIES
% ( sep_num(G,s,t) = k
% IFF
% (EXISTS (ips: set_of_paths(G,s,t)):
% card(ips) = k AND ind_path_set?(G,s,t,ips)))
END menger
[ zur Elbe Produktseite wechseln0.0Quellennavigators
Analyse erneut starten
]
|
