begin
theorem Th17:
for
i1,
j1,
i2,
j2 being
Element of
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)
theorem Th18:
for
i1,
j1,
i2,
j2 being
Element of
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)
theorem Th19:
for
i1,
j1,
i2,
j2 being
Element of
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))
Lm1:
for i, j being Element of 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 Element of NAT st
( k in dom f & (f /. k) `1 = ((GoB f) * (i,j)) `1 )
Lm2:
for i, j being Element of 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 Element of NAT st
( k in dom f & (f /. k) `2 = ((GoB f) * (i,j)) `2 )
definition
canceled;let f be
FinSequence of
(TOP-REAL 2);
let G be
Go-board;
let k be
Element of
NAT ;
assume
( 1
<= k &
k + 1
<= len f &
f is_sequence_on G )
;
then consider i1,
j1,
i2,
j2 being
Element of
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 :
Def2:
for
i1,
j1,
i2,
j2 being
Element of
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
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,(i1 -' 1),j2) )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Element of 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 & b2 = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell (G,i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell (G,(i1 -' 1),j2) ) ) holds
b1 = b2
func left_cell (
f,
k,
G)
-> Subset of
(TOP-REAL 2) means :
Def3:
for
i1,
j1,
i2,
j2 being
Element of
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
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,i1,j2) )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,i1,j2) ) ) & ( for i1, j1, i2, j2 being Element of 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 & b2 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell (G,i1,j2) ) ) holds
b1 = b2
end;
::
deftheorem Def2 defines
right_cell GOBRD13:def 2 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = right_cell (f,k,G) iff for i1, j1, i2, j2 being Element of 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 & b4 = cell (G,i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell (G,i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell (G,i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell (G,(i1 -' 1),j2) ) );
::
deftheorem Def3 defines
left_cell GOBRD13:def 3 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = left_cell (f,k,G) iff for i1, j1, i2, j2 being Element of 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 & b4 = cell (G,(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell (G,i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell (G,i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell (G,i1,j2) ) );
theorem Th21:
for
k,
i,
j being
Element of
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)
theorem Th22:
for
k,
i,
j being
Element of
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)
theorem Th23:
for
k,
i,
j being
Element of
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)
theorem Th24:
for
k,
i,
j being
Element of
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))
theorem Th25:
for
k,
i,
j being
Element of
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))
theorem Th26:
for
k,
i,
j being
Element of
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)
theorem Th27:
for
k,
i,
j being
Element of
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)
theorem Th28:
for
k,
i,
j being
Element of
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)
definition
let f be
FinSequence of
(TOP-REAL 2);
let G be
Go-board;
let k be
Element of
NAT ;
assume
( 1
<= k &
k + 1
<= len f &
f is_sequence_on G )
;
then consider i1,
j1,
i2,
j2 being
Element of
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 :
Def4:
for
i1,
j1,
i2,
j2 being
Element of
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
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,(i2 -' 1),j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,(i2 -' 1),(j2 -' 1)) )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,(i2 -' 1),j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,(i2 -' 1),(j2 -' 1)) ) ) & ( for i1, j1, i2, j2 being Element of 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 & b2 = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell (G,(i2 -' 1),j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell (G,(i2 -' 1),(j2 -' 1)) ) ) holds
b1 = b2
func front_left_cell (
f,
k,
G)
-> Subset of
(TOP-REAL 2) means :
Def5:
for
i1,
j1,
i2,
j2 being
Element of
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
ex b1 being Subset of (TOP-REAL 2) st
for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,i2,(j2 -' 1)) )
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for i1, j1, i2, j2 being Element of 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 & b1 = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b1 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b1 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b1 = cell (G,i2,(j2 -' 1)) ) ) & ( for i1, j1, i2, j2 being Element of 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 & b2 = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b2 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b2 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b2 = cell (G,i2,(j2 -' 1)) ) ) holds
b1 = b2
end;
::
deftheorem Def4 defines
front_right_cell GOBRD13:def 4 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = front_right_cell (f,k,G) iff for i1, j1, i2, j2 being Element of 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 & b4 = cell (G,i2,j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell (G,i2,(j2 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell (G,(i2 -' 1),j2) ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell (G,(i2 -' 1),(j2 -' 1)) ) );
::
deftheorem Def5 defines
front_left_cell GOBRD13:def 5 :
for f being FinSequence of (TOP-REAL 2)
for G being Go-board
for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
for b4 being Subset of (TOP-REAL 2) holds
( b4 = front_left_cell (f,k,G) iff for i1, j1, i2, j2 being Element of 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 & b4 = cell (G,(i2 -' 1),j2) ) & not ( i1 + 1 = i2 & j1 = j2 & b4 = cell (G,i2,j2) ) & not ( i1 = i2 + 1 & j1 = j2 & b4 = cell (G,(i2 -' 1),(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & b4 = cell (G,i2,(j2 -' 1)) ) );
theorem
for
k,
i,
j being
Element of
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))
theorem
for
k,
i,
j being
Element of
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))
theorem
for
k,
i,
j being
Element of
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)
theorem
for
k,
i,
j being
Element of
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))
theorem
for
k,
i,
j being
Element of
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))
theorem
for
k,
i,
j being
Element of
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)
theorem
for
k,
i,
j being
Element of
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))
theorem
for
k,
i,
j being
Element of
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))
definition
let D be
set ;
let f be
FinSequence of
D;
let G be
Matrix of
D;
let k be
Element of
NAT ;
pred f turns_right k,
G means :
Def6:
for
i1,
j1,
i2,
j2 being
Element of
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 :
Def7:
for
i1,
j1,
i2,
j2 being
Element of
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 :
Def8:
for
i1,
j1,
i2,
j2 being
Element of
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)) );
end;
::
deftheorem Def6 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 Element of NAT holds
( f turns_right k,G iff for i1, j1, i2, j2 being Element of 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 Def7 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 Element of NAT holds
( f turns_left k,G iff for i1, j1, i2, j2 being Element of 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 Def8 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 Element of NAT holds
( f goes_straight k,G iff for i1, j1, i2, j2 being Element of 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)) ) );