:: GOBRD12  semantic presentation begin  





















theorem :: GOBRD12: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 "i")) "," (Set (Var "j")) "being"    ($#m1_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")) ")" )))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  )))) ; 
 
theorem :: GOBRD12: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 "i")) "," (Set (Var "j")) "being"    ($#m1_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")) ")" )))) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ))))) ; 
 
theorem :: GOBRD12: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 "i")) "," (Set (Var "j")) "being"    ($#m1_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")) ")" )))) "holds"  (Bool  "("  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")"  ")" )) "is"   ($#v2_connsp_1 :::"connected"::: )  ) & (Bool (Set   ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )))  ")" ))) ; 
 
theorem :: GOBRD12:4 (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  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")"  ")" ) ")" ) where i, j "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (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")) ")" )))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD12:5 (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  "("  (Bool (Set (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")"  ")" )) "is"    ($#m1_connsp_3 :::"a_union_of_components"::: )   "of" (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ))) & (Bool (Set   ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")))) & (Bool (Set   ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f"))))  ")" )) ; 
 
theorem :: GOBRD12: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 "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "j1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "j2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2"))  ($#r2_gobrd10 :::"are_adjacent2"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i1")) "," (Set (Var "j1")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" ))) "iff" (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i2")) "," (Set (Var "j2")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" )))  ")" ))) ; 
 
theorem :: GOBRD12:7 (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 "F1")) "," (Set (Var "F2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F2")))) & (Bool  "ex" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F1")))) & (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "F1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "F2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" )))  ")" )) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F1")))) & (Bool (Set (Var "k1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "k2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))) "holds"  (Bool  "("  (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "k2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F1"))))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "F1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "F2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: GOBRD12:8 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::) (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_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   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" )))  ")" ))) ; 
 
theorem :: GOBRD12: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"    ($#m1_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")) ")" )))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: GOBRD12:10 (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  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f")) ")" )))) ;