let k, n be Element of NAT ; :: thesis: 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 )
let f be FinSequence of (TOP-REAL 2); :: thesis: 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 )
let G be Go-board; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G & k + 1 <= n implies ( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G ) )
assume that
A1:
( 1 <= k & k + 1 <= len f )
and
A2:
f is_sequence_on G
and
A3:
k + 1 <= n
; :: thesis: ( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G )
per cases
( len f <= n or n < len f )
;
suppose A4:
n < len f
;
:: thesis: ( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G )consider i1,
j1,
i2,
j2 being
Element of
NAT such that A5:
(
[i1,j1] in Indices G &
f /. k = G * i1,
j1 )
and A6:
(
[i2,j2] in Indices G &
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, A2, JORDAN8:6;
A8:
(
i1 + 1
> i1 &
i2 + 1
> i2 &
j1 + 1
> j1 &
j2 + 1
> j2 )
by NAT_1:13;
set lf =
left_cell f,
k,
G;
set lfn =
left_cell (f | n),
k,
G;
set rf =
right_cell f,
k,
G;
set rfn =
right_cell (f | n),
k,
G;
A9:
f | n is_sequence_on G
by A2, GOBOARD1:38;
A10:
len (f | n) = n
by A4, FINSEQ_1:80;
then
(
k in dom (f | n) &
k + 1
in dom (f | n) )
by A1, A3, GOBOARD2:3;
then A11:
(
(f | n) /. k = f /. k &
(f | n) /. (k + 1) = f /. (k + 1) )
by FINSEQ_4:85;
now 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 A12:
(
i1 = i2 &
j1 + 1
= j2 )
;
:: thesis: ( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G )hence left_cell f,
k,
G =
cell G,
(i1 -' 1),
j1
by A1, A2, A5, A6, A8, Def3
.=
left_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A12, Def3
;
:: thesis: right_cell f,k,G = right_cell (f | n),k,Gthus right_cell f,
k,
G =
cell G,
i1,
j1
by A1, A2, A5, A6, A8, A12, Def2
.=
right_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A12, Def2
;
:: thesis: verum end; suppose A13:
(
i1 + 1
= i2 &
j1 = j2 )
;
:: thesis: ( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G )hence left_cell f,
k,
G =
cell G,
i1,
j1
by A1, A2, A5, A6, A8, Def3
.=
left_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A13, Def3
;
:: thesis: right_cell f,k,G = right_cell (f | n),k,Gthus right_cell f,
k,
G =
cell G,
i1,
(j1 -' 1)
by A1, A2, A5, A6, A8, A13, Def2
.=
right_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A13, Def2
;
:: thesis: verum end; suppose A14:
(
i1 = i2 + 1 &
j1 = j2 )
;
:: thesis: ( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G )hence left_cell f,
k,
G =
cell G,
i2,
(j2 -' 1)
by A1, A2, A5, A6, A8, Def3
.=
left_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A14, Def3
;
:: thesis: right_cell f,k,G = right_cell (f | n),k,Gthus right_cell f,
k,
G =
cell G,
i2,
j2
by A1, A2, A5, A6, A8, A14, Def2
.=
right_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A14, Def2
;
:: thesis: verum end; suppose A15:
(
i1 = i2 &
j1 = j2 + 1 )
;
:: thesis: ( left_cell f,k,G = left_cell (f | n),k,G & right_cell f,k,G = right_cell (f | n),k,G )hence left_cell f,
k,
G =
cell G,
i1,
j2
by A1, A2, A5, A6, A8, Def3
.=
left_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A15, Def3
;
:: thesis: right_cell f,k,G = right_cell (f | n),k,Gthus right_cell f,
k,
G =
cell G,
(i1 -' 1),
j2
by A1, A2, A5, A6, A8, A15, Def2
.=
right_cell (f | n),
k,
G
by A1, A3, A5, A6, A8, A9, A10, A11, A15, Def2
;
:: thesis: verum end; hence
(
left_cell f,
k,
G = left_cell (f | n),
k,
G &
right_cell f,
k,
G = right_cell (f | n),
k,
G )
;
:: thesis: verum end;