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