:: by Czes{\l}aw Byli\'nski

::

:: Received April 23, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

::$CT 7

theorem :: GOBRD13:8

for f being FinSequence of (TOP-REAL 2)

for G being Matrix of (TOP-REAL 2) st f is_sequence_on G holds

rng f c= Values G

for G being Matrix of (TOP-REAL 2) st f is_sequence_on G holds

rng f c= Values G

proof end;

theorem Th2: :: GOBRD13:9

for i1, j1, j2 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (1,j2) holds

i1 = 1

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (1,j2) holds

i1 = 1

proof end;

theorem Th3: :: GOBRD13:10

for i1, j1, j2 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * ((len G2),j2) holds

i1 = len G1

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * ((len G2),j2) holds

i1 = len G1

proof end;

theorem Th4: :: GOBRD13:11

for i1, i2, j1 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * (i1,j1) = G2 * (i2,1) holds

j1 = 1

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * (i1,j1) = G2 * (i2,1) holds

j1 = 1

proof end;

theorem Th5: :: GOBRD13:12

for i1, i2, j1 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * (i1,j1) = G2 * (i2,(width G2)) holds

j1 = width G1

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 & G1 * (i1,j1) = G2 * (i2,(width G2)) holds

j1 = width G1

proof end;

theorem Th6: :: GOBRD13:13

for i1, i2, j1, j2 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 < len G1 & 1 <= j1 & j1 <= width G1 & 1 <= i2 & i2 < len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1

for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 < len G1 & 1 <= j1 & j1 <= width G1 & 1 <= i2 & i2 < len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1

proof end;

theorem Th7: :: GOBRD13:14

for i1, i2, j1, j2 being Nat

for G1, G2 being Go-board st G1 * ((i1 -' 1),j1) in Values G2 & 1 < i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 & 1 < i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G1 * ((i1 -' 1),j1)) `1 <= (G2 * ((i2 -' 1),j2)) `1

for G1, G2 being Go-board st G1 * ((i1 -' 1),j1) in Values G2 & 1 < i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 & 1 < i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G1 * ((i1 -' 1),j1)) `1 <= (G2 * ((i2 -' 1),j2)) `1

proof end;

theorem Th8: :: GOBRD13:15

for i1, i2, j1, j2 being Nat

for G1, G2 being Go-board st G1 * (i1,(j1 + 1)) in Values G2 & 1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 < width G1 & 1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 < width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G2 * (i2,(j2 + 1))) `2 <= (G1 * (i1,(j1 + 1))) `2

for G1, G2 being Go-board st G1 * (i1,(j1 + 1)) in Values G2 & 1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 < width G1 & 1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 < width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G2 * (i2,(j2 + 1))) `2 <= (G1 * (i1,(j1 + 1))) `2

proof end;

theorem Th9: :: GOBRD13:16

for i1, i2, j1, j2 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 <= len G1 & 1 < j1 & j1 <= width G1 & 1 <= i2 & i2 <= len G2 & 1 < j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G1 * (i1,(j1 -' 1))) `2 <= (G2 * (i2,(j2 -' 1))) `2

for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 <= len G1 & 1 < j1 & j1 <= width G1 & 1 <= i2 & i2 <= len G2 & 1 < j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G1 * (i1,(j1 -' 1))) `2 <= (G2 * (i2,(j2 -' 1))) `2

proof end;

theorem Th10: :: GOBRD13:17

for i1, i2, j1, j2 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

cell (G2,i2,j2) c= cell (G1,i1,j1)

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

cell (G2,i2,j2) c= cell (G1,i1,j1)

proof end;

theorem Th11: :: GOBRD13:18

for i1, i2, j1, j2 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

cell (G2,(i2 -' 1),j2) c= cell (G1,(i1 -' 1),j1)

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

cell (G2,(i2 -' 1),j2) c= cell (G1,(i1 -' 1),j1)

proof end;

theorem Th12: :: GOBRD13:19

for i1, i2, j1, j2 being Nat

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

cell (G2,i2,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1))

for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

cell (G2,i2,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1))

proof end;

Lm1: for i, j being Nat

for f being non empty FinSequence of (TOP-REAL 2) st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds

ex k being Nat st

( k in dom f & (f /. k) `1 = ((GoB f) * (i,j)) `1 )

proof end;

Lm2: for i, j being Nat

for f being non empty FinSequence of (TOP-REAL 2) st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds

ex k being Nat st

( k in dom f & (f /. k) `2 = ((GoB f) * (i,j)) `2 )

proof end;

theorem Th13: :: GOBRD13:20

for G being Go-board

for f being standard special_circular_sequence st f is_sequence_on G holds

Values (GoB f) c= Values G

for f being standard special_circular_sequence st f is_sequence_on G holds

Values (GoB f) c= Values G

proof end;

definition

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

let G be Go-board;

let k be Nat;

assume ( 1 <= k & k + 1 <= len f & f is_sequence_on G ) ;

then consider i1, j1, i2, j2 being Nat such that

A1: ( [i1,j1] in Indices G & f /. k = G * (i1,j1) ) and

A2: ( [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) ) and

A3: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by JORDAN8:3;

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

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i1 -' 1),j2) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{2} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{2} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{2} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{2} = cell (G,(i1 -' 1),j2) ) ) holds

b_{1} = b_{2}

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

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,i1,j2) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,i1,j2) ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{2} = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{2} = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{2} = cell (G,i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{2} = cell (G,i1,j2) ) ) holds

b_{1} = b_{2}

end;
let G be Go-board;

let k be Nat;

assume ( 1 <= k & k + 1 <= len f & f is_sequence_on G ) ;

then consider i1, j1, i2, j2 being Nat such that

A1: ( [i1,j1] in Indices G & f /. k = G * (i1,j1) ) and

A2: ( [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) ) and

A3: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by JORDAN8:3;

func right_cell (f,k,G) -> Subset of (TOP-REAL 2) means :Def1: :: GOBRD13:def 2

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,(i1 -' 1),j2) );

existence for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,(i1 -' 1),j2) );

ex b

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

proof end;

uniqueness for b

( i1 = i2 & j1 = j2 + 1 & b

( i1 = i2 & j1 = j2 + 1 & b

b

proof end;

func left_cell (f,k,G) -> Subset of (TOP-REAL 2) means :Def2: :: GOBRD13:def 3

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,i1,j2) );

existence for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,i1,j2) );

ex b

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

proof end;

uniqueness for b

( i1 = i2 & j1 = j2 + 1 & b

( i1 = i2 & j1 = j2 + 1 & b

b

proof end;

:: deftheorem Def1 defines right_cell GOBRD13:def 2 :

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b_{4} being Subset of (TOP-REAL 2) holds

( b_{4} = right_cell (f,k,G) iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{4} = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{4} = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{4} = cell (G,i2,j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{4} = cell (G,(i1 -' 1),j2) ) );

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b

( b

( i1 = i2 & j1 = j2 + 1 & b

:: deftheorem Def2 defines left_cell GOBRD13:def 3 :

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b_{4} being Subset of (TOP-REAL 2) holds

( b_{4} = left_cell (f,k,G) iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{4} = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{4} = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{4} = cell (G,i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{4} = cell (G,i1,j2) ) );

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b

( b

( i1 = i2 & j1 = j2 + 1 & b

theorem Th14: :: GOBRD13:21

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

left_cell (f,k,G) = cell (G,(i -' 1),j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

left_cell (f,k,G) = cell (G,(i -' 1),j)

proof end;

theorem Th15: :: GOBRD13:22

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

right_cell (f,k,G) = cell (G,i,j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

right_cell (f,k,G) = cell (G,i,j)

proof end;

theorem Th16: :: GOBRD13:23

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

left_cell (f,k,G) = cell (G,i,j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

left_cell (f,k,G) = cell (G,i,j)

proof end;

theorem Th17: :: GOBRD13:24

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

right_cell (f,k,G) = cell (G,i,(j -' 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

right_cell (f,k,G) = cell (G,i,(j -' 1))

proof end;

theorem Th18: :: GOBRD13:25

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

left_cell (f,k,G) = cell (G,i,(j -' 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

left_cell (f,k,G) = cell (G,i,(j -' 1))

proof end;

theorem Th19: :: GOBRD13:26

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

right_cell (f,k,G) = cell (G,i,j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

right_cell (f,k,G) = cell (G,i,j)

proof end;

theorem Th20: :: GOBRD13:27

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

left_cell (f,k,G) = cell (G,i,j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

left_cell (f,k,G) = cell (G,i,j)

proof end;

theorem Th21: :: GOBRD13:28

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

right_cell (f,k,G) = cell (G,(i -' 1),j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

right_cell (f,k,G) = cell (G,(i -' 1),j)

proof end;

theorem :: GOBRD13:29

for k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)

proof end;

theorem :: GOBRD13:30

for k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

right_cell (f,k,G) is closed

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

right_cell (f,k,G) is closed

proof end;

theorem :: GOBRD13:31

for k, n being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n holds

( left_cell (f,k,G) = left_cell ((f | n),k,G) & right_cell (f,k,G) = right_cell ((f | n),k,G) )

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n holds

( left_cell (f,k,G) = left_cell ((f | n),k,G) & right_cell (f,k,G) = right_cell ((f | n),k,G) )

proof end;

theorem :: GOBRD13:32

for k, n being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G holds

( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len (f /^ n) & n <= len f & f is_sequence_on G holds

( left_cell (f,(k + n),G) = left_cell ((f /^ n),k,G) & right_cell (f,(k + n),G) = right_cell ((f /^ n),k,G) )

proof end;

theorem :: GOBRD13:33

for n being Nat

for G being Go-board

for f being standard special_circular_sequence st 1 <= n & n + 1 <= len f & f is_sequence_on G holds

( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )

for G being Go-board

for f being standard special_circular_sequence st 1 <= n & n + 1 <= len f & f is_sequence_on G holds

( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )

proof end;

definition

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

let G be Go-board;

let k be Nat;

assume ( 1 <= k & k + 1 <= len f & f is_sequence_on G ) ;

then consider i1, j1, i2, j2 being Nat such that

A1: ( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) ) and

A2: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by JORDAN8:3;

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

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,(i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i2 -' 1),(j2 -' 1)) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,(i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,(i2 -' 1),(j2 -' 1)) ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{2} = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{2} = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{2} = cell (G,(i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{2} = cell (G,(i2 -' 1),(j2 -' 1)) ) ) holds

b_{1} = b_{2}

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

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,(i2 -' 1),(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,i2,(j2 -' 1)) )

for b_{1}, b_{2} being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{1} = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{1} = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{1} = cell (G,(i2 -' 1),(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{1} = cell (G,i2,(j2 -' 1)) ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{2} = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{2} = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{2} = cell (G,(i2 -' 1),(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{2} = cell (G,i2,(j2 -' 1)) ) ) holds

b_{1} = b_{2}

end;
let G be Go-board;

let k be Nat;

assume ( 1 <= k & k + 1 <= len f & f is_sequence_on G ) ;

then consider i1, j1, i2, j2 being Nat such that

A1: ( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) ) and

A2: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by JORDAN8:3;

func front_right_cell (f,k,G) -> Subset of (TOP-REAL 2) means :Def3: :: GOBRD13:def 4

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,(i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,(i2 -' 1),(j2 -' 1)) );

existence for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,(i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,(i2 -' 1),(j2 -' 1)) );

ex b

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

proof end;

uniqueness for b

( i1 = i2 & j1 = j2 + 1 & b

( i1 = i2 & j1 = j2 + 1 & b

b

proof end;

func front_left_cell (f,k,G) -> Subset of (TOP-REAL 2) means :Def4: :: GOBRD13:def 5

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,(i2 -' 1),(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,i2,(j2 -' 1)) );

existence for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & it = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & it = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & it = cell (G,(i2 -' 1),(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & it = cell (G,i2,(j2 -' 1)) );

ex b

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b

( i1 = i2 & j1 = j2 + 1 & b

proof end;

uniqueness for b

( i1 = i2 & j1 = j2 + 1 & b

( i1 = i2 & j1 = j2 + 1 & b

b

proof end;

:: deftheorem Def3 defines front_right_cell GOBRD13:def 4 :

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b_{4} being Subset of (TOP-REAL 2) holds

( b_{4} = front_right_cell (f,k,G) iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{4} = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{4} = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{4} = cell (G,(i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{4} = cell (G,(i2 -' 1),(j2 -' 1)) ) );

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b

( b

( i1 = i2 & j1 = j2 + 1 & b

:: deftheorem Def4 defines front_left_cell GOBRD13:def 5 :

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b_{4} being Subset of (TOP-REAL 2) holds

( b_{4} = front_left_cell (f,k,G) iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & b_{4} = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b_{4} = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b_{4} = cell (G,(i2 -' 1),(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & b_{4} = cell (G,i2,(j2 -' 1)) ) );

for f being FinSequence of (TOP-REAL 2)

for G being Go-board

for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

for b

( b

( i1 = i2 & j1 = j2 + 1 & b

theorem :: GOBRD13:34

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

front_left_cell (f,k,G) = cell (G,(i -' 1),(j + 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

front_left_cell (f,k,G) = cell (G,(i -' 1),(j + 1))

proof end;

theorem :: GOBRD13:35

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

front_right_cell (f,k,G) = cell (G,i,(j + 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds

front_right_cell (f,k,G) = cell (G,i,(j + 1))

proof end;

theorem :: GOBRD13:36

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

front_left_cell (f,k,G) = cell (G,(i + 1),j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

front_left_cell (f,k,G) = cell (G,(i + 1),j)

proof end;

theorem :: GOBRD13:37

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

front_right_cell (f,k,G) = cell (G,(i + 1),(j -' 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds

front_right_cell (f,k,G) = cell (G,(i + 1),(j -' 1))

proof end;

theorem :: GOBRD13:38

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

front_left_cell (f,k,G) = cell (G,(i -' 1),(j -' 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

front_left_cell (f,k,G) = cell (G,(i -' 1),(j -' 1))

proof end;

theorem :: GOBRD13:39

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

front_right_cell (f,k,G) = cell (G,(i -' 1),j)

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds

front_right_cell (f,k,G) = cell (G,(i -' 1),j)

proof end;

theorem :: GOBRD13:40

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

front_left_cell (f,k,G) = cell (G,i,(j -' 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

front_left_cell (f,k,G) = cell (G,i,(j -' 1))

proof end;

theorem :: GOBRD13:41

for i, j, k being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

front_right_cell (f,k,G) = cell (G,(i -' 1),(j -' 1))

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

front_right_cell (f,k,G) = cell (G,(i -' 1),(j -' 1))

proof end;

theorem :: GOBRD13:42

for k, n being Nat

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n holds

( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n holds

( front_left_cell (f,k,G) = front_left_cell ((f | n),k,G) & front_right_cell (f,k,G) = front_right_cell ((f | n),k,G) )

proof end;

definition

let D be set ;

let f be FinSequence of D;

let G be Matrix of D;

let k be Nat;

end;
let f be FinSequence of D;

let G be Matrix of D;

let k be Nat;

pred f turns_right k,G means :: GOBRD13:def 6

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) );

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) );

pred f turns_left k,G means :: GOBRD13:def 7

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) );

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) );

pred f goes_straight k,G means :: GOBRD13:def 8

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) );

for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) );

:: deftheorem defines turns_right GOBRD13:def 6 :

for D being set

for f being FinSequence of D

for G being Matrix of D

for k being Nat holds

( f turns_right k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) );

for D being set

for f being FinSequence of D

for G being Matrix of D

for k being Nat holds

( f turns_right k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) );

:: deftheorem defines turns_left GOBRD13:def 7 :

for D being set

for f being FinSequence of D

for G being Matrix of D

for k being Nat holds

( f turns_left k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) );

for D being set

for f being FinSequence of D

for G being Matrix of D

for k being Nat holds

( f turns_left k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) holds

( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) );

:: deftheorem defines goes_straight GOBRD13:def 8 :

for D being set

for f being FinSequence of D

for G being Matrix of D

for k being Nat holds

( f goes_straight k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) );

for D being set

for f being FinSequence of D

for G being Matrix of D

for k being Nat holds

( f goes_straight k,G iff for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 + 1)) ) & not ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices G & f /. (k + 2) = G * ((i2 + 1),j2) ) & not ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices G & f /. (k + 2) = G * ((i2 -' 1),j2) ) holds

( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices G & f /. (k + 2) = G * (i2,(j2 -' 1)) ) );

theorem :: GOBRD13:43

for k, n being Nat

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_right k,G holds

f turns_right k,G

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_right k,G holds

f turns_right k,G

proof end;

theorem :: GOBRD13:44

for k, n being Nat

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_left k,G holds

f turns_left k,G

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_left k,G holds

f turns_left k,G

proof end;

theorem :: GOBRD13:45

for k, n being Nat

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 2 <= n & f | n goes_straight k,G holds

f goes_straight k,G

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 2 <= n & f | n goes_straight k,G holds

f goes_straight k,G

proof end;

theorem :: GOBRD13:46

for k being Nat

for D being set

for f1, f2 being FinSequence of D

for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_right k -' 1,G & f2 turns_right k -' 1,G holds

f1 | (k + 1) = f2 | (k + 1)

for D being set

for f1, f2 being FinSequence of D

for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_right k -' 1,G & f2 turns_right k -' 1,G holds

f1 | (k + 1) = f2 | (k + 1)

proof end;

theorem :: GOBRD13:47

for k being Nat

for D being set

for f1, f2 being FinSequence of D

for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_left k -' 1,G & f2 turns_left k -' 1,G holds

f1 | (k + 1) = f2 | (k + 1)

for D being set

for f1, f2 being FinSequence of D

for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 turns_left k -' 1,G & f2 turns_left k -' 1,G holds

f1 | (k + 1) = f2 | (k + 1)

proof end;

theorem :: GOBRD13:48

for k being Nat

for D being set

for f1, f2 being FinSequence of D

for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 goes_straight k -' 1,G & f2 goes_straight k -' 1,G holds

f1 | (k + 1) = f2 | (k + 1)

for D being set

for f1, f2 being FinSequence of D

for G being Matrix of D st 1 < k & k + 1 <= len f1 & k + 1 <= len f2 & f1 is_sequence_on G & f1 | k = f2 | k & f1 goes_straight k -' 1,G & f2 goes_straight k -' 1,G holds

f1 | (k + 1) = f2 | (k + 1)

proof end;