:: GRAPH_2 semantic presentation begin theorem :: GRAPH_2:1 (Bool "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" )) ")" )) ; theorem :: GRAPH_2:2 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_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 "q"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ))) ; theorem :: GRAPH_2:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "X")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "X")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ) ")" ))))) ; theorem :: GRAPH_2:4 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "k")) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")))) ")" ) "}" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) ; theorem :: GRAPH_2:5 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) "{" (Set (Var "kk")) where kk "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "kk"))) & (Bool (Set (Var "kk")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")))) ")" ) "}" ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "l"))))) ; begin definitionlet "p" be ($#m1_hidden :::"FinSequence":::); let "m", "n" be ($#m1_hidden :::"Nat":::); func "(" "m" "," "n" ")" :::"-cut"::: "p" -> ($#m1_hidden :::"FinSequence":::) means :: GRAPH_2:def 1 (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ($#k2_nat_1 :::"+"::: ) "m") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) if (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) "m") & (Bool "m" ($#r1_xxreal_0 :::"<="::: ) "n") & (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"-cut"::: GRAPH_2:def 1 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" "(" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) "or" "not" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "or" "not" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" )))); theorem :: GRAPH_2:6 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#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 "m")) "," (Set (Var "m")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_finseq_1 :::"*>"::: ) )))) ; theorem :: GRAPH_2:7 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set "(" (Num 1) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) ; theorem :: GRAPH_2:8 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "r")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "r")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")))))) ; theorem :: GRAPH_2:9 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" "(" (Num 1) "," (Set (Var "m")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: GRAPH_2:10 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" "(" (Num 1) "," (Set (Var "m")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: GRAPH_2:11 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "m", "n" be ($#m1_hidden :::"Nat":::); :: original: :::"-cut"::: redefine func "(" "m" "," "n" ")" :::"-cut"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; theorem :: GRAPH_2:12 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) & (Bool (Set (Set "(" "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ))) ; begin definitionlet "p", "q" be ($#m1_hidden :::"FinSequence":::); func "p" :::"^'"::: "q" -> ($#m1_hidden :::"FinSequence":::) equals :: GRAPH_2:def 2 (Set "p" ($#k7_finseq_1 :::"^"::: ) (Set "(" "(" (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "q" ")" ) ")" ($#k1_graph_2 :::"-cut"::: ) "q" ")" )); end; :: deftheorem defines :::"^'"::: GRAPH_2:def 2 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set "(" "(" (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" ($#k1_graph_2 :::"-cut"::: ) (Set (Var "q")) ")" )))); theorem :: GRAPH_2:13 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" )))) ; theorem :: GRAPH_2:14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))))) ; theorem :: GRAPH_2:15 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: GRAPH_2:16 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" )))) ; theorem :: GRAPH_2:17 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q")) ")" )))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "p", "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); :: original: :::"^'"::: redefine func "p" :::"^'"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; theorem :: GRAPH_2:18 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "p")) ($#k3_graph_2 :::"^'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q")) ")" )))) ; begin definitionlet "f" be ($#m1_hidden :::"FinSequence":::); attr "f" is :::"TwoValued"::: means :: GRAPH_2:def 3 (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "f" ")" )) ($#r1_hidden :::"="::: ) (Num 2)); end; :: deftheorem defines :::"TwoValued"::: GRAPH_2:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_graph_2 :::"TwoValued"::: ) ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Num 2)) ")" )); theorem :: GRAPH_2:19 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_graph_2 :::"TwoValued"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" )) ")" ) ")" )) ; definitionlet "f" be ($#m1_hidden :::"FinSequence":::); attr "f" is :::"Alternating"::: means :: GRAPH_2:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"Alternating"::: GRAPH_2:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_graph_2 :::"Alternating"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); 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_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_graph_2 :::"TwoValued"::: ) ($#v2_graph_2 :::"Alternating"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: GRAPH_2:20 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#v1_graph_2 :::"TwoValued"::: ) ($#v2_graph_2 :::"Alternating"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a2")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a2")))) & (Bool (Set (Set (Var "a1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2")))) ; theorem :: GRAPH_2:21 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#v1_graph_2 :::"TwoValued"::: ) ($#v2_graph_2 :::"Alternating"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a2")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a2"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_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 "a1"))))) "holds" (Bool (Set (Set (Var "a1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "a2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ; theorem :: GRAPH_2:22 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#v1_graph_2 :::"TwoValued"::: ) ($#v2_graph_2 :::"Alternating"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a2")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a2"))))) "holds" (Bool "for" (Set (Var "a")) "being" ($#v1_graph_2 :::"TwoValued"::: ) ($#v2_graph_2 :::"Alternating"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a1")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a1"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))))) ; theorem :: GRAPH_2:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "a1")) "being" ($#v1_graph_2 :::"TwoValued"::: ) ($#v2_graph_2 :::"Alternating"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "a1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" )))) ; begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "fs" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "X")); cluster -> ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "fs"); end; theorem :: GRAPH_2:24 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSubsequence":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "fg")) "," (Set (Var "fh")) "," (Set (Var "fgh")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "fg")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")))) & (Bool (Set (Var "fh")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")))) & (Bool (Set (Var "fgh")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "h")) ")" )))) "holds" (Bool (Set (Var "fgh")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fg")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "fh")))))) ; theorem :: GRAPH_2:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "fss")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fss"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "fs")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "fss"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "fs")))) ")" )))) ; theorem :: GRAPH_2:26 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "fs")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs"))))) ; theorem :: GRAPH_2:27 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "fss")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) "holds" (Bool (Set (Set (Var "fss")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")))))) ; theorem :: GRAPH_2:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "," (Set (Var "fs1")) "," (Set (Var "fs2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "fss")) "," (Set (Var "fss2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) (Bool "for" (Set (Var "fss1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs1")) "st" (Bool (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss"))) ($#r1_hidden :::"="::: ) (Set (Var "fs1"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss1"))) ($#r1_hidden :::"="::: ) (Set (Var "fs2"))) & (Bool (Set (Var "fss2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fss")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "fss")) ")" ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "fss1")) ")" ) ")" ) ")" )))) "holds" (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss2"))) ($#r1_hidden :::"="::: ) (Set (Var "fs2"))))))) ; begin theorem :: GRAPH_2: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 "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_graph_1 :::"joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set (Var "e")) ($#r2_graph_1 :::"joins"::: ) (Set (Var "v2")) "," (Set (Var "v1")))))) ; theorem :: GRAPH_2:30 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "," (Set (Var "v4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_graph_1 :::"joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) & (Bool (Set (Var "e")) ($#r2_graph_1 :::"joins"::: ) (Set (Var "v3")) "," (Set (Var "v4"))) & (Bool "not" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v3"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "v4"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v4"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "v3"))) ")" )))) ; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; func "G" :::"-VSet"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: GRAPH_2:def 5 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "X") & (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" )) "}" ; end; :: deftheorem defines :::"-VSet"::: GRAPH_2:def 5 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "G")) ($#k5_graph_2 :::"-VSet"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" )) "}" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "vs" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); let "c" be ($#m1_hidden :::"FinSequence":::); pred "vs" :::"is_vertex_seq_of"::: "c" means :: GRAPH_2:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "vs") ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "c" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_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 ($#k3_finseq_1 :::"len"::: ) "c"))) "holds" (Bool (Set "c" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_graph_1 :::"joins"::: ) (Set "vs" ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) "," (Set "vs" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_vertex_seq_of"::: GRAPH_2:def 6 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "c")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_graph_1 :::"joins"::: ) (Set (Set (Var "vs")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) "," (Set (Set (Var "vs")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" )))); theorem :: GRAPH_2:31 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "G")) ($#k5_graph_2 :::"-VSet"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "vs"))))))) ; theorem :: GRAPH_2:32 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: GRAPH_2:33 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))))) ; theorem :: GRAPH_2:34 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) & (Bool (Set (Var "vs2")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) & (Bool (Set (Var "vs1")) ($#r1_hidden :::"<>"::: ) (Set (Var "vs2")))) "holds" (Bool "(" (Bool (Set (Set (Var "vs1")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "vs2")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" "not" (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) "or" (Bool (Set (Var "vs")) ($#r1_hidden :::"="::: ) (Set (Var "vs1"))) "or" (Bool (Set (Var "vs")) ($#r1_hidden :::"="::: ) (Set (Var "vs2"))) ")" ) ")" ) ")" )))) ; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "c" be ($#m1_hidden :::"FinSequence":::); pred "c" :::"alternates_vertices_in"::: "G" means :: GRAPH_2:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "c") ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" "G" ($#k5_graph_2 :::"-VSet"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "c" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 2)) & (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"::: ) "c"))) "holds" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "c" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "c" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"alternates_vertices_in"::: GRAPH_2:def 7 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Var "G"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k5_graph_2 :::"-VSet"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "c")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 2)) & (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 (Var "c"))))) "holds" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); theorem :: GRAPH_2:35 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Var "G"))) & (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))))) ; theorem :: GRAPH_2:36 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Var "G"))) & (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "vs"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; theorem :: GRAPH_2:37 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Var "G"))) & (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "vs")) "is" ($#v1_graph_2 :::"TwoValued"::: ) ($#v2_graph_2 :::"Alternating"::: ) ($#m1_hidden :::"FinSequence":::))))) ; theorem :: GRAPH_2:38 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Var "G")))) "holds" (Bool "ex" (Set (Var "vs1")) "," (Set (Var "vs2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "vs1")) ($#r1_hidden :::"<>"::: ) (Set (Var "vs2"))) & (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) & (Bool (Set (Var "vs2")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" "not" (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) "or" (Bool (Set (Var "vs")) ($#r1_hidden :::"="::: ) (Set (Var "vs1"))) "or" (Bool (Set (Var "vs")) ($#r1_hidden :::"="::: ) (Set (Var "vs2"))) ")" ) ")" ) ")" )))) ; theorem :: GRAPH_2:39 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Bool "not" (Set (Var "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Var "G")))) ")" ) ")" ) "iff" (Bool "for" (Set (Var "vs1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "vs1")) ($#r1_hidden :::"="::: ) (Set (Var "vs")))) ")" )))) ; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "c" be ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); assume (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G")))) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool "(" (Bool (Set (Const "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Bool "not" (Set (Const "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Const "G")))) ")" ) ")" ) ; func :::"vertex-seq"::: "c" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") means :: GRAPH_2:def 8 (Bool it ($#r1_graph_2 :::"is_vertex_seq_of"::: ) "c"); end; :: deftheorem defines :::"vertex-seq"::: GRAPH_2:def 8 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Bool "not" (Set (Var "c")) ($#r2_graph_2 :::"alternates_vertices_in"::: ) (Set (Var "G")))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_graph_2 :::"vertex-seq"::: ) (Set (Var "c")))) "iff" (Bool (Set (Var "b3")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) ")" )))); theorem :: GRAPH_2:40 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "," (Set (Var "vs1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "," (Set (Var "c1")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) & (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "vs1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) "holds" (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c1"))))))) ; theorem :: GRAPH_2:41 (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "c")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k2_graph_2 :::"-cut"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "q")) "is" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))))))) ; theorem :: GRAPH_2:42 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "," (Set (Var "vs1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "," (Set (Var "c1")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "c")))) & (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k2_graph_2 :::"-cut"::: ) (Set (Var "c")))) & (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c"))) & (Bool (Set (Var "vs1")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "m")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k2_graph_2 :::"-cut"::: ) (Set (Var "vs"))))) "holds" (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c1"))))))) ; theorem :: GRAPH_2:43 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c1"))) & (Bool (Set (Var "vs2")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c2"))) & (Bool (Set (Set (Var "vs1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs2")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "c1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "c2"))) "is" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))))) ; theorem :: GRAPH_2:44 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "," (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c1"))) & (Bool (Set (Var "vs2")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c2"))) & (Bool (Set (Set (Var "vs1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs2")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "c2")))) & (Bool (Set (Var "vs")) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs1")) ($#k4_graph_2 :::"^'"::: ) (Set (Var "vs2"))))) "holds" (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))))) ; begin definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "IT" be ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); attr "IT" is :::"simple"::: means :: GRAPH_2:def 9 (Bool "ex" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "st" (Bool "(" (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) "IT") & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_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 "vs")))) & (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs")))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"simple"::: GRAPH_2:def 9 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "IT")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_graph_2 :::"simple"::: ) ) "iff" (Bool "ex" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "IT"))) & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_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 "vs")))) & (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs")))) ")" ) ")" ) ")" )) ")" ))); registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v3_graph_2 :::"simple"::: ) for ($#m1_graph_1 :::"Chain"::: ) "of" "G"; end; theorem :: GRAPH_2:45 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "sc")) "being" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "sc")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) "is" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))))) ; theorem :: GRAPH_2:46 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "sc")) "being" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "sc")))) & (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "sc"))) & (Bool (Set (Var "vs2")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "sc")))) "holds" (Bool (Set (Var "vs1")) ($#r1_hidden :::"="::: ) (Set (Var "vs2")))))) ; theorem :: GRAPH_2:47 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "sc")) "being" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "sc")))) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_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 "vs")))) & (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs")))) ")" ))))) ; theorem :: GRAPH_2:48 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "c")) "is" (Bool "not" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "fc")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "c"))(Bool "ex" (Set (Var "fvs")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "vs"))(Bool "ex" (Set (Var "c1")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))(Bool "ex" (Set (Var "vs1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "c1"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "c")))) & (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c1"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs1"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs")))) & (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs1")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs1")) ")" ))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fc"))) ($#r1_hidden :::"="::: ) (Set (Var "c1"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fvs"))) ($#r1_hidden :::"="::: ) (Set (Var "vs1"))) ")" )))))))) ; theorem :: GRAPH_2:49 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "c")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "vs")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "fc")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "c"))(Bool "ex" (Set (Var "fvs")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "vs"))(Bool "ex" (Set (Var "sc")) "being" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))(Bool "ex" (Set (Var "vs1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fc"))) ($#r1_hidden :::"="::: ) (Set (Var "sc"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fvs"))) ($#r1_hidden :::"="::: ) (Set (Var "vs1"))) & (Bool (Set (Var "vs1")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "sc"))) & (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs1")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs1")) ")" ))) ")" )))))))) ; registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> bbbadV2_FUNCT_1() for ($#m1_graph_1 :::"Chain"::: ) "of" "G"; end; theorem :: GRAPH_2:50 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")))) "holds" (Bool (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) "is" ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")))))) ; registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v3_graph_2 :::"simple"::: ) for ($#m1_graph_1 :::"Chain"::: ) "of" "G"; end; theorem :: GRAPH_2:51 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "sc")) "being" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "sc"))))) "holds" (Bool (Set (Var "sc")) "is" ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))))) ; theorem :: GRAPH_2:52 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "sc")) "being" ($#v3_graph_2 :::"simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "sc")) "is" ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "sc"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "sc"))) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Set (Var "sc")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "sc")) ($#k1_funct_1 :::"."::: ) (Num 2))) ")" ) ")" ))) ; registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v7_graph_1 :::"oriented"::: ) for ($#m1_graph_1 :::"Chain"::: ) "of" "G"; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "oc" be ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); assume (Bool (Set (Const "oc")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"vertex-seq"::: "oc" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") means :: GRAPH_2:def 10 (Bool "(" (Bool it ($#r1_graph_2 :::"is_vertex_seq_of"::: ) "oc") & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "oc" ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) ")" ); end; :: deftheorem defines :::"vertex-seq"::: GRAPH_2:def 10 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "oc")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "oc")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_graph_2 :::"vertex-seq"::: ) (Set (Var "oc")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_graph_2 :::"is_vertex_seq_of"::: ) (Set (Var "oc"))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "oc")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) ")" ) ")" )))); begin theorem :: GRAPH_2:53 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k4_graph_2 :::"^'"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 1)))))) ; theorem :: GRAPH_2:54 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f2")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k4_graph_2 :::"^'"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f1")) ($#k4_graph_2 :::"^'"::: ) (Set (Var "f2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" )))))) ; theorem :: GRAPH_2:55 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_graph_2 :::"^'"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: GRAPH_2:56 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_graph_2 :::"^'"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: GRAPH_2:57 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "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 "f1"))))) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k4_graph_2 :::"^'"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))))))) ; theorem :: GRAPH_2:58 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "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 "f2"))))) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k4_graph_2 :::"^'"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; definitionlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); let "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); assume that (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "m"))) and (Bool (Set (Const "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "n"))) and (Bool (Set (Const "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "F")))) ; func :::"min_at"::: "(" "F" "," "m" "," "n" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GRAPH_2:def 11 (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" "m" "," "n" ")" ($#k2_graph_2 :::"-cut"::: ) "F" ")" ))) & (Bool (Set it ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "X")) ")" ) ($#k4_finseq_4 :::".."::: ) (Set "(" "(" "m" "," "n" ")" ($#k2_graph_2 :::"-cut"::: ) "F" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) "m")) ")" )); end; :: deftheorem defines :::"min_at"::: GRAPH_2:def 11 : (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_graph_2 :::"min_at"::: ) "(" (Set (Var "F")) "," (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k2_graph_2 :::"-cut"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set (Var "b4")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "X")) ")" ) ($#k4_finseq_4 :::".."::: ) (Set "(" "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k2_graph_2 :::"-cut"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")))) ")" )) ")" )))); theorem :: GRAPH_2:59 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "ma")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Var "ma")) ($#r1_hidden :::"="::: ) (Set ($#k8_graph_2 :::"min_at"::: ) "(" (Set (Var "F")) "," (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "ma"))) & (Bool (Set (Var "ma")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "ma"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ma")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "ma"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ))) ; theorem :: GRAPH_2:60 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k8_graph_2 :::"min_at"::: ) "(" (Set (Var "F")) "," (Set (Var "m")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))))) ; definitionlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); let "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "F" :::"is_non_decreasing_on"::: "m" "," "n" means :: GRAPH_2:def 12 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "m" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) "n")) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))); end; :: deftheorem defines :::"is_non_decreasing_on"::: GRAPH_2:def 12 : (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Set (Var "m")) "," (Set (Var "n"))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) ")" ))); definitionlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "F" :::"is_split_at"::: "n" means :: GRAPH_2:def 13 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_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 :::"<="::: ) "n") & (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F"))) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))); end; :: deftheorem defines :::"is_split_at"::: GRAPH_2:def 13 : (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r4_graph_2 :::"is_split_at"::: ) (Set (Var "n"))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_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 (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) ")" ))); theorem :: GRAPH_2:61 (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "ma")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set (Var "ma")) ($#r1_hidden :::"="::: ) (Set ($#k8_graph_2 :::"min_at"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ) ")" )) & (Bool (Set (Var "F")) ($#r4_graph_2 :::"is_split_at"::: ) (Set (Var "k"))) & (Bool (Set (Var "F")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Num 1) "," (Set (Var "k"))) & (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "ma")) ")" ) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "ma")) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) "holds" (Bool (Set (Var "F1")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Num 1) "," (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: GRAPH_2:62 (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "ma")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set (Var "ma")) ($#r1_hidden :::"="::: ) (Set ($#k8_graph_2 :::"min_at"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ) ")" )) & (Bool (Set (Var "F")) ($#r4_graph_2 :::"is_split_at"::: ) (Set (Var "k"))) & (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "ma")) ")" ) ")" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "ma")) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) "holds" (Bool (Set (Var "F1")) ($#r4_graph_2 :::"is_split_at"::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: GRAPH_2:63 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "f")) ($#r3_graph_2 :::"is_non_decreasing_on"::: ) (Set (Var "m")) "," (Set (Var "n"))))) ;