let f be V22() standard clockwise_oriented special_circular_sequence; for G being Go-board
for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds
ex i, j being Nat st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) )
let G be Go-board; for k being Nat st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds
ex i, j being Nat st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) )
let k be Nat; ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) implies ex i, j being Nat st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) )
assume that
A1:
f is_sequence_on G
and
A2:
1 <= k
and
A3:
k + 1 <= len f
and
A4:
f /. k = E-max (L~ f)
; ex i, j being Nat st
( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) )
consider i1, j1, i2, j2 being Nat such that
A5:
[i1,j1] in Indices G
and
A6:
f /. k = G * (i1,j1)
and
A7:
[i2,j2] in Indices G
and
A8:
f /. (k + 1) = G * (i2,j2)
and
A9:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A1, A2, A3, JORDAN8:3;
A10:
(G * (i1,j1)) `1 = E-bound (L~ f)
by A4, A6, EUCLID:52;
A11:
j2 <= width G
by A7, MATRIX_0:32;
take
i2
; ex j being Nat st
( [i2,(j + 1)] in Indices G & [i2,j] in Indices G & f /. k = G * (i2,(j + 1)) & f /. (k + 1) = G * (i2,j) )
take
j2
; ( [i2,(j2 + 1)] in Indices G & [i2,j2] in Indices G & f /. k = G * (i2,(j2 + 1)) & f /. (k + 1) = G * (i2,j2) )
A12:
i1 <= len G
by A5, MATRIX_0:32;
A13:
k + 1 >= 1 + 1
by A2, XREAL_1:7;
then A14:
len f >= 2
by A3, XXREAL_0:2;
k + 1 >= 1
by NAT_1:11;
then A15:
k + 1 in dom f
by A3, FINSEQ_3:25;
then
f /. (k + 1) in L~ f
by A3, A13, GOBOARD1:1, XXREAL_0:2;
then A16:
(G * (i1,j1)) `1 >= (G * (i2,j2)) `1
by A8, A10, PSCOMP_1:24;
A17:
( 1 <= i1 & 1 <= j1 )
by A5, MATRIX_0:32;
A18:
k < len f
by A3, NAT_1:13;
then A19:
k in dom f
by A2, FINSEQ_3:25;
A20:
i2 <= len G
by A7, MATRIX_0:32;
A21:
j1 <= width G
by A5, MATRIX_0:32;
A22:
( 1 <= i2 & 1 <= j2 )
by A7, MATRIX_0:32;
now ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )per cases
( ( i1 = i2 & j2 + 1 = j1 ) or ( i2 + 1 = i1 & j2 = j1 & k <> 1 ) or ( i2 + 1 = i1 & j2 = j1 & k = 1 ) or ( i2 = i1 + 1 & j1 = j2 ) or ( i1 = i2 & j2 = j1 + 1 ) )
by A9;
suppose A23:
(
i2 + 1
= i1 &
j2 = j1 &
k <> 1 )
;
( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )reconsider k9 =
k - 1 as
Nat by A19, FINSEQ_3:26;
k > 1
by A2, A23, XXREAL_0:1;
then
k >= 1
+ 1
by NAT_1:13;
then A24:
k9 >= (1 + 1) - 1
by XREAL_1:9;
then consider i3,
j3,
i4,
j4 being
Nat such that A25:
[i3,j3] in Indices G
and A26:
f /. k9 = G * (
i3,
j3)
and A27:
[i4,j4] in Indices G
and A28:
f /. (k9 + 1) = G * (
i4,
j4)
and A29:
( (
i3 = i4 &
j3 + 1
= j4 ) or (
i3 + 1
= i4 &
j3 = j4 ) or (
i3 = i4 + 1 &
j3 = j4 ) or (
i3 = i4 &
j3 = j4 + 1 ) )
by A1, A18, JORDAN8:3;
A30:
i1 = i4
by A5, A6, A27, A28, GOBOARD1:5;
k9 + 1
< len f
by A3, NAT_1:13;
then
k9 < len f
by NAT_1:13;
then A31:
k9 in dom f
by A24, FINSEQ_3:25;
A32:
i3 <= len G
by A25, MATRIX_0:32;
A33:
j1 = j4
by A5, A6, A27, A28, GOBOARD1:5;
A34:
j3 <= width G
by A25, MATRIX_0:32;
A35:
( 1
<= i3 & 1
<= j3 )
by A25, MATRIX_0:32;
A36:
j3 = j4
proof
assume A37:
j3 <> j4
;
contradiction
per cases
( ( i3 = i4 & j4 = j3 + 1 ) or ( i3 = i4 & j4 + 1 = j3 ) )
by A29, A37;
suppose A38:
(
i3 = i4 &
j4 = j3 + 1 )
;
contradictionthen
(G * (i3,j3)) `1 <> E-bound (L~ f)
by A1, A18, A24, A25, A26, A27, A28, Th18;
then
(G * (i3,1)) `1 <> E-bound (L~ f)
by A32, A35, A34, GOBOARD5:2;
then
(E-max (L~ f)) `1 <> E-bound (L~ f)
by A4, A6, A12, A17, A21, A30, A38, GOBOARD5:2;
hence
contradiction
by EUCLID:52;
verum end; suppose A39:
(
i3 = i4 &
j4 + 1
= j3 )
;
contradiction(G * (i3,j3)) `1 =
(G * (i3,1)) `1
by A32, A35, A34, GOBOARD5:2
.=
(E-max (L~ f)) `1
by A4, A6, A12, A17, A21, A30, A39, GOBOARD5:2
.=
E-bound (L~ f)
by EUCLID:52
;
then
G * (
i3,
j3)
in E-most (L~ f)
by A14, A26, A31, GOBOARD1:1, SPRECT_2:13;
then
(G * (i4,j4)) `2 >= (G * (i3,j3)) `2
by A4, A28, PSCOMP_1:47;
then
j4 >= j4 + 1
by A12, A17, A30, A33, A34, A39, GOBOARD5:4;
hence
contradiction
by NAT_1:13;
verum end; end;
end; A40:
k9 + 1
= k
;
f /. k9 in L~ f
by A3, A13, A31, GOBOARD1:1, XXREAL_0:2;
then A41:
(G * (i1,j1)) `1 >= (G * (i3,j3)) `1
by A10, A26, PSCOMP_1:24;
now contradictionper cases
( i4 + 1 = i3 or i4 = i3 + 1 )
by A29, A36;
suppose A42:
i4 = i3 + 1
;
contradiction
k9 + (1 + 1) <= len f
by A3;
then A43:
(LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)}
by A24, A40, TOPREAL1:def 6;
(
f /. k9 in LSeg (
f,
k9) &
f /. (k + 1) in LSeg (
f,
k) )
by A2, A3, A18, A24, A40, TOPREAL1:21;
then
f /. (k + 1) in {(f /. k)}
by A8, A23, A26, A30, A33, A36, A42, A43, XBOOLE_0:def 4;
then A44:
f /. (k + 1) = f /. k
by TARSKI:def 1;
i1 <> i2
by A23;
hence
contradiction
by A5, A6, A7, A8, A44, GOBOARD1:5;
verum end; end; end; hence
(
[i2,j2] in Indices G &
[i2,(j2 + 1)] in Indices G &
f /. k = G * (
i2,
(j2 + 1)) )
;
verum end; suppose A45:
(
i2 + 1
= i1 &
j2 = j1 &
k = 1 )
;
( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )set k1 =
len f;
k < len f
by A3, NAT_1:13;
then A46:
len f > 1
+ 0
by A2, XXREAL_0:2;
then
len f in dom f
by FINSEQ_3:25;
then reconsider k9 =
(len f) - 1 as
Nat by FINSEQ_3:26;
k + 1
>= 1
+ 1
by A2, XREAL_1:7;
then
len f >= 1
+ 1
by A3, XXREAL_0:2;
then A47:
k9 >= (1 + 1) - 1
by XREAL_1:9;
then consider i3,
j3,
i4,
j4 being
Nat such that A48:
[i3,j3] in Indices G
and A49:
f /. k9 = G * (
i3,
j3)
and A50:
[i4,j4] in Indices G
and A51:
f /. (k9 + 1) = G * (
i4,
j4)
and A52:
( (
i3 = i4 &
j3 + 1
= j4 ) or (
i3 + 1
= i4 &
j3 = j4 ) or (
i3 = i4 + 1 &
j3 = j4 ) or (
i3 = i4 &
j3 = j4 + 1 ) )
by A1, JORDAN8:3;
A53:
f /. (len f) = f /. 1
by FINSEQ_6:def 1;
then A54:
i1 = i4
by A5, A6, A45, A50, A51, GOBOARD1:5;
A55:
j1 = j4
by A5, A6, A45, A53, A50, A51, GOBOARD1:5;
A56:
j3 <= width G
by A48, MATRIX_0:32;
k9 + 1
<= len f
;
then
k9 < len f
by NAT_1:13;
then A57:
k9 in dom f
by A47, FINSEQ_3:25;
then
f /. k9 in L~ f
by A3, A13, GOBOARD1:1, XXREAL_0:2;
then A58:
(G * (i1,j1)) `1 >= (G * (i3,j3)) `1
by A10, A49, PSCOMP_1:24;
A59:
i3 <= len G
by A48, MATRIX_0:32;
A60:
( 1
<= i3 & 1
<= j3 )
by A48, MATRIX_0:32;
A61:
j3 = j4
proof
assume A62:
j3 <> j4
;
contradiction
per cases
( ( i3 = i4 & j4 = j3 + 1 ) or ( i3 = i4 & j4 + 1 = j3 ) )
by A52, A62;
suppose A63:
(
i3 = i4 &
j4 = j3 + 1 )
;
contradictionthen
(G * (i3,j3)) `1 <> E-bound (L~ f)
by A1, A47, A48, A49, A50, A51, Th18;
then
(G * (i3,1)) `1 <> E-bound (L~ f)
by A59, A60, A56, GOBOARD5:2;
then
(E-max (L~ f)) `1 <> E-bound (L~ f)
by A4, A6, A12, A17, A21, A54, A63, GOBOARD5:2;
hence
contradiction
by EUCLID:52;
verum end; suppose A64:
(
i3 = i4 &
j4 + 1
= j3 )
;
contradiction(G * (i3,j3)) `1 =
(G * (i3,1)) `1
by A59, A60, A56, GOBOARD5:2
.=
(E-max (L~ f)) `1
by A4, A6, A12, A17, A21, A54, A64, GOBOARD5:2
.=
E-bound (L~ f)
by EUCLID:52
;
then
G * (
i3,
j3)
in E-most (L~ f)
by A14, A49, A57, GOBOARD1:1, SPRECT_2:13;
then
(G * (i4,j4)) `2 >= (G * (i3,j3)) `2
by A4, A45, A53, A51, PSCOMP_1:47;
then
j4 >= j4 + 1
by A12, A17, A54, A55, A56, A64, GOBOARD5:4;
hence
contradiction
by NAT_1:13;
verum end; end;
end; A65:
k9 + 1
= len f
;
now contradictionper cases
( i4 + 1 = i3 or i4 = i3 + 1 )
by A52, A61;
suppose A66:
i4 = i3 + 1
;
contradiction
(len f) - 1
>= 0
by A46, XREAL_1:19;
then
(len f) -' 1
= (len f) - 1
by XREAL_0:def 2;
then A67:
(LSeg (f,k)) /\ (LSeg (f,k9)) =
{(f . k)}
by A45, JORDAN4:42
.=
{(f /. k)}
by A19, PARTFUN1:def 6
;
(
f /. k9 in LSeg (
f,
k9) &
f /. (k + 1) in LSeg (
f,
k) )
by A2, A3, A47, A65, TOPREAL1:21;
then
f /. (k + 1) in {(f /. k)}
by A8, A45, A49, A54, A55, A61, A66, A67, XBOOLE_0:def 4;
then A68:
f /. (k + 1) = f /. k
by TARSKI:def 1;
i1 <> i2
by A45;
hence
contradiction
by A5, A6, A7, A8, A68, GOBOARD1:5;
verum end; end; end; hence
(
[i2,j2] in Indices G &
[i2,(j2 + 1)] in Indices G &
f /. k = G * (
i2,
(j2 + 1)) )
;
verum end; suppose A69:
(
i1 = i2 &
j2 = j1 + 1 )
;
( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) )(G * (i2,j2)) `1 =
(G * (i2,1)) `1
by A20, A22, A11, GOBOARD5:2
.=
E-bound (L~ f)
by A12, A17, A21, A10, A69, GOBOARD5:2
;
then
G * (
i2,
j2)
in E-most (L~ f)
by A8, A14, A15, GOBOARD1:1, SPRECT_2:13;
then
(G * (i1,j1)) `2 >= (G * (i2,j2)) `2
by A4, A6, PSCOMP_1:47;
then
j1 >= j1 + 1
by A12, A17, A11, A69, GOBOARD5:4;
hence
(
[i2,j2] in Indices G &
[i2,(j2 + 1)] in Indices G &
f /. k = G * (
i2,
(j2 + 1)) )
by NAT_1:13;
verum end; end; end;
hence
( [i2,(j2 + 1)] in Indices G & [i2,j2] in Indices G & f /. k = G * (i2,(j2 + 1)) )
; f /. (k + 1) = G * (i2,j2)
thus
f /. (k + 1) = G * (i2,j2)
by A8; verum