let k be 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)
let f be 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)
let G be Go-board; ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies (left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k) )
assume that
A1:
1 <= k
and
A2:
k + 1 <= len f
and
A3:
f is_sequence_on G
; (left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)
k + 1 >= 1
by NAT_1:11;
then A4:
k + 1 in dom f
by A2, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A5:
[i2,j2] in Indices G
and
A6:
f /. (k + 1) = G * (i2,j2)
by A3, GOBOARD1:def 9;
A7:
1 <= j2
by A5, MATRIX_0:32;
A8:
i2 <= len G
by A5, MATRIX_0:32;
A9:
1 <= i2
by A5, MATRIX_0:32;
A10:
j2 <= width G
by A5, MATRIX_0:32;
k <= k + 1
by NAT_1:11;
then
k <= len f
by A2, XXREAL_0:2;
then A11:
k in dom f
by A1, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A12:
[i1,j1] in Indices G
and
A13:
f /. k = G * (i1,j1)
by A3, GOBOARD1:def 9;
A14:
0 + 1 <= j1
by A12, MATRIX_0:32;
then
j1 > 0
;
then consider j being Nat such that
A15:
j + 1 = j1
by NAT_1:6;
A16:
|.(i1 - i2).| + |.(j1 - j2).| = 1
by A3, A11, A12, A13, A4, A5, A6, GOBOARD1:def 9;
A17:
now ( ( |.(i1 - i2).| = 1 & j1 = j2 & ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 ) or ( i1 = i2 & |.(j1 - j2).| = 1 & ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 ) )end;
A22:
j1 -' 1 = j
by A15, NAT_D:34;
A23:
j1 <= width G
by A12, MATRIX_0:32;
then A24:
j < width G
by A15, NAT_1:13;
A25:
0 + 1 <= i1
by A12, MATRIX_0:32;
then
i1 > 0
;
then consider i being Nat such that
A26:
i + 1 = i1
by NAT_1:6;
A27:
i1 <= len G
by A12, MATRIX_0:32;
then A28:
i < len G
by A26, NAT_1:13;
A29:
i1 -' 1 = i
by A26, NAT_D:34;
reconsider i = i, j = j as Nat ;
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 A17;
suppose A30:
(
i1 = i2 &
j1 + 1
= j2 )
;
(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)then A31:
right_cell (
f,
k,
G)
= cell (
G,
i1,
j1)
by A1, A2, A3, A12, A13, A5, A6, Th15;
(
j1 < width G &
left_cell (
f,
k,
G)
= cell (
G,
i,
j1) )
by A1, A2, A3, A12, A13, A5, A6, A10, A29, A30, Th14, NAT_1:13;
hence (left_cell (f,k,G)) /\ (right_cell (f,k,G)) =
LSeg (
(G * (i1,j1)),
(G * (i1,(j1 + 1))))
by A14, A26, A28, A31, GOBOARD5:25
.=
LSeg (
f,
k)
by A1, A2, A13, A6, A30, TOPREAL1:def 3
;
verum end; suppose A32:
(
i1 + 1
= i2 &
j1 = j2 )
;
(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)then A33:
right_cell (
f,
k,
G)
= cell (
G,
i1,
j)
by A1, A2, A3, A12, A13, A5, A6, A22, Th17;
(
i1 < len G &
left_cell (
f,
k,
G)
= cell (
G,
i1,
j1) )
by A1, A2, A3, A12, A13, A5, A6, A8, A32, Th16, NAT_1:13;
hence (left_cell (f,k,G)) /\ (right_cell (f,k,G)) =
LSeg (
(G * (i1,j1)),
(G * ((i1 + 1),j1)))
by A25, A15, A24, A33, GOBOARD5:26
.=
LSeg (
f,
k)
by A1, A2, A13, A6, A32, TOPREAL1:def 3
;
verum end; suppose A34:
(
i1 = i2 + 1 &
j1 = j2 )
;
(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)then A35:
right_cell (
f,
k,
G)
= cell (
G,
i2,
j1)
by A1, A2, A3, A12, A13, A5, A6, Th19;
(
i2 < len G &
left_cell (
f,
k,
G)
= cell (
G,
i2,
j) )
by A1, A2, A3, A12, A13, A5, A6, A27, A22, A34, Th18, NAT_1:13;
hence (left_cell (f,k,G)) /\ (right_cell (f,k,G)) =
LSeg (
(G * ((i2 + 1),j1)),
(G * (i2,j1)))
by A9, A15, A24, A35, GOBOARD5:26
.=
LSeg (
f,
k)
by A1, A2, A13, A6, A34, TOPREAL1:def 3
;
verum end; suppose A36:
(
i1 = i2 &
j1 = j2 + 1 )
;
(left_cell (f,k,G)) /\ (right_cell (f,k,G)) = LSeg (f,k)then A37:
right_cell (
f,
k,
G)
= cell (
G,
i,
j2)
by A1, A2, A3, A12, A13, A5, A6, A29, Th21;
(
j2 < width G &
left_cell (
f,
k,
G)
= cell (
G,
i1,
j2) )
by A1, A2, A3, A12, A13, A5, A6, A23, A36, Th20, NAT_1:13;
hence (left_cell (f,k,G)) /\ (right_cell (f,k,G)) =
LSeg (
(G * (i1,(j2 + 1))),
(G * (i1,j2)))
by A7, A26, A28, A37, GOBOARD5:25
.=
LSeg (
f,
k)
by A1, A2, A13, A6, A36, TOPREAL1:def 3
;
verum end; end;