:: SPPOL_2 semantic presentation begin theorem :: SPPOL_2:1 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r19")) "," (Set (Var "r29")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k19_euclid :::"]|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "r19")) "," (Set (Var "r29")) ($#k19_euclid :::"]|"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Var "r19"))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set (Var "r29"))) ")" )) ; theorem :: SPPOL_2:2 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" ) "," (Set (Var "j")) ")" )))) ; theorem :: SPPOL_2:3 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )))) ; theorem :: SPPOL_2:4 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" ) ")" )))) ; theorem :: SPPOL_2:5 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" ) ")" )))) ; theorem :: SPPOL_2:6 (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 "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )))) ; theorem :: SPPOL_2:7 (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 "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "g")) "," (Set (Var "i")) ")" )))) ; theorem :: SPPOL_2:8 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ))) ; theorem :: SPPOL_2: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) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k1_finseq_5 :::"-:"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_finseq_5 :::"-:"::: ) (Set (Var "p")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ))))) ; theorem :: SPPOL_2: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) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_finseq_5 :::":-"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k4_finseq_4 :::".."::: ) (Set (Var "f")) ")" ) ")" ) ")" ))))) ; theorem :: SPPOL_2:11 (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: SPPOL_2:12 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SPPOL_2: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) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#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 "i")) ")" )) ")" )))) ; theorem :: SPPOL_2: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) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" )))) ; theorem :: SPPOL_2:15 (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 (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 (Var "f")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))))) ; theorem :: SPPOL_2:16 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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 (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 (Var "f"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))))) ; theorem :: SPPOL_2:17 (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 (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))))) ; theorem :: SPPOL_2:18 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) ; theorem :: SPPOL_2:19 (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 (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set (Var "p")) ")" ")" ))))) ; theorem :: SPPOL_2: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 (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ))))) ; theorem :: SPPOL_2:21 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) ; theorem :: SPPOL_2:22 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" )))) ; theorem :: SPPOL_2:23 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "f1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "f2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) ")" ) "," (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f2")) ")" )))) ; theorem :: SPPOL_2:24 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k1_finseq_5 :::"-:"::: ) (Set (Var "q")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k2_finseq_5 :::":-"::: ) (Set (Var "q")) ")" ) ")" ))))) ; theorem :: SPPOL_2: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) ")" ) (Bool "for" (Set (Var "n")) "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 "n")) ")" ))) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k5_finseq_5 :::"Ins"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "p")) ")" ")" )))))) ; begin registration cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_topreal1 :::"being_S-Seq"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); cluster ($#v4_topreal1 :::"being_S-Seq"::: ) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_topreal1 :::"special"::: ) ($#v2_topreal1 :::"unfolded"::: ) ($#v3_topreal1 :::"s.n.c."::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_topreal1 :::"special"::: ) ($#v2_topreal1 :::"unfolded"::: ) ($#v3_topreal1 :::"s.n.c."::: ) -> ($#v4_topreal1 :::"being_S-Seq"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); cluster ($#v4_topreal1 :::"being_S-Seq"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); end; registration cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_topreal1 :::"special"::: ) ($#v2_topreal1 :::"unfolded"::: ) ($#v3_topreal1 :::"s.n.c."::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); end; theorem :: SPPOL_2:26 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) )) ; registrationlet "f" be ($#v2_topreal1 :::"unfolded"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "f" ($#k16_finseq_1 :::"|"::: ) "n") -> ($#v2_topreal1 :::"unfolded"::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set "f" ($#k1_rfinseq :::"/^"::: ) "n") -> ($#v2_topreal1 :::"unfolded"::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; theorem :: SPPOL_2:27 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_finseq_5 :::":-"::: ) (Set (Var "p"))) "is" ($#v2_topreal1 :::"unfolded"::: ) ))) ; registrationlet "f" be ($#v2_topreal1 :::"unfolded"::: ) ($#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) ")" ); cluster (Set "f" ($#k1_finseq_5 :::"-:"::: ) "p") -> ($#v2_topreal1 :::"unfolded"::: ) ; end; theorem :: SPPOL_2:28 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) )) "holds" (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f"))) "is" ($#v2_topreal1 :::"unfolded"::: ) )) ; theorem :: SPPOL_2:29 (Bool "for" (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 "g")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "g")) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) "is" ($#v2_topreal1 :::"unfolded"::: ) ))) ; theorem :: SPPOL_2:30 (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 "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )) "is" ($#v2_topreal1 :::"unfolded"::: ) )))) ; theorem :: SPPOL_2:31 (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 "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "g")) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) "is" ($#v2_topreal1 :::"unfolded"::: ) ))) ; theorem :: SPPOL_2: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) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set ($#k5_finseq_5 :::"Ins"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "p")) ")" ) "is" ($#v2_topreal1 :::"unfolded"::: ) )))) ; theorem :: SPPOL_2:33 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "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 (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) )) ; registrationlet "f" be ($#v3_topreal1 :::"s.n.c."::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "f" ($#k16_finseq_1 :::"|"::: ) "n") -> ($#v3_topreal1 :::"s.n.c."::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set "f" ($#k1_rfinseq :::"/^"::: ) "n") -> ($#v3_topreal1 :::"s.n.c."::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; registrationlet "f" be ($#v3_topreal1 :::"s.n.c."::: ) ($#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) ")" ); cluster (Set "f" ($#k1_finseq_5 :::"-:"::: ) "p") -> ($#v3_topreal1 :::"s.n.c."::: ) ; end; theorem :: SPPOL_2: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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_finseq_5 :::":-"::: ) (Set (Var "p"))) "is" ($#v3_topreal1 :::"s.n.c."::: ) ))) ; theorem :: SPPOL_2:35 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) )) "holds" (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f"))) "is" ($#v3_topreal1 :::"s.n.c."::: ) )) ; theorem :: SPPOL_2:36 (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 (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_topreal1 :::"s.n.c."::: ) ) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "g")))) & (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 (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#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 (Var "g"))))) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "g")) "," (Set (Var "i")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) "is" ($#v3_topreal1 :::"s.n.c."::: ) )) ; theorem :: SPPOL_2:37 (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 "n")) "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 (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))))) "holds" (Bool (Set ($#k5_finseq_5 :::"Ins"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "p")) ")" ) "is" ($#v3_topreal1 :::"s.n.c."::: ) )))) ; registration cluster (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) -> ($#v1_topreal1 :::"special"::: ) ; end; registrationlet "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "p" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_topreal1 :::"special"::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; theorem :: SPPOL_2:38 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) "or" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) ")" )) "holds" (Bool (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_finseq_4 :::"*>"::: ) ) "is" ($#v1_topreal1 :::"special"::: ) )) ; registrationlet "f" be ($#v1_topreal1 :::"special"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "f" ($#k16_finseq_1 :::"|"::: ) "n") -> ($#v1_topreal1 :::"special"::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set "f" ($#k1_rfinseq :::"/^"::: ) "n") -> ($#v1_topreal1 :::"special"::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; theorem :: SPPOL_2:39 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_finseq_5 :::":-"::: ) (Set (Var "p"))) "is" ($#v1_topreal1 :::"special"::: ) ))) ; registrationlet "f" be ($#v1_topreal1 :::"special"::: ) ($#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) ")" ); cluster (Set "f" ($#k1_finseq_5 :::"-:"::: ) "p") -> ($#v1_topreal1 :::"special"::: ) ; end; theorem :: SPPOL_2:40 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) )) "holds" (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f"))) "is" ($#v1_topreal1 :::"special"::: ) )) ; theorem :: SPPOL_2: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) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set ($#k5_finseq_5 :::"Ins"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "p")) ")" ) "is" ($#v1_topreal1 :::"special"::: ) )))) ; theorem :: SPPOL_2:42 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k4_finseq_4 :::".."::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "q")) ($#k4_finseq_4 :::".."::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v2_topreal1 :::"unfolded"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_topreal1 :::"s.n.c."::: ) )) "holds" (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k1_finseq_5 :::"-:"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k2_finseq_5 :::":-"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "q")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: SPPOL_2:43 (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 "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) "or" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) ")" )) "holds" (Bool (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_finseq_4 :::"*>"::: ) ) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) )) ; definitionmode S-Sequence_in_R2 is ($#v4_topreal1 :::"being_S-Seq"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; registrationlet "f" be ($#m2_finseq_1 :::"S-Sequence_in_R2":::); cluster (Set ($#k3_finseq_5 :::"Rev"::: ) "f") -> ($#v4_topreal1 :::"being_S-Seq"::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; theorem :: SPPOL_2:44 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))))) ; theorem :: SPPOL_2:45 (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 "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) "or" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) ")" )) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v5_topreal1 :::"being_S-P_arc"::: ) )) ; theorem :: SPPOL_2:46 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "p")) ($#k4_finseq_4 :::".."::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "f")) ($#k1_finseq_5 :::"-:"::: ) (Set (Var "p"))) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: SPPOL_2:47 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "p")) ($#k4_finseq_4 :::".."::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_finseq_5 :::":-"::: ) (Set (Var "p"))) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ))) ; theorem :: SPPOL_2:48 (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"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))))) "holds" (Bool (Set ($#k5_finseq_5 :::"Ins"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) )))) ; begin registration cluster ($#v5_topreal1 :::"being_S-P_arc"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); end; theorem :: SPPOL_2:49 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "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 "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p2")) "," (Set (Var "p1"))))) ; definitionlet "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred "p1" "," "p2" :::"split"::: "P" means :: SPPOL_2:def 1 (Bool "(" (Bool "p1" ($#r1_hidden :::"<>"::: ) "p2") & (Bool "ex" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) "st" (Bool "(" (Bool "p1" ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool "p1" ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool "p2" ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ))) & (Bool "p2" ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) "p1" "," "p2" ($#k2_tarski :::"}"::: ) )) & (Bool "P" ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ); end; :: deftheorem defines :::"split"::: SPPOL_2:def 1 : (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))) "iff" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool "ex" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"S-Sequence_in_R2":::) "st" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ) ")" ))); theorem :: SPPOL_2:50 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "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 "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "p2")) "," (Set (Var "p1")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))))) ; theorem :: SPPOL_2:51 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1")))) "holds" (Bool (Set (Var "p1")) "," (Set (Var "q")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))))) ; theorem :: SPPOL_2:52 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool (Set (Var "q")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))))) ; theorem :: SPPOL_2:53 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 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 (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))) & (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2")))) "holds" (Bool (Set (Var "q1")) "," (Set (Var "q2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))))) ; notationlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); synonym :::"special_polygonal"::: "P" for :::"being_special_polygon"::: ; end; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); redefine attr "P" is :::"being_special_polygon"::: means :: SPPOL_2:def 2 (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) "P")); end; :: deftheorem defines :::"special_polygonal"::: SPPOL_2:def 2 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_topreal4 :::"special_polygonal"::: ) ) "iff" (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P")))) ")" )); definitionlet "r1", "r2", "r19", "r29" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"[.":::"r1" "," "r2" "," "r19" "," "r29":::".]"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: SPPOL_2:def 3 (Set (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "r1" "," "r19" ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) "r1" "," "r29" ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "r1" "," "r29" ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) "r2" "," "r29" ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "r2" "," "r29" ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) "r2" "," "r19" ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "r2" "," "r19" ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) "r1" "," "r19" ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ")" )); end; :: deftheorem defines :::"[."::: SPPOL_2:def 3 : (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r19")) "," (Set (Var "r29")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_sppol_2 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r19")) "," (Set (Var "r29")) ($#k1_sppol_2 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r1")) "," (Set (Var "r19")) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Set (Var "r1")) "," (Set (Var "r29")) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r1")) "," (Set (Var "r29")) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "r29")) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "r29")) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "r19")) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "r19")) ($#k19_euclid :::"]|"::: ) ) "," (Set ($#k19_euclid :::"|["::: ) (Set (Var "r1")) "," (Set (Var "r19")) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ")" )))); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p1" "," "p2" ")" ) -> ($#v2_compts_1 :::"compact"::: ) ; end; registrationlet "r1", "r2", "r19", "r29" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_sppol_2 :::"[."::: ) "r1" "," "r2" "," "r19" "," "r29" ($#k1_sppol_2 :::".]"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ; end; theorem :: SPPOL_2:54 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r19")) "," (Set (Var "r29")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Var "r19")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r29")))) "holds" (Bool (Set ($#k1_sppol_2 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r19")) "," (Set (Var "r29")) ($#k1_sppol_2 :::".]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r29"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r19"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r29"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r1"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r19"))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r2"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r29"))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r19"))) ")" ) ")" ) "}" )) ; theorem :: SPPOL_2:55 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r19")) "," (Set (Var "r29")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r1")) ($#r1_hidden :::"<>"::: ) (Set (Var "r2"))) & (Bool (Set (Var "r19")) ($#r1_hidden :::"<>"::: ) (Set (Var "r29")))) "holds" (Bool (Set ($#k1_sppol_2 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r19")) "," (Set (Var "r29")) ($#k1_sppol_2 :::".]"::: ) ) "is" ($#v1_topreal4 :::"special_polygonal"::: ) )) ; theorem :: SPPOL_2:56 (Bool (Set ($#k1_topreal1 :::"R^2-unit_square"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_sppol_2 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_sppol_2 :::".]"::: ) )) ; registration cluster ($#v1_topreal4 :::"special_polygonal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); end; registration cluster (Set ($#k1_topreal1 :::"R^2-unit_square"::: ) ) -> ($#v1_topreal4 :::"special_polygonal"::: ) ; end; registration cluster ($#v1_topreal4 :::"special_polygonal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); cluster ($#v1_topreal4 :::"special_polygonal"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); cluster ($#v1_topreal4 :::"special_polygonal"::: ) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); end; definitionmode Special_polygon_in_R2 is ($#v1_topreal4 :::"special_polygonal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; theorem :: SPPOL_2:57 (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" ($#v5_topreal1 :::"being_S-P_arc"::: ) )) "holds" (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) ; registration cluster ($#v1_topreal4 :::"special_polygonal"::: ) -> ($#v2_compts_1 :::"compact"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); end; theorem :: SPPOL_2:58 (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" ($#v1_topreal4 :::"special_polygonal"::: ) )) "holds" (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 "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_sppol_2 :::"split"::: ) (Set (Var "P"))))) ; theorem :: SPPOL_2:59 (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" ($#v1_topreal4 :::"special_polygonal"::: ) )) "holds" (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 "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P2")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "P1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2")))) ")" )))) ;