:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura

::

:: Received August 24, 1992

:: Copyright (c) 1992-2016 Association of Mizar Users

definition

let f be FinSequence of (TOP-REAL 2);

ex b_{1} being FinSequence of REAL st

( len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (f /. n) `1 ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (f /. n) `1 ) & len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = (f /. n) `1 ) holds

b_{1} = b_{2}

ex b_{1} being FinSequence of REAL st

( len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (f /. n) `2 ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (f /. n) `2 ) & len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = (f /. n) `2 ) holds

b_{1} = b_{2}

end;
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 ( len it = len f & ( for n being Nat st n in dom it holds

it . n = (f /. n) `1 ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

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 ( len it = len f & ( for n being Nat st n in dom it holds

it . n = (f /. n) `2 ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines X_axis GOBOARD1:def 1 :

for f being FinSequence of (TOP-REAL 2)

for b_{2} being FinSequence of REAL holds

( b_{2} = X_axis f iff ( len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = (f /. n) `1 ) ) );

for f being FinSequence of (TOP-REAL 2)

for b

( b

b

:: deftheorem Def2 defines Y_axis GOBOARD1:def 2 :

for f being FinSequence of (TOP-REAL 2)

for b_{2} being FinSequence of REAL holds

( b_{2} = Y_axis f iff ( len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = (f /. n) `2 ) ) );

for f being FinSequence of (TOP-REAL 2)

for b

( b

b

theorem Th1: :: GOBOARD1:1

for f being FinSequence of (TOP-REAL 2)

for i being Nat st i in dom f & 2 <= len f holds

f /. i in L~ f

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 (TOP-REAL 2);

end;
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 ;

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 (width M) holds

Y_axis (Col (M,n)) is constant ;

for n being Nat st n in Seg (width M) 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 ;

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 (width M) holds

X_axis (Col (M,n)) is increasing ;

for n being Nat st n in Seg (width M) holds

X_axis (Col (M,n)) is increasing ;

:: deftheorem Def3 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 Nat st n in dom M holds

X_axis (Line (M,n)) is constant );

for M being Matrix of (TOP-REAL 2) 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 (TOP-REAL 2) holds

( M is Y_equal-in-column iff for n being Nat st n in Seg (width M) holds

Y_axis (Col (M,n)) is constant );

for M being Matrix of (TOP-REAL 2) holds

( M is Y_equal-in-column iff for n being Nat st n in Seg (width M) holds

Y_axis (Col (M,n)) is constant );

:: deftheorem Def5 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 Nat st n in dom M holds

Y_axis (Line (M,n)) is increasing );

for M being Matrix of (TOP-REAL 2) 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 (TOP-REAL 2) holds

( M is X_increasing-in-column iff for n being Nat st n in Seg (width M) holds

X_axis (Col (M,n)) is increasing );

for M being Matrix of (TOP-REAL 2) holds

( M is X_increasing-in-column iff for n being Nat st n in Seg (width M) holds

X_axis (Col (M,n)) is increasing );

registration

ex b_{1} being Matrix of (TOP-REAL 2) st

( b_{1} is V3() & b_{1} is X_equal-in-line & b_{1} is Y_equal-in-column & b_{1} is Y_increasing-in-line & b_{1} is X_increasing-in-column )
end;

cluster Relation-like V3() NAT -defined K227( the U1 of (TOP-REAL 2)) -valued Function-like V41() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column for FinSequence of K227( the U1 of (TOP-REAL 2));

existence ex b

( b

proof end;

::$CT

theorem Th2: :: 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 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

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 (TOP-REAL 2)

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 (width M) & m in Seg (width M) holds

n = m

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 (width M) & m in Seg (width M) holds

n = m

proof end;

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

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;

::$CT 3

registration

let G be Go-board;

let i be Nat;

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

end;
let i be Nat;

cluster DelCol (G,i) -> X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;

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;

::$CT 3

theorem :: GOBOARD1:12

theorem :: GOBOARD1:14

theorem :: GOBOARD1:17

theorem :: GOBOARD1:18

theorem :: GOBOARD1:19

theorem :: GOBOARD1:21

definition

let D be set ;

let f be FinSequence of D;

let M be Matrix of D;

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

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

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

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

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 (TOP-REAL 2)

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

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 (TOP-REAL 2)

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

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

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)

proof end;

theorem Th19: :: GOBOARD1:26

for i being 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 Nat st

( n in dom G & f /. i in rng (Line (G,n)) )

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 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 (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 Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1

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

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

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 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 (TOP-REAL 2) st f is_sequence_on G & i in dom f holds

ex n being Nat st

( n in Seg (width G) & f /. i in rng (Col (G,n)) )

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 Nat st

( n in Seg (width G) & 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 (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 Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds

|.(n - k).| = 1

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 Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) 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 (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 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))) )

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

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 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 (TOP-REAL 2) st k in Seg (width G) & 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 (width G) & f /. i in rng (Col (G,m)) holds

m <= k

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 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 (width G) & 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 (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 )

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 )

proof end;

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 )

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 )

proof end;

theorem :: GOBOARD1:37

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

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