:: GLIB_003 semantic presentation begin definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "fs" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "fss" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "fs")); :: original: :::"Seq"::: redefine func :::"Seq"::: "fss" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; theorem :: GLIB_003:1 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "," (Set (Var "x10")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x2")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x3")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x4")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x5")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x6")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x7")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x8")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x9")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x10")) ($#k9_finseq_1 :::"*>"::: ) )))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 10)) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Var "x3"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Var "x4"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 5)) ($#r1_hidden :::"="::: ) (Set (Var "x5"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 6)) ($#r1_hidden :::"="::: ) (Set (Var "x6"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 7)) ($#r1_hidden :::"="::: ) (Set (Var "x7"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 8)) ($#r1_hidden :::"="::: ) (Set (Var "x8"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 9)) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 10)) ($#r1_hidden :::"="::: ) (Set (Var "x10"))) ")" ))) ; theorem :: GLIB_003:2 (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "fss")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "fs"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "fs")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k1_glib_003 :::"Seq"::: ) (Set (Var "fss")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "fs")))))) ; begin definitionfunc :::"WeightSelector"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_003:def 1 (Num 5); func :::"ELabelSelector"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_003:def 2 (Num 6); func :::"VLabelSelector"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_003:def 3 (Num 7); end; :: deftheorem defines :::"WeightSelector"::: GLIB_003:def 1 : (Bool (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 5)); :: deftheorem defines :::"ELabelSelector"::: GLIB_003:def 2 : (Bool (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 6)); :: deftheorem defines :::"VLabelSelector"::: GLIB_003:def 3 : (Bool (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)); definitionlet "G" be ($#m1_hidden :::"GraphStruct":::); attr "G" is :::"[Weighted]"::: means :: GLIB_003:def 4 (Bool "(" (Bool (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "G")) & (Bool (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_003 :::"WeightSelector"::: ) )) "is" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) ")" ); attr "G" is :::"[ELabeled]"::: means :: GLIB_003:def 5 (Bool "(" (Bool (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "G")) & (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_003 :::"ELabelSelector"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) ")" )) ")" ); attr "G" is :::"[VLabeled]"::: means :: GLIB_003:def 6 (Bool "(" (Bool (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "G")) & (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_003 :::"VLabelSelector"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G")) ")" )) ")" ); end; :: deftheorem defines :::"[Weighted]"::: GLIB_003:def 4 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_glib_003 :::"[Weighted]"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_003 :::"WeightSelector"::: ) )) "is" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) ")" ) ")" )); :: deftheorem defines :::"[ELabeled]"::: GLIB_003:def 5 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_glib_003 :::"[ELabeled]"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_003 :::"ELabelSelector"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) ")" )) ")" ) ")" )); :: deftheorem defines :::"[VLabeled]"::: GLIB_003:def 6 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_003 :::"[VLabeled]"::: ) ) "iff" (Bool "(" (Bool (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_003 :::"VLabelSelector"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) ")" )) ")" ) ")" )); 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode WGraph is ($#v1_glib_003 :::"[Weighted]"::: ) ($#m1_hidden :::"_Graph":::); mode EGraph is ($#v2_glib_003 :::"[ELabeled]"::: ) ($#m1_hidden :::"_Graph":::); mode VGraph is ($#v3_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"_Graph":::); mode WEGraph is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#m1_hidden :::"_Graph":::); mode WVGraph is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"_Graph":::); mode EVGraph is ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"_Graph":::); mode WEVGraph is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"_Graph":::); end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); func :::"the_Weight_of"::: "G" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G") equals :: GLIB_003:def 7 (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_003 :::"WeightSelector"::: ) )); end; :: deftheorem defines :::"the_Weight_of"::: GLIB_003:def 7 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) "holds" (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_003 :::"WeightSelector"::: ) )))); definitionlet "G" be ($#m1_hidden :::"EGraph":::); func :::"the_ELabel_of"::: "G" -> ($#m1_hidden :::"Function":::) equals :: GLIB_003:def 8 (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_003 :::"ELabelSelector"::: ) )); end; :: deftheorem defines :::"the_ELabel_of"::: GLIB_003:def 8 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) "holds" (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_003 :::"ELabelSelector"::: ) )))); definitionlet "G" be ($#m1_hidden :::"VGraph":::); func :::"the_VLabel_of"::: "G" -> ($#m1_hidden :::"Function":::) equals :: GLIB_003:def 9 (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_003 :::"VLabelSelector"::: ) )); end; :: deftheorem defines :::"the_VLabel_of"::: GLIB_003:def 9 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) "holds" (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_003 :::"VLabelSelector"::: ) )))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_000 :::"[Graph-like]"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_000 :::"[Graph-like]"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_000 :::"[Graph-like]"::: ) ; end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_000 :::"finite"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_000 :::"finite"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_000 :::"finite"::: ) ; end; registrationlet "G" be ($#v3_glib_000 :::"loopless"::: ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v3_glib_000 :::"loopless"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v3_glib_000 :::"loopless"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v3_glib_000 :::"loopless"::: ) ; end; registrationlet "G" be ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v4_glib_000 :::"trivial"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v4_glib_000 :::"trivial"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v4_glib_000 :::"trivial"::: ) ; end; registrationlet "G" be ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ; end; registrationlet "G" be ($#v5_glib_000 :::"non-multi"::: ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v5_glib_000 :::"non-multi"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v5_glib_000 :::"non-multi"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v5_glib_000 :::"non-multi"::: ) ; end; registrationlet "G" be ($#v6_glib_000 :::"non-Dmulti"::: ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v6_glib_000 :::"non-Dmulti"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v6_glib_000 :::"non-Dmulti"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v6_glib_000 :::"non-Dmulti"::: ) ; end; registrationlet "G" be ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_002 :::"connected"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_002 :::"connected"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_002 :::"connected"::: ) ; end; registrationlet "G" be ($#v2_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_002 :::"acyclic"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_002 :::"acyclic"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_002 :::"acyclic"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"WGraph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_003 :::"[Weighted]"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_003 :::"[Weighted]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G"))); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v1_glib_003 :::"[Weighted]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "WL" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "W" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G")) ")" ) "," (Set (Const "WL")); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "W" ")" ) -> ($#v1_glib_003 :::"[Weighted]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"EGraph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_003 :::"[ELabeled]"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_003 :::"[ELabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "Y" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G")) ")" ) "," (Set (Const "Y")); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_003 :::"[ELabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G"))); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v2_glib_003 :::"[ELabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"VGraph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v3_glib_003 :::"[VLabeled]"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v3_glib_003 :::"[VLabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "Y" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G")) ")" ) "," (Set (Const "Y")); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v3_glib_003 :::"[VLabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G"))); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v3_glib_003 :::"[VLabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) -> ($#v2_glib_003 :::"[ELabeled]"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) -> ($#v3_glib_003 :::"[VLabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); let "G2" be ($#v1_glib_003 :::"[Weighted]"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Const "G")); attr "G2" is :::"weight-inheriting"::: means :: GLIB_003:def 10 (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) "G2") ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) "G2" ")" ))); end; :: deftheorem defines :::"weight-inheriting"::: GLIB_003:def 10 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#v1_glib_003 :::"[Weighted]"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v4_glib_003 :::"weight-inheriting"::: ) ) "iff" (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")) ")" ))) ")" ))); definitionlet "G" be ($#m1_hidden :::"EGraph":::); let "G2" be ($#v2_glib_003 :::"[ELabeled]"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Const "G")); attr "G2" is :::"elabel-inheriting"::: means :: GLIB_003:def 11 (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) "G2") ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) "G" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) "G2" ")" ))); end; :: deftheorem defines :::"elabel-inheriting"::: GLIB_003:def 11 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#v2_glib_003 :::"[ELabeled]"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v5_glib_003 :::"elabel-inheriting"::: ) ) "iff" (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")) ")" ))) ")" ))); definitionlet "G" be ($#m1_hidden :::"VGraph":::); let "G2" be ($#v3_glib_003 :::"[VLabeled]"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Const "G")); attr "G2" is :::"vlabel-inheriting"::: means :: GLIB_003:def 12 (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) "G2") ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) "G" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k24_glib_000 :::"the_Vertices_of"::: ) "G2" ")" ))); end; :: deftheorem defines :::"vlabel-inheriting"::: GLIB_003:def 12 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#v3_glib_003 :::"[VLabeled]"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v6_glib_003 :::"vlabel-inheriting"::: ) ) "iff" (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")) ")" ))) ")" ))); registrationlet "G" be ($#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"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"EGraph":::); 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"VGraph":::); 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]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"WEGraph":::); 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"WVGraph":::); 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]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"EVGraph":::); 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"WEVGraph":::); 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); mode WSubgraph of "G" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"EGraph":::); mode ESubgraph of "G" is ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"VGraph":::); mode VSubgraph of "G" is ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"WEGraph":::); mode WESubgraph of "G" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"WVGraph":::); mode WVSubgraph of "G" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"EVGraph":::); mode EVSubgraph of "G" is ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"WEVGraph":::); mode WEVSubgraph of "G" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"WGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"EGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"VGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"WEGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"WVGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"EVGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"WEVGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode inducedWSubgraph of "G" "," "V" "," "E" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"EGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode inducedESubgraph of "G" "," "V" "," "E" is ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"VGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode inducedVSubgraph of "G" "," "V" "," "E" is ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"WEGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode inducedWESubgraph of "G" "," "V" "," "E" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"WVGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode inducedWVSubgraph of "G" "," "V" "," "E" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"EVGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode inducedEVSubgraph of "G" "," "V" "," "E" is ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"WEVGraph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode inducedWEVSubgraph of "G" "," "V" "," "E" is ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedWSubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedWSubgraph":::) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; definitionlet "G" be ($#m1_hidden :::"EGraph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedESubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedESubgraph":::) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; definitionlet "G" be ($#m1_hidden :::"VGraph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedVSubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedVSubgraph":::) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; definitionlet "G" be ($#m1_hidden :::"WEGraph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedWESubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedWESubgraph":::) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; definitionlet "G" be ($#m1_hidden :::"WVGraph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedWVSubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedWVSubgraph":::) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; definitionlet "G" be ($#m1_hidden :::"EVGraph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedEVSubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedEVSubgraph":::) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; definitionlet "G" be ($#m1_hidden :::"WEVGraph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedWEVSubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedWEVSubgraph":::) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); attr "G" is :::"real-weighted"::: means :: GLIB_003:def 13 (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) "G") "is" ($#v3_valued_0 :::"real-valued"::: ) ); end; :: deftheorem defines :::"real-weighted"::: GLIB_003:def 13 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v7_glib_003 :::"real-weighted"::: ) ) "iff" (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G"))) "is" ($#v3_valued_0 :::"real-valued"::: ) ) ")" )); definitionlet "G" be ($#m1_hidden :::"WGraph":::); attr "G" is :::"nonnegative-weighted"::: means :: GLIB_003:def 14 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k8_graph_5 :::"Real>=0"::: ) )); end; :: deftheorem defines :::"nonnegative-weighted"::: GLIB_003:def 14 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v8_glib_003 :::"nonnegative-weighted"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k8_graph_5 :::"Real>=0"::: ) )) ")" )); 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]"::: ) ($#v8_glib_003 :::"nonnegative-weighted"::: ) -> ($#v7_glib_003 :::"real-weighted"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"EGraph":::); attr "G" is :::"real-elabeled"::: means :: GLIB_003:def 15 (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) "G") "is" ($#v3_valued_0 :::"real-valued"::: ) ); end; :: deftheorem defines :::"real-elabeled"::: GLIB_003:def 15 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v9_glib_003 :::"real-elabeled"::: ) ) "iff" (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G"))) "is" ($#v3_valued_0 :::"real-valued"::: ) ) ")" )); definitionlet "G" be ($#m1_hidden :::"VGraph":::); attr "G" is :::"real-vlabeled"::: means :: GLIB_003:def 16 (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) "G") "is" ($#v3_valued_0 :::"real-valued"::: ) ); end; :: deftheorem defines :::"real-vlabeled"::: GLIB_003:def 16 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v10_glib_003 :::"real-vlabeled"::: ) ) "iff" (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G"))) "is" ($#v3_valued_0 :::"real-valued"::: ) ) ")" )); definitionlet "G" be ($#m1_hidden :::"WEVGraph":::); attr "G" is :::"real-WEV"::: means :: GLIB_003:def 17 (Bool "(" (Bool "G" "is" ($#v7_glib_003 :::"real-weighted"::: ) ) & (Bool "G" "is" ($#v9_glib_003 :::"real-elabeled"::: ) ) & (Bool "G" "is" ($#v10_glib_003 :::"real-vlabeled"::: ) ) ")" ); end; :: deftheorem defines :::"real-WEV"::: GLIB_003:def 17 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WEVGraph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v11_glib_003 :::"real-WEV"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v7_glib_003 :::"real-weighted"::: ) ) & (Bool (Set (Var "G")) "is" ($#v9_glib_003 :::"real-elabeled"::: ) ) & (Bool (Set (Var "G")) "is" ($#v10_glib_003 :::"real-vlabeled"::: ) ) ")" ) ")" )); 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v11_glib_003 :::"real-WEV"::: ) -> ($#v7_glib_003 :::"real-weighted"::: ) ($#v9_glib_003 :::"real-elabeled"::: ) ($#v10_glib_003 :::"real-vlabeled"::: ) for ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v7_glib_003 :::"real-weighted"::: ) ($#v9_glib_003 :::"real-elabeled"::: ) ($#v10_glib_003 :::"real-vlabeled"::: ) -> ($#v11_glib_003 :::"real-WEV"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v7_glib_003 :::"real-weighted"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v9_glib_003 :::"real-elabeled"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G"))); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v9_glib_003 :::"real-elabeled"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G"))); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) -> ($#v9_glib_003 :::"real-elabeled"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "val" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," (Set "(" "v" ($#k16_funcop_1 :::".-->"::: ) "val" ")" ) ")" ) -> ($#v3_glib_003 :::"[VLabeled]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "val" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," (Set "(" "v" ($#k16_funcop_1 :::".-->"::: ) "val" ")" ) ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; 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"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v2_glib_000 :::"finite"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#v3_glib_002 :::"Tree-like"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#v11_glib_003 :::"real-WEV"::: ) for ($#m1_hidden :::"set"::: ) ; 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]"::: ) ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v3_glib_002 :::"Tree-like"::: ) ($#v1_glib_003 :::"[Weighted]"::: ) ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#v11_glib_003 :::"real-WEV"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"WGraph":::); cluster (Set ($#k5_glib_003 :::"the_Weight_of"::: ) "G") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"EGraph":::); cluster (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) "G") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"VGraph":::); cluster (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) "G") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); cluster (Set ($#k5_glib_003 :::"the_Weight_of"::: ) "G") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "G" be ($#v9_glib_003 :::"real-elabeled"::: ) ($#m1_hidden :::"EGraph":::); cluster (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) "G") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "G" be ($#v10_glib_003 :::"real-vlabeled"::: ) ($#m1_hidden :::"VGraph":::); cluster (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) "G") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v7_glib_003 :::"real-weighted"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v7_glib_003 :::"real-weighted"::: ) ; end; registrationlet "G" be ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v8_glib_003 :::"nonnegative-weighted"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v8_glib_003 :::"nonnegative-weighted"::: ) ; end; registrationlet "G" be ($#v9_glib_003 :::"real-elabeled"::: ) ($#m1_hidden :::"EGraph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v9_glib_003 :::"real-elabeled"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," "X" ")" ) -> ($#v9_glib_003 :::"real-elabeled"::: ) ; end; registrationlet "G" be ($#v10_glib_003 :::"real-vlabeled"::: ) ($#m1_hidden :::"VGraph":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," "X" ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; cluster (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," "X" ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"WGraph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".weightSeq()"::: -> ($#m1_hidden :::"FinSequence":::) means :: GLIB_003:def 18 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" "W" ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" "W" ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::".weightSeq()"::: GLIB_003:def 18 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_003 :::".weightSeq()"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); :: original: :::".weightSeq()"::: redefine func "W" :::".weightSeq()"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".cost()"::: -> ($#m1_subset_1 :::"Real":::) equals :: GLIB_003:def 19 (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" "W" ($#k9_glib_003 :::".weightSeq()"::: ) ")" )); end; :: deftheorem defines :::".cost()"::: GLIB_003:def 19 : (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "W")) ($#k9_glib_003 :::".weightSeq()"::: ) ")" ))))); definitionlet "G" be ($#m1_hidden :::"EGraph":::); func "G" :::".labeledE()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) equals :: GLIB_003:def 20 (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) "G" ")" )); end; :: deftheorem defines :::".labeledE()"::: GLIB_003:def 20 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) "holds" (Bool (Set (Set (Var "G")) ($#k11_glib_003 :::".labeledE()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G")) ")" )))); definitionlet "G" be ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; func "G" :::".labelEdge"::: "(" "e" "," "x" ")" -> ($#m1_hidden :::"EGraph":::) equals :: GLIB_003:def 21 (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," (Set "(" (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) "G" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "e" ($#k16_funcop_1 :::".-->"::: ) "x" ")" ) ")" ) ")" ) if (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) otherwise "G"; end; :: deftheorem defines :::".labelEdge"::: GLIB_003:def 21 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))))) "implies" (Bool (Set (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," (Set "(" (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "e")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ")" ))); registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v2_glib_000 :::"finite"::: ) ; end; registrationlet "G" be ($#v3_glib_000 :::"loopless"::: ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v3_glib_000 :::"loopless"::: ) ; end; registrationlet "G" be ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v4_glib_000 :::"trivial"::: ) ; end; registrationlet "G" be ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ; end; registrationlet "G" be ($#v5_glib_000 :::"non-multi"::: ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v5_glib_000 :::"non-multi"::: ) ; end; registrationlet "G" be ($#v6_glib_000 :::"non-Dmulti"::: ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v6_glib_000 :::"non-Dmulti"::: ) ; end; registrationlet "G" be ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v1_glib_002 :::"connected"::: ) ; end; registrationlet "G" be ($#v2_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"EGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v2_glib_002 :::"acyclic"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"WEGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v1_glib_003 :::"[Weighted]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"EVGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v3_glib_003 :::"[VLabeled]"::: ) ; end; registrationlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WEGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v7_glib_003 :::"real-weighted"::: ) ; end; registrationlet "G" be ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WEGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v8_glib_003 :::"nonnegative-weighted"::: ) ; end; registrationlet "G" be ($#v9_glib_003 :::"real-elabeled"::: ) ($#m1_hidden :::"EGraph":::); let "e" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Real":::); cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v9_glib_003 :::"real-elabeled"::: ) ; end; registrationlet "G" be ($#v10_glib_003 :::"real-vlabeled"::: ) ($#m1_hidden :::"EVGraph":::); let "e", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k12_glib_003 :::".labelEdge"::: ) "(" "e" "," "x" ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; func "G" :::".labelVertex"::: "(" "v" "," "x" ")" -> ($#m1_hidden :::"VGraph":::) equals :: GLIB_003:def 22 (Set "G" ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," (Set "(" (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) "G" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "v" ($#k16_funcop_1 :::".-->"::: ) "x" ")" ) ")" ) ")" ) if (Bool "v" ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G")) otherwise "G"; end; :: deftheorem defines :::".labelVertex"::: GLIB_003:def 22 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "implies" (Bool (Set (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," (Set "(" (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "v")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ")" ))); definitionlet "G" be ($#m1_hidden :::"VGraph":::); func "G" :::".labeledV()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) equals :: GLIB_003:def 23 (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) "G" ")" )); end; :: deftheorem defines :::".labeledV()"::: GLIB_003:def 23 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) "holds" (Bool (Set (Set (Var "G")) ($#k14_glib_003 :::".labeledV()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G")) ")" )))); registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v2_glib_000 :::"finite"::: ) ; end; registrationlet "G" be ($#v3_glib_000 :::"loopless"::: ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v3_glib_000 :::"loopless"::: ) ; end; registrationlet "G" be ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v4_glib_000 :::"trivial"::: ) ; end; registrationlet "G" be ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ; end; registrationlet "G" be ($#v5_glib_000 :::"non-multi"::: ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v5_glib_000 :::"non-multi"::: ) ; end; registrationlet "G" be ($#v6_glib_000 :::"non-Dmulti"::: ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v6_glib_000 :::"non-Dmulti"::: ) ; end; registrationlet "G" be ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v1_glib_002 :::"connected"::: ) ; end; registrationlet "G" be ($#v2_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"VGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v2_glib_002 :::"acyclic"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"WVGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v1_glib_003 :::"[Weighted]"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"EVGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v2_glib_003 :::"[ELabeled]"::: ) ; end; registrationlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WVGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v7_glib_003 :::"real-weighted"::: ) ; end; registrationlet "G" be ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WVGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v8_glib_003 :::"nonnegative-weighted"::: ) ; end; registrationlet "G" be ($#v9_glib_003 :::"real-elabeled"::: ) ($#m1_hidden :::"EVGraph":::); let "v", "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v9_glib_003 :::"real-elabeled"::: ) ; end; registrationlet "G" be ($#v10_glib_003 :::"real-vlabeled"::: ) ($#m1_hidden :::"VGraph":::); let "v" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Real":::); cluster (Set "G" ($#k13_glib_003 :::".labelVertex"::: ) "(" "v" "," "x" ")" ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) ; end; registrationlet "G" be ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::); cluster ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) -> ($#v7_glib_003 :::"real-weighted"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::); cluster ($#v1_glib_003 :::"[Weighted]"::: ) ($#v4_glib_003 :::"weight-inheriting"::: ) -> ($#v8_glib_003 :::"nonnegative-weighted"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v9_glib_003 :::"real-elabeled"::: ) ($#m1_hidden :::"EGraph":::); cluster ($#v2_glib_003 :::"[ELabeled]"::: ) ($#v5_glib_003 :::"elabel-inheriting"::: ) -> ($#v9_glib_003 :::"real-elabeled"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v10_glib_003 :::"real-vlabeled"::: ) ($#m1_hidden :::"VGraph":::); cluster ($#v3_glib_003 :::"[VLabeled]"::: ) ($#v6_glib_003 :::"vlabel-inheriting"::: ) -> ($#v10_glib_003 :::"real-vlabeled"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "GSq" be ($#m1_hidden :::"GraphSeq":::); attr "GSq" is :::"[Weighted]"::: means :: GLIB_003:def 24 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_glib_003 :::"[Weighted]"::: ) )); attr "GSq" is :::"[ELabeled]"::: means :: GLIB_003:def 25 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_glib_003 :::"[ELabeled]"::: ) )); attr "GSq" is :::"[VLabeled]"::: means :: GLIB_003:def 26 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v3_glib_003 :::"[VLabeled]"::: ) )); end; :: deftheorem defines :::"[Weighted]"::: GLIB_003:def 24 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v12_glib_003 :::"[Weighted]"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_glib_003 :::"[Weighted]"::: ) )) ")" )); :: deftheorem defines :::"[ELabeled]"::: GLIB_003:def 25 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v13_glib_003 :::"[ELabeled]"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_glib_003 :::"[ELabeled]"::: ) )) ")" )); :: deftheorem defines :::"[VLabeled]"::: GLIB_003:def 26 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v14_glib_003 :::"[VLabeled]"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v3_glib_003 :::"[VLabeled]"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v12_glib_003 :::"[Weighted]"::: ) ($#v13_glib_003 :::"[ELabeled]"::: ) ($#v14_glib_003 :::"[VLabeled]"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode WGraphSeq is ($#v12_glib_003 :::"[Weighted]"::: ) ($#m1_hidden :::"GraphSeq":::); mode EGraphSeq is ($#v13_glib_003 :::"[ELabeled]"::: ) ($#m1_hidden :::"GraphSeq":::); mode VGraphSeq is ($#v14_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"GraphSeq":::); mode WEGraphSeq is ($#v12_glib_003 :::"[Weighted]"::: ) ($#v13_glib_003 :::"[ELabeled]"::: ) ($#m1_hidden :::"GraphSeq":::); mode WVGraphSeq is ($#v12_glib_003 :::"[Weighted]"::: ) ($#v14_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"GraphSeq":::); mode EVGraphSeq is ($#v13_glib_003 :::"[ELabeled]"::: ) ($#v14_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"GraphSeq":::); mode WEVGraphSeq is ($#v12_glib_003 :::"[Weighted]"::: ) ($#v13_glib_003 :::"[ELabeled]"::: ) ($#v14_glib_003 :::"[VLabeled]"::: ) ($#m1_hidden :::"GraphSeq":::); end; registrationlet "GSq" be ($#m1_hidden :::"WGraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_glib_003 :::"[Weighted]"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#m1_hidden :::"EGraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v2_glib_003 :::"[ELabeled]"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#m1_hidden :::"VGraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v3_glib_003 :::"[VLabeled]"::: ) for ($#m1_hidden :::"_Graph":::); end; definitionlet "GSq" be ($#m1_hidden :::"WGraphSeq":::); attr "GSq" is :::"real-weighted"::: means :: GLIB_003:def 27 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v7_glib_003 :::"real-weighted"::: ) )); attr "GSq" is :::"nonnegative-weighted"::: means :: GLIB_003:def 28 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v8_glib_003 :::"nonnegative-weighted"::: ) )); end; :: deftheorem defines :::"real-weighted"::: GLIB_003:def 27 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"WGraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v15_glib_003 :::"real-weighted"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v7_glib_003 :::"real-weighted"::: ) )) ")" )); :: deftheorem defines :::"nonnegative-weighted"::: GLIB_003:def 28 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"WGraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v16_glib_003 :::"nonnegative-weighted"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v8_glib_003 :::"nonnegative-weighted"::: ) )) ")" )); definitionlet "GSq" be ($#m1_hidden :::"EGraphSeq":::); attr "GSq" is :::"real-elabeled"::: means :: GLIB_003:def 29 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v9_glib_003 :::"real-elabeled"::: ) )); end; :: deftheorem defines :::"real-elabeled"::: GLIB_003:def 29 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"EGraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v17_glib_003 :::"real-elabeled"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v9_glib_003 :::"real-elabeled"::: ) )) ")" )); definitionlet "GSq" be ($#m1_hidden :::"VGraphSeq":::); attr "GSq" is :::"real-vlabeled"::: means :: GLIB_003:def 30 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v10_glib_003 :::"real-vlabeled"::: ) )); end; :: deftheorem defines :::"real-vlabeled"::: GLIB_003:def 30 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"VGraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v18_glib_003 :::"real-vlabeled"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v10_glib_003 :::"real-vlabeled"::: ) )) ")" )); definitionlet "GSq" be ($#m1_hidden :::"WEVGraphSeq":::); attr "GSq" is :::"real-WEV"::: means :: GLIB_003:def 31 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v11_glib_003 :::"real-WEV"::: ) )); end; :: deftheorem defines :::"real-WEV"::: GLIB_003:def 31 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"WEVGraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v19_glib_003 :::"real-WEV"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v11_glib_003 :::"real-WEV"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v12_glib_003 :::"[Weighted]"::: ) ($#v13_glib_003 :::"[ELabeled]"::: ) ($#v14_glib_003 :::"[VLabeled]"::: ) ($#v19_glib_003 :::"real-WEV"::: ) -> ($#v15_glib_003 :::"real-weighted"::: ) ($#v17_glib_003 :::"real-elabeled"::: ) ($#v18_glib_003 :::"real-vlabeled"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v12_glib_003 :::"[Weighted]"::: ) ($#v13_glib_003 :::"[ELabeled]"::: ) ($#v14_glib_003 :::"[VLabeled]"::: ) ($#v15_glib_003 :::"real-weighted"::: ) ($#v17_glib_003 :::"real-elabeled"::: ) ($#v18_glib_003 :::"real-vlabeled"::: ) -> ($#v19_glib_003 :::"real-WEV"::: ) 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_partfun1 :::"total"::: ) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v13_glib_000 :::"halting"::: ) ($#v14_glib_000 :::"finite"::: ) ($#v15_glib_000 :::"loopless"::: ) ($#v16_glib_000 :::"trivial"::: ) ($#v18_glib_000 :::"non-multi"::: ) ($#v20_glib_000 :::"simple"::: ) ($#v8_glib_002 :::"Tree-like"::: ) ($#v12_glib_003 :::"[Weighted]"::: ) ($#v13_glib_003 :::"[ELabeled]"::: ) ($#v14_glib_003 :::"[VLabeled]"::: ) ($#v16_glib_003 :::"nonnegative-weighted"::: ) ($#v19_glib_003 :::"real-WEV"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "GSq" be ($#v15_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v7_glib_003 :::"real-weighted"::: ) for ($#m1_hidden :::"WGraph":::); end; registrationlet "GSq" be ($#v16_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v8_glib_003 :::"nonnegative-weighted"::: ) for ($#m1_hidden :::"WGraph":::); end; registrationlet "GSq" be ($#v17_glib_003 :::"real-elabeled"::: ) ($#m1_hidden :::"EGraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v9_glib_003 :::"real-elabeled"::: ) for ($#m1_hidden :::"EGraph":::); end; registrationlet "GSq" be ($#v18_glib_003 :::"real-vlabeled"::: ) ($#m1_hidden :::"VGraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v10_glib_003 :::"real-vlabeled"::: ) for ($#m1_hidden :::"VGraph":::); end; begin theorem :: GLIB_003:3 (Bool "(" (Bool (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 5)) & (Bool (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 6)) & (Bool (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)) ")" ) ; theorem :: GLIB_003:4 (Bool "(" (Bool "(" "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) "holds" (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_003 :::"WeightSelector"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) "holds" (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) "holds" (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ))) ")" ) ")" ) ; theorem :: GLIB_003:5 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))))) ; theorem :: GLIB_003:6 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) ; theorem :: GLIB_003:7 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r5_glib_000 :::"=="::: ) (Set (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_003 :::"WeightSelector"::: ) ) "," (Set (Var "X")) ")" )) & (Bool (Set (Var "G")) ($#r5_glib_000 :::"=="::: ) (Set (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_003 :::"ELabelSelector"::: ) ) "," (Set (Var "X")) ")" )) & (Bool (Set (Var "G")) ($#r5_glib_000 :::"=="::: ) (Set (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_003 :::"VLabelSelector"::: ) ) "," (Set (Var "X")) ")" )) ")" ))) ; theorem :: GLIB_003:8 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "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")))) & (Bool (Set (Var "G1")) "is" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G3")))) "holds" (Bool (Set (Var "G2")) "is" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G3")))) ; theorem :: GLIB_003:9 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "G3")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G2")) "holds" (Bool (Set (Var "G3")) "is" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")))))) ; theorem :: GLIB_003:10 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G3")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) "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 "G3")) "is" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G2"))))) ; theorem :: GLIB_003:11 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: GLIB_003:12 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (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 (Set (Var "W")) ($#k8_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: GLIB_003:13 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_003 :::".weightSeq()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k15_glib_001 :::".length()"::: ) )))) ; theorem :: GLIB_003:14 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" ) ($#k8_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")) ")" ) ($#k9_finseq_1 :::"*>"::: ) )))) ; theorem :: GLIB_003:15 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k8_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_5 :::"Rev"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_003 :::".weightSeq()"::: ) ")" ))))) ; theorem :: GLIB_003:16 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k8_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k8_glib_003 :::".weightSeq()"::: ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "W2")) ($#k8_glib_003 :::".weightSeq()"::: ) ")" ))))) ; theorem :: GLIB_003:17 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k28_glib_000 :::".edgesInOut()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k8_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k8_glib_003 :::".weightSeq()"::: ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")) ")" ) ($#k9_finseq_1 :::"*>"::: ) )))))) ; theorem :: GLIB_003:18 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W2")) "being" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W1")) (Bool "ex" (Set (Var "ws")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "W1")) ($#k9_glib_003 :::".weightSeq()"::: ) ")" ) "st" (Bool (Set (Set (Var "W2")) ($#k9_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_glib_003 :::"Seq"::: ) (Set (Var "ws")))))))) ; theorem :: GLIB_003:19 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) & (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 (Set (Var "W1")) ($#k8_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k8_glib_003 :::".weightSeq()"::: ) ))))) ; theorem :: GLIB_003:20 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"WSubgraph":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k8_glib_003 :::".weightSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k8_glib_003 :::".weightSeq()"::: ) )))))) ; theorem :: GLIB_003:21 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (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 (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: GLIB_003:22 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "v1")) "," (Set (Var "e")) "," (Set (Var "v2")) ")" ")" ) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e"))))))) ; theorem :: GLIB_003:23 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k10_glib_003 :::".cost()"::: ) )))) ; theorem :: GLIB_003:24 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k10_glib_003 :::".cost()"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) ")" ))))) ; theorem :: GLIB_003:25 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k28_glib_000 :::".edgesInOut()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e")) ")" )))))) ; theorem :: GLIB_003:26 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v7_glib_003 :::"real-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) & (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 (Set (Var "W1")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) ))))) ; theorem :: GLIB_003:27 (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 "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) )))))) ; theorem :: GLIB_003:28 (Bool "for" (Set (Var "G")) "being" ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k9_glib_003 :::".weightSeq()"::: ) ")" )))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "W")) ($#k9_glib_003 :::".weightSeq()"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: GLIB_003:29 (Bool "for" (Set (Var "G")) "being" ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "W")) ($#k10_glib_003 :::".cost()"::: ) )))) ; theorem :: GLIB_003:30 (Bool "for" (Set (Var "G")) "being" ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W2")) "being" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W1")) "holds" (Bool (Set (Set (Var "W2")) ($#k10_glib_003 :::".cost()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "W1")) ($#k10_glib_003 :::".cost()"::: ) ))))) ; theorem :: GLIB_003:31 (Bool "for" (Set (Var "G")) "being" ($#v8_glib_003 :::"nonnegative-weighted"::: ) ($#m1_hidden :::"WGraph":::) (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 (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "e")))))) ; theorem :: GLIB_003:32 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "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 (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "e")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x")) ")" ))))) ; theorem :: GLIB_003:33 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "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 (Set (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: GLIB_003:34 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "G")) ($#r5_glib_000 :::"=="::: ) (Set (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" )))) ; theorem :: GLIB_003:35 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WEGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ))))) ; theorem :: GLIB_003:36 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EVGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ))))) ; theorem :: GLIB_003:37 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r1_hidden :::"<>"::: ) (Set (Var "e2")))) "holds" (Bool (Set (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e1")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e2")))))) ; theorem :: GLIB_003:38 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "v")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x")) ")" ))))) ; theorem :: GLIB_003:39 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: GLIB_003:40 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "G")) ($#r5_glib_000 :::"=="::: ) (Set (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" )))) ; theorem :: GLIB_003:41 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"WVGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_glib_003 :::"the_Weight_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ))))) ; theorem :: GLIB_003:42 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EVGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ))))) ; theorem :: GLIB_003:43 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool (Set (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v1")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v2")))))) ; theorem :: GLIB_003:44 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"EGraph":::) "st" (Bool (Bool (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_003 :::"the_ELabel_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Set (Var "G1")) ($#k11_glib_003 :::".labeledE()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k11_glib_003 :::".labeledE()"::: ) ))) ; theorem :: GLIB_003:45 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "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 (Set (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ) ($#k11_glib_003 :::".labeledE()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k11_glib_003 :::".labeledE()"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GLIB_003:46 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "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 (Set (Set (Var "G")) ($#k11_glib_003 :::".labeledE()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ) ($#k11_glib_003 :::".labeledE()"::: ) )))) ; theorem :: GLIB_003:47 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "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 "G")) ($#k11_glib_003 :::".labeledE()"::: ) )))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ) ($#k11_glib_003 :::".labeledE()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k11_glib_003 :::".labeledE()"::: ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: GLIB_003:48 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k11_glib_003 :::".labeledE()"::: ) ))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e1")) "," (Set (Var "x")) ")" ")" ) ($#k11_glib_003 :::".labeledE()"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2"))) & (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GLIB_003:49 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EVGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "G")) ($#k11_glib_003 :::".labeledE()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ) ($#k11_glib_003 :::".labeledE()"::: ) )))) ; theorem :: GLIB_003:50 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "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 (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ) ($#k11_glib_003 :::".labeledE()"::: ) )))) ; theorem :: GLIB_003:51 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"VGraph":::) "st" (Bool (Bool (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_003 :::"the_VLabel_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Set (Var "G1")) ($#k14_glib_003 :::".labeledV()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k14_glib_003 :::".labeledV()"::: ) ))) ; theorem :: GLIB_003:52 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ) ($#k14_glib_003 :::".labeledV()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k14_glib_003 :::".labeledV()"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GLIB_003:53 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k14_glib_003 :::".labeledV()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ) ($#k14_glib_003 :::".labeledV()"::: ) )))) ; theorem :: GLIB_003:54 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k14_glib_003 :::".labeledV()"::: ) )))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ) ($#k14_glib_003 :::".labeledV()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k14_glib_003 :::".labeledV()"::: ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: GLIB_003:55 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k14_glib_003 :::".labeledV()"::: ) ))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v1")) "," (Set (Var "x")) ")" ")" ) ($#k14_glib_003 :::".labeledV()"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GLIB_003:56 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"EVGraph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "G")) ($#k14_glib_003 :::".labeledV()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k12_glib_003 :::".labelEdge"::: ) "(" (Set (Var "e")) "," (Set (Var "x")) ")" ")" ) ($#k14_glib_003 :::".labeledV()"::: ) )))) ; theorem :: GLIB_003:57 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"VGraph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "G")) ($#k13_glib_003 :::".labelVertex"::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ")" ) ($#k14_glib_003 :::".labeledV()"::: ) ))))) ;