let k be Nat; for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
right_cell (f,k,(GoB f)) = right_cell (f,k)
let f be standard special_circular_sequence; ( 1 <= k & k + 1 <= len f implies right_cell (f,k,(GoB f)) = right_cell (f,k) )
assume that
A1:
1 <= k
and
A2:
k + 1 <= len f
; right_cell (f,k,(GoB f)) = right_cell (f,k)
set G = GoB f;
A3:
f is_sequence_on GoB f
by GOBOARD5:def 5;
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) )
proof
1
<= k + 1
by NAT_1:11;
then A4:
k + 1
in dom f
by A2, FINSEQ_3:25;
set IT =
right_cell (
f,
k);
let i1,
j1,
i2,
j2 be
Nat;
( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) )
assume A5:
(
[i1,j1] in Indices (GoB f) &
[i2,j2] in Indices (GoB f) &
f /. k = (GoB f) * (
i1,
j1) &
f /. (k + 1) = (GoB f) * (
i2,
j2) )
;
( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) )
k < len f
by A2, NAT_1:13;
then
k in dom f
by A1, FINSEQ_3:25;
then
|.(i1 - i2).| + |.(j1 - j2).| = 1
by A3, A5, A4, GOBOARD1:def 9;
then A6:
( (
|.(i1 - i2).| = 1 &
j1 = j2 ) or (
|.(j1 - j2).| = 1 &
i1 = i2 ) )
by SEQM_3:42;
right_cell (
f,
k)
= right_cell (
f,
k)
;
then A7:
( (
i1 = i2 &
j1 + 1
= j2 &
right_cell (
f,
k)
= cell (
(GoB f),
i1,
j1) ) or (
i1 + 1
= i2 &
j1 = j2 &
right_cell (
f,
k)
= cell (
(GoB f),
i1,
(j1 -' 1)) ) or (
i1 = i2 + 1 &
j1 = j2 &
right_cell (
f,
k)
= cell (
(GoB f),
i2,
j2) ) or (
i1 = i2 &
j1 = j2 + 1 &
right_cell (
f,
k)
= cell (
(GoB f),
(i1 -' 1),
j2) ) )
by A1, A2, A5, GOBOARD5:def 6;
end;
hence
right_cell (f,k,(GoB f)) = right_cell (f,k)
by A1, A2, A3, GOBRD13:def 2; verum