let i, j, k be Nat; for f being V8() standard special_circular_sequence st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) holds
( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )
let f be V8() standard special_circular_sequence; ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 1 <= width (GoB f) & 1 <= k & k + 1 < len f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1)) implies ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) )
assume that
A1:
1 <= i
and
A2:
i + 1 <= len (GoB f)
and
A3:
1 <= j
and
A4:
j + 1 <= width (GoB f)
and
A5:
1 <= k
and
A6:
k + 1 < len f
and
A7:
LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k)
and
A8:
LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,(k + 1))
; ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )
A9:
1 <= j + 1
by NAT_1:11;
A10:
i < i + 1
by NAT_1:13;
A11:
1 <= i + 1
by NAT_1:11;
j < width (GoB f)
by A4, NAT_1:13;
then ((GoB f) * ((i + 1),j)) `1 =
((GoB f) * ((i + 1),1)) `1
by A2, A3, A11, GOBOARD5:2
.=
((GoB f) * ((i + 1),(j + 1))) `1
by A2, A4, A9, A11, GOBOARD5:2
;
then A12:
(GoB f) * (i,(j + 1)) <> (GoB f) * ((i + 1),j)
by A1, A2, A4, A9, A10, GOBOARD5:3;
A13:
1 <= k + 1
by NAT_1:11;
A14:
k + (1 + 1) = (k + 1) + 1
;
then
k + 2 <= len f
by A6, NAT_1:13;
then A15:
LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) = LSeg ((f /. (k + 1)),(f /. (k + 2)))
by A8, A14, A13, TOPREAL1:def 3;
then A16:
( ( (GoB f) * ((i + 1),j) = f /. (k + 2) & (GoB f) * ((i + 1),(j + 1)) = f /. (k + 1) ) or ( (GoB f) * ((i + 1),j) = f /. (k + 1) & (GoB f) * ((i + 1),(j + 1)) = f /. (k + 2) ) )
by SPPOL_1:8;
A17:
LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) = LSeg ((f /. k),(f /. (k + 1)))
by A5, A6, A7, TOPREAL1:def 3;
then
( ( (GoB f) * ((i + 1),(j + 1)) = f /. (k + 1) & (GoB f) * (i,(j + 1)) = f /. k ) or ( (GoB f) * ((i + 1),(j + 1)) = f /. k & (GoB f) * (i,(j + 1)) = f /. (k + 1) ) )
by SPPOL_1:8;
hence
f /. k = (GoB f) * (i,(j + 1))
by A15, A12, SPPOL_1:8; ( f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) )
thus
f /. (k + 1) = (GoB f) * ((i + 1),(j + 1))
by A17, A16, A12, SPPOL_1:8; f /. (k + 2) = (GoB f) * ((i + 1),j)
thus
f /. (k + 2) = (GoB f) * ((i + 1),j)
by A17, A16, A12, SPPOL_1:8; verum