let i, j be Nat; for f being V8() standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) holds
ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) )
let f be V8() standard special_circular_sequence; ( 1 <= i & i <= len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f & not ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) implies ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) )
assume that
A1:
( 1 <= i & i <= len (GoB f) )
and
A2:
1 <= j
and
A3:
j + 1 < width (GoB f)
and
A4:
LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f
and
A5:
LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f
; ( ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) or ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) )
A6:
1 <= j + 1
by NAT_1:11;
(1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * (i,(j + 1)))) in LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1))))
by RLTOPSP1:69;
then consider k1 being Nat such that
A7:
1 <= k1
and
A8:
k1 + 1 <= len f
and
A9:
LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) = LSeg (f,k1)
by A1, A2, A3, A4, Th39;
A10:
k1 < len f
by A8, NAT_1:13;
A11:
now ( not k1 > 1 or k1 = 2 or k1 > 2 )end;
A12:
j < width (GoB f)
by A3, NAT_1:13;
A13:
j + (1 + 1) = (j + 1) + 1
;
then A14:
1 <= j + 2
by NAT_1:11;
A15:
j + 2 <= width (GoB f)
by A3, A13, NAT_1:13;
(1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * (i,(j + 2)))) in LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2))))
by RLTOPSP1:69;
then consider k2 being Nat such that
A16:
1 <= k2
and
A17:
k2 + 1 <= len f
and
A18:
LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) = LSeg (f,k2)
by A1, A5, A6, A13, A15, Th39;
A19:
k2 < len f
by A17, NAT_1:13;
A20:
now ( not k2 > 1 or k2 = 2 or k2 > 2 )end;
A21:
( k1 = 1 or k1 > 1 )
by A7, XXREAL_0:1;
now ( ( k1 = 1 & k2 = 2 & 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) ) or ( k1 = 1 & k2 > 2 & f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( k2 = 1 & k1 = 2 & 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) ) or ( k2 = 1 & k1 > 2 & f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) or ( k1 = k2 & contradiction ) or ( k1 > 1 & k2 > k1 & 1 <= k1 & k1 + 1 < len f & f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) ) or ( k2 > 1 & k1 > k2 & 1 <= k2 & k2 + 1 < len f & f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) ) )per cases
( ( k1 = 1 & k2 = 2 ) or ( k1 = 1 & k2 > 2 ) or ( k2 = 1 & k1 = 2 ) or ( k2 = 1 & k1 > 2 ) or k1 = k2 or ( k1 > 1 & k2 > k1 ) or ( k2 > 1 & k1 > k2 ) )
by A16, A11, A20, A21, XXREAL_0:1;
case that A22:
k1 = 1
and A23:
k2 = 2
;
( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) )A24:
LSeg (
f,2)
= LSeg (
(f /. 2),
(f /. (2 + 1)))
by A17, A23, TOPREAL1:def 3;
then A25:
( (
(GoB f) * (
i,
(j + 1))
= f /. 2 &
(GoB f) * (
i,
(j + 2))
= f /. (2 + 1) ) or (
(GoB f) * (
i,
(j + 1))
= f /. (2 + 1) &
(GoB f) * (
i,
(j + 2))
= f /. 2 ) )
by A18, A23, SPPOL_1:8;
thus
( 1
<= 1 & 1
+ 1
< len f )
by A17, A23, NAT_1:13;
( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) )A26:
3
< len f
by Th34, XXREAL_0:2;
then A27:
f /. 1
<> f /. 3
by Th36;
A28:
LSeg (
f,1)
= LSeg (
(f /. 1),
(f /. (1 + 1)))
by A8, A22, TOPREAL1:def 3;
then A29:
( (
(GoB f) * (
i,
j)
= f /. 1 &
(GoB f) * (
i,
(j + 1))
= f /. 2 ) or (
(GoB f) * (
i,
j)
= f /. 2 &
(GoB f) * (
i,
(j + 1))
= f /. 1 ) )
by A9, A22, SPPOL_1:8;
hence
f /. (1 + 1) = (GoB f) * (
i,
(j + 1))
by A25, A26, Th36;
( f /. 1 = (GoB f) * (i,j) & f /. (1 + 2) = (GoB f) * (i,(j + 2)) )thus
f /. 1
= (GoB f) * (
i,
j)
by A18, A23, A29, A24, A27, SPPOL_1:8;
f /. (1 + 2) = (GoB f) * (i,(j + 2))thus
f /. (1 + 2) = (GoB f) * (
i,
(j + 2))
by A9, A22, A28, A25, A27, SPPOL_1:8;
verum end; case that A30:
k1 = 1
and A31:
k2 > 2
;
( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) )A32:
LSeg (
f,1)
= LSeg (
(f /. 1),
(f /. (1 + 1)))
by A8, A30, TOPREAL1:def 3;
then A33:
( (
(GoB f) * (
i,
j)
= f /. 1 &
(GoB f) * (
i,
(j + 1))
= f /. 2 ) or (
(GoB f) * (
i,
j)
= f /. 2 &
(GoB f) * (
i,
(j + 1))
= f /. 1 ) )
by A9, A30, SPPOL_1:8;
A34:
2
< k2 + 1
by A31, NAT_1:13;
then A35:
f /. (k2 + 1) <> f /. 2
by A17, Th37;
LSeg (
f,
k2)
= LSeg (
(f /. k2),
(f /. (k2 + 1)))
by A16, A17, TOPREAL1:def 3;
then A36:
( (
(GoB f) * (
i,
(j + 1))
= f /. k2 &
(GoB f) * (
i,
(j + 2))
= f /. (k2 + 1) ) or (
(GoB f) * (
i,
(j + 1))
= f /. (k2 + 1) &
(GoB f) * (
i,
(j + 2))
= f /. k2 ) )
by A18, SPPOL_1:8;
A37:
f /. k2 <> f /. 2
by A19, A31, Th36;
hence
f /. 1
= (GoB f) * (
i,
(j + 1))
by A9, A30, A32, A36, A35, SPPOL_1:8;
( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) )thus
f /. 2
= (GoB f) * (
i,
j)
by A9, A30, A32, A36, A37, A35, SPPOL_1:8;
f /. ((len f) -' 1) = (GoB f) * (i,(j + 2))A38:
k2 > 1
by A31, XXREAL_0:2;
then A39:
k2 + 1
> 1
by NAT_1:13;
then
k2 + 1
= len f
by A17, A19, A31, A33, A36, A38, A34, Th37, Th38;
then
k2 + 1
= ((len f) -' 1) + 1
by A39, XREAL_1:235;
hence
f /. ((len f) -' 1) = (GoB f) * (
i,
(j + 2))
by A19, A31, A33, A36, A38, Th36;
verum end; case that A40:
k2 = 1
and A41:
k1 = 2
;
( 1 <= 1 & 1 + 1 < len f & f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) )A42:
LSeg (
f,2)
= LSeg (
(f /. 2),
(f /. (2 + 1)))
by A8, A41, TOPREAL1:def 3;
then A43:
( (
(GoB f) * (
i,
(j + 1))
= f /. 2 &
(GoB f) * (
i,
j)
= f /. (2 + 1) ) or (
(GoB f) * (
i,
(j + 1))
= f /. (2 + 1) &
(GoB f) * (
i,
j)
= f /. 2 ) )
by A9, A41, SPPOL_1:8;
thus
( 1
<= 1 & 1
+ 1
< len f )
by A8, A41, NAT_1:13;
( f /. (1 + 1) = (GoB f) * (i,(j + 1)) & f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) )A44:
3
< len f
by Th34, XXREAL_0:2;
then A45:
f /. 1
<> f /. 3
by Th36;
A46:
LSeg (
f,1)
= LSeg (
(f /. 1),
(f /. (1 + 1)))
by A17, A40, TOPREAL1:def 3;
then A47:
( (
(GoB f) * (
i,
(j + 2))
= f /. 1 &
(GoB f) * (
i,
(j + 1))
= f /. 2 ) or (
(GoB f) * (
i,
(j + 2))
= f /. 2 &
(GoB f) * (
i,
(j + 1))
= f /. 1 ) )
by A18, A40, SPPOL_1:8;
hence
f /. (1 + 1) = (GoB f) * (
i,
(j + 1))
by A43, A44, Th36;
( f /. 1 = (GoB f) * (i,(j + 2)) & f /. (1 + 2) = (GoB f) * (i,j) )thus
f /. 1
= (GoB f) * (
i,
(j + 2))
by A9, A41, A47, A42, A45, SPPOL_1:8;
f /. (1 + 2) = (GoB f) * (i,j)thus
f /. (1 + 2) = (GoB f) * (
i,
j)
by A18, A40, A46, A43, A45, SPPOL_1:8;
verum end; case that A48:
k2 = 1
and A49:
k1 > 2
;
( f /. 1 = (GoB f) * (i,(j + 1)) & f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )A50:
LSeg (
f,1)
= LSeg (
(f /. 1),
(f /. (1 + 1)))
by A17, A48, TOPREAL1:def 3;
then A51:
( (
(GoB f) * (
i,
(j + 2))
= f /. 1 &
(GoB f) * (
i,
(j + 1))
= f /. 2 ) or (
(GoB f) * (
i,
(j + 2))
= f /. 2 &
(GoB f) * (
i,
(j + 1))
= f /. 1 ) )
by A18, A48, SPPOL_1:8;
A52:
2
< k1 + 1
by A49, NAT_1:13;
then A53:
f /. (k1 + 1) <> f /. 2
by A8, Th37;
LSeg (
f,
k1)
= LSeg (
(f /. k1),
(f /. (k1 + 1)))
by A7, A8, TOPREAL1:def 3;
then A54:
( (
(GoB f) * (
i,
(j + 1))
= f /. k1 &
(GoB f) * (
i,
j)
= f /. (k1 + 1) ) or (
(GoB f) * (
i,
(j + 1))
= f /. (k1 + 1) &
(GoB f) * (
i,
j)
= f /. k1 ) )
by A9, SPPOL_1:8;
A55:
f /. k1 <> f /. 2
by A10, A49, Th36;
hence
f /. 1
= (GoB f) * (
i,
(j + 1))
by A18, A48, A50, A54, A53, SPPOL_1:8;
( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) )thus
f /. 2
= (GoB f) * (
i,
(j + 2))
by A18, A48, A50, A54, A55, A53, SPPOL_1:8;
f /. ((len f) -' 1) = (GoB f) * (i,j)A56:
k1 > 1
by A49, XXREAL_0:2;
then A57:
k1 + 1
> 1
by NAT_1:13;
then
k1 + 1
= len f
by A8, A10, A49, A51, A54, A56, A52, Th37, Th38;
then
k1 + 1
= ((len f) -' 1) + 1
by A57, XREAL_1:235;
hence
f /. ((len f) -' 1) = (GoB f) * (
i,
j)
by A10, A49, A51, A54, A56, Th36;
verum end; case
k1 = k2
;
contradictionthen A58:
(
(GoB f) * (
i,
j)
= (GoB f) * (
i,
(j + 2)) or
(GoB f) * (
i,
j)
= (GoB f) * (
i,
(j + 1)) )
by A9, A18, SPPOL_1:8;
A59:
[i,(j + 2)] in Indices (GoB f)
by A1, A15, A14, MATRIX_0:30;
(
[i,j] in Indices (GoB f) &
[i,(j + 1)] in Indices (GoB f) )
by A1, A2, A3, A6, A12, MATRIX_0:30;
then
(
j = j + 1 or
j = j + 2 )
by A58, A59, GOBOARD1:5;
hence
contradiction
;
verum end; case that A60:
k1 > 1
and A61:
k2 > k1
;
( 1 <= k1 & k1 + 1 < len f & f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) )A62:
( 1
< k1 + 1 &
k1 + 1
< k2 + 1 )
by A60, A61, NAT_1:13, XREAL_1:6;
A63:
k1 < k2 + 1
by A61, NAT_1:13;
then A64:
f /. k1 <> f /. (k2 + 1)
by A17, A60, Th37;
A65:
k1 + 1
<= k2
by A61, NAT_1:13;
LSeg (
f,
k2)
= LSeg (
(f /. k2),
(f /. (k2 + 1)))
by A16, A17, TOPREAL1:def 3;
then A66:
( (
(GoB f) * (
i,
(j + 1))
= f /. k2 &
(GoB f) * (
i,
(j + 2))
= f /. (k2 + 1) ) or (
(GoB f) * (
i,
(j + 1))
= f /. (k2 + 1) &
(GoB f) * (
i,
(j + 2))
= f /. k2 ) )
by A18, SPPOL_1:8;
A67:
k2 < len f
by A17, NAT_1:13;
then A68:
f /. k1 <> f /. k2
by A60, A61, Th37;
A69:
LSeg (
f,
k1)
= LSeg (
(f /. k1),
(f /. (k1 + 1)))
by A7, A8, TOPREAL1:def 3;
then
( (
(GoB f) * (
i,
j)
= f /. k1 &
(GoB f) * (
i,
(j + 1))
= f /. (k1 + 1) ) or (
(GoB f) * (
i,
j)
= f /. (k1 + 1) &
(GoB f) * (
i,
(j + 1))
= f /. k1 ) )
by A9, SPPOL_1:8;
then
k1 + 1
>= k2
by A17, A60, A61, A66, A63, A67, A62, Th37;
then A70:
k1 + 1
= k2
by A65, XXREAL_0:1;
hence
( 1
<= k1 &
k1 + 1
< len f )
by A17, A60, NAT_1:13;
( f /. (k1 + 1) = (GoB f) * (i,(j + 1)) & f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) )thus
f /. (k1 + 1) = (GoB f) * (
i,
(j + 1))
by A9, A69, A66, A64, A68, SPPOL_1:8;
( f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) )thus
f /. k1 = (GoB f) * (
i,
j)
by A9, A69, A66, A64, A68, SPPOL_1:8;
f /. (k1 + 2) = (GoB f) * (i,(j + 2))thus
f /. (k1 + 2) = (GoB f) * (
i,
(j + 2))
by A9, A69, A66, A64, A70, SPPOL_1:8;
verum end; case that A71:
k2 > 1
and A72:
k1 > k2
;
( 1 <= k2 & k2 + 1 < len f & f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) )A73:
( 1
< k2 + 1 &
k2 + 1
< k1 + 1 )
by A71, A72, NAT_1:13, XREAL_1:6;
A74:
k2 < k1 + 1
by A72, NAT_1:13;
then A75:
f /. k2 <> f /. (k1 + 1)
by A8, A71, Th37;
A76:
k2 + 1
<= k1
by A72, NAT_1:13;
LSeg (
f,
k1)
= LSeg (
(f /. k1),
(f /. (k1 + 1)))
by A7, A8, TOPREAL1:def 3;
then A77:
( (
(GoB f) * (
i,
(j + 1))
= f /. k1 &
(GoB f) * (
i,
j)
= f /. (k1 + 1) ) or (
(GoB f) * (
i,
(j + 1))
= f /. (k1 + 1) &
(GoB f) * (
i,
j)
= f /. k1 ) )
by A9, SPPOL_1:8;
A78:
k1 < len f
by A8, NAT_1:13;
then A79:
f /. k2 <> f /. k1
by A71, A72, Th37;
A80:
LSeg (
f,
k2)
= LSeg (
(f /. k2),
(f /. (k2 + 1)))
by A16, A17, TOPREAL1:def 3;
then
( (
(GoB f) * (
i,
(j + 2))
= f /. k2 &
(GoB f) * (
i,
(j + 1))
= f /. (k2 + 1) ) or (
(GoB f) * (
i,
(j + 2))
= f /. (k2 + 1) &
(GoB f) * (
i,
(j + 1))
= f /. k2 ) )
by A18, SPPOL_1:8;
then
k2 + 1
>= k1
by A8, A71, A72, A77, A74, A78, A73, Th37;
then A81:
k2 + 1
= k1
by A76, XXREAL_0:1;
hence
( 1
<= k2 &
k2 + 1
< len f )
by A8, A71, NAT_1:13;
( f /. (k2 + 1) = (GoB f) * (i,(j + 1)) & f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) )thus
f /. (k2 + 1) = (GoB f) * (
i,
(j + 1))
by A18, A80, A77, A75, A79, SPPOL_1:8;
( f /. k2 = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,j) )thus
f /. k2 = (GoB f) * (
i,
(j + 2))
by A18, A80, A77, A75, A79, SPPOL_1:8;
f /. (k2 + 2) = (GoB f) * (i,j)thus
f /. (k2 + 2) = (GoB f) * (
i,
j)
by A18, A80, A77, A75, A81, SPPOL_1:8;
verum end; end; end;
hence
( ( f /. 1 = (GoB f) * (i,(j + 1)) & ( ( f /. 2 = (GoB f) * (i,j) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,j) ) ) ) or ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) )
; verum