let f be non constant standard special_circular_sequence; for i, j being Nat st i >= 1 & j >= 1 & i + j = len f holds
left_cell (f,i) = right_cell ((Rev f),j)
let i, j be Nat; ( 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
; left_cell (f,i) = right_cell ((Rev f),j)
A4:
i + 1 <= len f
by A2, A3, XREAL_1:6;
len f = len (Rev f)
by FINSEQ_5:def 3;
then A5:
j + 1 <= len (Rev f)
by A1, A3, XREAL_1:6;
A6:
GoB (Rev f) = GoB f
by Lm1;
now for i1, j1, i2, j2 being Nat st [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 ( i1 = i2 & j1 + 1 = j2 & right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell ((Rev f),j) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & right_cell ((Rev f),j) = cell ((GoB f),i1,j2) )let i1,
j1,
i2,
j2 be
Nat;
( [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)
;
( ( 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:25;
(i + 1) + j = (len f) + 1
by A3;
then A12:
(Rev f) /. j = (GoB f) * (
i2,
j2)
by A10, A11, FINSEQ_5:66;
i <= len f
by A4, NAT_1:13;
then A13:
i in dom f
by A1, FINSEQ_3:25;
(j + 1) + i = (len f) + 1
by A3;
then A14:
(Rev f) /. (j + 1) = (GoB f) * (
i1,
j1)
by A9, A13, FINSEQ_5:66;
1
<= i1
by A7, MATRIX_0:32;
then A15:
(i1 -' 1) + 1
= i1
by XREAL_1:235;
1
<= j1
by A7, MATRIX_0:32;
then A16:
(j1 -' 1) + 1
= j1
by XREAL_1:235;
reconsider i19 =
i1,
i29 =
i2,
j19 =
j1,
j29 =
j2 as
Element of
REAL by XREAL_0:def 1;
f is_sequence_on GoB f
by GOBOARD5:def 5;
then
|.(i1 - i2).| + |.(j1 - j2).| = 1
by A7, A8, A9, A10, A11, A13;
then A17:
( (
|.(i19 - i29).| = 1 &
j1 = j2 ) or (
|.(j19 - j29).| = 1 &
i1 = i2 ) )
by SEQM_3:42;
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, SEQM_3:41;
case
(
i1 = i2 &
j1 + 1
= j2 )
;
right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1)hence
right_cell (
(Rev f),
j)
= cell (
(GoB f),
(i1 -' 1),
j1)
by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:30;
verum end; case
(
i1 + 1
= i2 &
j1 = j2 )
;
right_cell ((Rev f),j) = cell ((GoB f),i1,j1)hence
right_cell (
(Rev f),
j)
= cell (
(GoB f),
i1,
j1)
by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:29;
verum end; case
(
i1 = i2 + 1 &
j1 = j2 )
;
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:28;
verum end; case
(
i1 = i2 &
j1 = j2 + 1 )
;
right_cell ((Rev f),j) = cell ((GoB f),i1,j2)hence
right_cell (
(Rev f),
j)
= cell (
(GoB f),
i1,
j2)
by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:27;
verum end; end; end;
hence
left_cell (f,i) = right_cell ((Rev f),j)
by A1, A4, GOBOARD5:def 7; verum