let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg f,k c= right_cell f,k,G
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg f,k c= right_cell f,k,G )
assume A1:
f is_sequence_on G
; :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg f,k c= right_cell f,k,G
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len f implies LSeg f,k c= right_cell f,k,G )
assume that
A2:
1 <= k
and
A3:
k + 1 <= len f
; :: thesis: LSeg f,k c= right_cell f,k,G
A4:
( k in dom f & k + 1 in dom f )
by A2, A3, GOBOARD2:3;
then consider i1, j1 being Element of NAT such that
A5:
[i1,j1] in Indices G
and
A6:
f /. k = G * i1,j1
by A1, GOBOARD1:def 11;
consider i2, j2 being Element of NAT such that
A7:
[i2,j2] in Indices G
and
A8:
f /. (k + 1) = G * i2,j2
by A1, A4, GOBOARD1:def 11;
A9:
( 1 <= i1 & i1 <= len G )
by A5, MATRIX_1:39;
A10:
( 1 <= j1 & j1 <= width G )
by A5, MATRIX_1:39;
A11:
( 1 <= i2 & i2 <= len G )
by A7, MATRIX_1:39;
A12:
( 1 <= j2 & j2 <= width G )
by A7, MATRIX_1:39;
right_cell f,k,G = right_cell f,k,G
;
then A13:
( ( i1 = i2 & j1 + 1 = j2 & right_cell f,k,G = cell G,i1,j1 ) or ( i1 + 1 = i2 & j1 = j2 & right_cell f,k,G = cell G,i1,(j1 -' 1) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell f,k,G = cell G,i2,j2 ) or ( i1 = i2 & j1 = j2 + 1 & right_cell f,k,G = cell G,(i1 -' 1),j2 ) )
by A1, A2, A3, A5, A6, A7, A8, GOBRD13:def 2;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1
by A1, A4, A5, A6, A7, A8, GOBOARD1:def 11;
then A14:
( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) )
by GOBOARD1:2;
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 A14, GOBOARD1:1;
suppose A15:
(
i1 = i2 &
j1 + 1
= j2 )
;
:: thesis: LSeg f,k c= right_cell f,k,Gthen
j1 < width G
by A12, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= cell G,
i1,
j1
by A6, A8, A9, A10, A15, GOBOARD5:20;
hence
LSeg f,
k c= right_cell f,
k,
G
by A2, A3, A13, A15, TOPREAL1:def 5;
:: thesis: verum end; suppose A16:
(
i1 + 1
= i2 &
j1 = j2 )
;
:: thesis: LSeg f,k c= right_cell f,k,GA17:
(j1 -' 1) + 1
= j1
by A10, XREAL_1:237;
then A18:
j1 -' 1
< width G
by A10, NAT_1:13;
i1 < len G
by A11, A16, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= cell G,
i1,
(j1 -' 1)
by A6, A8, A9, A16, A17, A18, GOBOARD5:22;
hence
LSeg f,
k c= right_cell f,
k,
G
by A2, A3, A13, A16, TOPREAL1:def 5;
:: thesis: verum end; suppose A19:
(
i1 = i2 + 1 &
j1 = j2 )
;
:: thesis: LSeg f,k c= right_cell f,k,Gthen
i2 < len G
by A9, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= cell G,
i2,
j2
by A6, A8, A11, A12, A19, GOBOARD5:23;
hence
LSeg f,
k c= right_cell f,
k,
G
by A2, A3, A13, A19, TOPREAL1:def 5;
:: thesis: verum end; suppose A20:
(
i1 = i2 &
j1 = j2 + 1 )
;
:: thesis: LSeg f,k c= right_cell f,k,GA21:
(i1 -' 1) + 1
= i1
by A9, XREAL_1:237;
then A22:
i1 -' 1
< len G
by A9, NAT_1:13;
j2 < width G
by A10, A20, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= right_cell f,
k,
G
by A6, A8, A12, A13, A20, A21, A22, GOBOARD5:19;
hence
LSeg f,
k c= right_cell f,
k,
G
by A2, A3, TOPREAL1:def 5;
:: thesis: verum end;