let f be V22() standard clockwise_oriented special_circular_sequence; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 ;
A10: (G * (i1,j1)) `2 = N-bound (L~ f) by ;
A11: j2 <= width G by ;
A12: 1 <= i2 by ;
take i1 ; :: thesis: 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 ; :: thesis: ( [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 ;
A14: k + 1 >= 1 + 1 by ;
then A15: len f >= 2 by ;
k + 1 >= 1 by NAT_1:11;
then A16: k + 1 in dom f by ;
then f /. (k + 1) in L~ f by ;
then A17: (G * (i1,j1)) `2 >= (G * (i2,j2)) `2 by ;
A18: j1 <= width G by ;
A19: k < len f by ;
then A20: k in dom f by ;
A21: ( i2 <= len G & 1 <= j2 ) by ;
A22: ( i1 <= len G & 1 <= j1 ) by ;
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 ) ; :: thesis: ( [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; :: thesis: ( [(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 ; :: thesis: ( f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
thus f /. k = G * (i1,j1) by A6; :: thesis: f /. (k + 1) = G * ((i1 + 1),j1)
thus f /. (k + 1) = G * ((i1 + 1),j1) by ; :: thesis: verum
end;
suppose A24: ( i1 = i2 & j2 + 1 = j1 & k <> 1 ) ; :: thesis: ( [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 ;
k > 1 by ;
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 ;
A31: i1 = i4 by ;
k9 + 1 < len f by ;
then k9 < len f by NAT_1:13;
then A32: k9 in dom f by ;
A33: 1 <= i3 by ;
A34: j3 <= width G by ;
A35: j1 = j4 by ;
A36: ( i3 <= len G & 1 <= j3 ) by ;
A37: i3 = i4
proof
assume A38: i3 <> i4 ; :: thesis: contradiction
per cases ( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) ) by ;
suppose A39: ( j3 = j4 & i3 = i4 + 1 ) ; :: thesis: contradiction
then (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 ;
then (N-min (L~ f)) `2 <> N-bound (L~ f) by ;
hence contradiction by EUCLID:52; :: thesis: verum
end;
suppose A40: ( j3 = j4 & i3 + 1 = i4 ) ; :: thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by
.= (N-min (L~ f)) `2 by
.= N-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in N-most (L~ f) by ;
then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by ;
then i3 >= i3 + 1 by ;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;
end;
A41: k9 + 1 = k ;
f /. k9 in L~ f by ;
then A42: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by ;
now :: thesis: contradiction
per cases ( j4 + 1 = j3 or j4 = j3 + 1 ) by ;
suppose A43: j4 = j3 + 1 ; :: thesis: contradiction
k9 + (1 + 1) <= len f by A3;
then A44: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by ;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by ;
then f /. (k + 1) in {(f /. k)} by ;
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; :: thesis: 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) ) ; :: thesis: verum
end;
suppose A46: ( i1 = i2 & j2 + 1 = j1 & k = 1 ) ; :: thesis: ( [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 ;
then A47: len f > 1 + 0 by ;
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 ;
then len f >= 1 + 1 by ;
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 ;
A54: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
then A55: i1 = i4 by ;
k9 + 1 <= len f ;
then k9 < len f by NAT_1:13;
then A56: k9 in dom f by ;
then f /. k9 in L~ f by ;
then A57: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by ;
A58: 1 <= i3 by ;
A59: j1 = j4 by ;
A60: j3 <= width G by ;
A61: ( i3 <= len G & 1 <= j3 ) by ;
A62: i3 = i4
proof
assume A63: i3 <> i4 ; :: thesis: contradiction
per cases ( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) ) by ;
suppose A64: ( j3 = j4 & i3 = i4 + 1 ) ; :: thesis: contradiction
then (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 ;
then (N-min (L~ f)) `2 <> N-bound (L~ f) by ;
hence contradiction by EUCLID:52; :: thesis: verum
end;
suppose A65: ( j3 = j4 & i3 + 1 = i4 ) ; :: thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by
.= (N-min (L~ f)) `2 by
.= N-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in N-most (L~ f) by ;
then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by ;
then i3 >= i3 + 1 by ;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;
end;
A66: k9 + 1 = len f ;
now :: thesis: contradiction
per cases ( j4 + 1 = j3 or j4 = j3 + 1 ) by ;
suppose A67: j4 = j3 + 1 ; :: thesis: contradiction
(len f) - 1 >= 0 by ;
then (len f) -' 1 = (len f) - 1 by XREAL_0:def 2;
then A68: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by
.= {(f /. k)} by ;
( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by ;
then f /. (k + 1) in {(f /. k)} by ;
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; :: thesis: 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) ) ; :: thesis: verum
end;
suppose ( i1 = i2 & j2 = j1 + 1 ) ; :: thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) )
then j1 >= j1 + 1 by ;
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; :: thesis: verum
end;
suppose A70: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( [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
.= N-bound (L~ f) by ;
then G * (i2,j2) in N-most (L~ f) by ;
then (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 by ;
then i2 >= i2 + 1 by ;
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; :: thesis: verum
end;
end;