set n = 1;
let f be V22() standard special_circular_sequence; for p being Point of (TOP-REAL 2) st p in rng f holds
right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1)
let p be Point of (TOP-REAL 2); ( p in rng f implies right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) )
assume A1:
p in rng f
; right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1)
set k = p .. f;
len f > 1
by GOBOARD7:34, XXREAL_0:2;
then
p .. f < len f
by A1, SPRECT_5:7;
then A2:
(p .. f) + 1 <= len f
by NAT_1:13;
A3:
1 <= p .. f
by A1, FINSEQ_4:21;
A4:
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) )
proof
(Rotate (f,p)) /. (((1 + 1) + (p .. f)) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1)
by NAT_D:34;
then A5:
(Rotate (f,p)) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1)
;
A6:
right_cell (
f,
(p .. f))
= right_cell (
f,
(p .. f))
;
let i1,
j1,
i2,
j2 be
Nat;
( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) ) )
assume that A7:
(
[i1,j1] in Indices (GoB (Rotate (f,p))) &
[i2,j2] in Indices (GoB (Rotate (f,p))) )
and A8:
(Rotate (f,p)) /. 1
= (GoB (Rotate (f,p))) * (
i1,
j1)
and A9:
(Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (
i2,
j2)
;
( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) ) )
A10:
GoB (Rotate (f,p)) = GoB f
by REVROT_1:28;
len (Rotate (f,p)) = len f
by FINSEQ_6:179;
then
(Rotate (f,p)) /. (len f) = (Rotate (f,p)) /. 1
by FINSEQ_6:def 1;
then
(Rotate (f,p)) /. (((p .. f) + (len f)) -' (p .. f)) = (Rotate (f,p)) /. 1
by NAT_D:34;
then A11:
f /. (p .. f) = (GoB f) * (
i1,
j1)
by A1, A3, A8, A10, FINSEQ_6:183;
p .. f < (p .. f) + 1
by NAT_1:13;
then A12:
f /. ((p .. f) + 1) = (GoB f) * (
i2,
j2)
by A1, A2, A9, A10, A5, FINSEQ_6:175;
then A13:
( (
i1 = i2 &
j1 + 1
= j2 &
right_cell (
f,
(p .. f))
= cell (
(GoB f),
i1,
j1) ) or (
i1 + 1
= i2 &
j1 = j2 &
right_cell (
f,
(p .. f))
= cell (
(GoB f),
i1,
(j1 -' 1)) ) or (
i1 = i2 + 1 &
j1 = j2 &
right_cell (
f,
(p .. f))
= cell (
(GoB f),
i2,
j2) ) or (
i1 = i2 &
j1 = j2 + 1 &
right_cell (
f,
(p .. f))
= cell (
(GoB f),
(i1 -' 1),
j2) ) )
by A3, A2, A7, A10, A11, A6, GOBOARD5:def 6;
end;
1 + 1 <= len (Rotate (f,p))
by GOBOARD7:34, XXREAL_0:2;
hence
right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1)
by A4, GOBOARD5:def 6; verum