let k be Nat; :: thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
left_cell (f,k,(GoB f)) = left_cell (f,k)
let f be standard special_circular_sequence; :: thesis: ( 1 <= k & k + 1 <= len f implies left_cell (f,k,(GoB f)) = left_cell (f,k) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; :: thesis: left_cell (f,k,(GoB f)) = left_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 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) )
proof
1 <= k + 1 by NAT_1:11;
then A4: k + 1 in dom f by A2, FINSEQ_3:25;
let i1, j1, i2, j2 be Nat; :: thesis: ( [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 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,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) ) ; :: thesis: ( ( 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) ) )
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;
left_cell (f,k) = left_cell (f,k) ;
then A7: ( ( 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 A1, A2, A5, 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 A6, SEQM_3:41;
case ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1)
hence left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) by A7; :: thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: left_cell (f,k) = cell ((GoB f),i1,j1)
hence left_cell (f,k) = cell ((GoB f),i1,j1) by A7; :: thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1))
hence left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) by A7; :: thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: left_cell (f,k) = cell ((GoB f),i1,j2)
hence left_cell (f,k) = cell ((GoB f),i1,j2) by A7; :: thesis: verum
end;
end;
end;
hence left_cell (f,k,(GoB f)) = left_cell (f,k) by A1, A2, A3, GOBRD13:def 3; :: thesis: verum