:: GOBOARD6 semantic presentation begin theorem :: GOBOARD6:1 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))))) ; theorem :: GOBOARD6:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "q"))))))) ; theorem :: GOBOARD6:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: GOBOARD6:4 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "P")))) "iff" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) ")" )) ")" )))) ; theorem :: GOBOARD6:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "P")))) "iff" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) ")" )) ")" )))) ; theorem :: GOBOARD6:6 (Bool "for" (Set (Var "r1")) "," (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "r1")) "," (Set (Var "s1")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k19_euclid :::"]|"::: ) ))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k9_real_1 :::"-"::: ) (Set (Var "r2")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "s1")) ($#k9_real_1 :::"-"::: ) (Set (Var "s2")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: GOBOARD6:7 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "r2")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Var "r2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1")))) "holds" (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set (Var "r2")) ")" ) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r1")) ")" )))) ; theorem :: GOBOARD6:8 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s2")) "," (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Var "s2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s1")))) "holds" (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set (Var "s2")) ")" ) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "s1")) ")" )))) ; theorem :: GOBOARD6:9 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "r2")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Var "r2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1")))) "holds" (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "r2")) ")" ) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r1")) ")" )))) ; theorem :: GOBOARD6:10 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s2")) "," (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s2"))) & (Bool (Set (Var "s2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s1")))) "holds" (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set "(" (Set (Var "s")) ($#k9_real_1 :::"-"::: ) (Set (Var "s2")) ")" ) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "s1")) ")" )))) ; theorem :: GOBOARD6:11 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: GOBOARD6:12 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_goboard5 :::"v_strip"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) "}" )) ; theorem :: GOBOARD6:13 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_goboard5 :::"v_strip"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )) ; theorem :: GOBOARD6:14 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_goboard5 :::"v_strip"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) ")" ) "}" ))) ; theorem :: GOBOARD6:15 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_goboard5 :::"h_strip"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) "}" )) ; theorem :: GOBOARD6:16 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_goboard5 :::"h_strip"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) "}" )) ; theorem :: GOBOARD6:17 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_goboard5 :::"h_strip"::: ) "(" (Set (Var "G")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "}" ))) ; theorem :: GOBOARD6:18 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "}" )) ; theorem :: GOBOARD6:19 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) ")" ) "}" )) ; theorem :: GOBOARD6:20 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "}" ))) ; theorem :: GOBOARD6:21 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "}" )) ; theorem :: GOBOARD6:22 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) ")" ) "}" )) ; theorem :: GOBOARD6:23 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "}" ))) ; theorem :: GOBOARD6:24 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "}" ))) ; theorem :: GOBOARD6:25 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) ")" ) "}" ))) ; theorem :: GOBOARD6:26 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "}" ))) ; theorem :: GOBOARD6:27 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (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 "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_goboard5 :::"h_strip"::: ) "(" (Set (Var "G")) "," (Set (Var "j")) ")" ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k18_euclid :::"`2"::: ) ))))) ; theorem :: GOBOARD6:28 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_goboard5 :::"h_strip"::: ) "(" (Set (Var "G")) "," (Set (Var "j")) ")" ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ))))) ; theorem :: GOBOARD6:29 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_goboard5 :::"v_strip"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ))))) ; theorem :: GOBOARD6:30 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_goboard5 :::"v_strip"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k17_euclid :::"`1"::: ) ))))) ; theorem :: GOBOARD6:31 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: GOBOARD6:32 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ))))) ; theorem :: GOBOARD6:33 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ))))) ; theorem :: GOBOARD6:34 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: GOBOARD6:35 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: GOBOARD6:36 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )))) ; theorem :: GOBOARD6:37 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" )))) ; theorem :: GOBOARD6:38 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" )))) ; theorem :: GOBOARD6:39 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )))) ; theorem :: GOBOARD6:40 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:41 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:42 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:43 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:44 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:45 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:46 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:47 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:48 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:49 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:50 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:51 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:52 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:53 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:54 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:55 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:56 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:57 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:58 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:59 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:60 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:61 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:62 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:63 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:64 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:65 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:66 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (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 ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 2) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:67 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (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 ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:68 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Num 1) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:69 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:70 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:71 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:72 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:73 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: GOBOARD6:74 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:75 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 2) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:76 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:77 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:78 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:79 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:80 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:81 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: GOBOARD6:82 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) "," (Set (Var "p")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )))))) ; theorem :: GOBOARD6:83 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" )))))) ; theorem :: GOBOARD6:84 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set (Var "p")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )))))) ; theorem :: GOBOARD6:85 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) "," (Set (Var "p")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" ")" )))))) ; theorem :: GOBOARD6:86 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" ")" )))))) ; theorem :: GOBOARD6:87 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ))))) ; theorem :: GOBOARD6:88 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ))))) ; theorem :: GOBOARD6:89 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G")) ")" ) ")" ")" ))))) ; theorem :: GOBOARD6:90 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Num 1) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set ($#k19_euclid :::"|["::: ) (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ))))) ; theorem :: GOBOARD6:91 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "q"))))))) ; theorem :: GOBOARD6:92 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A")))) ")" )))) ; theorem :: GOBOARD6:93 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p9")) "," (Set (Var "r")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A")))) ")" )))))) ;