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= left_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= left_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= left_cell f,k,G
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len f implies LSeg f,k c= left_cell f,k,G )
assume that
A2:
1 <= k
and
A3:
k + 1 <= len f
; :: thesis: LSeg f,k c= left_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;
left_cell f,k,G = left_cell f,k,G
;
then A13:
( ( i1 = i2 & j1 + 1 = j2 & left_cell f,k,G = cell G,(i1 -' 1),j1 ) or ( i1 + 1 = i2 & j1 = j2 & left_cell f,k,G = cell G,i1,j1 ) or ( i1 = i2 + 1 & j1 = j2 & left_cell f,k,G = cell G,i2,(j2 -' 1) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell f,k,G = cell G,i1,j2 ) )
by A1, A2, A3, A5, A6, A7, A8, GOBRD13:def 3;
(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= left_cell f,k,GA16:
(i1 -' 1) + 1
= i1
by A9, XREAL_1:237;
then A17:
i1 -' 1
< len G
by A9, NAT_1:13;
j1 < width G
by A12, A15, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= cell G,
(i1 -' 1),
j1
by A6, A8, A10, A15, A16, A17, GOBOARD5:19;
hence
LSeg f,
k c= left_cell f,
k,
G
by A2, A3, A13, A15, TOPREAL1:def 5;
:: thesis: verum end; suppose A18:
(
i1 + 1
= i2 &
j1 = j2 )
;
:: thesis: LSeg f,k c= left_cell f,k,Gthen
i1 < len G
by A11, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= cell G,
i1,
j1
by A6, A8, A9, A10, A18, GOBOARD5:23;
hence
LSeg f,
k c= left_cell f,
k,
G
by A2, A3, A13, A18, TOPREAL1:def 5;
:: thesis: verum end; suppose A19:
(
i1 = i2 + 1 &
j1 = j2 )
;
:: thesis: LSeg f,k c= left_cell f,k,GA20:
(j2 -' 1) + 1
= j2
by A12, XREAL_1:237;
then A21:
j2 -' 1
< width G
by A12, NAT_1:13;
i2 < len G
by A9, A19, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= cell G,
i2,
(j2 -' 1)
by A6, A8, A11, A19, A20, A21, GOBOARD5:22;
hence
LSeg f,
k c= left_cell f,
k,
G
by A2, A3, A13, A19, TOPREAL1:def 5;
:: thesis: verum end; suppose A22:
(
i1 = i2 &
j1 = j2 + 1 )
;
:: thesis: LSeg f,k c= left_cell f,k,Gthen
j2 < width G
by A10, NAT_1:13;
then
LSeg (f /. k),
(f /. (k + 1)) c= left_cell f,
k,
G
by A6, A8, A9, A12, A13, A22, GOBOARD5:20;
hence
LSeg f,
k c= left_cell f,
k,
G
by A2, A3, TOPREAL1:def 5;
:: thesis: verum end;