:: GLIB_004 semantic presentation begin theorem :: GLIB_004:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "g")) ")" )))) ; theorem :: GLIB_004:2 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GLIB_004:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B"))) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "b2"))))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_uproots :::"Sum"::: ) (Set (Var "b1")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_uproots :::"Sum"::: ) (Set (Var "b2")) ")" ))))))) ; theorem :: GLIB_004:4 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: GLIB_004:5 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b2")))))) ; theorem :: GLIB_004:6 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b2")))))) ; theorem :: GLIB_004:7 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A2")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b2"))))))) ; theorem :: GLIB_004:8 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" )))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: GLIB_004:9 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" )))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_uproots :::"Sum"::: ) (Set (Var "b1")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; begin definitionlet "G1" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "G2" be ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Const "G1")); let "v" be ($#m1_hidden :::"set"::: ) ; pred "G2" :::"is_mincost_DTree_rooted_at"::: "v" means :: GLIB_004:def 1 (Bool "(" (Bool "G2" "is" ($#v3_glib_002 :::"Tree-like"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G2" (Bool "ex" (Set (Var "W2")) "being" ($#m3_glib_001 :::"DPath":::) "of" "G2" "st" (Bool "(" (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) "v" "," (Set (Var "x"))) & (Bool "(" "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"DPath":::) "of" "G1" "st" (Bool (Bool (Set (Var "W1")) ($#r1_glib_001 :::"is_Walk_from"::: ) "v" "," (Set (Var "x")))) "holds" (Bool (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "W1")) ($#k10_glib_003 :::".cost()"::: ) )) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"is_mincost_DTree_rooted_at"::: GLIB_004:def 1 : (Bool "for" (Set (Var "G1")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "G2")) ($#r1_glib_004 :::"is_mincost_DTree_rooted_at"::: ) (Set (Var "v"))) "iff" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v3_glib_002 :::"Tree-like"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) (Bool "ex" (Set (Var "W2")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G2")) "st" (Bool "(" (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "v")) "," (Set (Var "x"))) & (Bool "(" "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "v")) "," (Set (Var "x")))) "holds" (Bool (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "W1")) ($#k10_glib_003 :::".cost()"::: ) )) ")" ) ")" )) ")" ) ")" ) ")" )))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "W" be ($#m3_glib_001 :::"DPath":::) "of" (Set (Const "G")); let "x", "y" be ($#m1_hidden :::"set"::: ) ; pred "W" :::"is_mincost_DPath_from"::: "x" "," "y" means :: GLIB_004:def 2 (Bool "(" (Bool "W" ($#r1_glib_001 :::"is_Walk_from"::: ) "x" "," "y") & (Bool "(" "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"DPath":::) "of" "G" "st" (Bool (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) "x" "," "y")) "holds" (Bool (Set "W" ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"is_mincost_DPath_from"::: GLIB_004:def 2 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool "(" "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) )) ")" ) ")" ) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; func "G" :::".min_DPath_cost"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) means :: GLIB_004:def 3 (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DPath":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "W")) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) "x" "," "y") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) )) ")" )) if (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" "G" "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) "x" "," "y")) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::".min_DPath_cost"::: GLIB_004:def 3 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_004 :::".min_DPath_cost"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "W")) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) )) ")" )) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y")))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_004 :::".min_DPath_cost"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" )))); definitionfunc :::"WGraphSelectors"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_004:def 4 (Set ($#k10_domain_1 :::"{"::: ) (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) "," (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) "," (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) "," (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) "," (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) ($#k10_domain_1 :::"}"::: ) ); end; :: deftheorem defines :::"WGraphSelectors"::: GLIB_004:def 4 : (Bool (Set ($#k2_glib_004 :::"WGraphSelectors"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_domain_1 :::"{"::: ) (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) "," (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) "," (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) "," (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) "," (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) ($#k10_domain_1 :::"}"::: ) )); registrationlet "G" be ($#m1_hidden :::"WGraph":::); cluster (Set "G" ($#k5_relat_1 :::"|"::: ) (Set ($#k2_glib_004 :::"WGraphSelectors"::: ) )) -> ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); func "G" :::".allWSubgraphs()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: GLIB_004:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "G2")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_glib_004 :::"WGraphSelectors"::: ) )) ")" )) ")" )); end; :: deftheorem defines :::".allWSubgraphs()"::: GLIB_004:def 5 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_glib_004 :::".allWSubgraphs()"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "G2")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_glib_004 :::"WGraphSelectors"::: ) )) ")" )) ")" )) ")" ))); registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"WGraph":::); cluster (Set "G" ($#k3_glib_004 :::".allWSubgraphs()"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k3_glib_004 :::".allWSubgraphs()"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m1_glib_000 :::"WSubgraph":::) "of" "G"; end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); func "G" :::".cost()"::: -> ($#m1_subset_1 :::"Real":::) equals :: GLIB_004:def 6 (Set ($#k3_uproots :::"Sum"::: ) (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" )); end; :: deftheorem defines :::".cost()"::: GLIB_004:def 6 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_glib_004 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" )))); theorem :: GLIB_004:10 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G2")) "being" ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#m2_glib_000 :::"removeEdge":::) "of" (Set (Var "G1")) "," (Set (Var "e")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))))) "holds" (Bool (Set (Set (Var "G1")) ($#k4_glib_004 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G2")) ($#k4_glib_004 :::".cost()"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G1")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e")) ")" )))))) ; theorem :: GLIB_004:11 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "V1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "E1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "V1")) ")" ) (Bool "for" (Set (Var "G1")) "being" ($#m2_glib_000 :::"inducedWSubgraph":::) "of" (Set (Var "G")) "," (Set (Var "V1")) "," (Set (Var "E1")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedWSubgraph":::) "of" (Set (Var "G")) "," (Set (Var "V1")) "," (Set (Set (Var "E1")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) "st" (Bool (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "E1")))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "V1"))))) "holds" (Bool (Set (Set "(" (Set (Var "G1")) ($#k4_glib_004 :::".cost()"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k4_glib_004 :::".cost()"::: ) )))))))) ; theorem :: GLIB_004:12 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "W")) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k3_glib_001 :::".first()"::: ) ) "," (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k4_glib_001 :::".last()"::: ) )))))) ; theorem :: GLIB_004:13 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W1")) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "W2")) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Set (Var "W1")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) ))))) ; theorem :: GLIB_004:14 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"DPath":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W")) ($#r2_glib_004 :::"is_mincost_DPath_from"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Set (Var "G")) ($#k1_glib_004 :::".min_DPath_cost"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) ))))) ; begin definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode DIJK:Labeling of "G" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "X1", "X3" be ($#m1_hidden :::"set"::: ) ; let "X2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "X1")) "," (Set (Const "X3")) ")" ")" ) "," (Set (Const "X2")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "X1" "," "X3" ")" ); end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"DIJK:Labeling":::) "of" (Set (Const "G")); cluster (Set "L" ($#k1_xtuple_0 :::"`1"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "L" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "L" be ($#m1_subset_1 :::"DIJK:Labeling":::) "of" (Set (Const "G")); func :::"DIJK:NextBestEdges"::: "L" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) means :: GLIB_004:def 7 (Bool "for" (Set (Var "e1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "e1")) ($#r4_glib_000 :::"DSJoins"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" )) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) "," "G") & (Bool "(" "for" (Set (Var "e2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e2")) ($#r4_glib_000 :::"DSJoins"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" )) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) "," "G")) "holds" (Bool (Set (Set "(" (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e1")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e1")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e2")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e2")) ")" ))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"DIJK:NextBestEdges"::: GLIB_004:def 7 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"DIJK:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "e1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "e1")) ($#r4_glib_000 :::"DSJoins"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" )) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) "," (Set (Var "G"))) & (Bool "(" "for" (Set (Var "e2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e2")) ($#r4_glib_000 :::"DSJoins"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" )) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e1")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e1")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e2")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e2")) ")" ))) ")" ) ")" ) ")" )) ")" )))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "L" be ($#m1_subset_1 :::"DIJK:Labeling":::) "of" (Set (Const "G")); func :::"DIJK:Step"::: "L" -> ($#m1_subset_1 :::"DIJK:Labeling":::) "of" "G" equals :: GLIB_004:def 8 "L" if (Bool (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) "L") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) "L" ")" ) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set "(" "L" ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) "L" ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) "L" ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" "L" ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) "L" ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"DIJK:Step"::: GLIB_004:def 8 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"DIJK:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "L"))) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool (Set ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "L")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" ")" ))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "src" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"DIJK:Init"::: "src" -> ($#m1_subset_1 :::"DIJK:Labeling":::) "of" "G" equals :: GLIB_004:def 9 (Set ($#k4_tarski :::"["::: ) (Set "(" "src" ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"DIJK:Init"::: GLIB_004:def 9 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_glib_004 :::"DIJK:Init"::: ) (Set (Var "src"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "src")) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) )))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); mode :::"DIJK:LabelingSeq"::: "of" "G" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_004:def 10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"DIJK:Labeling":::) "of" "G")); end; :: deftheorem defines :::"DIJK:LabelingSeq"::: GLIB_004:def 10 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_glib_004 :::"DIJK:LabelingSeq"::: ) "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_subset_1 :::"DIJK:Labeling":::) "of" (Set (Var "G")))) ")" ))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "S" be ($#m2_glib_004 :::"DIJK:LabelingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "S" :::"."::: "n" -> ($#m1_subset_1 :::"DIJK:Labeling":::) "of" "G"; end; definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "src" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"DIJK:CompSeq"::: "src" -> ($#m2_glib_004 :::"DIJK:LabelingSeq"::: ) "of" "G" means :: GLIB_004:def 11 (Bool "(" (Bool (Set it ($#k9_glib_004 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_glib_004 :::"DIJK:Init"::: ) "src")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k9_glib_004 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_004 :::"DIJK:Step"::: ) (Set "(" it ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"DIJK:CompSeq"::: GLIB_004:def 11 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m2_glib_004 :::"DIJK:LabelingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k9_glib_004 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_glib_004 :::"DIJK:Init"::: ) (Set (Var "src")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k9_glib_004 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_004 :::"DIJK:Step"::: ) (Set "(" (Set (Var "b3")) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "src" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"DIJK:SSSP"::: "(" "G" "," "src" ")" -> ($#m1_subset_1 :::"DIJK:Labeling":::) "of" "G" equals :: GLIB_004:def 12 (Set (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) "src" ")" ) ($#k40_glib_000 :::".Result()"::: ) ); end; :: deftheorem defines :::"DIJK:SSSP"::: GLIB_004:def 12 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k11_glib_004 :::"DIJK:SSSP"::: ) "(" (Set (Var "G")) "," (Set (Var "src")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k40_glib_000 :::".Result()"::: ) )))); begin theorem :: GLIB_004:15 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"DIJK:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )))) "implies" (Bool (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "implies" (Bool (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ")" ))) ; theorem :: GLIB_004:16 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"DIJK:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k5_glib_004 :::"`1"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ))) & (Bool (Set (Set (Var "L")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k7_glib_004 :::"DIJK:Step"::: ) (Set (Var "L")) ")" ) ($#k3_domain_1 :::"`2"::: ) )) ")" ))) ; theorem :: GLIB_004:17 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k8_glib_004 :::"DIJK:Init"::: ) (Set (Var "src")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "src")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GLIB_004:18 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "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 "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "j")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "j")) ")" ) ($#k3_domain_1 :::"`2"::: ) )) ")" )))) ; theorem :: GLIB_004:19 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "src"))))))) ; theorem :: GLIB_004:20 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k6_glib_004 :::"DIJK:NextBestEdges"::: ) (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "src")))) ")" )))) ; theorem :: GLIB_004:21 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "s")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "s")) ")" ) ")" ) ")" ))))) ; theorem :: GLIB_004:22 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "src")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "src")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ")" )))))) ; theorem :: GLIB_004:23 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedWSubgraph":::) "of" (Set (Var "G")) "," (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "s")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )) "," (Set (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "s")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) "holds" (Bool "(" (Bool (Set (Var "G2")) ($#r1_glib_004 :::"is_mincost_DTree_rooted_at"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "s")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )))) "holds" (Bool (Set (Set (Var "G")) ($#k1_glib_004 :::".min_DPath_cost"::: ) "(" (Set (Var "s")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "s")) ")" ) ($#k9_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" ))))) ; theorem :: GLIB_004:24 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "s"))) "is" ($#v13_glib_000 :::"halting"::: ) ))) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "src" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); cluster (Set ($#k10_glib_004 :::"DIJK:CompSeq"::: ) "src") -> ($#v13_glib_000 :::"halting"::: ) ; end; theorem :: GLIB_004:25 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_glib_004 :::"DIJK:CompSeq"::: ) (Set (Var "s")) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "s")) ")" ))))) ; theorem :: GLIB_004:26 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k11_glib_004 :::"DIJK:SSSP"::: ) "(" (Set (Var "G")) "," (Set (Var "s")) ")" ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "s")))))) ; theorem :: GLIB_004:27 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedWSubgraph":::) "of" (Set (Var "G")) "," (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k11_glib_004 :::"DIJK:SSSP"::: ) "(" (Set (Var "G")) "," (Set (Var "s")) ")" ")" ) ($#k5_glib_004 :::"`1"::: ) ")" )) "," (Set (Set "(" ($#k11_glib_004 :::"DIJK:SSSP"::: ) "(" (Set (Var "G")) "," (Set (Var "s")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) "holds" (Bool "(" (Bool (Set (Var "G2")) ($#r1_glib_004 :::"is_mincost_DTree_rooted_at"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "s"))))) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G")) ($#k1_glib_004 :::".min_DPath_cost"::: ) "(" (Set (Var "s")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k11_glib_004 :::"DIJK:SSSP"::: ) "(" (Set (Var "G")) "," (Set (Var "s")) ")" ")" ) ($#k5_glib_004 :::"`1"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" ) ")" )))) ; begin definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode PRIM:Labeling of "G" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"PRIM:Labeling":::) "of" (Set (Const "G")); cluster (Set "L" ($#k1_xtuple_0 :::"`1"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "L" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "L" be ($#m1_subset_1 :::"PRIM:Labeling":::) "of" (Set (Const "G")); func :::"PRIM:NextBestEdges"::: "L" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) means :: GLIB_004:def 13 (Bool "for" (Set (Var "e1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "e1")) ($#r3_glib_000 :::"SJoins"::: ) (Set "L" ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" "L" ($#k2_domain_1 :::"`1"::: ) ")" )) "," "G") & (Bool "(" "for" (Set (Var "e2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e2")) ($#r3_glib_000 :::"SJoins"::: ) (Set "L" ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" "L" ($#k2_domain_1 :::"`1"::: ) ")" )) "," "G")) "holds" (Bool (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e2")))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"PRIM:NextBestEdges"::: GLIB_004:def 13 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"PRIM:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "e1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "e1")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ")" )) "," (Set (Var "G"))) & (Bool "(" "for" (Set (Var "e2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e2")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ")" )) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e2")))) ")" ) ")" ) ")" )) ")" )))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); func :::"PRIM:Init"::: "G" -> ($#m1_subset_1 :::"PRIM:Labeling":::) "of" "G" equals :: GLIB_004:def 14 (Set ($#k4_tarski :::"["::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"PRIM:Init"::: GLIB_004:def 14 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) "holds" (Bool (Set ($#k13_glib_004 :::"PRIM:Init"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "L" be ($#m1_subset_1 :::"PRIM:Labeling":::) "of" (Set (Const "G")); func :::"PRIM:Step"::: "L" -> ($#m1_subset_1 :::"PRIM:Labeling":::) "of" "G" equals :: GLIB_004:def 15 "L" if (Bool (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) "L") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "L" ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) "L" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set "(" "L" ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) "L" ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ) if (Bool "(" (Bool (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) "L") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) "L" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set "L" ($#k2_domain_1 :::"`1"::: ) )) ")" ) otherwise (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "L" ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) "L" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set "(" "L" ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) "L" ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"PRIM:Step"::: GLIB_004:def 15 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"PRIM:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k14_glib_004 :::"PRIM:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "L"))) ")" & "(" (Bool (Bool (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ))) "implies" (Bool (Set ($#k14_glib_004 :::"PRIM:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "L")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) & (Bool "(" "not" (Bool (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" "not" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) )) ")" )) "implies" (Bool (Set ($#k14_glib_004 :::"PRIM:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "L")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" ")" ))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); mode :::"PRIM:LabelingSeq"::: "of" "G" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_004:def 16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"PRIM:Labeling":::) "of" "G")); end; :: deftheorem defines :::"PRIM:LabelingSeq"::: GLIB_004:def 16 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_glib_004 :::"PRIM:LabelingSeq"::: ) "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_subset_1 :::"PRIM:Labeling":::) "of" (Set (Var "G")))) ")" ))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "S" be ($#m3_glib_004 :::"PRIM:LabelingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "S" :::"."::: "n" -> ($#m1_subset_1 :::"PRIM:Labeling":::) "of" "G"; end; definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); func :::"PRIM:CompSeq"::: "G" -> ($#m3_glib_004 :::"PRIM:LabelingSeq"::: ) "of" "G" means :: GLIB_004:def 17 (Bool "(" (Bool (Set it ($#k15_glib_004 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_glib_004 :::"PRIM:Init"::: ) "G")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k15_glib_004 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_glib_004 :::"PRIM:Step"::: ) (Set "(" it ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"PRIM:CompSeq"::: GLIB_004:def 17 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "b2")) "being" ($#m3_glib_004 :::"PRIM:LabelingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k15_glib_004 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_glib_004 :::"PRIM:Init"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k15_glib_004 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_glib_004 :::"PRIM:Step"::: ) (Set "(" (Set (Var "b2")) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); func :::"PRIM:MST"::: "G" -> ($#m1_subset_1 :::"PRIM:Labeling":::) "of" "G" equals :: GLIB_004:def 18 (Set (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) "G" ")" ) ($#k40_glib_000 :::".Result()"::: ) ); end; :: deftheorem defines :::"PRIM:MST"::: GLIB_004:def 18 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) "holds" (Bool (Set ($#k17_glib_004 :::"PRIM:MST"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k40_glib_000 :::".Result()"::: ) ))); theorem :: GLIB_004:28 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"PRIM:Labeling":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ))) & (Bool (Set ($#k14_glib_004 :::"PRIM:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "L")) ($#k3_domain_1 :::"`2"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set (Var "L")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )))) ; theorem :: GLIB_004:29 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"PRIM:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k14_glib_004 :::"PRIM:Step"::: ) (Set (Var "L")) ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set (Var "L")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k14_glib_004 :::"PRIM:Step"::: ) (Set (Var "L")) ")" ) ($#k3_domain_1 :::"`2"::: ) )) ")" ))) ; theorem :: GLIB_004:30 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )) & (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ))) ")" ))) ; theorem :: GLIB_004:31 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G1")) "," (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G1")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G1")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) "holds" (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) )))) ; theorem :: GLIB_004:32 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedSubgraph":::) "of" (Set (Var "G1")) "," (Set "(" (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G1")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) "holds" (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) )))) ; registrationlet "G1" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "n" be ($#m1_hidden :::"Nat":::); cluster -> ($#v1_glib_002 :::"connected"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G1" "," (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) "G1" ")" ) ($#k15_glib_004 :::"."::: ) "n" ")" ) ($#k2_domain_1 :::"`1"::: ) ) "," (Set "G1" ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) "G1" ")" ) ($#k15_glib_004 :::"."::: ) "n" ")" ) ($#k2_domain_1 :::"`1"::: ) ")" )); end; registrationlet "G1" be ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "n" be ($#m1_hidden :::"Nat":::); cluster -> ($#v1_glib_002 :::"connected"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G1" "," (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) "G1" ")" ) ($#k15_glib_004 :::"."::: ) "n" ")" ) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) "G1" ")" ) ($#k15_glib_004 :::"."::: ) "n" ")" ) ($#k3_domain_1 :::"`2"::: ) ); end; theorem :: GLIB_004:33 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ")" ))))) ; theorem :: GLIB_004:34 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (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 "(" (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "j")) ")" ) ($#k2_domain_1 :::"`1"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "j")) ")" ) ($#k3_domain_1 :::"`2"::: ) )) ")" ))) ; theorem :: GLIB_004:35 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k12_glib_004 :::"PRIM:NextBestEdges"::: ) (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ")" ))) ")" ))) ; theorem :: GLIB_004:36 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: GLIB_004:37 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) "holds" (Bool "(" (Bool (Set ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G"))) "is" ($#v13_glib_000 :::"halting"::: ) ) & (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ")" ) ")" ))) ")" )) ; theorem :: GLIB_004:38 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G1")) "," (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G1")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G1")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) "holds" (Bool (Set (Var "G2")) "is" ($#v3_glib_002 :::"Tree-like"::: ) )))) ; theorem :: GLIB_004:39 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) "holds" (Bool (Set (Set "(" ($#k17_glib_004 :::"PRIM:MST"::: ) (Set (Var "G")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); 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"::: ) ($#v9_glib_000 :::"spanning"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v7_glib_003 :::"real-weighted"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G1" be ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "G2" be ($#v9_glib_000 :::"spanning"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Const "G1")); attr "G2" is :::"min-cost"::: means :: GLIB_004:def 19 (Bool "for" (Set (Var "G3")) "being" ($#v9_glib_000 :::"spanning"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_glib_000 :::"WSubgraph":::) "of" "G1" "holds" (Bool (Set "G2" ($#k4_glib_004 :::".cost()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G3")) ($#k4_glib_004 :::".cost()"::: ) ))); end; :: deftheorem defines :::"min-cost"::: GLIB_004:def 19 : (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#v9_glib_000 :::"spanning"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v1_glib_004 :::"min-cost"::: ) ) "iff" (Bool "for" (Set (Var "G3")) "being" ($#v9_glib_000 :::"spanning"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) "holds" (Bool (Set (Set (Var "G2")) ($#k4_glib_004 :::".cost()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G3")) ($#k4_glib_004 :::".cost()"::: ) ))) ")" ))); registrationlet "G1" be ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); 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"::: ) ($#v3_glib_000 :::"loopless"::: ) ($#v5_glib_000 :::"non-multi"::: ) ($#v6_glib_000 :::"non-Dmulti"::: ) ($#v7_glib_000 :::"simple"::: ) ($#v8_glib_000 :::"Dsimple"::: ) ($#v9_glib_000 :::"spanning"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v2_glib_002 :::"acyclic"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#v1_glib_004 :::"min-cost"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G1"; end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); mode minimumSpanningTree of "G" is ($#v9_glib_000 :::"spanning"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#v1_glib_004 :::"min-cost"::: ) ($#m1_glib_000 :::"WSubgraph":::) "of" "G"; end; begin theorem :: GLIB_004:40 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G3")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "G3")) "is" ($#m1_glib_000 :::"minimumSpanningTree":::) "of" (Set (Var "G1"))) & (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "G3")) "is" ($#m1_glib_000 :::"minimumSpanningTree":::) "of" (Set (Var "G2"))))) ; theorem :: GLIB_004:41 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G1")) "being" ($#m1_glib_000 :::"minimumSpanningTree":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "G2")) "being" ($#m1_hidden :::"WGraph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "G2")) "is" ($#m1_glib_000 :::"minimumSpanningTree":::) "of" (Set (Var "G")))))) ; theorem :: GLIB_004:42 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_glib_004 :::"PRIM:CompSeq"::: ) (Set (Var "G")) ")" ) ($#k15_glib_004 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k17_glib_004 :::"PRIM:MST"::: ) (Set (Var "G")) ")" ) ($#k3_domain_1 :::"`2"::: ) )))) ; theorem :: GLIB_004:43 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedWSubgraph":::) "of" (Set (Var "G1")) "," (Set (Set "(" ($#k17_glib_004 :::"PRIM:MST"::: ) (Set (Var "G1")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) "," (Set (Set "(" ($#k17_glib_004 :::"PRIM:MST"::: ) (Set (Var "G1")) ")" ) ($#k3_domain_1 :::"`2"::: ) ) "holds" (Bool (Set (Var "G2")) "is" ($#m1_glib_000 :::"minimumSpanningTree":::) "of" (Set (Var "G1"))))) ;