:: JORDAN1H semantic presentation begin registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "D" ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; registrationlet "F" be ($#v2_relat_1 :::"non-empty"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k3_funct_6 :::"rngs"::: ) "F") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; theorem :: JORDAN1H:1 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_tarski :::"}"::: ) ) ")" )))) ; theorem :: JORDAN1H:2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) ; theorem :: JORDAN1H:3 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_tarski :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "S")))))) ; begin definitionfunc :::"RealOrd"::: -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: JORDAN1H:def 1 "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) "}" ; end; :: deftheorem defines :::"RealOrd"::: JORDAN1H:def 1 : (Bool (Set ($#k1_jordan1h :::"RealOrd"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) "}" ); theorem :: JORDAN1H:4 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_jordan1h :::"RealOrd"::: ) ))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) ; theorem :: JORDAN1H:5 (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set ($#k1_jordan1h :::"RealOrd"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; registration cluster (Set ($#k1_jordan1h :::"RealOrd"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v3_orders_1 :::"being_linear-order"::: ) ; end; theorem :: JORDAN1H:6 (Bool (Set ($#k1_jordan1h :::"RealOrd"::: ) ) ($#r3_orders_1 :::"linearly_orders"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: JORDAN1H:7 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set ($#k1_jordan1h :::"RealOrd"::: ) ) "," (Set (Var "A")) ")" ) "is" ($#v5_valued_0 :::"increasing"::: ) )) ; theorem :: JORDAN1H:8 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set ($#k1_jordan1h :::"RealOrd"::: ) ) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k28_seq_4 :::"Incr"::: ) (Set (Var "f")))))) ; registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set ($#k1_jordan1h :::"RealOrd"::: ) ) "," "A" ")" ) -> ($#v5_valued_0 :::"increasing"::: ) ; end; theorem :: JORDAN1H:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#v3_orders_1 :::"being_linear-order"::: ) ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))))) ; begin theorem :: JORDAN1H:10 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_goboard1 :::"X_axis"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))) ; theorem :: JORDAN1H:11 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k2_goboard1 :::"Y_axis"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); :: original: :::"Values"::: redefine func :::"Values"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" "D"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); cluster (Set ($#k16_matrix_1 :::"Values"::: ) "M") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: JORDAN1H:12 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan1h :::"Values"::: ) (Set (Var "M"))))))) ; theorem :: JORDAN1H:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_jordan1h :::"Values"::: ) (Set (Var "M"))))))) ; theorem :: JORDAN1H:14 (Bool "for" (Set (Var "G")) "being" bbbadV3_RELAT_1() ($#v5_goboard1 :::"X_increasing-in-column"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" )))) ; theorem :: JORDAN1H:15 (Bool "for" (Set (Var "G")) "being" ($#v2_goboard1 :::"X_equal-in-line"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) ; theorem :: JORDAN1H:16 (Bool "for" (Set (Var "G")) "being" bbbadV3_RELAT_1() ($#v2_goboard1 :::"X_equal-in-line"::: ) ($#v5_goboard1 :::"X_increasing-in-column"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" )))) ; theorem :: JORDAN1H:17 (Bool "for" (Set (Var "G")) "being" bbbadV3_RELAT_1() ($#v4_goboard1 :::"Y_increasing-in-line"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" )))) ; theorem :: JORDAN1H:18 (Bool "for" (Set (Var "G")) "being" bbbadV3_RELAT_1() ($#v3_goboard1 :::"Y_equal-in-column"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) ; theorem :: JORDAN1H:19 (Bool "for" (Set (Var "G")) "being" bbbadV3_RELAT_1() ($#v3_goboard1 :::"Y_equal-in-column"::: ) ($#v4_goboard1 :::"Y_increasing-in-line"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" )))) ; begin theorem :: JORDAN1H:20 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (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 (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ))))) ; theorem :: JORDAN1H:21 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_goboard5 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) ")" )))) ; theorem :: JORDAN1H:22 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (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 (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ))))) ; theorem :: JORDAN1H:23 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) ")" )))) ; theorem :: JORDAN1H:24 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "holds" (Bool "(" "not" (Bool (Set (Var "P")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k3_subset_1 :::"`"::: ) )) "or" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard9 :::"RightComp"::: ) (Set (Var "f")))) "or" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f")))) ")" ))) ; theorem :: JORDAN1H:25 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (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 (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_goboard9 :::"RightComp"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f")))) ")" )))) ; theorem :: JORDAN1H:26 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) ")" ))) ; theorem :: JORDAN1H:27 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" ) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "M")))))) ; registration cluster ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v1_matrix_1 :::"tabular"::: ) ($#v2_goboard1 :::"X_equal-in-line"::: ) ($#v3_goboard1 :::"Y_equal-in-column"::: ) ($#v4_goboard1 :::"Y_increasing-in-line"::: ) ($#v5_goboard1 :::"X_increasing-in-column"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ($#k3_finseq_2 :::"*"::: ) ); end; theorem :: JORDAN1H:28 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "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 "G"))))) "holds" (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set ($#k1_jordan1h :::"RealOrd"::: ) ) "," (Set "(" (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )))) ; theorem :: JORDAN1H:29 (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set ($#k1_jordan1h :::"RealOrd"::: ) ) "," (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: JORDAN1H:30 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" )) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" ))) "holds" (Bool (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ))))) ; theorem :: JORDAN1H:31 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" )) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" ))) "holds" (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ))))) ; registrationlet "G" be ($#m2_finseq_1 :::"Go-board":::); cluster (Set ($#k16_matrix_1 :::"Values"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: JORDAN1H:32 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_goboard2 :::"GoB"::: ) "(" (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set ($#k1_jordan1h :::"RealOrd"::: ) ) "," (Set "(" (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set ($#k1_jordan1h :::"RealOrd"::: ) ) "," (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ) ")" ) ")" ")" ) ")" ))) ; theorem :: JORDAN1H:33 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" ))) & (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_jordan1h :::"Values"::: ) (Set (Var "G")) ")" )))) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_goboard2 :::"GoB"::: ) (Set (Var "f")))))) ; theorem :: JORDAN1H:34 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" )) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" )) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" )) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" ))) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_goboard2 :::"GoB"::: ) (Set (Var "f")))))) ; begin theorem :: JORDAN1H:35 (Bool "for" (Set (Var "i")) "," (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 "i")))) "holds" (Bool (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 2) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "m")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: JORDAN1H:36 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 2) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "m")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) )) & (Bool (Set (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 2) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "m")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#k3_real_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "m")) ")" ")" ))) ")" ))) ; theorem :: JORDAN1H:37 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 2) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "m")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) )) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k9_real_1 :::"-"::: ) (Num 2) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "m")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2) ")" ) ($#k1_int_1 :::"/]"::: ) )) & (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" )) ")" )))) ; theorem :: JORDAN1H:38 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i1"))) & (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "m")) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j1"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "m")) ")" ")" ))) & (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" )) ")" )))) ; theorem :: JORDAN1H:39 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v9_rltopsp1 :::"bounded"::: ) )) "holds" (Bool "not" (Bool (Set ($#k2_jordan2c :::"UBD"::: ) (Set (Var "P"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: JORDAN1H:40 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "st" (Bool (Bool (Set ($#k1_finseq_6 :::"Rotate"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) "is" ($#v1_sprect_2 :::"clockwise_oriented"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v1_sprect_2 :::"clockwise_oriented"::: ) ))) ; theorem :: JORDAN1H:41 (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "st" (Bool (Bool (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_jordan2c :::"UBD"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Var "f")) "is" ($#v1_sprect_2 :::"clockwise_oriented"::: ) )) ; begin theorem :: JORDAN1H:42 (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "holds" (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard9 :::"RightComp"::: ) (Set (Var "f"))))) ; theorem :: JORDAN1H:43 (Bool "for" (Set (Var "f")) "being" ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "holds" (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k3_goboard9 :::"RightComp"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f"))))) ; theorem :: JORDAN1H:44 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set ($#k2_goboard2 :::"GoB"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )))) ; theorem :: JORDAN1H:45 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Num 1) ")" )))) ; theorem :: JORDAN1H:46 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "j")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k3_goboard9 :::"RightComp"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "i")) ")" ")" ) ")" ))))) ; theorem :: JORDAN1H:47 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "i")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: JORDAN1H:48 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k3_goboard9 :::"RightComp"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "j")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_goboard9 :::"RightComp"::: ) (Set "(" ($#k1_jordan9 :::"Cage"::: ) "(" (Set (Var "C")) "," (Set (Var "i")) ")" ")" ))))) ; begin definitionlet "C" be ($#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) ")" ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"X-SpanStart"::: "(" "C" "," "n" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: JORDAN1H:def 2 (Set (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)); end; :: deftheorem defines :::"X-SpanStart"::: JORDAN1H:def 2 : (Bool "for" (Set (Var "C")) "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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_jordan1h :::"X-SpanStart"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))))); theorem :: JORDAN1H:49 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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) ")" ) "holds" (Bool "(" (Bool (Num 2) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_jordan1h :::"X-SpanStart"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_jordan1h :::"X-SpanStart"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) ")" ))) ; theorem :: JORDAN1H:50 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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) ")" ) "holds" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_jordan1h :::"X-SpanStart"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k3_jordan1h :::"X-SpanStart"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) ")" ))) ; definitionlet "C" be ($#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) ")" ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "n" :::"is_sufficiently_large_for"::: "C" means :: JORDAN1H:def 3 (Bool "ex" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" "C" "," "n" ")" ")" ))) & (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" "C" "," "n" ")" ")" ) "," (Set "(" (Set "(" ($#k3_jordan1h :::"X-SpanStart"::: ) "(" "C" "," "n" ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_jordan2c :::"BDD"::: ) "C")) ")" )); end; :: deftheorem defines :::"is_sufficiently_large_for"::: JORDAN1H:def 3 : (Bool "for" (Set (Var "C")) "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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r1_jordan1h :::"is_sufficiently_large_for"::: ) (Set (Var "C"))) "iff" (Bool "ex" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) "," (Set "(" (Set "(" ($#k3_jordan1h :::"X-SpanStart"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_jordan2c :::"BDD"::: ) (Set (Var "C")))) ")" )) ")" ))); theorem :: JORDAN1H:51 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "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 (Set (Var "n")) ($#r1_jordan1h :::"is_sufficiently_large_for"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)))) ; theorem :: JORDAN1H:52 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:53 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:54 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "j1")) "," (Set (Var "i2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j1")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:55 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:56 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:57 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:58 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "j1")) "," (Set (Var "i2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j1")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:59 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:60 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:61 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:62 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "j1")) "," (Set (Var "i2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j1")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: JORDAN1H:63 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "j2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_jordan8 :::"Gauge"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ")" ))))))) ;