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