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))
A4:
p .. f <= len f
by A1, FINSEQ_4:31;
then A5:
k < len f
by A3, XXREAL_0:2;
0 < k
by A2, XXREAL_0:2;
then A6:
0 + 1 < k + 1
by XREAL_1:8;
A7:
k + 1 <= p .. f
by A3, NAT_1:13;
A8:
k + 1 <= len f
by A5, NAT_1:13;
set n = (k + (len f)) -' (p .. f);
len f <= k + (len f)
by NAT_1:11;
then A9:
((k + (len f)) -' (p .. f)) + 1 = ((k + (len f)) + 1) -' (p .. f)
by A4, NAT_D:38, XXREAL_0:2;
then A10:
((k + (len f)) -' (p .. f)) + 1 = ((k + 1) + (len f)) -' (p .. f)
;
1 + (p .. f) <= k + (len f)
by A2, A4, XREAL_1:9;
then A11:
1 <= (k + (len f)) -' (p .. f)
by NAT_D:55;
(k + 1) + (len f) <= (len f) + (p .. f)
by A7, XREAL_1:8;
then
((k + (len f)) -' (p .. f)) + 1 <= len f
by A9, NAT_D:53;
then A12:
((k + (len f)) -' (p .. f)) + 1 <= len (Rotate f,p)
by Th14;
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
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))
and A14:
[i2,j2] in Indices (GoB (Rotate f,p))
and A15:
(Rotate f,p) /. ((k + (len f)) -' (p .. f)) = (GoB (Rotate f,p)) * i1,
j1
and A16:
(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 ) )
A17:
GoB (Rotate f,p) = GoB f
by Th28;
then A18:
f /. k = (GoB f) * i1,
j1
by A1, A2, A3, A15, Th18;
A19:
f /. (k + 1) = (GoB f) * i2,
j2
by A1, A6, A7, A10, A16, A17, Th18;
A20:
left_cell f,
k = left_cell f,
k
;
then A21:
( (
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, A8, A13, A14, A17, A18, A19, GOBOARD5:def 7;
end;
hence
left_cell f,k = left_cell (Rotate f,p),((k + (len f)) -' (p .. f))
by A11, A12, GOBOARD5:def 7; :: thesis: verum