:: GLIB_005 semantic presentation begin begin definitionlet "G" be ($#m1_hidden :::"WGraph":::); attr "G" is :::"natural-weighted"::: means :: GLIB_005:def 1 (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) "G") "is" ($#v4_valued_0 :::"natural-valued"::: ) ); end; :: deftheorem defines :::"natural-weighted"::: GLIB_005:def 1 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_glib_005 :::"natural-weighted"::: ) ) "iff" (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G"))) "is" ($#v4_valued_0 :::"natural-valued"::: ) ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) -> ($#v8_glib_003 :::"nonnegative-weighted"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v2_glib_000 :::"finite"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "G" be ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::); cluster (Set ($#k5_glib_003 :::"the_Weight_of"::: ) "G") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode FF:ELabeling of "G" is ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G"); end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "source", "sink" be ($#m1_hidden :::"set"::: ) ; pred "EL" :::"has_valid_flow_from"::: "source" "," "sink" means :: GLIB_005:def 2 (Bool "(" (Bool "source" "is" ($#m1_subset_1 :::"Vertex":::) "of" "G") & (Bool "sink" "is" ($#m1_subset_1 :::"Vertex":::) "of" "G") & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G"))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set "EL" ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) & (Bool (Set "EL" ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) "source") & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) "sink")) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" "EL" ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set "(" "EL" ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"has_valid_flow_from"::: GLIB_005:def 2 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "EL")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) "iff" (Bool "(" (Bool (Set (Var "source")) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))) & (Bool (Set (Var "sink")) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) & (Bool (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "source"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "sink")))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "EL")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "EL")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) ")" ) ")" ))) ")" ) ")" ) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "source", "sink" be ($#m1_hidden :::"set"::: ) ; func "EL" :::".flow"::: "(" "source" "," "sink" ")" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: GLIB_005:def 3 (Set (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" "EL" ($#k5_relat_1 :::"|"::: ) (Set "(" "G" ($#k18_glib_000 :::".edgesInto"::: ) (Set ($#k1_tarski :::"{"::: ) "sink" ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" "EL" ($#k5_relat_1 :::"|"::: ) (Set "(" "G" ($#k19_glib_000 :::".edgesOutOf"::: ) (Set ($#k1_tarski :::"{"::: ) "sink" ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" )); end; :: deftheorem defines :::".flow"::: GLIB_005:def 3 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "EL")) ($#k1_glib_005 :::".flow"::: ) "(" (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "EL")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "G")) ($#k18_glib_000 :::".edgesInto"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "sink")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "EL")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "G")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "sink")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" )))))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "source", "sink" be ($#m1_hidden :::"set"::: ) ; pred "EL" :::"has_maximum_flow_from"::: "source" "," "sink" means :: GLIB_005:def 4 (Bool "(" (Bool "EL" ($#r1_glib_005 :::"has_valid_flow_from"::: ) "source" "," "sink") & (Bool "(" "for" (Set (Var "E2")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" "G" "st" (Bool (Bool (Set (Var "E2")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) "source" "," "sink")) "holds" (Bool (Set (Set (Var "E2")) ($#k1_glib_005 :::".flow"::: ) "(" "source" "," "sink" ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set "EL" ($#k1_glib_005 :::".flow"::: ) "(" "source" "," "sink" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"has_maximum_flow_from"::: GLIB_005:def 4 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "EL")) ($#r2_glib_005 :::"has_maximum_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) "iff" (Bool "(" (Bool (Set (Var "EL")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool "(" "for" (Set (Var "E2")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "E2")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink")))) "holds" (Bool (Set (Set (Var "E2")) ($#k1_glib_005 :::".flow"::: ) "(" (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "EL")) ($#k1_glib_005 :::".flow"::: ) "(" (Set (Var "source")) "," (Set (Var "sink")) ")" )) ")" ) ")" ) ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); mode :::"AP:VLabeling"::: "of" "EL" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ")" ) means :: GLIB_005:def 5 (Bool verum); end; :: deftheorem defines :::"AP:VLabeling"::: GLIB_005:def 5 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Var "EL"))) "iff" (Bool verum) ")" )))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "VL" be ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Const "EL")); let "e" be ($#m1_hidden :::"set"::: ) ; pred "e" :::"is_forward_edge_wrt"::: "VL" means :: GLIB_005:def 6 (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "VL")) & (Bool (Bool "not" (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "VL"))) & (Bool (Set "EL" ($#k1_funct_1 :::"."::: ) "e") ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e")) ")" ); end; :: deftheorem defines :::"is_forward_edge_wrt"::: GLIB_005:def 6 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "VL")) "being" ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Var "EL")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_glib_005 :::"is_forward_edge_wrt"::: ) (Set (Var "VL"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "VL")))) & (Bool (Bool "not" (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "VL"))))) & (Bool (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" ))))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "VL" be ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Const "EL")); let "e" be ($#m1_hidden :::"set"::: ) ; pred "e" :::"is_backward_edge_wrt"::: "VL" means :: GLIB_005:def 7 (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "VL")) & (Bool (Bool "not" (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "VL"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set "EL" ($#k1_funct_1 :::"."::: ) "e")) ")" ); end; :: deftheorem defines :::"is_backward_edge_wrt"::: GLIB_005:def 7 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "VL")) "being" ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Var "EL")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r4_glib_005 :::"is_backward_edge_wrt"::: ) (Set (Var "VL"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "VL")))) & (Bool (Bool "not" (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "VL"))))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" ))))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); pred "W" :::"is_augmenting_wrt"::: "EL" means :: GLIB_005:def 8 (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W"))) "holds" (Bool "(" "(" (Bool (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," "G")) "implies" (Bool (Set "EL" ($#k1_funct_1 :::"."::: ) (Set "(" "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," "G"))) "implies" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set "EL" ($#k1_funct_1 :::"."::: ) (Set "(" "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ")" )); end; :: deftheorem defines :::"is_augmenting_wrt"::: GLIB_005:def 8 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," (Set (Var "G")))) "implies" (Bool (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," (Set (Var "G"))))) "implies" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ")" )) ")" )))); theorem :: GLIB_005:1 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "holds" (Bool (Set (Var "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))))) ; theorem :: GLIB_005:2 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))) "holds" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))))))) ; theorem :: GLIB_005:3 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))) & (Bool "(" (Bool "(" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "v")) "," (Set (Var "G"))) & (Bool (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) "or" (Bool "(" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "v")) "," (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "G"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))))))) ; begin definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "VL" be ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Const "EL")); func :::"AP:NextBestEdges"::: "VL" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) means :: GLIB_005:def 9 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r3_glib_005 :::"is_forward_edge_wrt"::: ) "VL") "or" (Bool (Set (Var "e")) ($#r4_glib_005 :::"is_backward_edge_wrt"::: ) "VL") ")" ) ")" )); end; :: deftheorem defines :::"AP:NextBestEdges"::: GLIB_005:def 9 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "VL")) "being" ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Var "EL")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL")))) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r3_glib_005 :::"is_forward_edge_wrt"::: ) (Set (Var "VL"))) "or" (Bool (Set (Var "e")) ($#r4_glib_005 :::"is_backward_edge_wrt"::: ) (Set (Var "VL"))) ")" ) ")" )) ")" ))))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "VL" be ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Const "EL")); func :::"AP:Step"::: "VL" -> ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" "EL" equals :: GLIB_005:def 10 "VL" if (Bool (Set ($#k2_glib_005 :::"AP:NextBestEdges"::: ) "VL") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) (Set "VL" ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) "VL" ")" ) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) "VL" ")" ) ")" ) ")" )) if (Bool "(" (Bool (Set ($#k2_glib_005 :::"AP:NextBestEdges"::: ) "VL") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Bool "not" (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) "VL" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "VL"))) ")" ) otherwise (Set "VL" ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) "VL" ")" ) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) "VL" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"AP:Step"::: GLIB_005:def 10 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "VL")) "being" ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Var "EL")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k3_glib_005 :::"AP:Step"::: ) (Set (Var "VL"))) ($#r1_hidden :::"="::: ) (Set (Var "VL"))) ")" & "(" (Bool (Bool (Set ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Bool "not" (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "VL")))))) "implies" (Bool (Set ($#k3_glib_005 :::"AP:Step"::: ) (Set (Var "VL"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "VL")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL")) ")" ) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool "(" "not" (Bool (Set ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "VL")))) ")" )) "implies" (Bool (Set ($#k3_glib_005 :::"AP:Step"::: ) (Set (Var "VL"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "VL")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL")) ")" ) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k2_glib_005 :::"AP:NextBestEdges"::: ) (Set (Var "VL")) ")" ) ")" ) ")" ))) ")" ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); mode :::"AP:VLabelingSeq"::: "of" "EL" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_005:def 11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" "EL")); end; :: deftheorem defines :::"AP:VLabelingSeq"::: GLIB_005:def 11 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_glib_005 :::"AP:VLabelingSeq"::: ) "of" (Set (Var "EL"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" (Set (Var "EL")))) ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "VS" be ($#m2_glib_005 :::"AP:VLabelingSeq"::: ) "of" (Set (Const "EL")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "VS" :::"."::: "n" -> ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" "EL"; end; definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "source" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"AP:CompSeq"::: "(" "EL" "," "source" ")" -> ($#m2_glib_005 :::"AP:VLabelingSeq"::: ) "of" "EL" means :: GLIB_005:def 12 (Bool "(" (Bool (Set it ($#k4_glib_005 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "source" ($#k16_funcop_1 :::".-->"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k4_glib_005 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k3_glib_005 :::"AP:Step"::: ) (Set "(" it ($#k4_glib_005 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"AP:CompSeq"::: GLIB_005:def 12 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m2_glib_005 :::"AP:VLabelingSeq"::: ) "of" (Set (Var "EL")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k4_glib_005 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "source")) ($#k16_funcop_1 :::".-->"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k4_glib_005 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k3_glib_005 :::"AP:Step"::: ) (Set "(" (Set (Var "b4")) ($#k4_glib_005 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))))); theorem :: GLIB_005:4 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k4_glib_005 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "source")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: GLIB_005:5 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k4_glib_005 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k4_glib_005 :::"."::: ) (Set (Var "j")) ")" ))))))) ; definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "source" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"AP:FindAugPath"::: "(" "EL" "," "source" ")" -> ($#m1_glib_005 :::"AP:VLabeling"::: ) "of" "EL" equals :: GLIB_005:def 13 (Set (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" "EL" "," "source" ")" ")" ) ($#k40_glib_000 :::".Result()"::: ) ); end; :: deftheorem defines :::"AP:FindAugPath"::: GLIB_005:def 13 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k40_glib_000 :::".Result()"::: ) ))))); theorem :: GLIB_005:6 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ) "is" ($#v13_glib_000 :::"halting"::: ) )))) ; theorem :: GLIB_005:7 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k4_glib_005 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k4_glib_005 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))))))))) ; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "source", "sink" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"AP:GetAugPath"::: "(" "EL" "," "source" "," "sink" ")" -> ($#v6_glib_001 :::"vertex-distinct"::: ) ($#m3_glib_001 :::"Path":::) "of" "G" means :: GLIB_005:def 14 (Bool "(" (Bool it ($#r1_glib_001 :::"is_Walk_from"::: ) "source" "," "sink") & (Bool it ($#r5_glib_005 :::"is_augmenting_wrt"::: ) "EL") & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" "EL" "," "source" ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) if (Bool "sink" ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" "EL" "," "source" ")" ")" ))) otherwise (Bool it ($#r2_relset_1 :::"="::: ) (Set "G" ($#k1_glib_001 :::".walkOf"::: ) "source")); end; :: deftheorem defines :::"AP:GetAugPath"::: GLIB_005:def 14 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b5")) "being" ($#v6_glib_001 :::"vertex-distinct"::: ) ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "sink")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" )))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_005 :::"AP:GetAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b5")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool (Set (Var "b5")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "sink")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ))))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_005 :::"AP:GetAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" )) "iff" (Bool (Set (Var "b5")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "source")))) ")" ) ")" ")" ))))); theorem :: GLIB_005:8 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k4_glib_005 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "P")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))) & (Bool (Set (Var "P")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "source")) "," (Set (Var "v"))) & (Bool (Set (Set (Var "P")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k5_glib_005 :::"AP:CompSeq"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ) ($#k4_glib_005 :::"."::: ) (Set (Var "n")) ")" ))) ")" ))))))) ; theorem :: GLIB_005:9 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ))) "iff" (Bool "ex" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "source")) "," (Set (Var "v"))) & (Bool (Set (Var "P")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))) ")" )) ")" ))))) ; theorem :: GLIB_005:10 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "source")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" )))))) ; begin definitionlet "G" be ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); assume (Bool (Set (Const "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Const "EL"))) ; func "W" :::".flowSeq"::: "EL" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_005:def 15 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "W" ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool "(" "(" (Bool (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) "," (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," "G")) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" "EL" ($#k1_funct_1 :::"."::: ) (Set "(" "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) "," (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," "G"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "EL" ($#k1_funct_1 :::"."::: ) (Set "(" "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ))) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::".flowSeq"::: GLIB_005:def 15 : (Bool "for" (Set (Var "G")) "being" ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_005 :::".flowSeq"::: ) (Set (Var "EL")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) "," (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Var "G")))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) "," (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Var "G"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ))) ")" ")" ) ")" ) ")" ) ")" ))))); definitionlet "G" be ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); assume (Bool (Set (Const "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Const "EL"))) ; func "W" :::".tolerance"::: "EL" -> ($#m1_hidden :::"Nat":::) means :: GLIB_005:def 16 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" "W" ($#k8_glib_005 :::".flowSeq"::: ) "EL" ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" "W" ($#k8_glib_005 :::".flowSeq"::: ) "EL" ")" )))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ) if (Bool (Bool "not" "W" "is" ($#v3_glib_001 :::"trivial"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::".tolerance"::: GLIB_005:def 16 : (Bool "for" (Set (Var "G")) "being" ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_glib_005 :::".tolerance"::: ) (Set (Var "EL")))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_005 :::".flowSeq"::: ) (Set (Var "EL")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_005 :::".flowSeq"::: ) (Set (Var "EL")) ")" )))) "holds" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_glib_005 :::".tolerance"::: ) (Set (Var "EL")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))))); definitionlet "G" be ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "P" be ($#m3_glib_001 :::"Path":::) "of" (Set (Const "G")); assume (Bool (Set (Const "P")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Const "EL"))) ; func :::"FF:PushFlow"::: "(" "EL" "," "P" ")" -> ($#m1_hidden :::"FF:ELabeling":::) "of" "G" means :: GLIB_005:def 17 (Bool "(" (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "P" ($#k14_glib_001 :::".edges()"::: ) )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set "EL" ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "P"))) "holds" (Bool "(" "(" (Bool (Bool (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set "P" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," "G")) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "EL" ($#k1_funct_1 :::"."::: ) (Set "(" "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "P" ($#k9_glib_005 :::".tolerance"::: ) "EL" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set "P" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," "G"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "EL" ($#k1_funct_1 :::"."::: ) (Set "(" "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" "P" ($#k9_glib_005 :::".tolerance"::: ) "EL" ")" ))) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"FF:PushFlow"::: GLIB_005:def 17 : (Bool "for" (Set (Var "G")) "being" ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "P")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_glib_005 :::"FF:PushFlow"::: ) "(" (Set (Var "EL")) "," (Set (Var "P")) ")" )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k14_glib_001 :::".edges()"::: ) )))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," (Set (Var "G")))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "P")) ($#k9_glib_005 :::".tolerance"::: ) (Set (Var "EL")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "," (Set (Var "G"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "EL")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "P")) ($#k9_glib_005 :::".tolerance"::: ) (Set (Var "EL")) ")" ))) ")" ")" ) ")" ) ")" ) ")" ))))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "EL" be ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Const "G")); let "sink", "source" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"FF:Step"::: "(" "EL" "," "source" "," "sink" ")" -> ($#m1_hidden :::"FF:ELabeling":::) "of" "G" equals :: GLIB_005:def 18 (Set ($#k10_glib_005 :::"FF:PushFlow"::: ) "(" "EL" "," (Set "(" ($#k7_glib_005 :::"AP:GetAugPath"::: ) "(" "EL" "," "source" "," "sink" ")" ")" ) ")" ) if (Bool "sink" ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" "EL" "," "source" ")" ")" ))) otherwise "EL"; end; :: deftheorem defines :::"FF:Step"::: GLIB_005:def 18 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "sink")) "," (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "sink")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" )))) "implies" (Bool (Set ($#k11_glib_005 :::"FF:Step"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_glib_005 :::"FF:PushFlow"::: ) "(" (Set (Var "EL")) "," (Set "(" ($#k7_glib_005 :::"AP:GetAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "sink")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_glib_005 :::"AP:FindAugPath"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) ")" ")" ))))) "implies" (Bool (Set ($#k11_glib_005 :::"FF:Step"::: ) "(" (Set (Var "EL")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "EL"))) ")" ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode :::"FF:ELabelingSeq"::: "of" "G" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_005:def 19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_hidden :::"FF:ELabeling":::) "of" "G")); end; :: deftheorem defines :::"FF:ELabelingSeq"::: GLIB_005:def 19 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_glib_005 :::"FF:ELabelingSeq"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")))) ")" ))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "ES" be ($#m3_glib_005 :::"FF:ELabelingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "ES" ($#k1_funct_1 :::"."::: ) "n") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "ES" be ($#m3_glib_005 :::"FF:ELabelingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "ES" ($#k1_funct_1 :::"."::: ) "n") -> (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G") ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "ES" be ($#m3_glib_005 :::"FF:ELabelingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "ES" ($#k1_funct_1 :::"."::: ) "n") -> ($#v1_partfun1 :::"total"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "source", "sink" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"FF:CompSeq"::: "(" "G" "," "source" "," "sink" ")" -> ($#m3_glib_005 :::"FF:ELabelingSeq"::: ) "of" "G" means :: GLIB_005:def 20 (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_glib_005 :::"FF:Step"::: ) "(" (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," "source" "," "sink" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"FF:CompSeq"::: GLIB_005:def 20 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m3_glib_005 :::"FF:ELabelingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_glib_005 :::"FF:CompSeq"::: ) "(" (Set (Var "G")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_glib_005 :::"FF:Step"::: ) "(" (Set "(" (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "source")) "," (Set (Var "sink")) ")" )) ")" ) ")" ) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "sink", "source" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"FF:MaxFlow"::: "(" "G" "," "source" "," "sink" ")" -> ($#m1_hidden :::"FF:ELabeling":::) "of" "G" equals :: GLIB_005:def 21 (Set (Set "(" ($#k12_glib_005 :::"FF:CompSeq"::: ) "(" "G" "," "source" "," "sink" ")" ")" ) ($#k40_glib_000 :::".Result()"::: ) ); end; :: deftheorem defines :::"FF:MaxFlow"::: GLIB_005:def 21 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "sink")) "," (Set (Var "source")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k13_glib_005 :::"FF:MaxFlow"::: ) "(" (Set (Var "G")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_glib_005 :::"FF:CompSeq"::: ) "(" (Set (Var "G")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ")" ) ($#k40_glib_000 :::".Result()"::: ) )))); begin theorem :: GLIB_005:11 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "EL")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool (Set (Var "source")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Bool "not" (Set (Var "sink")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))))) "holds" (Bool (Set (Set (Var "EL")) ($#k1_glib_005 :::".flow"::: ) "(" (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "EL")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "V")) "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "V")) ")" ) ")" ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_uproots :::"Sum"::: ) (Set "(" (Set (Var "EL")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "V")) ")" ) "," (Set (Var "V")) ")" ")" ) ")" ) ")" ))))))) ; theorem :: GLIB_005:12 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "EL")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool (Set (Var "source")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Bool "not" (Set (Var "sink")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))))) "holds" (Bool (Set (Set (Var "EL")) ($#k1_glib_005 :::".flow"::: ) "(" (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "V")) "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "V")) ")" ) ")" ")" ) ")" ))))))) ; theorem :: GLIB_005:13 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) & (Bool (Set (Var "W")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "W")) ($#k9_glib_005 :::".tolerance"::: ) (Set (Var "EL"))))))) ; theorem :: GLIB_005:14 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "source")) ($#r1_hidden :::"<>"::: ) (Set (Var "sink"))) & (Bool (Set (Var "EL")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool (Set (Var "P")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool (Set (Var "P")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))) "holds" (Bool (Set ($#k10_glib_005 :::"FF:PushFlow"::: ) "(" (Set (Var "EL")) "," (Set (Var "P")) ")" ) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))))))) ; theorem :: GLIB_005:15 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "source")) ($#r1_hidden :::"<>"::: ) (Set (Var "sink"))) & (Bool (Set (Var "P")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool (Set (Var "P")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL")))) "holds" (Bool (Set (Set "(" (Set (Var "EL")) ($#k1_glib_005 :::".flow"::: ) "(" (Set (Var "source")) "," (Set (Var "sink")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "P")) ($#k9_glib_005 :::".tolerance"::: ) (Set (Var "EL")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_glib_005 :::"FF:PushFlow"::: ) "(" (Set (Var "EL")) "," (Set (Var "P")) ")" ")" ) ($#k1_glib_005 :::".flow"::: ) "(" (Set (Var "source")) "," (Set (Var "sink")) ")" )))))) ; theorem :: GLIB_005:16 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "source")) ($#r1_hidden :::"<>"::: ) (Set (Var "sink")))) "holds" (Bool (Set (Set "(" ($#k12_glib_005 :::"FF:CompSeq"::: ) "(" (Set (Var "G")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink")))))) ; theorem :: GLIB_005:17 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "source")) ($#r1_hidden :::"<>"::: ) (Set (Var "sink")))) "holds" (Bool (Set ($#k12_glib_005 :::"FF:CompSeq"::: ) "(" (Set (Var "G")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ) "is" ($#v13_glib_000 :::"halting"::: ) ))) ; theorem :: GLIB_005:18 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "EL")) "being" ($#m1_hidden :::"FF:ELabeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "EL")) ($#r1_glib_005 :::"has_valid_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) & (Bool "(" "for" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "holds" (Bool "(" "not" (Bool (Set (Var "P")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))) "or" "not" (Bool (Set (Var "P")) ($#r5_glib_005 :::"is_augmenting_wrt"::: ) (Set (Var "EL"))) ")" ) ")" )) "holds" (Bool (Set (Var "EL")) ($#r2_glib_005 :::"has_maximum_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink")))))) ; theorem :: GLIB_005:19 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_005 :::"natural-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "source")) "," (Set (Var "sink")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "sink")) ($#r1_hidden :::"<>"::: ) (Set (Var "source")))) "holds" (Bool (Set ($#k13_glib_005 :::"FF:MaxFlow"::: ) "(" (Set (Var "G")) "," (Set (Var "source")) "," (Set (Var "sink")) ")" ) ($#r2_glib_005 :::"has_maximum_flow_from"::: ) (Set (Var "source")) "," (Set (Var "sink"))))) ;