let f be constant 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 = S-max (L~ f) holds
ex i, j being Nat st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,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 = S-max (L~ f) holds
ex i, j being Nat st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) )
let k be Nat; :: thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) implies ex i, j being Nat st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & 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 = S-max (L~ f) ; :: thesis: ex i, j being Nat st
( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & 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)) `2 = S-bound (L~ f) by A4, A6, EUCLID:52;
A11: 1 <= j2 by A7, MATRIX_0:32;
take i2 ; :: thesis: ex j being Nat st
( [(i2 + 1),j] in Indices G & [i2,j] in Indices G & f /. k = G * ((i2 + 1),j) & f /. (k + 1) = G * (i2,j) )
take j2 ; :: thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) & 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)) `2 <= (G * (i2,j2)) `2 by A8, A10, PSCOMP_1:24;
A17: 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: ( 1 <= i1 & j1 <= width G ) by A5, MATRIX_0:32;
A22: ( 1 <= i2 & j2 <= width G ) by A7, MATRIX_0:32;
now :: thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
per cases ( ( i2 + 1 = i1 & j1 = j2 ) or ( i1 = i2 & j1 + 1 = j2 & k <> 1 ) or ( i1 = i2 & j1 + 1 = j2 & k = 1 ) or ( i1 = i2 & j1 = j2 + 1 ) or ( i2 = i1 + 1 & j1 = j2 ) ) by A9;
suppose ( i2 + 1 = i1 & j1 = j2 ) ; :: thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by A5, A6, A7; :: thesis: verum
end;
suppose A23: ( i1 = i2 & j1 + 1 = j2 & k <> 1 ) ; :: thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
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: 1 <= j3 by A25, MATRIX_0:32;
A34: j1 = j4 by A5, A6, A27, A28, GOBOARD1:5;
A35: ( 1 <= i3 & j3 <= width G ) by A25, MATRIX_0:32;
A36: i3 = i4
proof
assume A37: i3 <> i4 ; :: thesis: contradiction
per cases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A29, A37;
suppose A38: ( j3 = j4 & i4 = i3 + 1 ) ; :: thesis: contradiction
then (G * (i3,j3)) `2 <> S-bound (L~ f) by A1, A18, A24, A25, A26, A27, A28, Th19;
then (G * (1,j3)) `2 <> S-bound (L~ f) by A32, A33, A35, GOBOARD5:1;
then (S-max (L~ f)) `2 <> S-bound (L~ f) by A4, A6, A12, A17, A21, A34, A38, GOBOARD5:1;
hence contradiction by EUCLID:52; :: thesis: verum
end;
suppose A39: ( j3 = j4 & i4 + 1 = i3 ) ; :: thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by A32, A33, A35, GOBOARD5:1
.= (S-max (L~ f)) `2 by A4, A6, A12, A17, A21, A34, A39, GOBOARD5:1
.= S-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in S-most (L~ f) by A14, A26, A31, GOBOARD1:1, SPRECT_2:11;
then (G * (i4,j4)) `1 >= (G * (i3,j3)) `1 by A4, A28, PSCOMP_1:55;
then i4 >= i4 + 1 by A17, A21, A30, A34, A32, A39, GOBOARD5:3;
hence contradiction by NAT_1:13; :: thesis: 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)) `2 <= (G * (i3,j3)) `2 by A10, A26, PSCOMP_1:24;
now :: thesis: contradiction
per cases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A29, A36;
suppose A42: j3 = j4 + 1 ; :: thesis: 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, A34, A36, A42, A43, XBOOLE_0:def 4;
then A44: f /. (k + 1) = f /. k by TARSKI:def 1;
j1 <> j2 by A23;
hence contradiction by A5, A6, A7, A8, A44, GOBOARD1:5; :: thesis: verum
end;
end;
end;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; :: thesis: verum
end;
suppose A45: ( i1 = i2 & j1 + 1 = j2 & k = 1 ) ; :: thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
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;
k9 + 1 <= len f ;
then k9 < len f by NAT_1:13;
then A55: k9 in dom f by A47, FINSEQ_3:25;
then f /. k9 in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2;
then A56: (G * (i1,j1)) `2 <= (G * (i3,j3)) `2 by A10, A49, PSCOMP_1:24;
A57: i3 <= len G by A48, MATRIX_0:32;
A58: j1 = j4 by A5, A6, A45, A53, A50, A51, GOBOARD1:5;
A59: 1 <= j3 by A48, MATRIX_0:32;
A60: ( 1 <= i3 & j3 <= width G ) by A48, MATRIX_0:32;
A61: i3 = i4
proof
assume A62: i3 <> i4 ; :: thesis: contradiction
per cases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A52, A62;
suppose A63: ( j3 = j4 & i4 = i3 + 1 ) ; :: thesis: contradiction
then (G * (i3,j3)) `2 <> S-bound (L~ f) by A1, A47, A48, A49, A50, A51, Th19;
then (G * (1,j3)) `2 <> S-bound (L~ f) by A57, A59, A60, GOBOARD5:1;
then (S-max (L~ f)) `2 <> S-bound (L~ f) by A4, A6, A12, A17, A21, A58, A63, GOBOARD5:1;
hence contradiction by EUCLID:52; :: thesis: verum
end;
suppose A64: ( j3 = j4 & i4 + 1 = i3 ) ; :: thesis: contradiction
(G * (i3,j3)) `2 = (G * (1,j3)) `2 by A57, A59, A60, GOBOARD5:1
.= (S-max (L~ f)) `2 by A4, A6, A12, A17, A21, A58, A64, GOBOARD5:1
.= S-bound (L~ f) by EUCLID:52 ;
then G * (i3,j3) in S-most (L~ f) by A14, A49, A55, GOBOARD1:1, SPRECT_2:11;
then (G * (i4,j4)) `1 >= (G * (i3,j3)) `1 by A4, A45, A53, A51, PSCOMP_1:55;
then i4 >= i4 + 1 by A17, A21, A54, A58, A57, A64, GOBOARD5:3;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;
end;
A65: k9 + 1 = len f ;
now :: thesis: contradiction
per cases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A52, A61;
suppose A66: j3 = j4 + 1 ; :: thesis: 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, A58, A61, A66, A67, XBOOLE_0:def 4;
then A68: f /. (k + 1) = f /. k by TARSKI:def 1;
j1 <> j2 by A45;
hence contradiction by A5, A6, A7, A8, A68, GOBOARD1:5; :: thesis: verum
end;
end;
end;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; :: thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
then j2 >= j2 + 1 by A12, A21, A11, A16, GOBOARD5:4;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by NAT_1:13; :: thesis: verum
end;
suppose A69: ( i2 = i1 + 1 & j1 = j2 ) ; :: thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) )
(G * (i2,j2)) `2 = (G * (1,j2)) `2 by A20, A11, A22, GOBOARD5:1
.= S-bound (L~ f) by A12, A17, A21, A10, A69, GOBOARD5:1 ;
then G * (i2,j2) in S-most (L~ f) by A8, A14, A15, GOBOARD1:1, SPRECT_2:11;
then (G * (i1,j1)) `1 >= (G * (i2,j2)) `1 by A4, A6, PSCOMP_1:55;
then i1 >= i1 + 1 by A17, A21, A20, A69, GOBOARD5:3;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by NAT_1:13; :: thesis: verum
end;
end;
end;
hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; :: thesis: f /. (k + 1) = G * (i2,j2)
thus f /. (k + 1) = G * (i2,j2) by A8; :: thesis: verum