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