:: JORDAN3 semantic presentation begin theorem :: JORDAN3:1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) ")" ))) ; theorem :: JORDAN3:2 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) "or" (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) ")" ) & (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Bool "not" (Set (Set (Var "q1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q2")) ($#k17_euclid :::"`1"::: ) )))) "holds" (Bool (Set (Set (Var "q1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q2")) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN3:3 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) "or" (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) ")" ) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Bool "not" (Set (Set (Var "q1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q2")) ($#k17_euclid :::"`1"::: ) )))) "holds" (Bool (Set (Set (Var "q1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q2")) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: JORDAN3:4 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: JORDAN3:5 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n"))) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: JORDAN3:6 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k1"))) & (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2"))) & (Bool (Set (Var "k2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "k1")) ($#r1_hidden :::"<>"::: ) (Set (Var "k2")))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; begin definitionlet "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); assume (Bool (Set (Const "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Const "f")))) ; func :::"Index"::: "(" "p" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: JORDAN3:def 1 (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_seq_4 :::"min"::: ) (Set (Var "S")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "p" ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" "f" "," (Set (Var "i")) ")" )) "}" ) ")" )); end; :: deftheorem defines :::"Index"::: JORDAN3:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) "iff" (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_seq_4 :::"min"::: ) (Set (Var "S")))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) "}" ) ")" )) ")" )))); theorem :: JORDAN3:7 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))))) ; theorem :: JORDAN3:8 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) & (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" ))) ; theorem :: JORDAN3:9 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" )))) ; theorem :: JORDAN3:10 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ))) "holds" (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: JORDAN3:11 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: JORDAN3:12 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i1"))))) "holds" (Bool (Set (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i1")))))) ; theorem :: JORDAN3:13 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i1")) ")" )) & (Bool (Bool "not" (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )))) "holds" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: JORDAN3:14 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) ) & (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i1")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i1"))))) "holds" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ))))) ; definitionlet "g" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred "g" :::"is_S-Seq_joining"::: "p1" "," "p2" means :: JORDAN3:def 2 (Bool "(" (Bool "g" "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set "g" ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "p1") & (Bool (Set "g" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "g" ")" )) ($#r1_hidden :::"="::: ) "p2") ")" ); end; :: deftheorem defines :::"is_S-Seq_joining"::: JORDAN3:def 2 : (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" ) ")" ))); theorem :: JORDAN3:15 (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "g"))) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Var "p2")) "," (Set (Var "p1"))))) ; theorem :: JORDAN3:16 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "g")) "," (Set (Var "j")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: JORDAN3:17 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ")" )))) "holds" (Bool (Set (Var "g")) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Var "p")) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))))) ; theorem :: JORDAN3:18 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "g")) "," (Set (Var "j")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) ")" ))))) ; theorem :: JORDAN3:19 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds" (Bool (Set (Var "g")) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))))) ; begin definitionlet "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"L_Cut"::: "(" "f" "," "p" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN3:def 3 (Set (Set ($#k12_finseq_1 :::"<*"::: ) "p" ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" "f" "," (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ")" ")" )) if (Bool "p" ($#r1_hidden :::"<>"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) otherwise (Set ($#k3_finseq_6 :::"mid"::: ) "(" "f" "," (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ")" ); func :::"R_Cut"::: "(" "f" "," "p" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN3:def 4 (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" "f" "," (Num 1) "," (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) "p" ($#k12_finseq_1 :::"*>"::: ) )) if (Bool "p" ($#r1_hidden :::"<>"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Num 1))) otherwise (Set ($#k12_finseq_1 :::"<*"::: ) "p" ($#k12_finseq_1 :::"*>"::: ) ); end; :: deftheorem defines :::"L_Cut"::: JORDAN3:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "implies" (Bool (Set ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) "implies" (Bool (Set ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" )) ")" ")" ))); :: deftheorem defines :::"R_Cut"::: JORDAN3:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "implies" (Bool (Set ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1))))) "implies" (Bool (Set ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )) ")" ")" ))); theorem :: JORDAN3:20 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))))) ; theorem :: JORDAN3:21 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))))) ; theorem :: JORDAN3:22 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ))))) ; theorem :: JORDAN3:23 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (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 "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "implies" (Bool (Set (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "implies" (Bool (Set (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ))) ")" ")" ) ")" ) ")" ))) ; theorem :: JORDAN3:24 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (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 ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ))) "holds" (Bool (Set (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ))) ; theorem :: JORDAN3:25 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" )) ")" ")" ))) ; theorem :: JORDAN3:26 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1))) ")" ")" ))) ; definitionlet "p1", "p2", "q1", "q2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred :::"LE"::: "q1" "," "q2" "," "p1" "," "p2" means :: JORDAN3:def 5 (Bool "(" (Bool "q1" ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p1" "," "p2" ")" )) & (Bool "q2" ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p1" "," "p2" ")" )) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool "q1" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r1")) ")" ) ($#k1_rlvect_1 :::"*"::: ) "p1" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r1")) ($#k1_rlvect_1 :::"*"::: ) "p2" ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Var "r2")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool "q2" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r2")) ")" ) ($#k1_rlvect_1 :::"*"::: ) "p1" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k1_rlvect_1 :::"*"::: ) "p2" ")" )))) "holds" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) ")" ) ")" ); end; :: deftheorem defines :::"LE"::: JORDAN3:def 5 : (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool "(" (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r1")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Var "r2")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "q2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r2")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" )))) "holds" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) ")" ) ")" ) ")" )); definitionlet "p1", "p2", "q1", "q2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred :::"LT"::: "q1" "," "q2" "," "p1" "," "p2" means :: JORDAN3:def 6 (Bool "(" (Bool ($#r2_jordan3 :::"LE"::: ) "q1" "," "q2" "," "p1" "," "p2") & (Bool "q1" ($#r1_hidden :::"<>"::: ) "q2") ")" ); end; :: deftheorem defines :::"LT"::: JORDAN3:def 6 : (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool ($#r3_jordan3 :::"LT"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool "(" (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) ")" ) ")" )); theorem :: JORDAN3:27 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "q2")) "," (Set (Var "q1")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "q2")))) ; theorem :: JORDAN3:28 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool "(" (Bool "(" (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2"))) "or" (Bool ($#r3_jordan3 :::"LT"::: ) (Set (Var "q2")) "," (Set (Var "q1")) "," (Set (Var "p1")) "," (Set (Var "p2"))) ")" ) & (Bool "(" "not" (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1")) "," (Set (Var "p2"))) "or" "not" (Bool ($#r3_jordan3 :::"LT"::: ) (Set (Var "q2")) "," (Set (Var "q1")) "," (Set (Var "p1")) "," (Set (Var "p2"))) ")" ) ")" )) ; theorem :: JORDAN3:29 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" ))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ))))) ; theorem :: JORDAN3:30 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "q")) ")" )) ")" )) ; theorem :: JORDAN3:31 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" )) & (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ))))) ; begin definitionlet "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"B_Cut"::: "(" "f" "," "p" "," "q" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN3:def 7 (Set ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" "f" "," "p" ")" ")" ) "," "q" ")" ) if (Bool "(" (Bool "(" (Bool "p" ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) "f")) & (Bool "q" ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) "f")) & (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" "q" "," "f" ")" )) ")" ) "or" (Bool "(" (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" "q" "," "f" ")" )) & (Bool ($#r2_jordan3 :::"LE"::: ) "p" "," "q" "," (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ")" )) "," (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" "p" "," "f" ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) otherwise (Set ($#k4_finseq_5 :::"Rev"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" "f" "," "q" ")" ")" ) "," "p" ")" ")" )); end; :: deftheorem defines :::"B_Cut"::: JORDAN3:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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) ")" ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" )) ")" ) "or" (Bool "(" (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" )) & (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )) "implies" (Bool (Set ($#k4_jordan3 :::"B_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" )) ")" & (Bool "(" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" )) ")" ) "or" (Bool "(" (Bool (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "q")) "," (Set (Var "f")) ")" )) & (Bool ($#r2_jordan3 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" )) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k1_jordan3 :::"Index"::: ) "(" (Set (Var "p")) "," (Set (Var "f")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) "or" (Bool (Set ($#k4_jordan3 :::"B_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "p")) ")" ")" ))) ")" ) ")" ))); theorem :: JORDAN3:32 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))))) ; theorem :: JORDAN3:33 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Var "p")) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))))) ; theorem :: JORDAN3:34 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: JORDAN3:35 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: JORDAN3:36 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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 "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k4_jordan3 :::"B_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))))) ; theorem :: JORDAN3:37 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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 "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k4_jordan3 :::"B_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: JORDAN3:38 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "g")) "," (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ")" )) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) )) ; theorem :: JORDAN3:39 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "g")) "," (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ")" )) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" )))) ; theorem :: JORDAN3:40 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))))) ; theorem :: JORDAN3:41 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))))) ; theorem :: JORDAN3:42 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))))) ; theorem :: JORDAN3:43 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "g")) "," (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ")" )) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Var "p")) "," (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ))))) ; theorem :: JORDAN3:44 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_jordan3 :::"L_Cut"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "g")) "," (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ")" )) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: JORDAN3:45 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) )) ; theorem :: JORDAN3:46 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" )))) ; theorem :: JORDAN3:47 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "g")) "," (Set (Var "p")) ")" ")" )) ($#r1_jordan3 :::"is_S-Seq_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))))) ; theorem :: JORDAN3:48 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_jordan3 :::"R_Cut"::: ) "(" (Set (Var "g")) "," (Set (Var "p")) ")" ")" )) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ;