:: GOBOARD5  semantic presentation begin  



















definitionlet "G" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "i" be   ($#m1_hidden :::"Nat":::); func  :::"v_strip":::  "(" "G" "," "i" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) equals :: GOBOARD5:def 1  "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" "i" "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" "i"  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  ")" )  "}"   if (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i") & (Bool "i"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "G"))  ")" )  "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" "i" "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  "}"   if (Bool "i"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "G"))  otherwise  "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" "i"  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  "}"  ; func  :::"h_strip":::  "(" "G" "," "i" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) equals :: GOBOARD5:def 2  "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," "i" ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" "i"  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"   if (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  "i") & (Bool "i"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  "G"))  ")" )  "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," "i" ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  "}"   if (Bool "i"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  "G"))  otherwise  "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" "G"  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" "i"  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  "}"  ; end; 












:: deftheorem    defines :::"v_strip"::: GOBOARD5:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("   "("  (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"))))) "implies" (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  ")" )  "}"  )  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "implies" (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  "}"  )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) "or"  "not" (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))  ")" ) & (Bool (Bool  "not" (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))))) "implies" (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  "}"  )  ")"   ")" ))); 
 
:: deftheorem    defines :::"h_strip"::: GOBOARD5:def 2 :  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("   "("  (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "implies" (Bool (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "i")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  )  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "implies" (Bool (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "i")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  "}"  )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) "or"  "not" (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))  ")" ) & (Bool (Bool  "not" (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))))) "implies" (Bool (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  "}"  )  ")"   ")" ))); 
 
theorem :: GOBOARD5:1 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (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  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )))) ; 
 
theorem :: GOBOARD5:2 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (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  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )))) ; 
 
theorem :: GOBOARD5:3 (Bool  "for" (Set (Var "j")) "," (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v5_goboard1 :::"X_increasing-in-column"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (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 "G"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )))) ; 
 
theorem :: GOBOARD5:4 (Bool  "for" (Set (Var "j1")) "," (Set (Var "j2")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v4_goboard1 :::"Y_increasing-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j1"))) & (Bool (Set (Var "j1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j2"))) & (Bool (Set (Var "j2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (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  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j1")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j2")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )))) ; 
 
theorem :: GOBOARD5:5 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (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   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  ))) ; 
 
theorem :: GOBOARD5:6 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (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   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  "}"  ))) ; 
 
theorem :: GOBOARD5:7 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (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   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  "}"  ))) ; 
 
theorem :: GOBOARD5:8 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  ")" )  "}"  ))) ; 
 
theorem :: GOBOARD5:9 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Set (Var "j")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  "}"  ))) ; 
 
theorem :: GOBOARD5:10 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  "}"  ))) ; 
 definitionlet "G" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "i", "j" be   ($#m1_hidden :::"Nat":::); func  :::"cell":::  "(" "G" "," "i" "," "j" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) equals :: GOBOARD5:def 3 (Set (Set  "("  ($#k1_goboard5 :::"v_strip"::: )   "(" "G" "," "i" ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_goboard5 :::"h_strip"::: )   "(" "G" "," "j" ")"  ")" )); end; 







:: deftheorem    defines :::"cell"::: GOBOARD5:def 3 :  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")"  ")" ))))); 
 definitionlet "IT" be   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); attr "IT" is  :::"s.c.c.":::  means :: GOBOARD5:def 4 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool  "("  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "IT"))  ")" ) "or" (Bool (Set (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "IT"))  ")" )) "holds"  (Bool (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" "IT" "," (Set (Var "i")) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" "IT" "," (Set (Var "j")) ")" ))); end; 




:: deftheorem    defines :::"s.c.c."::: GOBOARD5:def 4 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_goboard5 :::"s.c.c."::: )  ) "iff" (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool  "("  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "IT"))))  ")" ) "or" (Bool (Set (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "IT"))))  ")" )) "holds"  (Bool (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "IT")) "," (Set (Var "i")) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "IT")) "," (Set (Var "j")) ")" )))  ")" )); 
 definitionlet "IT" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); attr "IT" is  :::"standard":::  means :: GOBOARD5:def 5 (Bool "IT"  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k2_goboard2 :::"GoB"::: )  "IT")); end; 




:: deftheorem    defines :::"standard"::: GOBOARD5:def 5 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_goboard5 :::"standard"::: )  ) "iff" (Bool (Set (Var "IT"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k2_goboard2 :::"GoB"::: )  (Set (Var "IT"))))  ")" )); 
 registration
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k5_numbers :::"NAT"::: )  )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))   ($#v1_funct_1 :::"Function-like"::: )    ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )   ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v1_finseq_6 :::"circular"::: )     ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v1_goboard5 :::"s.c.c."::: )     ($#v2_goboard5 :::"standard"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )); 
end; 
theorem :: GOBOARD5:11 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m2_finseq_1 :::"FinSequence":::) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" )))) ; 
 
theorem :: GOBOARD5:12 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "m")) "," (Set (Var "k")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds"  (Bool (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "m"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))))) ; 
 definitionmode special_circular_sequence is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finseq_6 :::"circular"::: )     ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v1_goboard5 :::"s.c.c."::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); end; 


definitionlet "f" be   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); let "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); assume that  
(Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "k")))
 and  
(Bool (Set (Set (Const "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Const "f"))))
 ; func  :::"right_cell":::  "(" "f" "," "k" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: GOBOARD5:def 6 (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  ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ))) & (Bool (Set "f"  ($#k7_partfun1 :::"/."::: )  "k")  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "k"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "j1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set (Var "i1")) "," (Set  "(" (Set (Var "j1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set (Var "i2")) "," (Set (Var "j2")) ")" ))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "j2")) ")" ))  ")" )); func  :::"left_cell":::  "(" "f" "," "k" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: GOBOARD5:def 7 (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  ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ))) & (Bool (Set "f"  ($#k7_partfun1 :::"/."::: )  "k")  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" "k"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "j1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "j1")) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set (Var "i2")) "," (Set  "(" (Set (Var "j2"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  "f" ")" ) "," (Set (Var "i1")) "," (Set (Var "j2")) ")" ))  ")" )); end; 














:: deftheorem    defines :::"right_cell"::: GOBOARD5:def 6 :  (Bool  "for" (Set (Var "f")) "being"   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (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 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )) "iff" (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  ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "j1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i1")) "," (Set  "(" (Set (Var "j1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i2")) "," (Set (Var "j2")) ")" ))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "j2")) ")" ))  ")" ))  ")" )))); 
 
:: deftheorem    defines :::"left_cell"::: GOBOARD5:def 7 :  (Bool  "for" (Set (Var "f")) "being"   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  (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 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )) "iff" (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  ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Set (Var "j1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "i1"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "j1")) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i2")) "," (Set  "(" (Set (Var "j2"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j2"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i1")) "," (Set (Var "j2")) ")" ))  ")" ))  ")" )))); 
 
theorem :: GOBOARD5:13 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v5_goboard1 :::"X_increasing-in-column"::: )  ) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )))) ; 
 
theorem :: GOBOARD5:14 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v5_goboard1 :::"X_increasing-in-column"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )))) ; 
 
theorem :: GOBOARD5:15 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v4_goboard1 :::"Y_increasing-in-line"::: )  ) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (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   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD5:16 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v4_goboard1 :::"Y_increasing-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (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   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD5:17 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v4_goboard1 :::"Y_increasing-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD5:18 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_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 (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD5:19 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "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")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD5:20 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v5_goboard1 :::"X_increasing-in-column"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )))) ; 
 
theorem :: GOBOARD5:21 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_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")))) & (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   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD5:22 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "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")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )))) ; 
 
theorem :: GOBOARD5:23 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v5_goboard1 :::"X_increasing-in-column"::: )  ) & (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  "("  ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  "}"  ))) ; 
 
theorem :: GOBOARD5:24 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is" bbbadV3_RELAT_1()) & (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v4_goboard1 :::"Y_increasing-in-line"::: )  ) & (Bool (Set (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set  "("  ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "q")) where q "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  "}"  ))) ; 
 
theorem :: GOBOARD5:25 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_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 (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )))) ; 
 
theorem :: GOBOARD5:26 (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m1_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")))) & (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  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) "," (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" )))) ; 
 
theorem :: GOBOARD5:27 (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  "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")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set   ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" ))  ")" ))) ; 
 
theorem :: GOBOARD5:28 (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  "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")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set   ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))) ; 
 
theorem :: GOBOARD5:29 (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  "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")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set   ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ")" ))) ; 
 
theorem :: GOBOARD5:30 (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  "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")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")" )) & (Bool (Set   ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))) ; 
 
theorem :: GOBOARD5:31 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  "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 (Set  "("  ($#k5_goboard5 :::"left_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_goboard5 :::"right_cell"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")" )))) ;