let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell f,i = right_cell (Rev f),j
let i, j be Element of NAT ; :: thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell f,i = right_cell (Rev f),j )
assume that
A1:
i >= 1
and
A2:
j >= 1
and
A3:
i + j = len f
; :: thesis: left_cell f,i = right_cell (Rev f),j
A4:
i + 1 <= len f
by A2, A3, XREAL_1:8;
len f = len (Rev f)
by FINSEQ_5:def 3;
then A5:
j + 1 <= len (Rev f)
by A1, A3, XREAL_1:8;
A6:
GoB (Rev f) = GoB f
by Lm1;
now let i1,
j1,
i2,
j2 be
Element of
NAT ;
:: thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. i = (GoB f) * i1,j1 & f /. (i + 1) = (GoB f) * i2,j2 & not ( b1 = b3 & b2 + 1 = b4 & right_cell (Rev f),j = cell (GoB f),(b1 -' 1),b2 ) & not ( b1 + 1 = b3 & b2 = b4 & right_cell (Rev f),j = cell (GoB f),b1,b2 ) & not ( b1 = b3 + 1 & b2 = b4 & right_cell (Rev f),j = cell (GoB f),b3,(b4 -' 1) ) implies ( b1 = b3 & b2 = b4 + 1 & right_cell (Rev f),j = cell (GoB f),b1,b4 ) )assume that A7:
[i1,j1] in Indices (GoB f)
and A8:
[i2,j2] in Indices (GoB f)
and A9:
f /. i = (GoB f) * i1,
j1
and A10:
f /. (i + 1) = (GoB f) * i2,
j2
;
:: thesis: ( ( b1 = b3 & b2 + 1 = b4 & right_cell (Rev f),j = cell (GoB f),(b1 -' 1),b2 ) or ( b1 + 1 = b3 & b2 = b4 & right_cell (Rev f),j = cell (GoB f),b1,b2 ) or ( b1 = b3 + 1 & b2 = b4 & right_cell (Rev f),j = cell (GoB f),b3,(b4 -' 1) ) or ( b1 = b3 & b2 = b4 + 1 & right_cell (Rev f),j = cell (GoB f),b1,b4 ) )
1
<= i + 1
by NAT_1:11;
then A11:
i + 1
in dom f
by A4, FINSEQ_3:27;
(i + 1) + j = (len f) + 1
by A3;
then A12:
(Rev f) /. j = (GoB f) * i2,
j2
by A10, A11, FINSEQ_5:69;
i <= len f
by A4, NAT_1:13;
then A13:
i in dom f
by A1, FINSEQ_3:27;
(j + 1) + i = (len f) + 1
by A3;
then A14:
(Rev f) /. (j + 1) = (GoB f) * i1,
j1
by A9, A13, FINSEQ_5:69;
1
<= i1
by A7, MATRIX_1:39;
then A15:
(i1 -' 1) + 1
= i1
by XREAL_1:237;
1
<= j1
by A7, MATRIX_1:39;
then A16:
(j1 -' 1) + 1
= j1
by XREAL_1:237;
reconsider i1' =
i1,
i2' =
i2,
j1' =
j1,
j2' =
j2 as
Element of
REAL ;
f is_sequence_on GoB f
by GOBOARD5:def 5;
then
(abs (i1 - i2)) + (abs (j1 - j2)) = 1
by A7, A8, A9, A10, A11, A13, GOBOARD1:def 11;
then A17:
( (
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 A17, GOBOARD1:1;
case
(
i1 = i2 &
j1 + 1
= j2 )
;
:: thesis: right_cell (Rev f),j = cell (GoB f),(i1 -' 1),j1hence
right_cell (Rev f),
j = cell (GoB f),
(i1 -' 1),
j1
by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:31;
:: thesis: verum end; case
(
i1 + 1
= i2 &
j1 = j2 )
;
:: thesis: right_cell (Rev f),j = cell (GoB f),i1,j1hence
right_cell (Rev f),
j = cell (GoB f),
i1,
j1
by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:30;
:: thesis: verum end; case
(
i1 = i2 + 1 &
j1 = j2 )
;
:: thesis: right_cell (Rev f),j = cell (GoB f),i2,(j2 -' 1)hence
right_cell (Rev f),
j = cell (GoB f),
i2,
(j2 -' 1)
by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:29;
:: thesis: verum end; case
(
i1 = i2 &
j1 = j2 + 1 )
;
:: thesis: right_cell (Rev f),j = cell (GoB f),i1,j2hence
right_cell (Rev f),
j = cell (GoB f),
i1,
j2
by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:28;
:: thesis: verum end; end;
hence
left_cell f,i = right_cell (Rev f),j
by A1, A4, GOBOARD5:def 7; :: thesis: verum