let G be Go-board; 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); ( f is_sequence_on G implies ( f is standard & f is special ) )
assume A1:
f is_sequence_on G
; ( f is standard & f is special )
thus
f is_sequence_on GoB f
GOBOARD5:def 5 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;
GOBOARD1:def 9 for b1 being set holds
( not b1 in dom f or not b1 + 1 in dom f or for b2, b3, b4, b5 being set holds
( not [b2,b3] in Indices (GoB f) or not [b4,b5] in Indices (GoB f) or not f /. b1 = (GoB f) * (b2,b3) or not f /. (b1 + 1) = (GoB f) * (b4,b5) or |.(b2 - b4).| + |.(b3 - b5).| = 1 ) )
let n be
Nat;
( not n in dom f or not n + 1 in dom f or for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 ) )
assume that A2:
n in dom f
and A3:
n + 1
in dom f
;
for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 )
let m,
k,
i,
j be
Nat;
( 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)
;
|.(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 )
;
|.(m - i).| + |.(k - j).| = 1now not m <> iassume
m <> i
;
contradictionthen
(
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;
verum end; then A47:
|.(m - i).| = 0
by ABSVALUE:2;
now not j <= kassume
j <= k
;
contradictionthen 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;
verum end; then A49:
k + 1
<= j
by NAT_1:13;
now not k + 1 < jassume A50:
k + 1
< j
;
contradictionthen 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 not j1 >= j19assume
j1 >= j19
;
contradictionthen
(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;
verum end; now not j2 <= j19assume
j2 <= j19
;
contradictionthen
(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;
verum end; hence
contradiction
by A46, A67, NAT_1:13;
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;
verum end; suppose A68:
(
i1 + 1
= i2 &
j1 = j2 )
;
|.(m - i).| + |.(k - j).| = 1now not k <> jassume
k <> j
;
contradictionthen
(
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;
verum end; then A69:
|.(k - j).| = 0
by ABSVALUE:2;
now not i <= massume
i <= m
;
contradictionthen 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;
verum end; then A71:
m + 1
<= i
by NAT_1:13;
now not m + 1 < iassume A72:
m + 1
< i
;
contradictionthen 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 not i1 >= i19assume
i1 >= i19
;
contradictionthen
(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;
verum end; now not i2 <= i19assume
i2 <= i19
;
contradictionthen
(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;
verum end; hence
contradiction
by A68, A89, NAT_1:13;
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;
verum end; suppose A90:
(
i1 = i2 + 1 &
j1 = j2 )
;
|.(m - i).| + |.(k - j).| = 1now not k <> jassume
k <> j
;
contradictionthen
(
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;
verum end; then A91:
|.(k - j).| = 0
by ABSVALUE:2;
now not m <= iassume
m <= i
;
contradictionthen 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;
verum end; then A93:
i + 1
<= m
by NAT_1:13;
now not i + 1 < massume A94:
i + 1
< m
;
contradictionthen 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 not i2 >= i19assume
i2 >= i19
;
contradictionthen
(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;
verum end; now not i1 <= i19assume
i1 <= i19
;
contradictionthen
(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;
verum end; hence
contradiction
by A90, A112, NAT_1:13;
verum end; then
i + 1
= m
by A93, XXREAL_0:1;
hence
|.(m - i).| + |.(k - j).| = 1
by A91, ABSVALUE:def 1;
verum end; suppose A113:
(
i1 = i2 &
j1 = j2 + 1 )
;
|.(m - i).| + |.(k - j).| = 1now not m <> iassume
m <> i
;
contradictionthen
(
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;
verum end; then A114:
|.(m - i).| = 0
by ABSVALUE:2;
now not j >= kassume
j >= k
;
contradictionthen 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;
verum end; then A116:
j + 1
<= k
by NAT_1:13;
now not j + 1 < kassume A117:
j + 1
< k
;
contradictionthen 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 not j2 >= j19assume
j2 >= j19
;
contradictionthen
(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;
verum end; now not j1 <= j19assume
j1 <= j19
;
contradictionthen
(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;
verum end; hence
contradiction
by A113, A135, NAT_1:13;
verum end; then
j + 1
= k
by A116, XXREAL_0:1;
hence
|.(m - i).| + |.(k - j).| = 1
by A114, ABSVALUE:def 1;
verum end; end;
end;
thus
f is special
verumproof
let i be
Nat;
TOPREAL1:def 5 ( 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
;
( (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;
verum
end;