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

begin

theorem Th1: :: GOBOARD1:1

for r, s being Real holds
( abs (r - s) = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )

proof end;

theorem Th2: :: GOBOARD1:2

for i, j, n, m being Element of NAT holds
( (abs (i - j)) + (abs (n - m)) = 1 iff ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) )

proof end;

theorem Th3: :: GOBOARD1:3

for n being Element of NAT holds
( n > 1 iff ex m being Element of NAT st
( n = m + 1 & m > 0 ) )

proof end;

begin

theorem :: GOBOARD1:4

canceled;

theorem :: GOBOARD1:5

canceled;

theorem :: GOBOARD1:6

canceled;

theorem Th7: :: GOBOARD1:7

for f being FinSequence
for n, m, k being Element of NAT st len f = m + 1 & n in dom f & k in Seg m & not (Del f,n) . k = f . k holds
(Del f,n) . k = f . (k + 1)

proof end;

theorem :: GOBOARD1:8

canceled;

theorem :: GOBOARD1:9

canceled;

definition

canceled;
let f be FinSequence;
redefine attr f is constant means :Def2: :: GOBOARD1:def 2
for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m;
compatibility
( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m )

proof end;

end;

:: deftheorem GOBOARD1:def 1 :

canceled;

:: deftheorem Def2 defines constant GOBOARD1:def 2 :

for f being FinSequence holds
( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m );

registration

cluster -> real-valued FinSequence of REAL ;
coherence
for b₁ being FinSequence of REAL holds b₁ is real-valued ;

end;

registration

cluster non empty real-valued increasing FinSequence of REAL ;
existence
ex b₁ being FinSequence of REAL st
( not b₁ is empty & b₁ is increasing )

proof end;

end;

registration

cluster constant real-valued FinSequence of REAL ;
existence
ex b₁ being FinSequence of REAL st b₁ is constant

proof end;

end;

definition

let f be FinSequence of ;
func X_axis f -> FinSequence of REAL means :Def3: :: GOBOARD1:def 3
( len it = len f & ( for n being Element of NAT st n in dom it holds
it . n = (f /. n) `1 ) );
existence
ex b<sub>1</sub> being FinSequence of REAL st
( len b<sub>1</sub> = len f & ( for n being Element of NAT st n in dom b<sub>1</sub> holds
b<sub>1</sub> . n = (f /. n) `1 ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = len f & ( for n being Element of NAT st n in dom b₁ holds
b₁ . n = (f /. n) `1 ) & len b<sub>2</sub> = len f & ( for n being Element of NAT st n in dom b<sub>2</sub> holds
b<sub>2</sub> . n = (f /. n) `1 ) holds
b₁ = b₂

proof end;

func Y_axis f -> FinSequence of REAL means :Def4: :: GOBOARD1:def 4
( len it = len f & ( for n being Element of NAT st n in dom it holds
it . n = (f /. n) `2 ) );
existence
ex b<sub>1</sub> being FinSequence of REAL st
( len b<sub>1</sub> = len f & ( for n being Element of NAT st n in dom b<sub>1</sub> holds
b<sub>1</sub> . n = (f /. n) `2 ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = len f & ( for n being Element of NAT st n in dom b₁ holds
b₁ . n = (f /. n) `2 ) & len b<sub>2</sub> = len f & ( for n being Element of NAT st n in dom b<sub>2</sub> holds
b<sub>2</sub> . n = (f /. n) `2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines X_axis GOBOARD1:def 3 :

for f being FinSequence of
for b₂ being FinSequence of REAL holds
( b₂ = X_axis f iff ( len b₂ = len f & ( for n being Element of NAT st n in dom b₂ holds
b₂ . n = (f /. n) `1 ) ) );

:: deftheorem Def4 defines Y_axis GOBOARD1:def 4 :

for f being FinSequence of
for b₂ being FinSequence of REAL holds
( b₂ = Y_axis f iff ( len b₂ = len f & ( for n being Element of NAT st n in dom b₂ holds
b₂ . n = (f /. n) `2 ) ) );

theorem :: GOBOARD1:10

canceled;

theorem :: GOBOARD1:11

canceled;

theorem :: GOBOARD1:12

canceled;

theorem :: GOBOARD1:13

canceled;

theorem Th14: :: GOBOARD1:14

for v being FinSequence of REAL
for n, i, m being Element of NAT st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Element of NAT st k in dom v & v . k = i holds
k <= m ) holds
( m + 1 in dom v & v . (m + 1) = i + 1 )

proof end;

theorem :: GOBOARD1:15

for v being FinSequence of REAL
for n being Element of NAT st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) holds
( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )

proof end;

theorem Th16: :: GOBOARD1:16

for f being FinSequence of
for i being Element of NAT st i in dom f & 2 <= len f holds
f /. i in L~ f

proof end;

begin

theorem Th17: :: GOBOARD1:17

for D being non empty set
for M being Matrix of
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

proof end;

definition

let D be non empty set ;
let M be Matrix of ;
:: original: empty-yielding
redefine attr M is empty-yielding means :Def5: :: GOBOARD1:def 5
( 0 = len M or 0 = width M );
compatibility
( M is empty-yielding iff ( 0 = len M or 0 = width M ) )

proof end;

end;

:: deftheorem Def5 defines empty-yielding GOBOARD1:def 5 :

for D being non empty set
for M being Matrix of holds
( M is empty-yielding iff ( 0 = len M or 0 = width M ) );

definition

let M be Matrix of ;
attr M is X_equal-in-line means :Def6: :: GOBOARD1:def 6
for n being Element of NAT st n in dom M holds
X_axis (Line M,n) is constant ;
attr M is Y_equal-in-column means :Def7: :: GOBOARD1:def 7
for n being Element of NAT st n in Seg (width M) holds
Y_axis (Col M,n) is constant ;
attr M is Y_increasing-in-line means :Def8: :: GOBOARD1:def 8
for n being Element of NAT st n in dom M holds
Y_axis (Line M,n) is increasing ;
attr M is X_increasing-in-column means :Def9: :: GOBOARD1:def 9
for n being Element of NAT st n in Seg (width M) holds
X_axis (Col M,n) is increasing ;

end;

:: deftheorem Def6 defines X_equal-in-line GOBOARD1:def 6 :

for M being Matrix of 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 Def7 defines Y_equal-in-column GOBOARD1:def 7 :

for M being Matrix of 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 Def8 defines Y_increasing-in-line GOBOARD1:def 8 :

for M being Matrix of 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 Def9 defines X_increasing-in-column GOBOARD1:def 9 :

for M being Matrix of 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 holds
( not M is empty-yielding iff ( 0 < len M & 0 < width M ) )

proof end;

registration

cluster V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K164(the carrier of (TOP-REAL 2));
existence
ex b₁ being Matrix of st
( not b₁ is empty-yielding & b₁ is X_equal-in-line & b₁ is Y_equal-in-column & b₁ is Y_increasing-in-line & b₁ is X_increasing-in-column )

proof end;

end;

theorem :: GOBOARD1:18

canceled;

theorem Th19: :: GOBOARD1:19

for M being X_equal-in-line X_increasing-in-column Matrix of
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

proof end;

theorem Th20: :: GOBOARD1:20

for M being Y_equal-in-column Y_increasing-in-line Matrix of
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

proof end;

begin

definition

mode Go-board is V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of ;

end;

theorem :: GOBOARD1:21

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 )

proof end;

theorem :: GOBOARD1:22

for f being FinSequence of
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)

proof end;

theorem :: GOBOARD1:23

for f being FinSequence of
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))

proof end;

theorem Th24: :: GOBOARD1:24

for f being FinSequence of
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

proof end;

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 :Def10: :: GOBOARD1:def 10
( 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 b₁ being Go-board st
( len b₁ = len G & ( for k being Element of NAT st k in dom G holds
b₁ . k = Del (Line G,k),i ) )

proof end;

uniqueness
for b₁, b₂ being Go-board st len b₁ = len G & ( for k being Element of NAT st k in dom G holds
b₁ . k = Del (Line G,k),i ) & len b₂ = len G & ( for k being Element of NAT st k in dom G holds
b₂ . k = Del (Line G,k),i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines DelCol GOBOARD1:def 10 :

for G being Go-board
for i being Element of NAT st i in Seg (width G) & width G > 1 holds
for b₃ being Go-board holds
( b₃ = DelCol G,i iff ( len b₃ = len G & ( for k being Element of NAT st k in dom G holds
b₃ . k = Del (Line G,k),i ) ) );

theorem Th25: :: GOBOARD1:25

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

proof end;

theorem Th26: :: GOBOARD1:26

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

proof end;

theorem :: GOBOARD1:27

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

proof end;

theorem Th28: :: GOBOARD1:28

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

proof end;

theorem Th29: :: GOBOARD1:29

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) )

proof end;

theorem Th30: :: GOBOARD1:30

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) )

proof end;

theorem Th31: :: GOBOARD1:31

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) )

proof end;

theorem Th32: :: GOBOARD1:32

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) )

proof end;

theorem :: GOBOARD1:33

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) )

proof end;

theorem :: GOBOARD1:34

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) )

proof end;

theorem :: GOBOARD1:35

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))) )

proof end;

theorem Th36: :: GOBOARD1:36

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) )

proof end;

theorem :: GOBOARD1:37

for f being FinSequence of
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)

proof end;

definition

let D be set ;
let f be FinSequence of D;
let M be Matrix of ;
pred f is_sequence_on M means :Def11: :: GOBOARD1:def 11
( ( 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 Def11 defines is_sequence_on GOBOARD1:def 11 :

for D being set
for f being FinSequence of D
for M being Matrix of 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 holds <*> D is_sequence_on M

proof end;

theorem :: GOBOARD1:38

for m being Element of NAT
for D being set
for f being FinSequence of D
for M being Matrix of 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:39

for f1, f2 being FinSequence of
for D being set
for M being Matrix of 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 )

proof end;

theorem :: GOBOARD1:40

for f1, f2 being FinSequence of
for D being set
for M being Matrix of 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

proof end;

theorem :: GOBOARD1:41

for i being Element of NAT
for G being Go-board
for f being FinSequence of 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

proof end;

theorem Th42: :: GOBOARD1:42

for i being Element of 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 Element of NAT st
( n in dom G & f /. i in rng (Line G,n) )

proof end;

theorem Th43: :: GOBOARD1:43

for i, n being Element of 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 Element of NAT st f /. (i + 1) in rng (Line G,k) & k in dom G holds
abs (n - k) = 1

proof end;

theorem Th44: :: GOBOARD1:44

for i, m being Element of 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 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)) )

proof end;

theorem :: GOBOARD1:45

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 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 ) )

proof end;

theorem Th46: :: GOBOARD1:46

for i being Element of 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 Element of NAT st
( n in Seg (width G) & f /. i in rng (Col G,n) )

proof end;

theorem Th47: :: GOBOARD1:47

for i, n being Element of 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 (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

proof end;

theorem Th48: :: GOBOARD1:48

for i, m being Element of NAT
for G being Go-board
for f being FinSequence of 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)) )

proof end;

theorem Th49: :: GOBOARD1:49

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,(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 ) )

proof end;

theorem Th50: :: GOBOARD1:50

for k, n being Element of NAT
for G being Go-board
for f being FinSequence of 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

proof end;

theorem :: GOBOARD1:51

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)) & width G > 1 & 1 <= len f holds
ex g being FinSequence of 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 )

proof end;

theorem :: GOBOARD1:52

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,(width 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,(width G)) & 1 <= len g & g is_sequence_on G )

proof end;

theorem :: GOBOARD1:53

for k, n being Element of 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 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) ) ) )

proof end;