:: Introduction to Go-Board - Part I. Basic Notations :: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura :: :: Received August 24, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin definition let f be FinSequence of (TOP-REAL 2); func X_axis f -> FinSequence of REAL means :Def1: :: GOBOARD1:def 1 ( len it = len f & ( for n being Element of NAT st n in dom it holds it . n = (f /. n) `1 ) ); existence ex b1 being FinSequence of REAL st ( len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = (f /. n) `1 ) ) proofend; uniqueness for b1, b2 being FinSequence of REAL st len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = (f /. n) `1 ) & len b2 = len f & ( for n being Element of NAT st n in dom b2 holds b2 . n = (f /. n) `1 ) holds b1 = b2 proofend; func Y_axis f -> FinSequence of REAL means :Def2: :: GOBOARD1:def 2 ( len it = len f & ( for n being Element of NAT st n in dom it holds it . n = (f /. n) `2 ) ); existence ex b1 being FinSequence of REAL st ( len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = (f /. n) `2 ) ) proofend; uniqueness for b1, b2 being FinSequence of REAL st len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = (f /. n) `2 ) & len b2 = len f & ( for n being Element of NAT st n in dom b2 holds b2 . n = (f /. n) `2 ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines X_axis GOBOARD1:def_1_:_ for f being FinSequence of (TOP-REAL 2) for b2 being FinSequence of REAL holds ( b2 = X_axis f iff ( len b2 = len f & ( for n being Element of NAT st n in dom b2 holds b2 . n = (f /. n) `1 ) ) ); :: deftheorem Def2 defines Y_axis GOBOARD1:def_2_:_ for f being FinSequence of (TOP-REAL 2) for b2 being FinSequence of REAL holds ( b2 = Y_axis f iff ( len b2 = len f & ( for n being Element of NAT st n in dom b2 holds b2 . n = (f /. n) `2 ) ) ); theorem Th1: :: GOBOARD1:1 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st i in dom f & 2 <= len f holds f /. i in L~ f proofend; begin :: Matrix preliminaries theorem Th2: :: GOBOARD1:2 for D being non empty set for M being Matrix of D for i, j being Element of NAT st j in dom M & i in Seg (width M) holds (Col (M,i)) . j = (Line (M,j)) . i proofend; definition let D be non empty set ; let M be Matrix of D; :: original:empty-yielding redefine attrM is empty-yielding means :Def3: :: GOBOARD1:def 3 ( 0 = len M or 0 = width M ); compatibility ( M is empty-yielding iff ( 0 = len M or 0 = width M ) ) proofend; end; :: deftheorem Def3 defines empty-yielding GOBOARD1:def_3_:_ for D being non empty set for M being Matrix of D holds ( M is empty-yielding iff ( 0 = len M or 0 = width M ) ); definition let M be Matrix of (TOP-REAL 2); attrM is X_equal-in-line means :Def4: :: GOBOARD1:def 4 for n being Element of NAT st n in dom M holds X_axis (Line (M,n)) is constant ; attrM is Y_equal-in-column means :Def5: :: GOBOARD1:def 5 for n being Element of NAT st n in Seg (width M) holds Y_axis (Col (M,n)) is constant ; attrM is Y_increasing-in-line means :Def6: :: GOBOARD1:def 6 for n being Element of NAT st n in dom M holds Y_axis (Line (M,n)) is increasing ; attrM is X_increasing-in-column means :Def7: :: GOBOARD1:def 7 for n being Element of NAT st n in Seg (width M) holds X_axis (Col (M,n)) is increasing ; end; :: deftheorem Def4 defines X_equal-in-line GOBOARD1:def_4_:_ for M being Matrix of (TOP-REAL 2) holds ( M is X_equal-in-line iff for n being Element of NAT st n in dom M holds X_axis (Line (M,n)) is constant ); :: deftheorem Def5 defines Y_equal-in-column GOBOARD1:def_5_:_ for M being Matrix of (TOP-REAL 2) holds ( M is Y_equal-in-column iff for n being Element of NAT st n in Seg (width M) holds Y_axis (Col (M,n)) is constant ); :: deftheorem Def6 defines Y_increasing-in-line GOBOARD1:def_6_:_ for M being Matrix of (TOP-REAL 2) holds ( M is Y_increasing-in-line iff for n being Element of NAT st n in dom M holds Y_axis (Line (M,n)) is increasing ); :: deftheorem Def7 defines X_increasing-in-column GOBOARD1:def_7_:_ for M being Matrix of (TOP-REAL 2) holds ( M is X_increasing-in-column iff for n being Element of NAT st n in Seg (width M) holds X_axis (Col (M,n)) is increasing ); Lm1: for D being non empty set for M being Matrix of D holds ( M is V3() iff ( 0 < len M & 0 < width M ) ) proofend; registration cluster Relation-like V3() NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column for FinSequence of K196( the carrier of (TOP-REAL 2)); existence ex b1 being Matrix of (TOP-REAL 2) st ( b1 is V3() & b1 is X_equal-in-line & b1 is Y_equal-in-column & b1 is Y_increasing-in-line & b1 is X_increasing-in-column ) proofend; end; theorem Th3: :: GOBOARD1:3 for M being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) for x being set for n, m being Element of NAT st x in rng (Line (M,n)) & x in rng (Line (M,m)) & n in dom M & m in dom M holds n = m proofend; theorem Th4: :: GOBOARD1:4 for M being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) for x being set for n, m being Element of NAT st x in rng (Col (M,n)) & x in rng (Col (M,m)) & n in Seg (width M) & m in Seg (width M) holds n = m proofend; begin :: Go board definition mode Go-board is V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of (TOP-REAL 2); end; theorem :: GOBOARD1:5 for m, k, i, j being Element of NAT for x being set for G being Go-board st x = G * (m,k) & x = G * (i,j) & [m,k] in Indices G & [i,j] in Indices G holds ( m = i & k = j ) proofend; theorem :: GOBOARD1:6 for f being FinSequence of (TOP-REAL 2) for m being Element of NAT for G being Go-board st m in dom f & f /. 1 in rng (Col (G,1)) holds (f | m) /. 1 in rng (Col (G,1)) proofend; theorem :: GOBOARD1:7 for f being FinSequence of (TOP-REAL 2) for m being Element of NAT for G being Go-board st m in dom f & f /. m in rng (Col (G,(width G))) holds (f | m) /. (len (f | m)) in rng (Col (G,(width G))) proofend; theorem Th8: :: GOBOARD1:8 for f being FinSequence of (TOP-REAL 2) for i, n, m, k being Element of NAT for G being Go-board st rng f misses rng (Col (G,i)) & f /. n = G * (m,k) & n in dom f & m in dom G holds i <> k proofend; definition let G be Go-board; let i be Element of NAT ; assume A1: ( i in Seg (width G) & width G > 1 ) ; func DelCol (G,i) -> Go-board means :Def8: :: GOBOARD1:def 8 ( len it = len G & ( for k being Element of NAT st k in dom G holds it . k = Del ((Line (G,k)),i) ) ); existence ex b1 being Go-board st ( len b1 = len G & ( for k being Element of NAT st k in dom G holds b1 . k = Del ((Line (G,k)),i) ) ) proofend; uniqueness for b1, b2 being Go-board st len b1 = len G & ( for k being Element of NAT st k in dom G holds b1 . k = Del ((Line (G,k)),i) ) & len b2 = len G & ( for k being Element of NAT st k in dom G holds b2 . k = Del ((Line (G,k)),i) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines DelCol GOBOARD1:def_8_:_ for G being Go-board for i being Element of NAT st i in Seg (width G) & width G > 1 holds for b3 being Go-board holds ( b3 = DelCol (G,i) iff ( len b3 = len G & ( for k being Element of NAT st k in dom G holds b3 . k = Del ((Line (G,k)),i) ) ) ); theorem Th9: :: GOBOARD1:9 for i, k being Element of NAT for G being Go-board st i in Seg (width G) & width G > 1 & k in dom G holds Line ((DelCol (G,i)),k) = Del ((Line (G,k)),i) proofend; theorem Th10: :: GOBOARD1:10 for i, m being Element of NAT for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 holds width (DelCol (G,i)) = m proofend; theorem :: GOBOARD1:11 for i being Element of NAT for G being Go-board st i in Seg (width G) & width G > 1 holds width G = (width (DelCol (G,i))) + 1 proofend; theorem Th12: :: GOBOARD1:12 for i, n, m being Element of NAT for G being Go-board st i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) holds (DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m proofend; theorem Th13: :: GOBOARD1:13 for i, m, k being Element of NAT for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & 1 <= k & k < i holds ( Col ((DelCol (G,i)),k) = Col (G,k) & k in Seg (width (DelCol (G,i))) & k in Seg (width G) ) proofend; theorem Th14: :: GOBOARD1:14 for i, m, k being Element of NAT for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & i <= k & k <= m holds ( Col ((DelCol (G,i)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,i))) & k + 1 in Seg (width G) ) proofend; theorem Th15: :: GOBOARD1:15 for i, m, n, k being Element of NAT for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & 1 <= k & k < i holds ( (DelCol (G,i)) * (n,k) = G * (n,k) & k in Seg (width G) ) proofend; theorem Th16: :: GOBOARD1:16 for i, m, n, k being Element of NAT for G being Go-board st i in Seg (width G) & width G = m + 1 & m > 0 & n in dom G & i <= k & k <= m holds ( (DelCol (G,i)) * (n,k) = G * (n,(k + 1)) & k + 1 in Seg (width G) ) proofend; theorem :: GOBOARD1:17 for m, k being Element of NAT for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds ( Col ((DelCol (G,1)),k) = Col (G,(k + 1)) & k in Seg (width (DelCol (G,1))) & k + 1 in Seg (width G) ) proofend; theorem :: GOBOARD1:18 for m, k, n being Element of NAT for G being Go-board st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds ( (DelCol (G,1)) * (n,k) = G * (n,(k + 1)) & 1 in Seg (width G) ) proofend; theorem :: GOBOARD1:19 for m, k being Element of NAT for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds ( Col ((DelCol (G,(width G))),k) = Col (G,k) & k in Seg (width (DelCol (G,(width G)))) ) proofend; theorem Th20: :: GOBOARD1:20 for m, k, n being Element of NAT for G being Go-board st width G = m + 1 & m > 0 & k in Seg m & n in dom G holds ( k in Seg (width G) & (DelCol (G,(width G))) * (n,k) = G * (n,k) & width G in Seg (width G) ) proofend; theorem :: GOBOARD1:21 for f being FinSequence of (TOP-REAL 2) for i, n, m being Element of NAT for G being Go-board st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds f /. n in rng (Line ((DelCol (G,i)),m)) proofend; definition let D be set ; let f be FinSequence of D; let M be Matrix of D; predf is_sequence_on M means :Def9: :: GOBOARD1:def 9 ( ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 ) ); end; :: deftheorem Def9 defines is_sequence_on GOBOARD1:def_9_:_ for D being set for f being FinSequence of D for M being Matrix of D holds ( f is_sequence_on M iff ( ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 ) ) ); Lm2: for D being set for M being Matrix of D holds <*> D is_sequence_on M proofend; theorem :: GOBOARD1:22 for m being Element of NAT for D being set for f being FinSequence of D for M being Matrix of D holds ( ( m in dom f implies 1 <= len (f | m) ) & ( f is_sequence_on M implies f | m is_sequence_on M ) ) proofend; theorem :: GOBOARD1:23 for f1, f2 being FinSequence of (TOP-REAL 2) for D being set for M being Matrix of D st ( for n being Element of NAT st n in dom f1 holds ex i, j being Element of NAT st ( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f2 holds ex i, j being Element of NAT st ( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds for n being Element of NAT st n in dom (f1 ^ f2) holds ex i, j being Element of NAT st ( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) ) proofend; theorem :: GOBOARD1:24 for f1, f2 being FinSequence of (TOP-REAL 2) for D being set for M being Matrix of D st ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * (m,k) & f2 /. 1 = M * (i,j) & len f1 in dom f1 & 1 in dom f2 holds (abs (m - i)) + (abs (k - j)) = 1 ) holds for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) holds (abs (m - i)) + (abs (k - j)) = 1 proofend; theorem :: GOBOARD1:25 for i being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds f is_sequence_on DelCol (G,i) proofend; theorem Th26: :: GOBOARD1:26 for i being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds ex n being Element of NAT st ( n in dom G & f /. i in rng (Line (G,n)) ) proofend; theorem Th27: :: GOBOARD1:27 for i, n being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds for k being Element of NAT st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds abs (n - k) = 1 proofend; theorem Th28: :: GOBOARD1:28 for i, m being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G & i in dom G & i + 1 in dom G & m in dom f & f /. m in rng (Line (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Line (G,i)) holds k <= m ) holds ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(i + 1))) ) proofend; theorem :: GOBOARD1:29 for G being Go-board for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. 1 in rng (Line (G,1)) & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G holds ( ( for i being Element of NAT st 1 <= i & i <= len G holds ex k being Element of NAT st ( k in dom f & f /. k in rng (Line (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= len G & 2 <= len f holds L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Line (G,i)) holds n <= k ) & k < m & f /. m in rng (Line (G,j)) holds i < j ) ) proofend; theorem Th30: :: GOBOARD1:30 for i being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds ex n being Element of NAT st ( n in Seg (width G) & f /. i in rng (Col (G,n)) ) proofend; theorem Th31: :: GOBOARD1:31 for i, n being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg (width G) & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds for k being Element of NAT st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds abs (n - k) = 1 proofend; theorem Th32: :: GOBOARD1:32 for i, m being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Element of NAT st k in dom f & f /. k in rng (Col (G,i)) holds k <= m ) holds ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) ) proofend; theorem Th33: :: GOBOARD1:33 for G being Go-board for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G holds ( ( for i being Element of NAT st 1 <= i & i <= width G holds ex k being Element of NAT st ( k in dom f & f /. k in rng (Col (G,i)) ) ) & ( for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds L~ f meets rng (Col (G,i)) ) & ( for i, j, k, m being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= width G & k in dom f & m in dom f & f /. k in rng (Col (G,i)) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col (G,i)) holds n <= k ) & k < m & f /. m in rng (Col (G,j)) holds i < j ) ) proofend; theorem Th34: :: GOBOARD1:34 for k, n being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st k in Seg (width G) & f /. 1 in rng (Col (G,1)) & f is_sequence_on G & ( for i being Element of NAT st i in dom f & f /. i in rng (Col (G,k)) holds n <= i ) holds for i being Element of NAT st i in dom f & i <= n holds for m being Element of NAT st m in Seg (width G) & f /. i in rng (Col (G,m)) holds m <= k proofend; theorem :: GOBOARD1:35 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,(width G))) & width G > 1 & 1 <= len f holds ex g being FinSequence of (TOP-REAL 2) st ( g /. 1 in rng (Col ((DelCol (G,(width G))),1)) & g /. (len g) in rng (Col ((DelCol (G,(width G))),(width (DelCol (G,(width G)))))) & 1 <= len g & g is_sequence_on DelCol (G,(width G)) & rng g c= rng f ) proofend; theorem :: GOBOARD1:36 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & (rng f) /\ (rng (Col (G,1))) <> {} & (rng f) /\ (rng (Col (G,(width G)))) <> {} holds ex g being FinSequence of (TOP-REAL 2) st ( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,(width G))) & 1 <= len g & g is_sequence_on G ) proofend; theorem :: GOBOARD1:37 for k, n being Element of NAT for G being Go-board for f being FinSequence of (TOP-REAL 2) st k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) holds ( ( for i being Element of NAT st k <= i & i <= len G holds ex j being Element of NAT st ( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Element of NAT st k < i & i <= len G holds ex j being Element of NAT st ( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) ) proofend;