:: JORDAN13  semantic presentation begin  











definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#~v1_sppol_1  "non"   ($#v1_sppol_1 :::"horizontal"::: )   )   ($#~v2_sppol_1  "non"   ($#v2_sppol_1 :::"vertical"::: )   )    ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); assume 
(Bool (Set (Const "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Const "C")))
 ; func  :::"Span":::  "(" "C" "," "n" ")"  ->  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )     ($#v1_sprect_2 :::"clockwise_oriented"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::) means :: JORDAN13:def 1 (Bool  "("  (Bool it  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")" )) & (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" "C" "," "n" ")"  ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" "C" "," "n" ")"  ")" ) ")" )) & (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" "C" "," "n" ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" "C" "," "n" ")"  ")" ) ")" )) & (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 (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  it))) "holds"  (Bool  "("   "("  (Bool (Bool (Set   ($#k4_gobrd13 :::"front_right_cell"::: )   "(" it "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ) ")" )  ($#r1_xboole_0 :::"misses"::: )  "C") & (Bool (Set   ($#k5_gobrd13 :::"front_left_cell"::: )   "(" it "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ) ")" )  ($#r1_xboole_0 :::"misses"::: )  "C")) "implies" (Bool it  ($#r2_gobrd13 :::"turns_left"::: )  (Set (Var "k")) "," (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")" ))  ")"  &  "("  (Bool (Bool (Set   ($#k4_gobrd13 :::"front_right_cell"::: )   "(" it "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ) ")" )  ($#r1_xboole_0 :::"misses"::: )  "C") & (Bool (Set   ($#k5_gobrd13 :::"front_left_cell"::: )   "(" it "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ) ")" )  ($#r1_xboole_0 :::"meets"::: )  "C")) "implies" (Bool it  ($#r3_gobrd13 :::"goes_straight"::: )  (Set (Var "k")) "," (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")" ))  ")"  &  "("  (Bool (Bool (Set   ($#k4_gobrd13 :::"front_right_cell"::: )   "(" it "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")"  ")" ) ")" )  ($#r1_xboole_0 :::"meets"::: )  "C")) "implies" (Bool it  ($#r1_gobrd13 :::"turns_right"::: )  (Set (Var "k")) "," (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" "C" "," "n" ")" ))  ")"   ")" )  ")" )  ")" ); end; 







:: deftheorem    defines :::"Span"::: JORDAN13:def 1 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#~v1_sppol_1  "non"   ($#v1_sppol_1 :::"horizontal"::: )   )   ($#~v2_sppol_1  "non"   ($#v2_sppol_1 :::"vertical"::: )   )    ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_jordan1h :::"is_sufficiently_large_for"::: )  (Set (Var "C")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )     ($#v1_sprect_2 :::"clockwise_oriented"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_jordan13 :::"Span"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "b3"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )) & (Bool (Set (Set (Var "b3"))  ($#k7_partfun1 :::"/."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set  "("  ($#k3_jordan1h :::"X-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_jordan11 :::"Y-SpanStart"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )) & (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 (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set   ($#k4_gobrd13 :::"front_right_cell"::: )   "(" (Set (Var "b3")) "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "C"))) & (Bool (Set   ($#k5_gobrd13 :::"front_left_cell"::: )   "(" (Set (Var "b3")) "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "C")))) "implies" (Bool (Set (Var "b3"))  ($#r2_gobrd13 :::"turns_left"::: )  (Set (Var "k")) "," (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" ))  ")"  &  "("  (Bool (Bool (Set   ($#k4_gobrd13 :::"front_right_cell"::: )   "(" (Set (Var "b3")) "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "C"))) & (Bool (Set   ($#k5_gobrd13 :::"front_left_cell"::: )   "(" (Set (Var "b3")) "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "C")))) "implies" (Bool (Set (Var "b3"))  ($#r3_gobrd13 :::"goes_straight"::: )  (Set (Var "k")) "," (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" ))  ")"  &  "("  (Bool (Bool (Set   ($#k4_gobrd13 :::"front_right_cell"::: )   "(" (Set (Var "b3")) "," (Set (Var "k")) "," (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "C")))) "implies" (Bool (Set (Var "b3"))  ($#r1_gobrd13 :::"turns_right"::: )  (Set (Var "k")) "," (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" ))  ")"   ")" )  ")" )  ")" )  ")" ))));