let f be constant standard clockwise_oriented special_circular_sequence; :: thesis:
let G be Go-board; :: thesis:
let k be Nat; :: thesis:
assume that
A1: f is_sequence_on G and
A2: 1 <= k and
A3: k + 1 <= len f and
A4: f /. k = W-min (L~ f) ; :: thesis:
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 = W-bound (L~ f) by A4, A6, EUCLID:52;
A11: 1 <= j2 by A7, MATRIX_0:32;
A12: 1 <= i2 by A7, MATRIX_0:32;
take i1 ; :: thesis:
take j1 ; :: thesis:
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)) `1 <= (G * (i2,j2)) `1 by A8, A10, PSCOMP_1:24;
A18: ( i1 <= len G & 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 & j2 <= width G ) by A7, MATRIX_0:32;
A22: 1 <= j1 by A5, MATRIX_0:32;

per cases by A9;

suppose A23: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

thus [i1,j1] in Indices G by A5; :: thesis:
thus [i1,(j1 + 1)] in Indices G by A7, A23; :: thesis:
thus f /. k = G * (i1,j1) by A6; :: thesis:
thus f /. (k + 1) = G * (i1,(j1 + 1)) by A8, A23; :: thesis:

end;

suppose A24: ( i1 + 1 = i2 & j1 = j2 & k <> 1 ) ; :: thesis:

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: j1 = j4 by A5, A6, A28, A29, GOBOARD1:5;
A35: 1 <= j3 by A26, MATRIX_0:32;
A36: ( i3 <= len G & j3 <= width G ) by A26, MATRIX_0:32;
A37: j3 = j4

proof

assume A38: j3 <> j4 ; :: thesis:

per cases by A30, A38;

suppose A39: ( i3 = i4 & j3 = j4 + 1 ) ; :: thesis:

then (G * (i3,j3)) `1 <> W-bound (L~ f) by A1, A19, A25, A26, A27, A28, A29, Th20;
then (G * (i3,1)) `1 <> W-bound (L~ f) by A33, A35, A36, GOBOARD5:2;
then (W-min (L~ f)) `1 <> W-bound (L~ f) by A4, A6, A13, A22, A18, A31, A39, GOBOARD5:2;
hence contradiction by EUCLID:52; :: thesis:

end;

suppose A40: ( i3 = i4 & j3 + 1 = j4 ) ; :: thesis:

(G * (i3,j3)) `1 = (G * (i3,1)) `1 by A33, A35, A36, GOBOARD5:2
.= (W-min (L~ f)) `1 by A4, A6, A13, A22, A18, A31, A40, GOBOARD5:2
.= W-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in W-most (L~ f) by A15, A27, A32, GOBOARD1:1, SPRECT_2:12;
then (G * (i4,j4)) `2 <= (G * (i3,j3)) `2 by A4, A29, PSCOMP_1:31;
then j3 >= j3 + 1 by A13, A18, A31, A34, A35, A40, GOBOARD5:4;
hence contradiction by NAT_1:13; :: thesis:

end;

A41: k9 + 1 = k ;
f /. k9 in L~ f by A3, A14, A32, GOBOARD1:1, XXREAL_0:2;
then A42: (G * (i1,j1)) `1 <= (G * (i3,j3)) `1 by A10, A27, PSCOMP_1:24;

now :: thesis:

per cases by A30, A37;

suppose i3 + 1 = i4 ; :: thesis:

then i3 >= i3 + 1 by A22, A18, A31, A34, A33, A42, A37, GOBOARD5:3;
hence contradiction by NAT_1:13; :: thesis:

end;

suppose A43: i3 = i4 + 1 ; :: thesis:

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, A34, A37, A43, A44, XBOOLE_0:def 4;
then A45: f /. (k + 1) = f /. k by TARSKI:def 1;
i1 <> i2 by A24;
hence contradiction by A5, A6, A7, A8, A45, GOBOARD1:5; :: thesis:

end;

hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) ; :: thesis:

end;

suppose A46: ( i1 + 1 = i2 & j1 = j2 & k = 1 ) ; :: thesis:

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;
A56: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1:5;
A57: 1 <= j3 by A49, MATRIX_0:32;
k9 + 1 <= len f ;
then k9 < len f by NAT_1:13;
then A58: k9 in dom f by A48, FINSEQ_3:25;
then f /. k9 in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2;
then A59: (G * (i1,j1)) `1 <= (G * (i3,j3)) `1 by A10, A50, PSCOMP_1:24;
A60: 1 <= i3 by A49, MATRIX_0:32;
A61: ( i3 <= len G & j3 <= width G ) by A49, MATRIX_0:32;
A62: j3 = j4

proof

assume A63: j3 <> j4 ; :: thesis:

per cases by A53, A63;

suppose A64: ( i3 = i4 & j3 = j4 + 1 ) ; :: thesis:

then (G * (i3,j3)) `1 <> W-bound (L~ f) by A1, A48, A49, A50, A51, A52, Th20;
then (G * (i3,1)) `1 <> W-bound (L~ f) by A60, A57, A61, GOBOARD5:2;
then (W-min (L~ f)) `1 <> W-bound (L~ f) by A4, A6, A13, A22, A18, A55, A64, GOBOARD5:2;
hence contradiction by EUCLID:52; :: thesis:

end;

suppose A65: ( i3 = i4 & j3 + 1 = j4 ) ; :: thesis:

(G * (i3,j3)) `1 = (G * (i3,1)) `1 by A60, A57, A61, GOBOARD5:2
.= (W-min (L~ f)) `1 by A4, A6, A13, A22, A18, A55, A65, GOBOARD5:2
.= W-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in W-most (L~ f) by A15, A50, A58, GOBOARD1:1, SPRECT_2:12;
then (G * (i4,j4)) `2 <= (G * (i3,j3)) `2 by A4, A46, A54, A52, PSCOMP_1:31;
then j3 >= j3 + 1 by A13, A18, A55, A56, A57, A65, GOBOARD5:4;
hence contradiction by NAT_1:13; :: thesis:

end;

A66: k9 + 1 = len f ;

now :: thesis:

per cases by A53, A62;

suppose i3 + 1 = i4 ; :: thesis:

then i3 >= i3 + 1 by A22, A18, A55, A56, A60, A59, A62, GOBOARD5:3;
hence contradiction by NAT_1:13; :: thesis:

end;

suppose A67: i3 = i4 + 1 ; :: thesis:

(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, A56, A62, A67, A68, XBOOLE_0:def 4;
then A69: f /. (k + 1) = f /. k by TARSKI:def 1;
i1 <> i2 by A46;
hence contradiction by A5, A6, A7, A8, A69, GOBOARD1:5; :: thesis:

end;

hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) ; :: thesis:

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then i2 >= i2 + 1 by A22, A18, A12, A17, GOBOARD5:3;
hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) by NAT_1:13; :: thesis:

end;

suppose A70: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

(G * (i2,j2)) `1 = (G * (i2,1)) `1 by A12, A11, A21, GOBOARD5:2
.= W-bound (L~ f) by A13, A22, A18, A10, A70, GOBOARD5:2 ;
then G * (i2,j2) in W-most (L~ f) by A8, A15, A16, GOBOARD1:1, SPRECT_2:12;
then (G * (i1,j1)) `2 <= (G * (i2,j2)) `2 by A4, A6, PSCOMP_1:31;
then j2 >= j2 + 1 by A13, A18, A11, A70, GOBOARD5:4;
hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) by NAT_1:13; :: thesis:

end;