:: GOBOARD2  semantic presentation begin  































theorem :: GOBOARD2:1 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (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")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "n")) ")" )  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "m")) ")" ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_topreal1 :::"s.n.c."::: )  )) ; 
 
theorem :: GOBOARD2:2 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_topreal1 :::"unfolded"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v3_topreal1 :::"s.n.c."::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) & (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"))))) "holds"  (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))))) ; 
 
theorem :: GOBOARD2:3 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" ))))) ; 
 
theorem :: GOBOARD2:4 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (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   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "f")) "is"   ($#v2_topreal1 :::"unfolded"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v3_topreal1 :::"s.n.c."::: )  )) "holds"  (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: GOBOARD2:5 (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 "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set  "(" (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f2")) "," (Set (Var "m")) ")" )))) ; 
 
theorem :: GOBOARD2:6 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "(" (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "g")) ")" )))) ; 
 
theorem :: GOBOARD2:7 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_topreal1 :::"s.n.c."::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "i"))) "is"   ($#v3_topreal1 :::"s.n.c."::: )  ))) ; 
 
theorem :: GOBOARD2:8 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" )  ($#k17_euclid :::"`1"::: )  )) "or" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f2"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )) "holds"  (Bool (Set (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "f2"))) "is"   ($#v1_topreal1 :::"special"::: )  )) ; 
 
theorem :: GOBOARD2:9 (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_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: GOBOARD2:10 (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_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); 
cluster (Set   ($#k1_goboard1 :::"X_axis"::: )  "f") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set   ($#k2_goboard1 :::"Y_axis"::: )  "f") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: GOBOARD2:11 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_topreal1 :::"special"::: )  )) "holds"  (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 "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "k")) "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 (Var "G")))) & (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 (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")" )) & (Bool (Bool  "not" (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "j"))))))) ; 
 
theorem :: GOBOARD2:12 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (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 (Var "G")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))  ")" ))  ")" ) & (Bool (Set (Var "f")) "is"   ($#v1_topreal1 :::"special"::: )  ) & (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 (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "g"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))) & (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "g")))) & (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))) & (Bool (Set (Set (Var "g"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g"))))  ")" )))) ; 
 definitionlet "v1", "v2" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); assume 
(Bool (Set (Const "v1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))
 ; func  :::"GoB":::  "(" "v1" "," "v2" ")"  ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: GOBOARD2:def 1 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "v1")) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "v2")) & (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "n")) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  it))) "holds"  (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" "v1"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" "v2"  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" ); end; 







:: deftheorem    defines :::"GoB"::: GOBOARD2:def 1 :  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_goboard2 :::"GoB"::: )   "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "v1")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "v2")))) & (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "n")) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set (Var "v1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "v2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" ) ($#k19_euclid :::"]|"::: ) ))  ")" )  ")" )  ")" ))); 
 registrationlet "v1", "v2" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
cluster (Set   ($#k1_goboard2 :::"GoB"::: )   "(" "v1" "," "v2" ")" ) -> bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )   ; 
end; registrationlet "v1", "v2" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_valued_0 :::"increasing"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
cluster (Set   ($#k1_goboard2 :::"GoB"::: )   "(" "v1" "," "v2" ")" ) ->   ($#v4_goboard1 :::"Y_increasing-in-line"::: )     ($#v5_goboard1 :::"X_increasing-in-column"::: )   ; 
end; definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); func  :::"GoB"::: "f" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) equals :: GOBOARD2:def 2 (Set   ($#k1_goboard2 :::"GoB"::: )   "(" (Set  "("  ($#k28_seq_4 :::"Incr"::: )  (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  "f" ")" ) ")" ) "," (Set  "("  ($#k28_seq_4 :::"Incr"::: )  (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  "f" ")" ) ")" ) ")" ); end; 





:: deftheorem    defines :::"GoB"::: GOBOARD2:def 2 :  (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) ")" ) "holds"  (Bool (Set   ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_goboard2 :::"GoB"::: )   "(" (Set  "("  ($#k28_seq_4 :::"Incr"::: )  (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set  "("  ($#k28_seq_4 :::"Incr"::: )  (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")) ")" ) ")" ) ")" ))); 
 registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); 
cluster (Set   ($#k2_goboard2 :::"GoB"::: )  "f") -> 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"::: )   ; 
end; 



theorem :: GOBOARD2:13 (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) ")" ) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")) ")" ) ")" )))  ")" )) ; 
 
theorem :: GOBOARD2:14 (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 :: GOBOARD2:15 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m"))))  ")" )) "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  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Num 1) ")"  ")" ))))) ; 
 
theorem :: GOBOARD2:16 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_goboard1 :::"X_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )) "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  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ))))) ; 
 
theorem :: GOBOARD2:17 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Num 1) ")"  ")" ))))) ; 
 
theorem :: GOBOARD2:18 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k2_goboard1 :::"Y_axis"::: )  (Set (Var "f")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) ")" ) ")"  ")" ))))) ;