let G be Go-board; :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
( f is standard & f is special )
let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies ( f is standard & f is special ) )
assume A1: f is_sequence_on G ; :: thesis: ( f is standard & f is special )
thus f is_sequence_on GoB f :: according to GOBOARD5:def 5 :: thesis: f is special

proof

set F = GoB f;
thus for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * i,j ) by GOBOARD2:25; :: according to GOBOARD1:def 11 :: thesis: for b₁ being Element of NAT holds
( not b₁ in dom f or not b₁ + 1 in dom f or for b₂, b₃, b₄, b₅ being Element of NAT holds
( not [b₂,b₃] in Indices (GoB f) or not [b₄,b₅] in Indices (GoB f) or not f /. b₁ = (GoB f) * b₂,b₃ or not f /. (b₁ + 1) = (GoB f) * b₄,b₅ or (abs (b₂ - b₄)) + (abs (b₃ - b₅)) = 1 ) )
let n be Element of NAT ; :: thesis: ( not n in dom f or not n + 1 in dom f or for b₁, b₂, b₃, b₄ being Element of NAT holds
( not [b₁,b₂] in Indices (GoB f) or not [b₃,b₄] in Indices (GoB f) or not f /. n = (GoB f) * b₁,b₂ or not f /. (n + 1) = (GoB f) * b₃,b₄ or (abs (b₁ - b₃)) + (abs (b₂ - b₄)) = 1 ) )
assume A2: ( n in dom f & n + 1 in dom f ) ; :: thesis: for b₁, b₂, b₃, b₄ being Element of NAT holds
( not [b₁,b₂] in Indices (GoB f) or not [b₃,b₄] in Indices (GoB f) or not f /. n = (GoB f) * b₁,b₂ or not f /. (n + 1) = (GoB f) * b₃,b₄ or (abs (b₁ - b₃)) + (abs (b₂ - b₄)) = 1 )
let m, k, i, j be Element of NAT ; :: thesis: ( not [m,k] in Indices (GoB f) or not [i,j] in Indices (GoB f) or not f /. n = (GoB f) * m,k or not f /. (n + 1) = (GoB f) * i,j or (abs (m - i)) + (abs (k - j)) = 1 )
assume that
A3: [m,k] in Indices (GoB f) and
A4: [i,j] in Indices (GoB f) and
A5: f /. n = (GoB f) * m,k and
A6: f /. (n + 1) = (GoB f) * i,j ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1
A7: ( 1 <= m & m <= len (GoB f) & 1 <= k & k <= width (GoB f) ) by A3, MATRIX_1:39;
A8: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) ) by A4, MATRIX_1:39;
then A9: ( ((GoB f) * i,j) `1 = ((GoB f) * i,1) `1 & ((GoB f) * i,k) `1 = ((GoB f) * i,1) `1 ) by A7, GOBOARD5:3;
A10: ( ((GoB f) * i,j) `2 = ((GoB f) * 1,j) `2 & ((GoB f) * m,j) `2 = ((GoB f) * 1,j) `2 ) by A7, A8, GOBOARD5:2;
( 1 <= n & n + 1 <= len f ) by A2, FINSEQ_3:27;
then consider i1, j1, i2, j2 being Element of NAT such that
A11: [i1,j1] in Indices G and
A12: f /. n = G * i1,j1 and
A13: [i2,j2] in Indices G and
A14: f /. (n + 1) = G * i2,j2 and
A15: ( ( 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, Th6;
A16: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G ) by A11, MATRIX_1:39;
A17: ( 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A13, MATRIX_1:39;
then A18: ( (G * i1,j1) `1 = (G * i1,1) `1 & (G * i2,j2) `1 = (G * i2,1) `1 ) by A16, GOBOARD5:3;
A19: ( (G * i1,j1) `2 = (G * 1,j1) `2 & (G * i2,j1) `2 = (G * 1,j1) `2 ) by A16, A17, GOBOARD5:2;
A20: ( k + 1 >= 1 & j + 1 >= 1 & m + 1 >= 1 & i + 1 >= 1 ) by NAT_1:12;
A21: ( k + 1 > k & j + 1 > j & m + 1 > m & i + 1 > i ) by NAT_1:13;

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A15;

suppose A22: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

now

assume m <> i ; :: thesis: contradiction
then ( m < i or m > i ) by XXREAL_0:1;
hence contradiction by A5, A6, A7, A8, A9, A12, A14, A18, A22, GOBOARD5:4; :: thesis: verum

end;

then A23: abs (m - i) = 0 by ABSVALUE:7;

now

assume j <= k ; :: thesis: contradiction
then A24: ((GoB f) * i,j) `2 <= ((GoB f) * m,k) `2 by A7, A8, A10, SPRECT_3:24;
j1 < j2 by A22, NAT_1:13;
hence contradiction by A5, A6, A12, A14, A16, A17, A19, A24, GOBOARD5:5; :: thesis: verum

end;

then A25: k + 1 <= j by NAT_1:13;

now

assume A26: k + 1 < j ; :: thesis: contradiction
then A27: k + 1 < width (GoB f) by A8, XXREAL_0:2;
then consider l, i' being Element of NAT such that
A28: l in dom f and
A29: [i',(k + 1)] in Indices (GoB f) and
A30: f /. l = (GoB f) * i',(k + 1) by A20, JORDAN5D:10;
( 1 <= i' & i' <= len (GoB f) ) by A29, MATRIX_1:39;
then A31: ( ((GoB f) * i',(k + 1)) `2 = ((GoB f) * 1,(k + 1)) `2 & ((GoB f) * m,(k + 1)) `2 = ((GoB f) * 1,(k + 1)) `2 ) by A7, A20, A27, GOBOARD5:2;
consider i1', j1' being Element of NAT such that
A32: [i1',j1'] in Indices G and
A33: f /. l = G * i1',j1' by A1, A28, GOBOARD1:def 11;
A34: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A32, MATRIX_1:39;
then A35: ( (G * i1',j1') `2 = (G * 1,j1') `2 & (G * i1',j1) `2 = (G * 1,j1) `2 ) by A16, GOBOARD5:2;
A36: ( (G * i2,j2) `2 = (G * 1,j2) `2 & (G * i1',j2) `2 = (G * 1,j2) `2 ) by A17, A34, GOBOARD5:2;

A37: now

assume j1 >= j1' ; :: thesis: contradiction
then (G * i1',j1') `2 <= (G * i1,j1) `2 by A16, A19, A34, A35, SPRECT_3:24;
hence contradiction by A5, A7, A12, A21, A27, A30, A31, A33, GOBOARD5:5; :: thesis: verum

end;

now

assume j2 <= j1' ; :: thesis: contradiction
then (G * i2,j2) `2 <= (G * i1',j1') `2 by A17, A34, A36, SPRECT_3:24;
hence contradiction by A6, A7, A8, A10, A14, A20, A26, A30, A31, A33, GOBOARD5:5; :: thesis: verum

end;

hence contradiction by A22, A37, NAT_1:13; :: thesis: verum

end;

then k + 1 = j by A25, XXREAL_0:1;
then abs (j - k) = 1 by ABSVALUE:def 1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A23, UNIFORM1:13; :: thesis: verum

end;

suppose A38: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

now

assume k <> j ; :: thesis: contradiction
then ( k < j or k > j ) by XXREAL_0:1;
hence contradiction by A5, A6, A7, A8, A10, A12, A14, A19, A38, GOBOARD5:5; :: thesis: verum

end;

then A39: abs (k - j) = 0 by ABSVALUE:7;

now

assume i <= m ; :: thesis: contradiction
then A40: ((GoB f) * i,j) `1 <= ((GoB f) * m,k) `1 by A7, A8, A9, SPRECT_3:25;
i1 < i2 by A38, NAT_1:13;
hence contradiction by A5, A6, A12, A14, A16, A17, A38, A40, GOBOARD5:4; :: thesis: verum

end;

then A41: m + 1 <= i by NAT_1:13;

now

assume A42: m + 1 < i ; :: thesis: contradiction
then A43: m + 1 < len (GoB f) by A8, XXREAL_0:2;
then consider l, j' being Element of NAT such that
A44: l in dom f and
A45: [(m + 1),j'] in Indices (GoB f) and
A46: f /. l = (GoB f) * (m + 1),j' by A20, JORDAN5D:9;
( 1 <= j' & j' <= width (GoB f) ) by A45, MATRIX_1:39;
then A47: ( ((GoB f) * (m + 1),j') `1 = ((GoB f) * (m + 1),1) `1 & ((GoB f) * (m + 1),k) `1 = ((GoB f) * (m + 1),1) `1 ) by A7, A20, A43, GOBOARD5:3;
consider i1', j1' being Element of NAT such that
A48: [i1',j1'] in Indices G and
A49: f /. l = G * i1',j1' by A1, A44, GOBOARD1:def 11;
A50: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A48, MATRIX_1:39;
then A51: ( (G * i1',j1') `1 = (G * i1',1) `1 & (G * i1,j1') `1 = (G * i1,1) `1 ) by A16, GOBOARD5:3;
A52: ( (G * i2,j2) `1 = (G * i2,1) `1 & (G * i2,j1') `1 = (G * i2,1) `1 ) by A17, A50, GOBOARD5:3;

A53: now

assume i1 >= i1' ; :: thesis: contradiction
then (G * i1',j1') `1 <= (G * i1,j1) `1 by A16, A18, A50, A51, SPRECT_3:25;
hence contradiction by A5, A7, A12, A21, A43, A46, A47, A49, GOBOARD5:4; :: thesis: verum

end;

now

assume i2 <= i1' ; :: thesis: contradiction
then (G * i2,j2) `1 <= (G * i1',j1') `1 by A17, A50, A52, SPRECT_3:25;
hence contradiction by A6, A7, A8, A9, A14, A20, A42, A46, A47, A49, GOBOARD5:4; :: thesis: verum

end;

hence contradiction by A38, A53, NAT_1:13; :: thesis: verum

end;

then m + 1 = i by A41, XXREAL_0:1;
then abs (i - m) = 1 by ABSVALUE:def 1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A39, UNIFORM1:13; :: thesis: verum

end;

suppose A54: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

now

assume k <> j ; :: thesis: contradiction
then ( k < j or k > j ) by XXREAL_0:1;
hence contradiction by A5, A6, A7, A8, A10, A12, A14, A19, A54, GOBOARD5:5; :: thesis: verum

end;

then A55: abs (k - j) = 0 by ABSVALUE:7;

now

assume m <= i ; :: thesis: contradiction
then A56: ((GoB f) * i,j) `1 >= ((GoB f) * m,k) `1 by A7, A8, A9, SPRECT_3:25;
i1 > i2 by A54, NAT_1:13;
hence contradiction by A5, A6, A12, A14, A16, A17, A54, A56, GOBOARD5:4; :: thesis: verum

end;

then A57: i + 1 <= m by NAT_1:13;

now

assume A58: i + 1 < m ; :: thesis: contradiction
then A59: i + 1 < len (GoB f) by A7, XXREAL_0:2;
then consider l, j' being Element of NAT such that
A60: l in dom f and
A61: [(i + 1),j'] in Indices (GoB f) and
A62: f /. l = (GoB f) * (i + 1),j' by A20, JORDAN5D:9;
( 1 <= j' & j' <= width (GoB f) ) by A61, MATRIX_1:39;
then A63: ( ((GoB f) * (i + 1),j') `1 = ((GoB f) * (i + 1),1) `1 & ((GoB f) * (i + 1),j) `1 = ((GoB f) * (i + 1),j) `1 ) by A20, A59, GOBOARD5:3;
A64: ( ((GoB f) * (i + 1),k) `1 = ((GoB f) * (i + 1),1) `1 & ((GoB f) * (i + 1),j) `1 = ((GoB f) * (i + 1),1) `1 ) by A7, A8, A20, A59, GOBOARD5:3;
consider i1', j1' being Element of NAT such that
A65: [i1',j1'] in Indices G and
A66: f /. l = G * i1',j1' by A1, A60, GOBOARD1:def 11;
A67: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A65, MATRIX_1:39;
then A68: ( (G * i1',j1') `1 = (G * i1',1) `1 & (G * i1,j1') `1 = (G * i1,1) `1 ) by A16, GOBOARD5:3;
A69: ( (G * i2,j2) `1 = (G * i2,1) `1 & (G * i2,j1') `1 = (G * i2,1) `1 ) by A17, A67, GOBOARD5:3;

A70: now

assume i2 >= i1' ; :: thesis: contradiction
then (G * i1',j1') `1 <= (G * i2,j2) `1 by A17, A67, A69, SPRECT_3:25;
hence contradiction by A6, A8, A14, A21, A59, A62, A63, A64, A66, GOBOARD5:4; :: thesis: verum

end;

now

assume i1 <= i1' ; :: thesis: contradiction
then (G * i1,j1) `1 <= (G * i1',j1') `1 by A16, A18, A67, A68, SPRECT_3:25;
hence contradiction by A5, A7, A12, A20, A58, A62, A63, A64, A66, GOBOARD5:4; :: thesis: verum

end;

hence contradiction by A54, A70, NAT_1:13; :: thesis: verum

end;

then i + 1 = m by A57, XXREAL_0:1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A55, ABSVALUE:def 1; :: thesis: verum

end;

suppose A71: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: (abs (m - i)) + (abs (k - j)) = 1

now

assume m <> i ; :: thesis: contradiction
then ( m < i or m > i ) by XXREAL_0:1;
hence contradiction by A5, A6, A7, A8, A9, A12, A14, A18, A71, GOBOARD5:4; :: thesis: verum

end;

then A72: abs (m - i) = 0 by ABSVALUE:7;

now

assume j >= k ; :: thesis: contradiction
then A73: ((GoB f) * i,j) `2 >= ((GoB f) * m,k) `2 by A7, A8, A10, SPRECT_3:24;
j1 > j2 by A71, NAT_1:13;
hence contradiction by A5, A6, A12, A14, A16, A17, A19, A73, GOBOARD5:5; :: thesis: verum

end;

then A74: j + 1 <= k by NAT_1:13;

now

assume A75: j + 1 < k ; :: thesis: contradiction
then A76: j + 1 < width (GoB f) by A7, XXREAL_0:2;
then consider l, i' being Element of NAT such that
A77: l in dom f and
A78: [i',(j + 1)] in Indices (GoB f) and
A79: f /. l = (GoB f) * i',(j + 1) by A20, JORDAN5D:10;
( 1 <= i' & i' <= len (GoB f) ) by A78, MATRIX_1:39;
then A80: ( ((GoB f) * i',(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 & ((GoB f) * i,(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 ) by A8, A20, A76, GOBOARD5:2;
A81: ( ((GoB f) * m,(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 & ((GoB f) * i,(j + 1)) `2 = ((GoB f) * 1,(j + 1)) `2 ) by A7, A8, A20, A76, GOBOARD5:2;
consider i1', j1' being Element of NAT such that
A82: [i1',j1'] in Indices G and
A83: f /. l = G * i1',j1' by A1, A77, GOBOARD1:def 11;
A84: ( 1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G ) by A82, MATRIX_1:39;
then A85: ( (G * i1',j1') `2 = (G * 1,j1') `2 & (G * i1',j1) `2 = (G * 1,j1) `2 ) by A16, GOBOARD5:2;
A86: ( (G * i2,j2) `2 = (G * 1,j2) `2 & (G * i1',j2) `2 = (G * 1,j2) `2 ) by A17, A84, GOBOARD5:2;

A87: now

assume j2 >= j1' ; :: thesis: contradiction
then (G * i1',j1') `2 <= (G * i2,j2) `2 by A17, A84, A86, SPRECT_3:24;
hence contradiction by A6, A8, A14, A21, A76, A79, A80, A83, GOBOARD5:5; :: thesis: verum

end;

now

assume j1 <= j1' ; :: thesis: contradiction
then (G * i1,j1) `2 <= (G * i1',j1') `2 by A16, A19, A84, A85, SPRECT_3:24;
hence contradiction by A5, A7, A12, A20, A75, A79, A80, A81, A83, GOBOARD5:5; :: thesis: verum

end;

hence contradiction by A71, A87, NAT_1:13; :: thesis: verum

end;

then j + 1 = k by A74, XXREAL_0:1;
hence (abs (m - i)) + (abs (k - j)) = 1 by A72, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

thus f is special :: thesis: verum

proof

let i be Nat; :: according to TOPREAL1:def 7 :: thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
A88: i in NAT by ORDINAL1:def 13;
assume ( 1 <= i & i + 1 <= len f ) ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
then consider i1, j1, i2, j2 being Element of NAT such that
A89: [i1,j1] in Indices G and
A90: f /. i = G * i1,j1 and
A91: [i2,j2] in Indices G and
A92: f /. (i + 1) = G * i2,j2 and
A93: ( ( 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, A88, Th6;
( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A89, A91, MATRIX_1:39;
then ( (G * i1,j1) `2 = (G * 1,j1) `2 & (G * i2,j1) `2 = (G * 1,j1) `2 & (G * i1,j2) `2 = (G * 1,j2) `2 & (G * i2,j2) `2 = (G * 1,j2) `2 & (G * i1,j1) `1 = (G * i1,1) `1 & (G * i1,j2) `1 = (G * i1,1) `1 & (G * i2,j1) `1 = (G * i2,1) `1 & (G * i2,j2) `1 = (G * i2,1) `1 ) by GOBOARD5:2, GOBOARD5:3;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A90, A92, A93; :: thesis: verum

end;