:: GOBRD13 semantic presentation begin definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "S")); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "E")); :: original: :::"."::: redefine func "F" :::"."::: "e" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); end; theorem :: GOBRD13:1 canceled; theorem :: GOBRD13:2 canceled; theorem :: GOBRD13:3 canceled; theorem :: GOBRD13:4 canceled; theorem :: GOBRD13:5 canceled; theorem :: GOBRD13:6 canceled; theorem :: GOBRD13:7 canceled; theorem :: GOBRD13:8 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G")))))) ; theorem :: GOBRD13:9 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j2"))) & (Bool (Set (Var "j2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: GOBRD13:10 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j2"))) & (Bool (Set (Var "j2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G2")) ")" ) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G1")))))) ; theorem :: GOBRD13:11 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) & (Bool (Set (Var "i2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Num 1) ")" ))) "holds" (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: GOBRD13:12 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) & (Bool (Set (Var "i2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "G2")) ")" ) ")" ))) "holds" (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G1")))))) ; theorem :: GOBRD13:13 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j1"))) & (Bool (Set (Var "j1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) & (Bool (Set (Var "i2")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j2"))) & (Bool (Set (Var "j2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" ")" ) ($#k17_euclid :::"`1"::: ) )))) ; theorem :: GOBRD13:14 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j1"))) & (Bool (Set (Var "j1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Var "i2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j2"))) & (Bool (Set (Var "j2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" ")" ) ($#k17_euclid :::"`1"::: ) )))) ; theorem :: GOBRD13:15 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j1"))) & (Bool (Set (Var "j1")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) & (Bool (Set (Var "i2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j2"))) & (Bool (Set (Var "j2")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: GOBRD13:16 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j1"))) & (Bool (Set (Var "j1")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G1")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) & (Bool (Set (Var "i2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j2"))) & (Bool (Set (Var "j2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: GOBRD13:17 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G1")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G2")) "," (Set (Var "i2")) "," (Set (Var "j2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G1")) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" )))) ; theorem :: GOBRD13:18 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G1")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G2")) "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G1")) "," (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" )))) ; theorem :: GOBRD13:19 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G1")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "G1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" ))) "holds" (Bool (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G2")) "," (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G1")) "," (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )))) ; theorem :: GOBRD13:20 (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "f")) "being" ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k16_matrix_1 :::"Values"::: ) (Set "(" ($#k2_goboard2 :::"GoB"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k16_matrix_1 :::"Values"::: ) (Set (Var "G")))))) ; definitioncanceled; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "G" be ($#m2_finseq_1 :::"Go-board":::); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); assume (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "k"))) & (Bool (Set (Set (Const "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "f")))) & (Bool (Set (Const "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Const "G"))) ")" ) ; func :::"right_cell"::: "(" "f" "," "k" "," "G" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: GOBRD13:def 2 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) "k") ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i1")) "," (Set (Var "j1")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i2")) "," (Set (Var "j2")) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )); func :::"left_cell"::: "(" "f" "," "k" "," "G" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: GOBRD13:def 3 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) "k") ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i1")) "," (Set (Var "j1")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i1")) "," (Set (Var "j2")) ")" )) ")" )); end; :: deftheorem GOBRD13:def 1 : canceled; :: deftheorem defines :::"right_cell"::: GOBRD13:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i1")) "," (Set "(" (Set (Var "j1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i2")) "," (Set (Var "j2")) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) ")" ))))); :: deftheorem defines :::"left_cell"::: GOBRD13:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j1")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i1")) "," (Set (Var "j1")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i1")) "," (Set (Var "j2")) ")" )) ")" )) ")" ))))); theorem :: GOBRD13:21 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) "holds" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:22 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) "holds" (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:23 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:24 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:25 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:26 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:27 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:28 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:29 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set "(" ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) ")" ))))) ; theorem :: GOBRD13:30 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) "is" ($#v4_pre_topc :::"closed"::: ) )))) ; theorem :: GOBRD13:31 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) ")" )))) ; theorem :: GOBRD13:32 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool "(" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) ")" )))) ; theorem :: GOBRD13:33 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "f")) "being" ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool "(" (Bool (Set ($#k3_gobrd13 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "G")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k5_goboard5 :::"left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k2_gobrd13 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "G")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_goboard5 :::"right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) ")" )))) ; definitionlet "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "G" be ($#m2_finseq_1 :::"Go-board":::); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); assume (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "k"))) & (Bool (Set (Set (Const "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "f")))) & (Bool (Set (Const "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Const "G"))) ")" ) ; func :::"front_right_cell"::: "(" "f" "," "k" "," "G" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: GOBRD13:def 4 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) "k") ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i2")) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )); func :::"front_left_cell"::: "(" "f" "," "k" "," "G" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: GOBRD13:def 5 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) "k") ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i2")) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" "G" "," (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )); end; :: deftheorem defines :::"front_right_cell"::: GOBRD13:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i2")) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) ")" ))))); :: deftheorem defines :::"front_left_cell"::: GOBRD13:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i2")) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) ")" ))))); theorem :: GOBRD13:34 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) "holds" (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:35 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) "holds" (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:36 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:37 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:38 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:39 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j")) ")" ))))) ; theorem :: GOBRD13:40 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:41 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_goboard5 :::"cell"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: GOBRD13:42 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Go-board":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_gobrd13 :::"front_left_cell"::: ) "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_gobrd13 :::"front_right_cell"::: ) "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) "," (Set (Var "k")) "," (Set (Var "G")) ")" )) ")" )))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "G" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "f" :::"turns_right"::: "k" "," "G" means :: GOBRD13:def 6 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) "k") ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )); pred "f" :::"turns_left"::: "k" "," "G" means :: GOBRD13:def 7 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) "k") ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )); pred "f" :::"goes_straight"::: "k" "," "G" means :: GOBRD13:def 8 (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) "k") ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "G")) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )); end; :: deftheorem defines :::"turns_right"::: GOBRD13:def 6 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_gobrd13 :::"turns_right"::: ) (Set (Var "k")) "," (Set (Var "G"))) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) ")" ))))); :: deftheorem defines :::"turns_left"::: GOBRD13:def 7 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_gobrd13 :::"turns_left"::: ) (Set (Var "k")) "," (Set (Var "G"))) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) ")" ))))); :: deftheorem defines :::"goes_straight"::: GOBRD13:def 8 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_gobrd13 :::"goes_straight"::: ) (Set (Var "k")) "," (Set (Var "G"))) "iff" (Bool "for" (Set (Var "i1")) "," (Set (Var "j1")) "," (Set (Var "i2")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i1")) "," (Set (Var "j1")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set (Var "j2")) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "j1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Var "j2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set (Var "j2")) ")" )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Var "j1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j2")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i2")) "," (Set "(" (Set (Var "j2")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" )) ")" ))))); theorem :: GOBRD13:43 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) ($#r1_gobrd13 :::"turns_right"::: ) (Set (Var "k")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "f")) ($#r1_gobrd13 :::"turns_right"::: ) (Set (Var "k")) "," (Set (Var "G"))))))) ; theorem :: GOBRD13:44 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) ($#r2_gobrd13 :::"turns_left"::: ) (Set (Var "k")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "f")) ($#r2_gobrd13 :::"turns_left"::: ) (Set (Var "k")) "," (Set (Var "G"))))))) ; theorem :: GOBRD13:45 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) ($#r3_gobrd13 :::"goes_straight"::: ) (Set (Var "k")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "f")) ($#r3_gobrd13 :::"goes_straight"::: ) (Set (Var "k")) "," (Set (Var "G"))))))) ; theorem :: GOBRD13:46 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")))) & (Bool (Set (Var "f1")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set (Set (Var "f1")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k")))) & (Bool (Set (Var "f1")) ($#r1_gobrd13 :::"turns_right"::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1)) "," (Set (Var "G"))) & (Bool (Set (Var "f2")) ($#r1_gobrd13 :::"turns_right"::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1)) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f1")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))))) ; theorem :: GOBRD13:47 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")))) & (Bool (Set (Var "f1")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set (Set (Var "f1")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k")))) & (Bool (Set (Var "f1")) ($#r2_gobrd13 :::"turns_left"::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1)) "," (Set (Var "G"))) & (Bool (Set (Var "f2")) ($#r2_gobrd13 :::"turns_left"::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1)) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f1")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))))) ; theorem :: GOBRD13:48 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")))) & (Bool (Set (Var "f1")) ($#r1_goboard1 :::"is_sequence_on"::: ) (Set (Var "G"))) & (Bool (Set (Set (Var "f1")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k")))) & (Bool (Set (Var "f1")) ($#r3_gobrd13 :::"goes_straight"::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1)) "," (Set (Var "G"))) & (Bool (Set (Var "f2")) ($#r3_gobrd13 :::"goes_straight"::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1)) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "f1")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))))) ;