let f be V8() standard special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2)
for k being Element of NAT st p in rng f & 1 <= k & k < p .. f holds
left_cell f,k = left_cell (Rotate f,p),((k + (len f)) -' (p .. f))
let p be Point of (TOP-REAL 2); :: thesis: for k being Element of NAT st p in rng f & 1 <= k & k < p .. f holds
left_cell f,k = left_cell (Rotate f,p),((k + (len f)) -' (p .. f))
let k be Element of NAT ; :: thesis: ( p in rng f & 1 <= k & k < p .. f implies left_cell f,k = left_cell (Rotate f,p),((k + (len f)) -' (p .. f)) )
assume that
A1: p in rng f and
A2: 1 <= k and
A3: k < p .. f ; :: thesis: left_cell f,k = left_cell (Rotate f,p),((k + (len f)) -' (p .. f))
set n = (k + (len f)) -' (p .. f);
A4: p .. f <= len f by A1, FINSEQ_4:31;
then k < len f by A3, XXREAL_0:2;
then A5: k + 1 <= len f by NAT_1:13;
0 < k by A2, XXREAL_0:2;
then A6: 0 + 1 < k + 1 by XREAL_1:8;
len f <= k + (len f) by NAT_1:11;
then A7: ((k + (len f)) -' (p .. f)) + 1 = ((k + (len f)) + 1) -' (p .. f) by A4, NAT_D:38, XXREAL_0:2;
A8: k + 1 <= p .. f by A3, NAT_1:13;
then (k + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:8;
then ((k + (len f)) -' (p .. f)) + 1 <= len f by A7, NAT_D:53;
then A9: ((k + (len f)) -' (p .. f)) + 1 <= len (Rotate f,p) by Th14;
A10: ((k + (len f)) -' (p .. f)) + 1 = ((k + 1) + (len f)) -' (p .. f) by A7;
A11: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Rotate f,p)) & [i2,j2] in Indices (GoB (Rotate f,p)) & (Rotate f,p) /. ((k + (len f)) -' (p .. f)) = (GoB (Rotate f,p)) * i1,j1 & (Rotate f,p) /. (((k + (len f)) -' (p .. f)) + 1) = (GoB (Rotate f,p)) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),i2,(j2 -' 1) ) holds
( i1 = i2 & j1 = j2 + 1 & left_cell f,k = cell (GoB (Rotate f,p)),i1,j2 )

proof

A12: left_cell f,k = left_cell f,k ;
let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( [i1,j1] in Indices (GoB (Rotate f,p)) & [i2,j2] in Indices (GoB (Rotate f,p)) & (Rotate f,p) /. ((k + (len f)) -' (p .. f)) = (GoB (Rotate f,p)) * i1,j1 & (Rotate f,p) /. (((k + (len f)) -' (p .. f)) + 1) = (GoB (Rotate f,p)) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),(i1 -' 1),j1 ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),i1,j1 ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),i2,(j2 -' 1) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell f,k = cell (GoB (Rotate f,p)),i1,j2 ) )
assume that
A13: ( [i1,j1] in Indices (GoB (Rotate f,p)) & [i2,j2] in Indices (GoB (Rotate f,p)) ) and
A14: ( (Rotate f,p) /. ((k + (len f)) -' (p .. f)) = (GoB (Rotate f,p)) * i1,j1 & (Rotate f,p) /. (((k + (len f)) -' (p .. f)) + 1) = (GoB (Rotate f,p)) * i2,j2 ) ; :: thesis: ( ( i1 = i2 & j1 + 1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),(i1 -' 1),j1 ) or ( i1 + 1 = i2 & j1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),i1,j1 ) or ( i1 = i2 + 1 & j1 = j2 & left_cell f,k = cell (GoB (Rotate f,p)),i2,(j2 -' 1) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell f,k = cell (GoB (Rotate f,p)),i1,j2 ) )
A15: GoB (Rotate f,p) = GoB f by Th28;
then A16: ( f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 ) by A1, A2, A3, A6, A8, A10, A14, Th18;
then A17: ( ( i1 = i2 & j1 + 1 = j2 & left_cell f,k = cell (GoB f),(i1 -' 1),j1 ) or ( i1 + 1 = i2 & j1 = j2 & left_cell f,k = cell (GoB f),i1,j1 ) or ( i1 = i2 + 1 & j1 = j2 & left_cell f,k = cell (GoB f),i2,(j2 -' 1) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell f,k = cell (GoB f),i1,j2 ) ) by A2, A5, A13, A15, A12, GOBOARD5:def 7;

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 A2, A5, A13, A15, A16, A12, GOBOARD5:def 7;

case ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: left_cell f,k = cell (GoB (Rotate f,p)),(i1 -' 1),j1

hence left_cell f,k = cell (GoB (Rotate f,p)),(i1 -' 1),j1 by A17, Th28; :: thesis: verum

end;

case ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: left_cell f,k = cell (GoB (Rotate f,p)),i1,j1

hence left_cell f,k = cell (GoB (Rotate f,p)),i1,j1 by A17, Th28; :: thesis: verum

end;

case ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: left_cell f,k = cell (GoB (Rotate f,p)),i2,(j2 -' 1)

hence left_cell f,k = cell (GoB (Rotate f,p)),i2,(j2 -' 1) by A17, Th28; :: thesis: verum

end;

case ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: left_cell f,k = cell (GoB (Rotate f,p)),i1,j2

hence left_cell f,k = cell (GoB (Rotate f,p)),i1,j2 by A17, Th28; :: thesis: verum

end;

end;

end;

1 + (p .. f) <= k + (len f) by A2, A4, XREAL_1:9;
then 1 <= (k + (len f)) -' (p .. f) by NAT_D:55;
hence left_cell f,k = left_cell (Rotate f,p),((k + (len f)) -' (p .. f)) by A9, A11, GOBOARD5:def 7; :: thesis: verum