:: JORDAN1D semantic presentation begin theorem :: JORDAN1D:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "K")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "K")))) ")" )) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "B"))))) ; registrationlet "m" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set (Num 2) ($#k1_newton :::"|^"::: ) "m") -> ($#v1_abian :::"even"::: ) ; end; registrationlet "n" be ($#v1_abian :::"even"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "m" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "n" ($#k1_newton :::"|^"::: ) "m") -> ($#v1_abian :::"even"::: ) ; end; theorem :: JORDAN1D:2 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "r")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_newton :::"|^"::: ) (Set (Var "i")))))) ; begin theorem :: JORDAN1D:3 (Bool "for" (Set (Var "m")) "," (Set (Var "i")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "m")) "," (Set (Var "a")) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) "," (Set (Var "b")) ")" ")" ) ($#k17_euclid :::"`1"::: ) )))) ; theorem :: JORDAN1D:4 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "b")) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: JORDAN1D:5 (Bool "for" (Set (Var "m")) "," (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ))))) ; theorem :: JORDAN1D:6 (Bool "for" (Set (Var "m")) "," (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "D")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) where a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1))) ")" ) "}" ))))) ; theorem :: JORDAN1D:7 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k21_pscomp_1 :::"N-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k21_pscomp_1 :::"N-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" )))) ; theorem :: JORDAN1D:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k23_pscomp_1 :::"E-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k23_pscomp_1 :::"E-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" )))) ; theorem :: JORDAN1D:11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:12 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" )))) ; theorem :: JORDAN1D:13 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k25_pscomp_1 :::"S-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:14 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k25_pscomp_1 :::"S-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" )))) ; theorem :: JORDAN1D:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k24_pscomp_1 :::"S-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k24_pscomp_1 :::"S-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" )))) ; theorem :: JORDAN1D:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" )))) ; theorem :: JORDAN1D:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k19_pscomp_1 :::"W-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:20 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k19_pscomp_1 :::"W-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" )))) ; theorem :: JORDAN1D:21 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:22 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k21_pscomp_1 :::"N-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ")" )) ")" )))) ; theorem :: JORDAN1D:23 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) ")" )))) ; theorem :: JORDAN1D:24 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k23_pscomp_1 :::"E-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) "," (Set (Var "j")) ")" )) ")" )))) ; theorem :: JORDAN1D:25 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) "," (Set (Var "j")) ")" )) ")" )))) ; theorem :: JORDAN1D:26 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) "," (Set (Var "j")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) ")" )))) ; theorem :: JORDAN1D:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k25_pscomp_1 :::"S-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" )) ")" )))) ; theorem :: JORDAN1D:28 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k24_pscomp_1 :::"S-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" )) ")" )))) ; theorem :: JORDAN1D:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (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 "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) ")" )))) ; theorem :: JORDAN1D:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" )) ")" )))) ; theorem :: JORDAN1D:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k19_pscomp_1 :::"W-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" )) ")" )))) ; theorem :: JORDAN1D:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) ")" )))) ;