:: GRAPH_5 semantic presentation begin theorem :: GRAPH_5:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" )))) ; scheme :: GRAPH_5:sch 1 LambdaAB{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" ) ")" )) proof end; theorem :: GRAPH_5:2 (Bool "for" (Set (Var "D")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) "}" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) )))) ; theorem :: GRAPH_5:3 (Bool "for" (Set (Var "D")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) )))) ; theorem :: GRAPH_5:4 (Bool "for" (Set (Var "D")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D"))(Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ))))) ; theorem :: GRAPH_5:5 (Bool "for" (Set (Var "D")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; scheme :: GRAPH_5:sch 2 MinValue{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F2 "(" (Set (Var "x")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set F2 "(" (Set (Var "y")) ")" )))) proof end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; begin theorem :: GRAPH_5:6 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) ")" ) "iff" (Bool (Set (Var "p")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )) ; theorem :: GRAPH_5:7 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) ")" ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) ")" )) ; theorem :: GRAPH_5:8 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "pe"))))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" )))) ; theorem :: GRAPH_5:9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ))) ")" )))) ; begin theorem :: GRAPH_5:10 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))) & (Bool (Set (Var "q")) "is" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))) ")" ))) ; theorem :: GRAPH_5:11 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))) & (Bool (Set (Var "q")) "is" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))) ")" ))) ; theorem :: GRAPH_5:12 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))))) ; begin theorem :: GRAPH_5:13 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))) ; theorem :: GRAPH_5:14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))) & (Bool (Set (Var "q")) "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))) ")" ))) ; theorem :: GRAPH_5:15 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "pe")) "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))))) ; theorem :: GRAPH_5:16 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "not" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "or" "not" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) "or" "not" (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))))) ; theorem :: GRAPH_5:17 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "p")) "is" bbbadV2_FUNCT_1()))) ; begin definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))); func :::"vertices"::: "e" -> ($#m1_hidden :::"set"::: ) equals :: GRAPH_5:def 1 (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) "e" ")" ) "," (Set "(" (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) "e" ")" ) ($#k2_tarski :::"}"::: ) ); end; :: deftheorem defines :::"vertices"::: GRAPH_5:def 1 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set ($#k1_graph_5 :::"vertices"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "e")) ")" ) "," (Set "(" (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "e")) ")" ) ($#k2_tarski :::"}"::: ) )))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "pe" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))); func :::"vertices"::: "pe" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") equals :: GRAPH_5:def 2 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vertex":::) "of" "G" : (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "pe")) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_graph_5 :::"vertices"::: ) (Set "(" "pe" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )) "}" ; end; :: deftheorem defines :::"vertices"::: GRAPH_5:def 2 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) : (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "pe")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_graph_5 :::"vertices"::: ) (Set "(" (Set (Var "pe")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )) "}" ))); theorem :: GRAPH_5:18 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "," (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "pe")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "qe")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qe"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Bool "not" (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "qe"))))) & (Bool (Bool "not" (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe"))))) ")" )))) ; theorem :: GRAPH_5:19 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "pe"))))) "holds" (Bool (Set ($#k1_graph_5 :::"vertices"::: ) (Set "(" (Set (Var "pe")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) ")" )))) ; theorem :: GRAPH_5:20 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Bool "not" (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe")))) & (Bool (Bool "not" (Set ($#k1_graph_5 :::"vertices"::: ) (Set "(" (Set (Var "pe")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Var "pe")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )))))) ; theorem :: GRAPH_5:21 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "qe")) "," (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "qe"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "pe"))))) "holds" (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "qe"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe")))))) ; theorem :: GRAPH_5:22 (Bool "for" (Set (Var "X")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "qe")) "," (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "qe"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "pe")))) & (Bool (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) (Set (Var "qe")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))))) ; theorem :: GRAPH_5:23 (Bool "for" (Set (Var "X")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "," (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) (Set "(" (Set (Var "pe")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "qe")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) (Set (Var "qe")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )))) ; theorem :: GRAPH_5:24 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "pe")))) & (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe")))))))) ; theorem :: GRAPH_5:25 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) (Set ($#k1_graph_5 :::"vertices"::: ) (Set "(" (Set (Var "pe")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ))))) ; theorem :: GRAPH_5:26 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "," (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "pe"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set "(" (Set (Var "pe")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "qe")) ")" ))) & (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "qe"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set "(" (Set (Var "pe")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "qe")) ")" ))) ")" ))) ; theorem :: GRAPH_5:27 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "pe")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) (Set (Var "q")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: GRAPH_5:28 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ))))) ; begin definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "p" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); pred "p" :::"is_orientedpath_of"::: "v1" "," "v2" means :: GRAPH_5:def 3 (Bool "(" (Bool "p" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) "v1") & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" )) ($#r1_hidden :::"="::: ) "v2") ")" ); end; :: deftheorem defines :::"is_orientedpath_of"::: GRAPH_5:def 3 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v1"))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) ")" ) ")" )))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "p" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); let "V" be ($#m1_hidden :::"set"::: ) ; pred "p" :::"is_orientedpath_of"::: "v1" "," "v2" "," "V" means :: GRAPH_5:def 4 (Bool "(" (Bool "p" ($#r1_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2") & (Bool (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) "p" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "v2" ($#k1_tarski :::"}"::: ) )) ($#r1_tarski :::"c="::: ) "V") ")" ); end; :: deftheorem defines :::"is_orientedpath_of"::: GRAPH_5:def 4 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) & (Bool (Set (Set "(" ($#k2_graph_5 :::"vertices"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ) ")" ))))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"OrientedPaths"::: "(" "v1" "," "v2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: GRAPH_5:def 5 "{" (Set (Var "p")) where p "is" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" : (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2") "}" ; end; :: deftheorem defines :::"OrientedPaths"::: GRAPH_5:def 5 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_graph_5 :::"OrientedPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) : (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) "}" ))); theorem :: GRAPH_5:29 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "p")))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_graph_5 :::"vertices"::: ) (Set (Var "p")))) ")" )))) ; theorem :: GRAPH_5:30 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_graph_5 :::"OrientedPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )) "iff" (Bool "ex" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" )) ")" )))) ; theorem :: GRAPH_5:31 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))))))) ; theorem :: GRAPH_5:32 (Bool "for" (Set (Var "V")) "," (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U")))) "holds" (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "U"))))))) ; theorem :: GRAPH_5:33 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) & (Bool (Set (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v2")) "," (Set (Var "v3"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "pe")))) & (Bool (Set (Var "q")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3"))) ")" )))))) ; theorem :: GRAPH_5:34 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "pe")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) & (Bool (Set (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v2")) "," (Set (Var "v3")))) "holds" (Bool (Set (Var "q")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) )))))))) ; begin definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "p" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); pred "p" :::"is_acyclicpath_of"::: "v1" "," "v2" means :: GRAPH_5:def 6 (Bool "(" (Bool "p" "is" ($#v1_graph_4 :::"Simple"::: ) ) & (Bool "p" ($#r1_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2") ")" ); end; :: deftheorem defines :::"is_acyclicpath_of"::: GRAPH_5:def 6 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_graph_5 :::"is_acyclicpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) "iff" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_graph_4 :::"Simple"::: ) ) & (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" ) ")" )))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "p" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "V" be ($#m1_hidden :::"set"::: ) ; pred "p" :::"is_acyclicpath_of"::: "v1" "," "v2" "," "V" means :: GRAPH_5:def 7 (Bool "(" (Bool "p" "is" ($#v1_graph_4 :::"Simple"::: ) ) & (Bool "p" ($#r2_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2" "," "V") ")" ); end; :: deftheorem defines :::"is_acyclicpath_of"::: GRAPH_5:def 7 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r4_graph_5 :::"is_acyclicpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) "iff" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_graph_4 :::"Simple"::: ) ) & (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) ")" ) ")" ))))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"AcyclicPaths"::: "(" "v1" "," "v2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: GRAPH_5:def 8 "{" (Set (Var "p")) where p "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" : (Bool (Set (Var "p")) ($#r3_graph_5 :::"is_acyclicpath_of"::: ) "v1" "," "v2") "}" ; end; :: deftheorem defines :::"AcyclicPaths"::: GRAPH_5:def 8 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) : (Bool (Set (Var "p")) ($#r3_graph_5 :::"is_acyclicpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) "}" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "V" be ($#m1_hidden :::"set"::: ) ; func :::"AcyclicPaths"::: "(" "v1" "," "v2" "," "V" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: GRAPH_5:def 9 "{" (Set (Var "p")) where p "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" : (Bool (Set (Var "p")) ($#r4_graph_5 :::"is_acyclicpath_of"::: ) "v1" "," "v2" "," "V") "}" ; end; :: deftheorem defines :::"AcyclicPaths"::: GRAPH_5:def 9 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) : (Bool (Set (Var "p")) ($#r4_graph_5 :::"is_acyclicpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) "}" )))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "p" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); func :::"AcyclicPaths"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: GRAPH_5:def 10 "{" (Set (Var "q")) where q "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "p")) ")" ) "}" ; end; :: deftheorem defines :::"AcyclicPaths"::: GRAPH_5:def 10 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) ")" ) "}" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); func :::"AcyclicPaths"::: "G" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: GRAPH_5:def 11 "{" (Set (Var "q")) where q "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" : (Bool verum) "}" ; end; :: deftheorem defines :::"AcyclicPaths"::: GRAPH_5:def 11 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set ($#k7_graph_5 :::"AcyclicPaths"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) : (Bool verum) "}" )); theorem :: GRAPH_5:35 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r3_graph_5 :::"is_acyclicpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))))))) ; theorem :: GRAPH_5:36 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r3_graph_5 :::"is_acyclicpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))))) ; theorem :: GRAPH_5:37 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_graph_5 :::"OrientedPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )))) ; theorem :: GRAPH_5:38 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_graph_5 :::"AcyclicPaths"::: ) (Set (Var "G")))))) ; theorem :: GRAPH_5:39 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k7_graph_5 :::"AcyclicPaths"::: ) (Set (Var "G")))))) ; theorem :: GRAPH_5:40 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ))))) ; theorem :: GRAPH_5:41 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")))) "holds" (Bool (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" )))))) ; theorem :: GRAPH_5:42 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))))) ; theorem :: GRAPH_5:43 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool "(" (Bool (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: GRAPH_5:44 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")))) "holds" (Bool "(" (Bool (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))))) ; theorem :: GRAPH_5:45 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k7_graph_5 :::"AcyclicPaths"::: ) (Set (Var "G"))))))) ; begin notationsynonym :::"Real>=0"::: for :::"REAL+"::: ; end; definition:: original: :::"Real>=0"::: redefine func :::"Real>=0"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: GRAPH_5:def 12 "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ; end; :: deftheorem defines :::"Real>=0"::: GRAPH_5:def 12 : (Bool (Set ($#k8_graph_5 :::"Real>=0"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ); registration cluster (Set ($#k2_arytm_2 :::"Real>=0"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "W" be ($#m1_hidden :::"Function":::); pred "W" :::"is_weight>=0of"::: "G" means :: GRAPH_5:def 13 (Bool "W" "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") "," (Set ($#k8_graph_5 :::"Real>=0"::: ) )); end; :: deftheorem defines :::"is_weight>=0of"::: GRAPH_5:def 13 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G"))) "iff" (Bool (Set (Var "W")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) )) ")" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "W" be ($#m1_hidden :::"Function":::); pred "W" :::"is_weight_of"::: "G" means :: GRAPH_5:def 14 (Bool "W" "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") "," (Set ($#k1_numbers :::"REAL"::: ) )); end; :: deftheorem defines :::"is_weight_of"::: GRAPH_5:def 14 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Var "G"))) "iff" (Bool (Set (Var "W")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k1_numbers :::"REAL"::: ) )) ")" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))); let "W" be ($#m1_hidden :::"Function":::); assume (Bool (Set (Const "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Const "G"))) ; func :::"RealSequence"::: "(" "p" "," "W" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: GRAPH_5:def 15 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it)) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"RealSequence"::: GRAPH_5:def 15 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_graph_5 :::"RealSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "W")) ")" )) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))); let "W" be ($#m1_hidden :::"Function":::); func :::"cost"::: "(" "p" "," "W" ")" -> ($#m1_subset_1 :::"Real":::) equals :: GRAPH_5:def 16 (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k9_graph_5 :::"RealSequence"::: ) "(" "p" "," "W" ")" ")" )); end; :: deftheorem defines :::"cost"::: GRAPH_5:def 16 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "p")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k9_graph_5 :::"RealSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "W")) ")" ")" )))))); theorem :: GRAPH_5:46 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Var "G"))))) ; theorem :: GRAPH_5:47 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k9_graph_5 :::"RealSequence"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))))) ; theorem :: GRAPH_5:48 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "qe")) "," (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "qe"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "pe")))) & (Bool (Set (Var "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "qe"))))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "pe")))) & (Bool (Set (Set "(" ($#k9_graph_5 :::"RealSequence"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_graph_5 :::"RealSequence"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )))))) ; theorem :: GRAPH_5:49 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "qe")) "," (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qe"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "qe"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "pe")))) & (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ))))) ; theorem :: GRAPH_5:50 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: GRAPH_5:51 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "pe")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: GRAPH_5:52 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ))) "holds" (Bool "ex" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "pe")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "qe")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" )) ")" ) ")" )))))) ; theorem :: GRAPH_5:53 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" ))) "holds" (Bool "ex" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "pe")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "qe")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" )) ")" ) ")" ))))))) ; theorem :: GRAPH_5:54 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "," (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set "(" (Set (Var "pe")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "qe")) ")" ) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" ")" )))))) ; theorem :: GRAPH_5:55 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "qe")) "," (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "qe")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "qe"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "pe")))) & (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ))))) ; theorem :: GRAPH_5:56 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "pe")) ($#r2_hidden :::"in"::: ) (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) (Set (Var "p")))) & (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "p")) "," (Set (Var "W")) ")" )))))) ; begin definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "p" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); let "W" be ($#m1_hidden :::"Function":::); pred "p" :::"is_shortestpath_of"::: "v1" "," "v2" "," "W" means :: GRAPH_5:def 17 (Bool "(" (Bool "p" ($#r1_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2") & (Bool "(" "for" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" "st" (Bool (Bool (Set (Var "q")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2")) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" "p" "," "W" ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "q")) "," "W" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"is_shortestpath_of"::: GRAPH_5:def 17 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r7_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) & (Bool "(" "for" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "q")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "p")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "q")) "," (Set (Var "W")) ")" )) ")" ) ")" ) ")" ))))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "p" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); let "V" be ($#m1_hidden :::"set"::: ) ; let "W" be ($#m1_hidden :::"Function":::); pred "p" :::"is_shortestpath_of"::: "v1" "," "v2" "," "V" "," "W" means :: GRAPH_5:def 18 (Bool "(" (Bool "p" ($#r2_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2" "," "V") & (Bool "(" "for" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" "st" (Bool (Bool (Set (Var "q")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) "v1" "," "v2" "," "V")) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" "p" "," "W" ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "q")) "," "W" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"is_shortestpath_of"::: GRAPH_5:def 18 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) & (Bool "(" "for" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "q")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "p")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "q")) "," (Set (Var "W")) ")" )) ")" ) ")" ) ")" )))))); begin theorem :: GRAPH_5:57 (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "ps")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "ps"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_graph_1 :::"VerticesCount"::: ) (Set (Var "G")))))) ; theorem :: GRAPH_5:58 (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "ps")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "ps"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_graph_1 :::"EdgesCount"::: ) (Set (Var "G")))))) ; registrationlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::); cluster (Set ($#k7_graph_5 :::"AcyclicPaths"::: ) "G") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::); let "P" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); cluster (Set ($#k6_graph_5 :::"AcyclicPaths"::: ) "P") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" "v1" "," "v2" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "V" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" "v1" "," "v2" "," "V" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: GRAPH_5:59 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "pe")) ($#r2_hidden :::"in"::: ) (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )) & (Bool "(" "for" (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "qe")) ($#r2_hidden :::"in"::: ) (Set ($#k4_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" )) ")" ) ")" ))))) ; theorem :: GRAPH_5:60 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "pe")) ($#r2_hidden :::"in"::: ) (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" )) & (Bool "(" "for" (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "qe")) ($#r2_hidden :::"in"::: ) (Set ($#k5_graph_5 :::"AcyclicPaths"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) ")" ))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "qe")) "," (Set (Var "W")) ")" )) ")" ) ")" )))))) ; theorem :: GRAPH_5:61 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "P")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) & (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "q")) ($#r7_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W")))))))) ; theorem :: GRAPH_5:62 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "P")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) & (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))))))))) ; begin theorem :: GRAPH_5:63 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G"))) & (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool "(" "for" (Set (Var "Q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "v3")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) & (Bool (Set (Var "Q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Var "V")) "," (Set (Var "W")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "P")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "Q")) "," (Set (Var "W")) ")" ))) ")" )) "holds" (Bool (Set (Var "P")) ($#r7_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W")))))))) ; theorem :: GRAPH_5:64 (Bool "for" (Set (Var "V")) "," (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G"))) & (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) & (Bool "(" "for" (Set (Var "Q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "v3")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) & (Bool (Set (Var "Q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Var "V")) "," (Set (Var "W")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "P")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "Q")) "," (Set (Var "W")) ")" ))) ")" )) "holds" (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "U")) "," (Set (Var "W")))))))) ; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "pe" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))); let "V" be ($#m1_hidden :::"set"::: ) ; let "v1" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "W" be ($#m1_hidden :::"Function":::); pred "pe" :::"islongestInShortestpath"::: "V" "," "v1" "," "W" means :: GRAPH_5:def 19 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "V") & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) "v1")) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G" "st" (Bool "(" (Bool (Set (Var "q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) "v1" "," (Set (Var "v")) "," "V" "," "W") & (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "q")) "," "W" ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" "pe" "," "W" ")" )) ")" ))); end; :: deftheorem defines :::"islongestInShortestpath"::: GRAPH_5:def 19 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "pe")) ($#r9_graph_5 :::"islongestInShortestpath"::: ) (Set (Var "V")) "," (Set (Var "v1")) "," (Set (Var "W"))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "v1")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "q")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" )) ")" ))) ")" )))))); theorem :: GRAPH_5:65 (Bool "for" (Set (Var "e")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v3"))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "Q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v2")) "," (Set (Var "v3"))) & (Bool (Set (Var "P")) ($#r9_graph_5 :::"islongestInShortestpath"::: ) (Set (Var "V")) "," (Set (Var "v1")) "," (Set (Var "W")))) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "Q")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "R")) "," (Set (Var "W")) ")" ))) "implies" (Bool (Set (Var "Q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) )) "," (Set (Var "W"))) ")" & "(" (Bool (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "Q")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "R")) "," (Set (Var "W")) ")" ))) "implies" (Bool (Set (Var "R")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) )) "," (Set (Var "W"))) ")" ")" )))))) ;