:: Introduction to Go-Board - Part I. Basic Notations
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Copyright (c) 1992-2021 Association of Mizar Users

definition
let f be FinSequence of ();
func X_axis f -> FinSequence of REAL means :Def1: :: GOBOARD1:def 1
( len it = len f & ( for n being 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 Nat st n in dom b1 holds
b1 . n = (f /. n) 1 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len f & ( for n being Nat st n in dom b1 holds
b1 . n = (f /. n) 1 ) & len b2 = len f & ( for n being Nat st n in dom b2 holds
b2 . n = (f /. n) 1 ) holds
b1 = b2
proof end;
func Y_axis f -> FinSequence of REAL means :Def2: :: GOBOARD1:def 2
( len it = len f & ( for n being 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 Nat st n in dom b1 holds
b1 . n = (f /. n) 2 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len f & ( for n being Nat st n in dom b1 holds
b1 . n = (f /. n) 2 ) & len b2 = len f & ( for n being Nat st n in dom b2 holds
b2 . n = (f /. n) 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines X_axis GOBOARD1:def 1 :
for f being FinSequence of ()
for b2 being FinSequence of REAL holds
( b2 = X_axis f iff ( len b2 = len f & ( for n being 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 ()
for b2 being FinSequence of REAL holds
( b2 = Y_axis f iff ( len b2 = len f & ( for n being Nat st n in dom b2 holds
b2 . n = (f /. n) 2 ) ) );

theorem Th1: :: GOBOARD1:1
for f being FinSequence of ()
for i being Nat st i in dom f & 2 <= len f holds
f /. i in L~ f
proof end;

:: Matrix preliminaries
definition
let M be Matrix of ();
attr M is X_equal-in-line means :Def3: :: GOBOARD1:def 4
for n being Nat st n in dom M holds
X_axis (Line (M,n)) is constant ;
attr M is Y_equal-in-column means :Def4: :: GOBOARD1:def 5
for n being Nat st n in Seg () holds
Y_axis (Col (M,n)) is constant ;
attr M is Y_increasing-in-line means :Def5: :: GOBOARD1:def 6
for n being Nat st n in dom M holds
Y_axis (Line (M,n)) is increasing ;
attr M is X_increasing-in-column means :Def6: :: GOBOARD1:def 7
for n being Nat st n in Seg () holds
X_axis (Col (M,n)) is increasing ;
end;

:: deftheorem GOBOARD1:def 3 :
canceled;

:: deftheorem Def3 defines X_equal-in-line GOBOARD1:def 4 :
for M being Matrix of () holds
( M is X_equal-in-line iff for n being Nat st n in dom M holds
X_axis (Line (M,n)) is constant );

:: deftheorem Def4 defines Y_equal-in-column GOBOARD1:def 5 :
for M being Matrix of () holds
( M is Y_equal-in-column iff for n being Nat st n in Seg () holds
Y_axis (Col (M,n)) is constant );

:: deftheorem Def5 defines Y_increasing-in-line GOBOARD1:def 6 :
for M being Matrix of () holds
( M is Y_increasing-in-line iff for n being Nat st n in dom M holds
Y_axis (Line (M,n)) is increasing );

:: deftheorem Def6 defines X_increasing-in-column GOBOARD1:def 7 :
for M being Matrix of () holds
( M is X_increasing-in-column iff for n being Nat st n in Seg () holds
X_axis (Col (M,n)) is increasing );

registration
existence
ex b1 being Matrix of () 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 )
proof end;
end;

theorem :: GOBOARD1:2
canceled;

::$CT theorem Th2: :: GOBOARD1:3 for M being X_equal-in-line X_increasing-in-column Matrix of () for x being set for n, m being 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 proof end; theorem Th3: :: GOBOARD1:4 for M being Y_equal-in-column Y_increasing-in-line Matrix of () for x being set for n, m being Nat st x in rng (Col (M,n)) & x in rng (Col (M,m)) & n in Seg () & m in Seg () holds n = m proof end; :: Go board definition end; theorem :: GOBOARD1:5 for m, i, j, k being 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 ) proof end; theorem :: GOBOARD1:6 canceled; theorem :: GOBOARD1:7 canceled; theorem :: GOBOARD1:8 canceled; ::$CT 3
registration
let G be Go-board;
let i be Nat;
coherence
( DelCol (G,i) is X_equal-in-line & DelCol (G,i) is Y_equal-in-column & DelCol (G,i) is Y_increasing-in-line & DelCol (G,i) is X_increasing-in-column )
proof end;
end;

theorem :: GOBOARD1:9
canceled;

theorem :: GOBOARD1:10
canceled;

theorem :: GOBOARD1:11
canceled;

::\$CT 3
theorem :: GOBOARD1:12
for n, m, i being Nat
for G being Go-board st i in Seg () & 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 by MATRIX_0:66;

theorem Th6: :: GOBOARD1:13
for m, i, k being Nat
for G being Go-board st i in Seg () & 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 () ) by MATRIX_0:67;

theorem :: GOBOARD1:14
for m, i, k being Nat
for G being Go-board st i in Seg () & 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 () ) by MATRIX_0:68;

theorem Th8: :: GOBOARD1:15
for n, m, i, k being Nat
for G being Go-board st i in Seg () & 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 () ) by MATRIX_0:69;

theorem Th9: :: GOBOARD1:16
for n, m, i, k being Nat
for G being Go-board st i in Seg () & 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 () ) by MATRIX_0:70;

theorem :: GOBOARD1:17
for m, k being 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 () ) by MATRIX_0:71;

theorem :: GOBOARD1:18
for n, m, k being 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 () ) by MATRIX_0:72;

theorem :: GOBOARD1:19
for m, k being Nat
for G being Go-board st width G = m + 1 & m > 0 & k in Seg m holds
( Col ((DelCol (G,())),k) = Col (G,k) & k in Seg (width (DelCol (G,()))) ) by MATRIX_0:73;

theorem Th13: :: GOBOARD1:20
for n, m, k being 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 () & (DelCol (G,())) * (n,k) = G * (n,k) & width G in Seg () ) by MATRIX_0:74;

theorem :: GOBOARD1:21
for f being FinSequence of ()
for n, m, i being 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 () & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m)) by MATRIX_0:75;

definition
let D be set ;
let f be FinSequence of D;
let M be Matrix of D;
pred f is_sequence_on M means :: GOBOARD1:def 9
( ( for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) );
end;

:: deftheorem GOBOARD1:def 8 :
canceled;

:: deftheorem 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 Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) ) );

theorem :: GOBOARD1:22
for m being 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 ) )
proof end;

theorem :: GOBOARD1:23
for f1, f2 being FinSequence of ()
for D being set
for M being Matrix of D st ( for n being Nat st n in dom f1 holds
ex i, j being Nat st
( [i,j] in Indices M & f1 /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f2 holds
ex i, j being Nat st
( [i,j] in Indices M & f2 /. n = M * (i,j) ) ) holds
for n being Nat st n in dom (f1 ^ f2) holds
ex i, j being Nat st
( [i,j] in Indices M & (f1 ^ f2) /. n = M * (i,j) )
proof end;

theorem :: GOBOARD1:24
for f1, f2 being FinSequence of ()
for D being set
for M being Matrix of D st ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 ) holds
for n being Nat st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1
proof end;

theorem :: GOBOARD1:25
for i being Nat
for G being Go-board
for f being FinSequence of () st f is_sequence_on G & i in Seg () & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)
proof end;

theorem Th19: :: GOBOARD1:26
for i being Nat
for G being Go-board
for f being FinSequence of () st f is_sequence_on G & i in dom f holds
ex n being Nat st
( n in dom G & f /. i in rng (Line (G,n)) )
proof end;

theorem Th20: :: GOBOARD1:27
for n, i being Nat
for G being Go-board
for f being FinSequence of () 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 Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
|.(n - k).| = 1
proof end;

theorem Th21: :: GOBOARD1:28
for m, i being Nat
for G being Go-board
for f being FinSequence of () 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 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))) )
proof end;

theorem :: GOBOARD1:29
for G being Go-board
for f being FinSequence of () 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 Nat st 1 <= i & i <= len G holds
ex k being Nat st
( k in dom f & f /. k in rng (Line (G,i)) ) ) & ( for i being Nat st 1 <= i & i <= len G & 2 <= len f holds
L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being 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 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 ) )
proof end;

theorem Th23: :: GOBOARD1:30
for i being Nat
for G being Go-board
for f being FinSequence of () st f is_sequence_on G & i in dom f holds
ex n being Nat st
( n in Seg () & f /. i in rng (Col (G,n)) )
proof end;

theorem Th24: :: GOBOARD1:31
for n, i being Nat
for G being Go-board
for f being FinSequence of () st f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg () & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds
for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1
proof end;

theorem Th25: :: GOBOARD1:32
for m, i being Nat
for G being Go-board
for f being FinSequence of () st 1 <= len f & f /. (len f) in rng (Col (G,())) & f is_sequence_on G & i in Seg () & i + 1 in Seg () & m in dom f & f /. m in rng (Col (G,i)) & ( for k being 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))) )
proof end;

theorem Th26: :: GOBOARD1:33
for G being Go-board
for f being FinSequence of () st 1 <= len f & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,())) & f is_sequence_on G holds
( ( for i being Nat st 1 <= i & i <= width G holds
ex k being Nat st
( k in dom f & f /. k in rng (Col (G,i)) ) ) & ( for i being Nat st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) ) & ( for i, j, k, m being 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 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 ) )
proof end;

theorem Th27: :: GOBOARD1:34
for n, k being Nat
for G being Go-board
for f being FinSequence of () st k in Seg () & f /. 1 in rng (Col (G,1)) & f is_sequence_on G & ( for i being Nat st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ) holds
for i being Nat st i in dom f & i <= n holds
for m being Nat st m in Seg () & f /. i in rng (Col (G,m)) holds
m <= k
proof end;

theorem :: GOBOARD1:35
for G being Go-board
for f being FinSequence of () st f is_sequence_on G & f /. 1 in rng (Col (G,1)) & f /. (len f) in rng (Col (G,())) & width G > 1 & 1 <= len f holds
ex g being FinSequence of () st
( g /. 1 in rng (Col ((DelCol (G,())),1)) & g /. (len g) in rng (Col ((DelCol (G,())),(width (DelCol (G,()))))) & 1 <= len g & g is_sequence_on DelCol (G,()) & rng g c= rng f )
proof end;

theorem :: GOBOARD1:36
for G being Go-board
for f being FinSequence of () st f is_sequence_on G & (rng f) /\ (rng (Col (G,1))) <> {} & (rng f) /\ (rng (Col (G,()))) <> {} holds
ex g being FinSequence of () st
( rng g c= rng f & g /. 1 in rng (Col (G,1)) & g /. (len g) in rng (Col (G,())) & 1 <= len g & g is_sequence_on G )
proof end;

theorem :: GOBOARD1:37
for n, k being Nat
for G being Go-board
for f being FinSequence of () 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 Nat st k <= i & i <= len G holds
ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Nat st k < i & i <= len G holds
ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )
proof end;