let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: for G being Go-board
for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds
ex i, j being Element of 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 Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds
ex i, j being Element of 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 Element of NAT ; :: thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) implies ex i, j being Element of 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 & k + 1 <= len f ) and
A3: f /. k = S-max (L~ f) ; :: thesis: ex i, j being Element of 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 Element of NAT such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * i1,j1 and
A6: [i2,j2] in Indices G and
A7: f /. (k + 1) = G * i2,j2 and
A8: ( ( 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, JORDAN8:6;
A9: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G ) by A4, MATRIX_1:39;
A10: ( 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A6, MATRIX_1:39;
A11: (G * i1,j1) `2 = S-bound (L~ f) by A3, A5, EUCLID:56;
A12: k + 1 >= 1 + 1 by A2, XREAL_1:9;
then A13: len f >= 2 by A2, XXREAL_0:2;
k + 1 >= 1 by NAT_1:11;
then A14: k + 1 in dom f by A2, FINSEQ_3:27;
then f /. (k + 1) in L~ f by A2, A12, GOBOARD1:16, XXREAL_0:2;
then A15: (G * i1,j1) `2 <= (G * i2,j2) `2 by A7, A11, PSCOMP_1:71;
reconsider f1 = f as non trivial FinSequence of (TOP-REAL 2) ;
take i2 ; :: thesis: ex j being Element of 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 )
A16: k < len f by A2, NAT_1:13;
then A17: k in dom f by A2, FINSEQ_3:27;
now
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 A8;
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 A4, A5, A6; :: thesis: verum
end;
suppose A18: ( 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 k' = k - 1 as Element of NAT by A17, FINSEQ_3:28;
k > 1 by A2, A18, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then A19: k' >= (1 + 1) - 1 by XREAL_1:11;
A20: k' + 1 < len f by A2, NAT_1:13;
consider i3, j3, i4, j4 being Element of NAT such that
A21: [i3,j3] in Indices G and
A22: f /. k' = G * i3,j3 and
A23: [i4,j4] in Indices G and
A24: f /. (k' + 1) = G * i4,j4 and
A25: ( ( 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, A16, A19, JORDAN8:6;
A26: k' + 1 = k ;
A27: ( i1 = i4 & j1 = j4 ) by A4, A5, A23, A24, GOBOARD1:21;
A28: ( 1 <= i3 & i3 <= len G & 1 <= j3 & j3 <= width G ) by A21, MATRIX_1:39;
k' < len f by A20, NAT_1:13;
then A29: k' in dom f by A19, FINSEQ_3:27;
then f /. k' in L~ f by A2, A12, GOBOARD1:16, XXREAL_0:2;
then A30: (G * i1,j1) `2 <= (G * i3,j3) `2 by A11, A22, PSCOMP_1:71;
A31: i3 = i4
proof
assume A32: i3 <> i4 ; :: thesis: contradiction
per cases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A25, A32;
suppose A33: ( j3 = j4 & i4 = i3 + 1 ) ; :: thesis: contradiction
then (G * i3,j3) `2 <> S-bound (L~ f) by A1, A16, A19, A21, A22, A23, A24, Th21;
then (G * 1,j3) `2 <> S-bound (L~ f) by A28, GOBOARD5:2;
then (S-max (L~ f)) `2 <> S-bound (L~ f) by A3, A5, A9, A27, A33, GOBOARD5:2;
hence contradiction by EUCLID:56; :: thesis: verum
end;
suppose A34: ( j3 = j4 & i4 + 1 = i3 ) ; :: thesis: contradiction
(G * i3,j3) `2 = (G * 1,j3) `2 by A28, GOBOARD5:2
.= (S-max (L~ f)) `2 by A3, A5, A9, A27, A34, GOBOARD5:2
.= S-bound (L~ f) by EUCLID:56 ;
then ( G * i3,j3 in S-most (L~ f) & L~ f = L~ f1 ) by A13, A22, A29, GOBOARD1:16, SPRECT_2:15;
then (G * i4,j4) `1 >= (G * i3,j3) `1 by A3, A24, PSCOMP_1:118;
then i4 >= i4 + 1 by A9, A27, A28, A34, GOBOARD5:4;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;
end;
now
per cases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A25, A31;
suppose A35: j3 = j4 + 1 ; :: thesis: contradiction
k' + (1 + 1) <= len f by A2;
then A36: (LSeg f,k') /\ (LSeg f,k) = {(f /. k)} by A19, A26, TOPREAL1:def 8;
A37: j1 <> j2 by A18;
( f /. k' in LSeg f,k' & f /. (k + 1) in LSeg f,k ) by A2, A16, A19, A26, TOPREAL1:27;
then f /. (k + 1) in {(f /. k)} by A7, A18, A22, A27, A31, A35, A36, XBOOLE_0:def 4;
then f /. (k + 1) = f /. k by TARSKI:def 1;
hence contradiction by A4, A5, A6, A7, A37, GOBOARD1:21; :: 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 A38: ( 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;
A39: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
k < len f by A2, NAT_1:13;
then A40: len f > 1 + 0 by A2, XXREAL_0:2;
then len f in dom f by FINSEQ_3:27;
then reconsider k' = (len f) - 1 as Element of NAT by FINSEQ_3:28;
k + 1 >= 1 + 1 by A2, XREAL_1:9;
then len f >= 1 + 1 by A2, XXREAL_0:2;
then A41: k' >= (1 + 1) - 1 by XREAL_1:11;
A42: k' + 1 <= len f ;
consider i3, j3, i4, j4 being Element of NAT such that
A43: [i3,j3] in Indices G and
A44: f /. k' = G * i3,j3 and
A45: [i4,j4] in Indices G and
A46: f /. (k' + 1) = G * i4,j4 and
A47: ( ( 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, A41, JORDAN8:6;
A48: k' + 1 = len f ;
A49: ( i1 = i4 & j1 = j4 ) by A4, A5, A38, A39, A45, A46, GOBOARD1:21;
A50: ( 1 <= i3 & i3 <= len G & 1 <= j3 & j3 <= width G ) by A43, MATRIX_1:39;
k' < len f by A42, NAT_1:13;
then A51: k' in dom f by A41, FINSEQ_3:27;
then f /. k' in L~ f by A2, A12, GOBOARD1:16, XXREAL_0:2;
then A52: (G * i1,j1) `2 <= (G * i3,j3) `2 by A11, A44, PSCOMP_1:71;
A53: i3 = i4
proof
assume A54: i3 <> i4 ; :: thesis: contradiction
per cases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A47, A54;
suppose A55: ( j3 = j4 & i4 = i3 + 1 ) ; :: thesis: contradiction
then (G * i3,j3) `2 <> S-bound (L~ f) by A1, A41, A43, A44, A45, A46, Th21;
then (G * 1,j3) `2 <> S-bound (L~ f) by A50, GOBOARD5:2;
then (S-max (L~ f)) `2 <> S-bound (L~ f) by A3, A5, A9, A49, A55, GOBOARD5:2;
hence contradiction by EUCLID:56; :: thesis: verum
end;
suppose A56: ( j3 = j4 & i4 + 1 = i3 ) ; :: thesis: contradiction
(G * i3,j3) `2 = (G * 1,j3) `2 by A50, GOBOARD5:2
.= (S-max (L~ f)) `2 by A3, A5, A9, A49, A56, GOBOARD5:2
.= S-bound (L~ f) by EUCLID:56 ;
then ( G * i3,j3 in S-most (L~ f) & L~ f = L~ f1 ) by A13, A44, A51, GOBOARD1:16, SPRECT_2:15;
then (G * i4,j4) `1 >= (G * i3,j3) `1 by A3, A38, A39, A46, PSCOMP_1:118;
then i4 >= i4 + 1 by A9, A49, A50, A56, GOBOARD5:4;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;
end;
now
per cases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A47, A53;
suppose A57: j3 = j4 + 1 ; :: thesis: contradiction
(len f) - 1 >= 0 by A40, XREAL_1:21;
then (len f) -' 1 = (len f) - 1 by XREAL_0:def 2;
then A58: (LSeg f,k) /\ (LSeg f,k') = {(f . k)} by A38, JORDAN4:54
.= {(f /. k)} by A17, PARTFUN1:def 8 ;
A59: j1 <> j2 by A38;
( f /. k' in LSeg f,k' & f /. (k + 1) in LSeg f,k ) by A2, A41, A48, TOPREAL1:27;
then f /. (k + 1) in {(f /. k)} by A7, A38, A44, A49, A53, A57, A58, XBOOLE_0:def 4;
then f /. (k + 1) = f /. k by TARSKI:def 1;
hence contradiction by A4, A5, A6, A7, A59, GOBOARD1:21; :: 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 A9, A10, A15, GOBOARD5:5;
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 A60: ( 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 A10, GOBOARD5:2
.= S-bound (L~ f) by A9, A11, A60, GOBOARD5:2 ;
then ( G * i2,j2 in S-most (L~ f) & L~ f = L~ f1 ) by A7, A13, A14, GOBOARD1:16, SPRECT_2:15;
then (G * i1,j1) `1 >= (G * i2,j2) `1 by A3, A5, PSCOMP_1:118;
then i1 >= i1 + 1 by A9, A10, A60, 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;
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 A7; :: thesis: verum