let G be Go-board; for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )
let f be FinSequence of (TOP-REAL 2); ( f is_sequence_on G implies for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) )
assume A1:
f is_sequence_on G
; for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )
let k be Nat; ( 1 <= k & k + 1 <= len f implies ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) )
assume A2:
( 1 <= k & k + 1 <= len f )
; ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )
then consider i1, j1, i2, j2 being Nat such that
A3:
[i1,j1] in Indices G
and
A4:
f /. k = G * (i1,j1)
and
A5:
[i2,j2] in Indices G
and
A6:
f /. (k + 1) = G * (i2,j2)
and
A7:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A1, JORDAN8:3;
A8:
i2 <= len G
by A5, MATRIX_0:32;
A9:
i1 <= len G
by A3, MATRIX_0:32;
then A10:
i1 -' 1 <= len G
by NAT_D:44;
A11:
j2 <= width G
by A5, MATRIX_0:32;
then A12:
j2 -' 1 <= width G
by NAT_D:44;
A13:
( j1 + 1 > j1 & j2 + 1 > j2 )
by NAT_1:13;
A14:
j1 <= width G
by A3, MATRIX_0:32;
then A15:
j1 -' 1 <= width G
by NAT_D:44;
A16:
( i1 + 1 > i1 & i2 + 1 > i2 )
by NAT_1:13;
per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A7;
suppose
(
i1 = i2 &
j1 + 1
= j2 )
;
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )then
(
right_cell (
f,
k,
G)
= cell (
G,
i1,
j1) &
left_cell (
f,
k,
G)
= cell (
G,
(i1 -' 1),
j1) )
by A1, A3, A4, A5, A6, A13, GOBRD13:def 2, GOBRD13:def 3, A2;
hence
(
Int (left_cell (f,k,G)) <> {} &
Int (right_cell (f,k,G)) <> {} )
by A9, A14, A10, GOBOARD9:14;
verum end; suppose
(
i1 + 1
= i2 &
j1 = j2 )
;
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )then
(
right_cell (
f,
k,
G)
= cell (
G,
i1,
(j1 -' 1)) &
left_cell (
f,
k,
G)
= cell (
G,
i1,
j1) )
by A1, A3, A4, A5, A6, A16, GOBRD13:def 2, GOBRD13:def 3, A2;
hence
(
Int (left_cell (f,k,G)) <> {} &
Int (right_cell (f,k,G)) <> {} )
by A9, A14, A15, GOBOARD9:14;
verum end; suppose
(
i1 = i2 + 1 &
j1 = j2 )
;
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )then
(
right_cell (
f,
k,
G)
= cell (
G,
i2,
j2) &
left_cell (
f,
k,
G)
= cell (
G,
i2,
(j2 -' 1)) )
by A1, A3, A4, A5, A6, A16, GOBRD13:def 2, GOBRD13:def 3, A2;
hence
(
Int (left_cell (f,k,G)) <> {} &
Int (right_cell (f,k,G)) <> {} )
by A8, A11, A12, GOBOARD9:14;
verum end; suppose
(
i1 = i2 &
j1 = j2 + 1 )
;
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )then
(
right_cell (
f,
k,
G)
= cell (
G,
(i1 -' 1),
j2) &
left_cell (
f,
k,
G)
= cell (
G,
i1,
j2) )
by A1, A3, A4, A5, A6, A13, GOBRD13:def 2, GOBRD13:def 3, A2;
hence
(
Int (left_cell (f,k,G)) <> {} &
Int (right_cell (f,k,G)) <> {} )
by A9, A11, A10, GOBOARD9:14;
verum end;