:: GOBOARD9  semantic presentation begin  



























theorem :: GOBOARD9:1 (Bool  "for" (Set (Var "GX")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Var "B"))) & (Bool (Set (Var "A2"))  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Var "B"))) & (Bool (Bool  "not" (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "A2"))))) "holds"  (Bool (Set (Var "A1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "A2"))))) ; 
 
theorem :: GOBOARD9:2 (Bool  "for" (Set (Var "GX")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX"))  (Bool  "for" (Set (Var "AA")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "GX"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "AA")))) "holds"  (Bool (Set (Set (Var "GX"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "GX"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "AA"))))))) ; 
 
theorem :: GOBOARD9:3 (Bool  "for" (Set (Var "GX")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "A")) "is"   ($#v2_connsp_1 :::"connected"::: )  )) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "C")))  ")" )))) ; 
 
theorem :: GOBOARD9:4 (Bool  "for" (Set (Var "GX")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX"))  "st" (Bool (Bool (Set (Var "B")) "is"   ($#v2_connsp_1 :::"connected"::: )  ) & (Bool (Set (Var "C"))  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Var "D"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "D")))) "holds"  (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))))) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_convex1 :::"convex"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))); 
end; 
theorem :: GOBOARD9:5 canceled; 
 
theorem :: GOBOARD9:6 (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#v1_convex1 :::"convex"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "P"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q"))) "is"   ($#v1_convex1 :::"convex"::: )  )) ; 
 
theorem :: GOBOARD9:7 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set  "("  ($#k4_finseq_5 :::"Rev"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: GOBOARD9:8 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set  "("  ($#k4_finseq_5 :::"Rev"::: )  (Set (Var "f")) ")" )))) ; 
 registration
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k5_numbers :::"NAT"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )    ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  bbbadV1_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )   ($#m1_hidden :::"FinSequence":::); 
cluster (Set   ($#k3_finseq_5 :::"Rev"::: )  "f") ->  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  ; 
end; definitionlet "f" be   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); :: original: :::"Rev"::: redefine func  :::"Rev"::: "f" ->   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); end; 
theorem :: GOBOARD9:9 (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 "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_goboard5 :::"right_cell"::: )   "(" (Set  "("  ($#k1_goboard9 :::"Rev"::: )  (Set (Var "f")) ")" ) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD9:10 (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 "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set  "("  ($#k1_goboard9 :::"Rev"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD9:11 (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" ))  ")" )))) ; 
 
theorem :: GOBOARD9:12 (Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")"  ")" )) "is"   ($#v1_convex1 :::"convex"::: )  ))) ; 
 
theorem :: GOBOARD9:13 (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )) "is"   ($#v1_convex1 :::"convex"::: )  ))) ; 
 
theorem :: GOBOARD9:14 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: GOBOARD9:15 (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: GOBOARD9:16 (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: GOBOARD9:17 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )) "is"   ($#v1_convex1 :::"convex"::: )  ))) ; 
 
theorem :: GOBOARD9:18 canceled; 
 
theorem :: GOBOARD9:19 (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" )) "is"   ($#v1_convex1 :::"convex"::: )  ))) ; 
 
theorem :: GOBOARD9:20 (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" )) "is"   ($#v1_convex1 :::"convex"::: )  ))) ; 
 definitionlet "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); func  :::"LeftComp"::: "f" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: GOBOARD9:def 1 (Bool  "("  (Bool it  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  "f" ")" )  ($#k3_subset_1 :::"`"::: )  )) & (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k5_goboard5 :::"left_cell"::: )   "(" "f" "," (Num 1) ")"  ")" ))  ($#r1_tarski :::"c="::: )  it)  ")" ); func  :::"RightComp"::: "f" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: GOBOARD9:def 2 (Bool  "("  (Bool it  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  "f" ")" )  ($#k3_subset_1 :::"`"::: )  )) & (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k4_goboard5 :::"right_cell"::: )   "(" "f" "," (Num 1) ")"  ")" ))  ($#r1_tarski :::"c="::: )  it)  ")" ); end; 










:: deftheorem    defines :::"LeftComp"::: GOBOARD9:def 1 :  (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 "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set (Var "b2"))  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  )) & (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Num 1) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "b2")))  ")" )  ")" ))); 
 
:: deftheorem    defines :::"RightComp"::: GOBOARD9: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 "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set (Var "b2"))  ($#r3_connsp_1 :::"is_a_component_of"::: )  (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  )) & (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Num 1) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "b2")))  ")" )  ")" ))); 
 
theorem :: GOBOARD9:21 (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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")))))) ; 
 
theorem :: GOBOARD9:22 (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   ($#k2_goboard2 :::"GoB"::: )  (Set  "("  ($#k1_goboard9 :::"Rev"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f"))))) ; 
 
theorem :: GOBOARD9:23 (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   ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set  "("  ($#k1_goboard9 :::"Rev"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: GOBOARD9:24 (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   ($#k3_goboard9 :::"RightComp"::: )  (Set  "("  ($#k1_goboard9 :::"Rev"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f"))))) ; 
 
theorem :: GOBOARD9: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 "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")))))) ;