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 Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) by GOBOARD2:14; :: according to GOBOARD1:def 9 :: thesis: for b₁ being set holds
( not b₁ in dom f or not b₁ + 1 in dom f or for b₂, b₃, b₄, b₅ being set 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 |.(b₂ - b₄).| + |.(b₃ - b₅).| = 1 ) )
let n be Nat; :: thesis: ( not n in dom f or not n + 1 in dom f or for b₁, b₂, b₃, b₄ being set 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 |.(b₁ - b₃).| + |.(b₂ - b₄).| = 1 ) )
assume that
A2: n in dom f and
A3: n + 1 in dom f ; :: thesis: for b₁, b₂, b₃, b₄ being set 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 |.(b₁ - b₃).| + |.(b₂ - b₄).| = 1 )
let m, k, i, j be 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 |.(m - i).| + |.(k - j).| = 1 )
assume that
A4: [m,k] in Indices (GoB f) and
A5: [i,j] in Indices (GoB f) and
A6: f /. n = (GoB f) * (m,k) and
A7: f /. (n + 1) = (GoB f) * (i,j) ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A8: 1 <= m by A4, MATRIX_0:32;
A9: m <= len (GoB f) by A4, MATRIX_0:32;
A10: 1 <= k by A4, MATRIX_0:32;
A11: k <= width (GoB f) by A4, MATRIX_0:32;
A12: 1 <= i by A5, MATRIX_0:32;
A13: i <= len (GoB f) by A5, MATRIX_0:32;
A14: 1 <= j by A5, MATRIX_0:32;
A15: j <= width (GoB f) by A5, MATRIX_0:32;
then A16: ((GoB f) * (i,j)) `1 = ((GoB f) * (i,1)) `1 by A12, A13, A14, GOBOARD5:2;
A17: ((GoB f) * (i,k)) `1 = ((GoB f) * (i,1)) `1 by A10, A11, A12, A13, GOBOARD5:2;
A18: ((GoB f) * (i,j)) `2 = ((GoB f) * (1,j)) `2 by A12, A13, A14, A15, GOBOARD5:1;
A19: ((GoB f) * (m,j)) `2 = ((GoB f) * (1,j)) `2 by A8, A9, A14, A15, GOBOARD5:1;
A20: 1 <= n by A2, FINSEQ_3:25;
n + 1 <= len f by A3, FINSEQ_3:25;
then consider i1, j1, i2, j2 being Nat such that
A21: [i1,j1] in Indices G and
A22: f /. n = G * (i1,j1) and
A23: [i2,j2] in Indices G and
A24: f /. (n + 1) = G * (i2,j2) and
A25: ( ( 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, A20, Th3;
A26: 1 <= i1 by A21, MATRIX_0:32;
A27: i1 <= len G by A21, MATRIX_0:32;
A28: 1 <= j1 by A21, MATRIX_0:32;
A29: j1 <= width G by A21, MATRIX_0:32;
A30: 1 <= i2 by A23, MATRIX_0:32;
A31: i2 <= len G by A23, MATRIX_0:32;
A32: 1 <= j2 by A23, MATRIX_0:32;
A33: j2 <= width G by A23, MATRIX_0:32;
A34: (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A26, A27, A28, A29, GOBOARD5:2;
A35: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A30, A31, A32, A33, GOBOARD5:2;
A36: (G * (i1,j1)) `2 = (G * (1,j1)) `2 by A26, A27, A28, A29, GOBOARD5:1;
A37: (G * (i2,j1)) `2 = (G * (1,j1)) `2 by A28, A29, A30, A31, GOBOARD5:1;
A38: k + 1 >= 1 by NAT_1:12;
A39: j + 1 >= 1 by NAT_1:12;
A40: m + 1 >= 1 by NAT_1:12;
A41: i + 1 >= 1 by NAT_1:12;
A42: k + 1 > k by NAT_1:13;
A43: j + 1 > j by NAT_1:13;
A44: m + 1 > m by NAT_1:13;
A45: 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 A25;

suppose A46: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

now :: thesis: not m <> i

assume m <> i ; :: thesis: contradiction
then ( m < i or m > i ) by XXREAL_0:1;
hence contradiction by A6, A7, A8, A9, A10, A11, A12, A13, A16, A17, A22, A24, A34, A35, A46, GOBOARD5:3; :: thesis: verum

end;

then A47: |.(m - i).| = 0 by ABSVALUE:2;

now :: thesis: not j <= k

assume j <= k ; :: thesis: contradiction
then A48: ((GoB f) * (i,j)) `2 <= ((GoB f) * (m,k)) `2 by A8, A9, A11, A14, A18, A19, SPRECT_3:12;
j1 < j2 by A46, NAT_1:13;
hence contradiction by A6, A7, A22, A24, A28, A30, A31, A33, A36, A37, A48, GOBOARD5:4; :: thesis: verum

end;

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

now :: thesis: not k + 1 < j

assume A50: k + 1 < j ; :: thesis: contradiction
then A51: k + 1 < width (GoB f) by A15, XXREAL_0:2;
then consider l, i9 being Nat such that
A52: l in dom f and
A53: [i9,(k + 1)] in Indices (GoB f) and
A54: f /. l = (GoB f) * (i9,(k + 1)) by JORDAN5D:8, NAT_1:12;
A55: 1 <= i9 by A53, MATRIX_0:32;
i9 <= len (GoB f) by A53, MATRIX_0:32;
then A56: ((GoB f) * (i9,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2 by A38, A51, A55, GOBOARD5:1;
A57: ((GoB f) * (m,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2 by A8, A9, A38, A51, GOBOARD5:1;
consider i19, j19 being Nat such that
A58: [i19,j19] in Indices G and
A59: f /. l = G * (i19,j19) by A1, A52;
A60: 1 <= i19 by A58, MATRIX_0:32;
A61: i19 <= len G by A58, MATRIX_0:32;
A62: 1 <= j19 by A58, MATRIX_0:32;
A63: j19 <= width G by A58, MATRIX_0:32;
A64: (G * (i19,j1)) `2 = (G * (1,j1)) `2 by A28, A29, A60, A61, GOBOARD5:1;
A65: (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A30, A31, A32, A33, GOBOARD5:1;
A66: (G * (i19,j2)) `2 = (G * (1,j2)) `2 by A32, A33, A60, A61, GOBOARD5:1;

A67: now :: thesis: not j1 >= j19

assume j1 >= j19 ; :: thesis: contradiction
then (G * (i19,j19)) `2 <= (G * (i1,j1)) `2 by A29, A36, A60, A61, A62, A64, SPRECT_3:12;
hence contradiction by A6, A8, A9, A10, A22, A42, A51, A54, A56, A57, A59, GOBOARD5:4; :: thesis: verum

end;

now :: thesis: not j2 <= j19

assume j2 <= j19 ; :: thesis: contradiction
then (G * (i2,j2)) `2 <= (G * (i19,j19)) `2 by A32, A60, A61, A63, A65, A66, SPRECT_3:12;
hence contradiction by A7, A8, A9, A15, A18, A19, A24, A38, A50, A54, A56, A57, A59, GOBOARD5:4; :: thesis: verum

end;

hence contradiction by A46, A67, NAT_1:13; :: thesis: verum

end;

then k + 1 = j by A49, XXREAL_0:1;
then |.(j - k).| = 1 by ABSVALUE:def 1;
hence |.(m - i).| + |.(k - j).| = 1 by A47, UNIFORM1:11; :: thesis: verum

end;

suppose A68: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

now :: thesis: not k <> j

assume k <> j ; :: thesis: contradiction
then ( k < j or k > j ) by XXREAL_0:1;
hence contradiction by A6, A7, A8, A9, A10, A11, A14, A15, A18, A19, A22, A24, A36, A37, A68, GOBOARD5:4; :: thesis: verum

end;

then A69: |.(k - j).| = 0 by ABSVALUE:2;

now :: thesis: not i <= m

assume i <= m ; :: thesis: contradiction
then A70: ((GoB f) * (i,j)) `1 <= ((GoB f) * (m,k)) `1 by A9, A10, A11, A12, A16, A17, SPRECT_3:13;
i1 < i2 by A68, NAT_1:13;
hence contradiction by A6, A7, A22, A24, A26, A28, A29, A31, A68, A70, GOBOARD5:3; :: thesis: verum

end;

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

now :: thesis: not m + 1 < i

assume A72: m + 1 < i ; :: thesis: contradiction
then A73: m + 1 < len (GoB f) by A13, XXREAL_0:2;
then consider l, j9 being Nat such that
A74: l in dom f and
A75: [(m + 1),j9] in Indices (GoB f) and
A76: f /. l = (GoB f) * ((m + 1),j9) by JORDAN5D:7, NAT_1:12;
A77: 1 <= j9 by A75, MATRIX_0:32;
j9 <= width (GoB f) by A75, MATRIX_0:32;
then A78: ((GoB f) * ((m + 1),j9)) `1 = ((GoB f) * ((m + 1),1)) `1 by A40, A73, A77, GOBOARD5:2;
A79: ((GoB f) * ((m + 1),k)) `1 = ((GoB f) * ((m + 1),1)) `1 by A10, A11, A40, A73, GOBOARD5:2;
consider i19, j19 being Nat such that
A80: [i19,j19] in Indices G and
A81: f /. l = G * (i19,j19) by A1, A74;
A82: 1 <= i19 by A80, MATRIX_0:32;
A83: i19 <= len G by A80, MATRIX_0:32;
A84: 1 <= j19 by A80, MATRIX_0:32;
A85: j19 <= width G by A80, MATRIX_0:32;
then A86: (G * (i1,j19)) `1 = (G * (i1,1)) `1 by A26, A27, A84, GOBOARD5:2;
A87: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A30, A31, A32, A33, GOBOARD5:2;
A88: (G * (i2,j19)) `1 = (G * (i2,1)) `1 by A30, A31, A84, A85, GOBOARD5:2;

A89: now :: thesis: not i1 >= i19

assume i1 >= i19 ; :: thesis: contradiction
then (G * (i19,j19)) `1 <= (G * (i1,j1)) `1 by A27, A34, A82, A84, A85, A86, SPRECT_3:13;
hence contradiction by A6, A8, A10, A11, A22, A44, A73, A76, A78, A79, A81, GOBOARD5:3; :: thesis: verum

end;

now :: thesis: not i2 <= i19

assume i2 <= i19 ; :: thesis: contradiction
then (G * (i2,j2)) `1 <= (G * (i19,j19)) `1 by A30, A83, A84, A85, A87, A88, SPRECT_3:13;
hence contradiction by A7, A10, A11, A13, A16, A17, A24, A40, A72, A76, A78, A79, A81, GOBOARD5:3; :: thesis: verum

end;

hence contradiction by A68, A89, NAT_1:13; :: thesis: verum

end;

then m + 1 = i by A71, XXREAL_0:1;
then |.(i - m).| = 1 by ABSVALUE:def 1;
hence |.(m - i).| + |.(k - j).| = 1 by A69, UNIFORM1:11; :: thesis: verum

end;

suppose A90: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

now :: thesis: not k <> j

assume k <> j ; :: thesis: contradiction
then ( k < j or k > j ) by XXREAL_0:1;
hence contradiction by A6, A7, A8, A9, A10, A11, A14, A15, A18, A19, A22, A24, A36, A37, A90, GOBOARD5:4; :: thesis: verum

end;

then A91: |.(k - j).| = 0 by ABSVALUE:2;

now :: thesis: not m <= i

assume m <= i ; :: thesis: contradiction
then A92: ((GoB f) * (i,j)) `1 >= ((GoB f) * (m,k)) `1 by A8, A10, A11, A13, A16, A17, SPRECT_3:13;
i1 > i2 by A90, NAT_1:13;
hence contradiction by A6, A7, A22, A24, A27, A28, A29, A30, A90, A92, GOBOARD5:3; :: thesis: verum

end;

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

now :: thesis: not i + 1 < m

assume A94: i + 1 < m ; :: thesis: contradiction
then A95: i + 1 < len (GoB f) by A9, XXREAL_0:2;
then consider l, j9 being Nat such that
A96: l in dom f and
A97: [(i + 1),j9] in Indices (GoB f) and
A98: f /. l = (GoB f) * ((i + 1),j9) by JORDAN5D:7, NAT_1:12;
A99: 1 <= j9 by A97, MATRIX_0:32;
j9 <= width (GoB f) by A97, MATRIX_0:32;
then A100: ((GoB f) * ((i + 1),j9)) `1 = ((GoB f) * ((i + 1),1)) `1 by A41, A95, A99, GOBOARD5:2;
A101: ((GoB f) * ((i + 1),k)) `1 = ((GoB f) * ((i + 1),1)) `1 by A10, A11, A41, A95, GOBOARD5:2;
A102: ((GoB f) * ((i + 1),j)) `1 = ((GoB f) * ((i + 1),1)) `1 by A14, A15, A41, A95, GOBOARD5:2;
consider i19, j19 being Nat such that
A103: [i19,j19] in Indices G and
A104: f /. l = G * (i19,j19) by A1, A96;
A105: 1 <= i19 by A103, MATRIX_0:32;
A106: i19 <= len G by A103, MATRIX_0:32;
A107: 1 <= j19 by A103, MATRIX_0:32;
A108: j19 <= width G by A103, MATRIX_0:32;
then A109: (G * (i1,j19)) `1 = (G * (i1,1)) `1 by A26, A27, A107, GOBOARD5:2;
A110: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A30, A31, A32, A33, GOBOARD5:2;
A111: (G * (i2,j19)) `1 = (G * (i2,1)) `1 by A30, A31, A107, A108, GOBOARD5:2;

A112: now :: thesis: not i2 >= i19

assume i2 >= i19 ; :: thesis: contradiction
then (G * (i19,j19)) `1 <= (G * (i2,j2)) `1 by A31, A105, A107, A108, A110, A111, SPRECT_3:13;
hence contradiction by A7, A12, A14, A15, A24, A45, A95, A98, A100, A102, A104, GOBOARD5:3; :: thesis: verum

end;

now :: thesis: not i1 <= i19

assume i1 <= i19 ; :: thesis: contradiction
then (G * (i1,j1)) `1 <= (G * (i19,j19)) `1 by A26, A34, A106, A107, A108, A109, SPRECT_3:13;
hence contradiction by A6, A9, A10, A11, A22, A41, A94, A98, A100, A101, A104, GOBOARD5:3; :: thesis: verum

end;

hence contradiction by A90, A112, NAT_1:13; :: thesis: verum

end;

then i + 1 = m by A93, XXREAL_0:1;
hence |.(m - i).| + |.(k - j).| = 1 by A91, ABSVALUE:def 1; :: thesis: verum

end;

suppose A113: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

now :: thesis: not m <> i

assume m <> i ; :: thesis: contradiction
then ( m < i or m > i ) by XXREAL_0:1;
hence contradiction by A6, A7, A8, A9, A10, A11, A12, A13, A16, A17, A22, A24, A34, A35, A113, GOBOARD5:3; :: thesis: verum

end;

then A114: |.(m - i).| = 0 by ABSVALUE:2;

now :: thesis: not j >= k

assume j >= k ; :: thesis: contradiction
then A115: ((GoB f) * (i,j)) `2 >= ((GoB f) * (m,k)) `2 by A8, A9, A10, A15, A18, A19, SPRECT_3:12;
j1 > j2 by A113, NAT_1:13;
hence contradiction by A6, A7, A22, A24, A29, A30, A31, A32, A36, A37, A115, GOBOARD5:4; :: thesis: verum

end;

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

now :: thesis: not j + 1 < k

assume A117: j + 1 < k ; :: thesis: contradiction
then A118: j + 1 < width (GoB f) by A11, XXREAL_0:2;
then consider l, i9 being Nat such that
A119: l in dom f and
A120: [i9,(j + 1)] in Indices (GoB f) and
A121: f /. l = (GoB f) * (i9,(j + 1)) by JORDAN5D:8, NAT_1:12;
A122: 1 <= i9 by A120, MATRIX_0:32;
i9 <= len (GoB f) by A120, MATRIX_0:32;
then A123: ((GoB f) * (i9,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A39, A118, A122, GOBOARD5:1;
A124: ((GoB f) * (i,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A12, A13, A39, A118, GOBOARD5:1;
A125: ((GoB f) * (m,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A8, A9, A39, A118, GOBOARD5:1;
consider i19, j19 being Nat such that
A126: [i19,j19] in Indices G and
A127: f /. l = G * (i19,j19) by A1, A119;
A128: 1 <= i19 by A126, MATRIX_0:32;
A129: i19 <= len G by A126, MATRIX_0:32;
A130: 1 <= j19 by A126, MATRIX_0:32;
A131: j19 <= width G by A126, MATRIX_0:32;
A132: (G * (i19,j1)) `2 = (G * (1,j1)) `2 by A28, A29, A128, A129, GOBOARD5:1;
A133: (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A30, A31, A32, A33, GOBOARD5:1;
A134: (G * (i19,j2)) `2 = (G * (1,j2)) `2 by A32, A33, A128, A129, GOBOARD5:1;

A135: now :: thesis: not j2 >= j19

assume j2 >= j19 ; :: thesis: contradiction
then (G * (i19,j19)) `2 <= (G * (i2,j2)) `2 by A33, A128, A129, A130, A133, A134, SPRECT_3:12;
hence contradiction by A7, A12, A13, A14, A24, A43, A118, A121, A123, A124, A127, GOBOARD5:4; :: thesis: verum

end;

now :: thesis: not j1 <= j19

assume j1 <= j19 ; :: thesis: contradiction
then (G * (i1,j1)) `2 <= (G * (i19,j19)) `2 by A28, A36, A128, A129, A131, A132, SPRECT_3:12;
hence contradiction by A6, A8, A9, A11, A22, A39, A117, A121, A123, A125, A127, GOBOARD5:4; :: thesis: verum

end;

hence contradiction by A113, A135, NAT_1:13; :: thesis: verum

end;

then j + 1 = k by A116, XXREAL_0:1;
hence |.(m - i).| + |.(k - j).| = 1 by A114, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

thus f is special :: thesis: verum

proof

let i be Nat; :: according to TOPREAL1:def 5 :: 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 )
assume that
A136: 1 <= i and
A137: i + 1 <= len f ; :: thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
consider i1, j1, i2, j2 being Nat such that
A138: [i1,j1] in Indices G and
A139: f /. i = G * (i1,j1) and
A140: [i2,j2] in Indices G and
A141: f /. (i + 1) = G * (i2,j2) and
A142: ( ( 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, A136, A137, Th3;
A143: 1 <= i1 by A138, MATRIX_0:32;
A144: i1 <= len G by A138, MATRIX_0:32;
A145: 1 <= j1 by A138, MATRIX_0:32;
A146: j1 <= width G by A138, MATRIX_0:32;
A147: 1 <= i2 by A140, MATRIX_0:32;
A148: i2 <= len G by A140, MATRIX_0:32;
A149: 1 <= j2 by A140, MATRIX_0:32;
A150: j2 <= width G by A140, MATRIX_0:32;
A151: (G * (i1,j1)) `2 = (G * (1,j1)) `2 by A143, A144, A145, A146, GOBOARD5:1;
(G * (i1,j1)) `1 = (G * (i1,1)) `1 by A143, A144, A145, A146, GOBOARD5:2;
hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A139, A141, A142, A147, A148, A149, A150, A151, GOBOARD5:1, GOBOARD5:2; :: thesis: verum

end;