:: GOBOARD1  semantic presentation begin  



























definitionlet "f" be   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"X_axis"::: "f" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) means :: GOBOARD1:def 1 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k17_euclid :::"`1"::: )  ))  ")" )  ")" ); func  :::"Y_axis"::: "f" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) means :: GOBOARD1:def 2 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  ")" ); end; 










:: deftheorem    defines :::"X_axis"::: GOBOARD1:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k17_euclid :::"`1"::: )  ))  ")" )  ")" )  ")" ))); 
 
:: deftheorem    defines :::"Y_axis"::: GOBOARD1:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  ")" )  ")" ))); 
 
theorem :: GOBOARD1:1 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))))) ; 
 begin  
theorem :: GOBOARD1:2 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "M")))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "j")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))))) ; 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "M" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); :: original: :::"empty-yielding"::: redefine attr "M" is  :::"empty-yielding":::  means :: GOBOARD1:def 3 (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "M")) "or" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  "M"))  ")" ); end; 





:: deftheorem    defines :::"empty-yielding"::: GOBOARD1:def 3 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v3_relat_1 :::"empty-yielding"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")))) "or" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "M"))))  ")" )  ")" ))); 
 definitionlet "M" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); attr "M" is  :::"X_equal-in-line":::  means :: GOBOARD1:def 4 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "M"))) "holds"  (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" "M" "," (Set (Var "n")) ")"  ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  )); attr "M" is  :::"Y_equal-in-column":::  means :: GOBOARD1:def 5 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  "M" ")" )))) "holds"  (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" "M" "," (Set (Var "n")) ")"  ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  )); attr "M" is  :::"Y_increasing-in-line":::  means :: GOBOARD1:def 6 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "M"))) "holds"  (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" "M" "," (Set (Var "n")) ")"  ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  )); attr "M" is  :::"X_increasing-in-column":::  means :: GOBOARD1:def 7 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  "M" ")" )))) "holds"  (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" "M" "," (Set (Var "n")) ")"  ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  )); end; 
















:: deftheorem    defines :::"X_equal-in-line"::: GOBOARD1:def 4 :  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "M"))))) "holds"  (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "n")) ")"  ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"Y_equal-in-column"::: GOBOARD1:def 5 :  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M")) ")" )))) "holds"  (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "n")) ")"  ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"Y_increasing-in-line"::: GOBOARD1:def 6 :  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v4_goboard1 :::"Y_increasing-in-line"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "M"))))) "holds"  (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "n")) ")"  ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"X_increasing-in-column"::: GOBOARD1:def 7 :  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v5_goboard1 :::"X_increasing-in-column"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M")) ")" )))) "holds"  (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "n")) ")"  ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   bbbadV3_RELAT_1() (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set bbbadK3_FINSEQ_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v1_matrix_1 :::"tabular"::: )     ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )     ($#v4_goboard1 :::"Y_increasing-in-line"::: )     ($#v5_goboard1 :::"X_increasing-in-column"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set bbbadK3_FINSEQ_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))); 
end; 
theorem :: GOBOARD1:3 (Bool  "for" (Set (Var "M")) "being"   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v5_goboard1 :::"X_increasing-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "m")) ")"  ")" ))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "M")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "M"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))))) ; 
 
theorem :: GOBOARD1:4 (Bool  "for" (Set (Var "M")) "being"   ($#v3_goboard1 :::"Y_equal-in-column"::: )     ($#v4_goboard1 :::"Y_increasing-in-line"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "m")) ")"  ")" ))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M")) ")" ))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M")) ")" )))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))))) ; 
 begin  definitionmode Go-board is bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )     ($#v4_goboard1 :::"Y_increasing-in-line"::: )     ($#v5_goboard1 :::"X_increasing-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); end; 



theorem :: GOBOARD1:5 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "m")) "," (Set (Var "k")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G"))))) "holds"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "j")))  ")" )))) ; 
 
theorem :: GOBOARD1:6 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "m")) "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 "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "m")) ")" )  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" )))))) ; 
 
theorem :: GOBOARD1:7 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "m")) "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 "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "m")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "m")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )))))) ; 
 
theorem :: GOBOARD1:8 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "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   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "k")))))) ; 
 definitionlet "G" be   ($#m2_finseq_1 :::"Go-board":::); let "i" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); assume 
(Bool  "("  (Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Const "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Const "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))  ")" )
 ; func  :::"DelCol":::  "(" "G" "," "i" ")"  ->   ($#m2_finseq_1 :::"Go-board":::) means :: GOBOARD1:def 8 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "G")) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "G"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" "G" "," (Set (Var "k")) ")"  ")" ) "," "i" ")" ))  ")" )  ")" ); end; 







:: deftheorem    defines :::"DelCol"::: GOBOARD1:def 8 :  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"Go-board":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "i")) ")" ))  ")" )  ")" )  ")" )))); 
 
theorem :: GOBOARD1:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")"  ")" ) "," (Set (Var "i")) ")" )))) ; 
 
theorem :: GOBOARD1:10 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "m"))))) ; 
 
theorem :: GOBOARD1:11 (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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))) ; 
 
theorem :: GOBOARD1:12 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "m")) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_finseq_3 :::"Del"::: )   "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))))) ; 
 
theorem :: GOBOARD1:13 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "k")) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) ")" ))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:14 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "k")) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) ")" ))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:15 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:16 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:17 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "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   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m"))))) "holds"  (Bool  "("  (Bool (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ) ")" ))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:18 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "n")) "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   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )) & (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:19 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "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   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m"))))) "holds"  (Bool  "("  (Bool (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:20 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "n")) "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   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool  "("  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "k")) ")" )) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 
theorem :: GOBOARD1:21 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "m")) "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   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "m")) ")"  ")" ))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ) "," (Set (Var "m")) ")"  ")" )))))) ; 
 








definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "D")); let "M" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); pred "f" :::"is_sequence_on"::: "M" means :: GOBOARD1:def 9 (Bool  "("  (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "f"))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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"::: )  "M")) & (Bool (Set "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set "M"  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "f")) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "f"))) "holds"  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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"::: )  "M")) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  "M")) & (Bool (Set "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set "M"  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set "f"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set "M"  ($#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")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_sequence_on"::: GOBOARD1:def 9 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "M"))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_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"    ($#m2_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 (Var "M")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_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"    ($#m2_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 (Var "M")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "M")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#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 (Var "M"))  ($#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")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))  ")" )  ")" )  ")" )))); 
 
theorem :: GOBOARD1:22 (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "implies" (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "m")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "M")))) "implies" (Bool (Set (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "m")))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "M")))  ")"   ")" ))))) ; 
 
theorem :: GOBOARD1:23 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1"))))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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 (Var "M")))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f2"))))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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 (Var "M")))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" )))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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 (Var "M")))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" )))))) ; 
 
theorem :: GOBOARD1:24 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1"))))) "holds"  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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 (Var "M")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "M")))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#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")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f2"))))) "holds"  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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 (Var "M")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "M")))) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#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")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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 (Var "M")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "M")))) & (Bool (Set (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f2"))))) "holds"  (Bool (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "m"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" )))) "holds"  (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_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 (Var "M")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "M")))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#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")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))))))) ; 
 



theorem :: GOBOARD1:25 (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":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" ))))) ; 
 
theorem :: GOBOARD1:26 (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":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "n")) ")"  ")" )))  ")" ))))) ; 
 
theorem :: GOBOARD1:27 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Bool  "not" (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "n")) ")"  ")" ))))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")"  ")" ))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))))) ; 
 
theorem :: GOBOARD1:28 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )))  ")" )))) ; 
 
theorem :: GOBOARD1:29 (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G")))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_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 "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" ) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")"  ")" )))) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j")))  ")" )  ")" ))) ; 
 
theorem :: GOBOARD1:30 (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":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "n")) ")"  ")" )))  ")" ))))) ; 
 
theorem :: GOBOARD1:31 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Bool  "not" (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "n")) ")"  ")" ))))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")"  ")" ))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" )))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))))) ; 
 
theorem :: GOBOARD1:32 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )))  ")" )))) ; 
 
theorem :: GOBOARD1:33 (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G")))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (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")))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_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 "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" ) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")"  ")" )))) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j")))  ")" )  ")" ))) ; 
 
theorem :: GOBOARD1:34 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")"  ")" )))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))  ")" )) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set (Var "m")) ")"  ")" )))) "holds"  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))))))) ; 
 
theorem :: GOBOARD1:35 (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ) ")" ) ")"  ")" ))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool (Set (Var "g"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k3_goboard1 :::"DelCol"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")" )) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))))  ")" )))) ; 
 
theorem :: GOBOARD1:36 (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Num 1) ")"  ")" ))) & (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool (Set (Var "g"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G")))  ")" )))) ; 
 
theorem :: GOBOARD1:37 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")"  ")" ))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "k")) ")"  ")" )))) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")"  ")" )))  ")" ))  ")" )  ")" )))) ;