:: JORDAN4  semantic presentation begin  











theorem :: JORDAN4:1 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "j"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j"))))) "holds"  (Bool (Set (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: JORDAN4:2 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "j"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")))) & (Bool (Set (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j"))))  ")" )) ; 
 
theorem :: JORDAN4:3 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "j"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: JORDAN4:4 (Bool  "for" (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Set (Var "k"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "j")))) ; 
 begin  






theorem :: JORDAN4:5 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v1_finseq_6 :::"circular"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))))) ; 
 
theorem :: JORDAN4:6 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "k")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "f1"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "k")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "f1"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" )))  ")" )))) ; 
 
theorem :: JORDAN4:7 (Bool  "for" (Set (Var "g")) "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 (Set (Var "g")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "i"))) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ))) ; 
 
theorem :: JORDAN4:8 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i2")) "," (Set (Var "i1")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))))) ; 
 
theorem :: JORDAN4:9 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))))) ; 
 
theorem :: JORDAN4:10 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:11 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:12 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 
theorem :: JORDAN4:13 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i2")) "," (Set (Var "i1")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i2")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "j")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i2")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "j")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" ))))) ; 
 
theorem :: JORDAN4:14 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i2")) "," (Set (Var "i1")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "i2"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i1")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "j")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "i2"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i1")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "j")) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" ))))) ; 
 
theorem :: JORDAN4:15 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1"))))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "k")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "k")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )))) ; 
 
theorem :: JORDAN4:16 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k17_finseq_1 :::"|"::: )  (Num 1))))) ; 
 
theorem :: JORDAN4:17 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "k")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set (Var "D"))))))) ; 
 
theorem :: JORDAN4:18 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f1")) "," (Set (Var "i2")) "," (Set (Var "i1")) ")"  ")" )))))) ; 
 
theorem :: JORDAN4:19 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "i1")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )))) ; 
 
theorem :: JORDAN4:20 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i2")) "," (Set (Var "i1")) ")"  ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" ) ")" )))) ; 
 begin  definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_hidden :::"FinSequence":::); func  :::"S_Drop":::  "(" "n" "," "f" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: JORDAN4:def 1 (Set "n"  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  "f" ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )) if (Bool (Set "n"  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  "f" ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  "f" ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1)); end; 






:: deftheorem    defines :::"S_Drop"::: JORDAN4:def 1 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1)))  ")"   ")" ))); 
 
theorem :: JORDAN4:21 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1)))) ; 
 
theorem :: JORDAN4:22 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "n"))))) ; 
 
theorem :: JORDAN4:23 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) "," (Set (Var "f")) ")" )) & (Bool (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")) ")" ) "," (Set (Var "f")) ")" ))  ")" ))) ; 
 definitionlet "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); let "g" be   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "i1", "i2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); pred "g" :::"is_a_part>_of"::: "f" "," "i1" "," "i2" means :: JORDAN4:def 2 (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i1") & (Bool (Set "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i2") & (Bool (Set "i2"  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool (Set "g"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  "g" ")" ))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  "i2")) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "g")) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "g")  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "g"))) "holds"  (Bool (Set "g"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Set (Var "i")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," "f" ")"  ")" )))  ")" )  ")" ); end; 







:: deftheorem    defines :::"is_a_part>_of"::: JORDAN4:def 2 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "g"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) "iff" (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "i")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "f")) ")"  ")" )))  ")" )  ")" )  ")" )))); 
 definitionlet "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); let "g" be   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "i1", "i2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); pred "g" :::"is_a_part<_of"::: "f" "," "i1" "," "i2" means :: JORDAN4:def 3 (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i1") & (Bool (Set "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i2") & (Bool (Set "i2"  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool (Set "g"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  "g" ")" ))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  "i2")) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "g")) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "g")  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "g"))) "holds"  (Bool (Set "g"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  "f" ")" )  ($#k2_nat_1 :::"+"::: )  "i1" ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" ) "," "f" ")"  ")" )))  ")" )  ")" ); end; 







:: deftheorem    defines :::"is_a_part<_of"::: JORDAN4:def 3 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "g"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) "iff" (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "i1")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" ) "," (Set (Var "f")) ")"  ")" )))  ")" )  ")" )  ")" )))); 
 definitionlet "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); let "g" be   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "i1", "i2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); pred "g" :::"is_a_part_of"::: "f" "," "i1" "," "i2" means :: JORDAN4:def 4 (Bool  "("  (Bool "g"  ($#r1_jordan4 :::"is_a_part>_of"::: )  "f" "," "i1" "," "i2") "or" (Bool "g"  ($#r2_jordan4 :::"is_a_part<_of"::: )  "f" "," "i1" "," "i2")  ")" ); end; 







:: deftheorem    defines :::"is_a_part_of"::: JORDAN4:def 4 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "g"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) "iff" (Bool  "("  (Bool (Set (Var "g"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) "or" (Bool (Set (Var "g"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")))  ")" )  ")" )))); 
 
theorem :: JORDAN4:24 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")))) "holds"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("  (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 (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "i")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "f")) ")"  ")" )))) "or" (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 (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "i1")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" ) "," (Set (Var "f")) ")"  ")" ))))  ")" )  ")" )))) ; 
 
theorem :: JORDAN4:25 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2")))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i2"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" ))  ")" )))) ; 
 
theorem :: JORDAN4:26 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "i2")))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "i2")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "i1")))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "i2")) ")" ))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Num 1) "," (Set (Var "i2")) ")"  ")" )))  ")" )))) ; 
 
theorem :: JORDAN4:27 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "i2")))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" ))  ")" )))) ; 
 
theorem :: JORDAN4:28 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2")))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "i1")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "i2")))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Num 1) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "i2")) ")"  ")" )))  ")" )))) ; 
 
theorem :: JORDAN4:29 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")))) "holds"  (Bool (Set   ($#k4_finseq_5 :::"Rev"::: )  (Set (Var "g")))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i2")) "," (Set (Var "i1")))))) ; 
 
theorem :: JORDAN4:30 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")))) "holds"  (Bool (Set   ($#k4_finseq_5 :::"Rev"::: )  (Set (Var "g")))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i2")) "," (Set (Var "i1")))))) ; 
 
theorem :: JORDAN4:31 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" )  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))))) ; 
 
theorem :: JORDAN4:32 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i2")) "," (Set (Var "i1")) ")" )  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i2")) "," (Set (Var "i1"))))) ; 
 
theorem :: JORDAN4:33 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Num 1) "," (Set (Var "i2")) ")"  ")" ))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))))) ; 
 
theorem :: JORDAN4:34 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Num 1) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "i2")) ")"  ")" ))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))))) ; 
 
theorem :: JORDAN4:35 (Bool  "for" (Set (Var "h")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "h")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "h"))))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "h")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "h")))))) ; 
 
theorem :: JORDAN4:36 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) "iff" (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool  "("  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")))) "or" (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2"))))  ")" )) "holds"  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))))  ")" ))) ; 
 
theorem :: JORDAN4:37 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "i2"))) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ))) ; 
 
theorem :: JORDAN4:38 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "i2"))) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ))) ; 
 
theorem :: JORDAN4:39 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" ) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ))) ; 
 
theorem :: JORDAN4:40 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" ) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ))) ; 
 
theorem :: JORDAN4:41 (Bool  "for" (Set (Var "p0")) "," (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q1")) ")" )) & (Bool (Set (Var "p0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q2")) ")" )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p0"))) & (Bool (Bool  "not" (Set (Var "q1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q2")) ")" )))) "holds"  (Bool (Set (Var "q2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q1")) ")" ))) ; 
 
theorem :: JORDAN4:42 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::) "holds"  (Bool (Set (Set  "("  ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Num 1) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: JORDAN4:43 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" )) & (Bool (Set (Var "g2"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Num 1) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "i2")) ")"  ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g1")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g2")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i1")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g1")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f"))))  ")" )))) ; 
 
theorem :: JORDAN4:44 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2")))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:45 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "i2")))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:46 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:47 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:48 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:49 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2"))))))) ; 
 
theorem :: JORDAN4:50 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool  "ex" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "g1"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "g2"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g1")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g2")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i1")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g1")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "g2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))) & (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g1")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2")))) & (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g2")))  ($#r1_topreal4 :::"is_S-P_arc_joining"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i2")))) & (Bool  "("   "for" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "holds"  (Bool  "("   "not" (Bool (Set (Var "g"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) "or" (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "g1"))) "or" (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "g2")))  ")" )  ")" )  ")" )))) ; 
 





theorem :: JORDAN4:51 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "P")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  ))) ; 
 
theorem :: JORDAN4:52 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "g1"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "g2"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")))) "holds"  (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set (Var "g2")))))) ; 
 
theorem :: JORDAN4:53 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "g1"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "g2"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")))) "holds"  (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set (Var "g2")))))) ; 
 
theorem :: JORDAN4:54 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2"))) & (Bool (Set (Var "g1"))  ($#r1_jordan4 :::"is_a_part>_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "g2"))  ($#r2_jordan4 :::"is_a_part<_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")))) "holds"  (Bool (Set (Set (Var "g1"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "g2"))  ($#k1_funct_1 :::"."::: )  (Num 2)))))) ; 
 
theorem :: JORDAN4:55 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2"))) & (Bool (Set (Var "g1"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "g2"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Set (Var "g1"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g2"))  ($#k1_funct_1 :::"."::: )  (Num 2)))) "holds"  (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set (Var "g2")))))) ; 
 definitionlet "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); let "i1", "i2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); assume that  
(Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "i1")))
 and  
(Bool (Set (Set (Const "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Const "f"))))
 and  
(Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "i2")))
 and  
(Bool (Set (Set (Const "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Const "f"))))
 and  
(Bool (Set (Const "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Const "i2")))
 ; func  :::"Lower":::  "(" "f" "," "i1" "," "i2" ")"  ->   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: JORDAN4:def 5 (Bool  "("  (Bool it  ($#r3_jordan4 :::"is_a_part_of"::: )  "f" "," "i1" "," "i2") &  "("  (Bool (Bool  "("  (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"  &  "("  (Bool (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k18_euclid :::"`2"::: )  ))) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" "i1"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," "f" ")"  ")" )))  ")"   ")" ); func  :::"Upper":::  "(" "f" "," "i1" "," "i2" ")"  ->   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: JORDAN4:def 6 (Bool  "("  (Bool it  ($#r3_jordan4 :::"is_a_part_of"::: )  "f" "," "i1" "," "i2") &  "("  (Bool (Bool  "("  (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"  &  "("  (Bool (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "i1"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "i1" ")" )  ($#k18_euclid :::"`2"::: )  ))) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" "i1"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," "f" ")"  ")" )))  ")"   ")" ); end; 
















:: deftheorem    defines :::"Lower"::: JORDAN4:def 5 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_jordan4 :::"Lower"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b4"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) &  "("  (Bool (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )) "implies" (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"  &  "("  (Bool (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k18_euclid :::"`2"::: )  ))) "implies" (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "f")) ")"  ")" )))  ")"   ")" )  ")" )))); 
 
:: deftheorem    defines :::"Upper"::: JORDAN4:def 6 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_jordan4 :::"Upper"::: )   "(" (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b4"))  ($#r3_jordan4 :::"is_a_part_of"::: )  (Set (Var "f")) "," (Set (Var "i1")) "," (Set (Var "i2"))) &  "("  (Bool (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )) "implies" (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"  &  "("  (Bool (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i1")) ")" )  ($#k18_euclid :::"`2"::: )  ))) "implies" (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_jordan4 :::"S_Drop"::: )   "(" (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "f")) ")"  ")" )))  ")"   ")" )  ")" ))));