let n be Nat; for G being Go-board
for f being standard special_circular_sequence st 1 <= n & n + 1 <= len f & f is_sequence_on G holds
( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )
let G be Go-board; for f being standard special_circular_sequence st 1 <= n & n + 1 <= len f & f is_sequence_on G holds
( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )
let f be standard special_circular_sequence; ( 1 <= n & n + 1 <= len f & f is_sequence_on G implies ( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) ) )
assume that
A1:
( 1 <= n & n + 1 <= len f )
and
A2:
f is_sequence_on G
; ( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )
consider i1, j1, i2, j2 being Nat such that
A3:
[i1,j1] in Indices G
and
A4:
f /. n = G * (i1,j1)
and
A5:
[i2,j2] in Indices G
and
A6:
f /. (n + 1) = G * (i2,j2)
and
A7:
( ( 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:3;
A8:
1 <= j1
by A3, MATRIX_0:32;
A9:
( j1 + 1 > j1 & j2 + 1 > j2 )
by NAT_1:13;
A10:
( i1 + 1 > i1 & i2 + 1 > i2 )
by NAT_1:13;
A11:
j2 <= width G
by A5, MATRIX_0:32;
A12:
j1 <= width G
by A3, MATRIX_0:32;
A13:
i2 <= len G
by A5, MATRIX_0:32;
A14:
1 <= i2
by A5, MATRIX_0:32;
then A15:
(G * (i2,j1)) `2 = (G * (1,j1)) `2
by A8, A12, A13, GOBOARD5:1;
A16:
1 <= j2
by A5, MATRIX_0:32;
then A17:
(G * (i2,j2)) `1 = (G * (i2,1)) `1
by A14, A13, A11, GOBOARD5:2;
A18:
i1 <= len G
by A3, MATRIX_0:32;
set F = GoB f;
A19:
Values (GoB f) c= Values G
by A2, Th13;
f is_sequence_on GoB f
by GOBOARD5:def 5;
then consider m, k, i, j being Nat such that
A20:
[m,k] in Indices (GoB f)
and
A21:
f /. n = (GoB f) * (m,k)
and
A22:
[i,j] in Indices (GoB f)
and
A23:
f /. (n + 1) = (GoB f) * (i,j)
and
( ( m = i & k + 1 = j ) or ( m + 1 = i & k = j ) or ( m = i + 1 & k = j ) or ( m = i & k = j + 1 ) )
by A1, JORDAN8:3;
A24:
1 <= m
by A20, MATRIX_0:32;
A25:
1 <= i1
by A3, MATRIX_0:32;
then A26:
(G * (i1,j1)) `1 = (G * (i1,1)) `1
by A18, A8, A12, GOBOARD5:2;
A27:
(G * (i1,j1)) `2 = (G * (1,j1)) `2
by A25, A18, A8, A12, GOBOARD5:1;
A28:
m <= len (GoB f)
by A20, MATRIX_0:32;
A29:
j + 1 > j
by NAT_1:13;
A30:
k + 1 > k
by NAT_1:13;
A31:
k + 1 >= 1
by NAT_1:12;
A32:
j + 1 >= 1
by NAT_1:12;
A33:
j <= width (GoB f)
by A22, MATRIX_0:32;
A34:
i + 1 > i
by NAT_1:13;
A35:
m + 1 > m
by NAT_1:13;
A36:
i <= len (GoB f)
by A22, MATRIX_0:32;
A37:
i + 1 >= 1
by NAT_1:12;
A38:
m + 1 >= 1
by NAT_1:12;
A39:
k <= width (GoB f)
by A20, MATRIX_0:32;
A40:
1 <= j
by A22, MATRIX_0:32;
then A41:
((GoB f) * (m,j)) `2 = ((GoB f) * (1,j)) `2
by A24, A28, A33, GOBOARD5:1;
A42:
1 <= i
by A22, MATRIX_0:32;
then A43:
((GoB f) * (i,j)) `1 = ((GoB f) * (i,1)) `1
by A36, A40, A33, GOBOARD5:2;
A44:
((GoB f) * (i,j)) `2 = ((GoB f) * (1,j)) `2
by A42, A36, A40, A33, GOBOARD5:1;
A45:
1 <= k
by A20, MATRIX_0:32;
then A46:
((GoB f) * (i,k)) `1 = ((GoB f) * (i,1)) `1
by A39, A42, A36, GOBOARD5:2;
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 A7;
suppose A47:
(
i1 = i2 &
j1 + 1
= j2 )
;
( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )A48:
now not k + 1 < jA49:
(G * (i2,j2)) `2 = (G * (1,j2)) `2
by A14, A13, A16, A11, GOBOARD5:1;
assume A50:
k + 1
< j
;
contradictionthen A51:
k + 1
< width (GoB f)
by A33, 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:
((GoB f) * (m,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2
by A24, A28, A31, A51, GOBOARD5:1;
( 1
<= i9 &
i9 <= len (GoB f) )
by A53, MATRIX_0:32;
then A56:
((GoB f) * (i9,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2
by A31, A51, GOBOARD5:1;
consider i19,
j19 being
Nat such that A57:
[i19,j19] in Indices G
and A58:
f /. l = G * (
i19,
j19)
by A2, A52, GOBOARD1:def 9;
A59:
1
<= j19
by A57, MATRIX_0:32;
A60:
( 1
<= i19 &
i19 <= len G )
by A57, MATRIX_0:32;
then A61:
(G * (i19,j1)) `2 = (G * (1,j1)) `2
by A8, A12, GOBOARD5:1;
A62:
now not j1 >= j19assume
j1 >= j19
;
contradictionthen
(G * (i19,j19)) `2 <= (G * (i1,j1)) `2
by A12, A27, A60, A59, A61, SPRECT_3:12;
hence
contradiction
by A21, A24, A28, A45, A4, A30, A51, A54, A56, A55, A58, GOBOARD5:4;
verum end; A63:
j19 <= width G
by A57, MATRIX_0:32;
A64:
(G * (i19,j2)) `2 = (G * (1,j2)) `2
by A16, A11, A60, GOBOARD5:1;
now not j2 <= j19assume
j2 <= j19
;
contradictionthen
(G * (i2,j2)) `2 <= (G * (i19,j19)) `2
by A16, A60, A63, A49, A64, SPRECT_3:12;
hence
contradiction
by A23, A24, A28, A33, A44, A41, A6, A31, A50, A54, A56, A55, A58, GOBOARD5:4;
verum end; hence
contradiction
by A47, A62, NAT_1:13;
verum end; now not j <= kassume
j <= k
;
contradictionthen A65:
((GoB f) * (i,j)) `2 <= ((GoB f) * (m,k)) `2
by A24, A28, A39, A40, A44, A41, SPRECT_3:12;
j1 < j2
by A47, NAT_1:13;
hence
contradiction
by A21, A23, A4, A6, A8, A14, A13, A11, A27, A15, A65, GOBOARD5:4;
verum end; then
k + 1
<= j
by NAT_1:13;
then
k + 1
= j
by A48, XXREAL_0:1;
then A66:
(
right_cell (
f,
n)
= cell (
(GoB f),
m,
k) &
left_cell (
f,
n)
= cell (
(GoB f),
(m -' 1),
k) )
by A1, A20, A21, A22, A23, A30, A29, GOBOARD5:def 6, GOBOARD5:def 7;
(
right_cell (
f,
n,
G)
= cell (
G,
i1,
j1) &
left_cell (
f,
n,
G)
= cell (
G,
(i1 -' 1),
j1) )
by A1, A2, A3, A4, A5, A6, A9, A47, Def1, Def2;
hence
(
left_cell (
f,
n,
G)
c= left_cell (
f,
n) &
right_cell (
f,
n,
G)
c= right_cell (
f,
n) )
by A19, A20, A21, A3, A4, A66, Th10, Th11;
verum end; suppose A67:
(
i1 + 1
= i2 &
j1 = j2 )
;
( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )A68:
now not m + 1 < iassume A69:
m + 1
< i
;
contradictionthen A70:
m + 1
< len (GoB f)
by A36, XXREAL_0:2;
then consider l,
j9 being
Nat such that A71:
l in dom f
and A72:
[(m + 1),j9] in Indices (GoB f)
and A73:
f /. l = (GoB f) * (
(m + 1),
j9)
by JORDAN5D:7, NAT_1:12;
A74:
((GoB f) * ((m + 1),k)) `1 = ((GoB f) * ((m + 1),1)) `1
by A45, A39, A38, A70, GOBOARD5:2;
( 1
<= j9 &
j9 <= width (GoB f) )
by A72, MATRIX_0:32;
then A75:
((GoB f) * ((m + 1),j9)) `1 = ((GoB f) * ((m + 1),1)) `1
by A38, A70, GOBOARD5:2;
A76:
( 1
<= m + 1 &
((GoB f) * ((m + 1),j)) `1 = ((GoB f) * ((m + 1),1)) `1 )
by A40, A33, A38, A70, GOBOARD5:2;
A77:
(G * (i2,j2)) `1 = (G * (i2,1)) `1
by A14, A13, A16, A11, GOBOARD5:2;
consider i19,
j19 being
Nat such that A78:
[i19,j19] in Indices G
and A79:
f /. l = G * (
i19,
j19)
by A2, A71, GOBOARD1:def 9;
A80:
i19 <= len G
by A78, MATRIX_0:32;
A81:
( 1
<= j19 &
j19 <= width G )
by A78, MATRIX_0:32;
A82:
1
<= i19
by A78, MATRIX_0:32;
then A83:
(G * (i19,j19)) `1 = (G * (i19,1)) `1
by A80, A81, GOBOARD5:2;
A84:
(G * (i19,j1)) `1 = (G * (i19,1)) `1
by A8, A12, A82, A80, GOBOARD5:2;
A85:
now not i1 >= i19assume
i1 >= i19
;
contradictionthen
(G * (i19,j19)) `1 <= (G * (i1,j1)) `1
by A18, A8, A12, A82, A83, A84, SPRECT_3:13;
hence
contradiction
by A21, A24, A45, A39, A4, A35, A70, A73, A75, A74, A79, GOBOARD5:3;
verum end; A86:
(G * (i2,j19)) `1 = (G * (i2,1)) `1
by A14, A13, A81, GOBOARD5:2;
now not i2 <= i19assume
i2 <= i19
;
contradictionthen
(G * (i2,j2)) `1 <= (G * (i19,j19)) `1
by A14, A80, A81, A77, A86, SPRECT_3:13;
hence
contradiction
by A23, A36, A40, A33, A6, A69, A73, A75, A76, A79, GOBOARD5:3;
verum end; hence
contradiction
by A67, A85, NAT_1:13;
verum end; now not i <= massume
i <= m
;
contradictionthen A87:
((GoB f) * (i,j)) `1 <= ((GoB f) * (m,k)) `1
by A28, A45, A39, A42, A43, A46, SPRECT_3:13;
i1 < i2
by A67, NAT_1:13;
hence
contradiction
by A21, A23, A4, A6, A25, A8, A12, A13, A67, A87, GOBOARD5:3;
verum end; then
m + 1
<= i
by NAT_1:13;
then
m + 1
= i
by A68, XXREAL_0:1;
then A88:
(
right_cell (
f,
n)
= cell (
(GoB f),
m,
(k -' 1)) &
left_cell (
f,
n)
= cell (
(GoB f),
m,
k) )
by A1, A20, A21, A22, A23, A35, A34, GOBOARD5:def 6, GOBOARD5:def 7;
(
right_cell (
f,
n,
G)
= cell (
G,
i1,
(j1 -' 1)) &
left_cell (
f,
n,
G)
= cell (
G,
i1,
j1) )
by A1, A2, A3, A4, A5, A6, A10, A67, Def1, Def2;
hence
(
left_cell (
f,
n,
G)
c= left_cell (
f,
n) &
right_cell (
f,
n,
G)
c= right_cell (
f,
n) )
by A19, A20, A21, A3, A4, A88, Th10, Th12;
verum end; suppose A89:
(
i1 = i2 + 1 &
j1 = j2 )
;
( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )A90:
now not m > i + 1assume A91:
m > i + 1
;
contradictionthen A92:
i + 1
< len (GoB f)
by A28, XXREAL_0:2;
then consider l,
j9 being
Nat such that A93:
l in dom f
and A94:
[(i + 1),j9] in Indices (GoB f)
and A95:
f /. l = (GoB f) * (
(i + 1),
j9)
by JORDAN5D:7, NAT_1:12;
A96:
( 1
<= i + 1 &
((GoB f) * ((i + 1),k)) `1 = ((GoB f) * ((i + 1),1)) `1 )
by A45, A39, A37, A92, GOBOARD5:2;
( 1
<= j9 &
j9 <= width (GoB f) )
by A94, MATRIX_0:32;
then A97:
((GoB f) * ((i + 1),j9)) `1 = ((GoB f) * ((i + 1),1)) `1
by A37, A92, GOBOARD5:2;
A98:
((GoB f) * ((i + 1),j)) `1 = ((GoB f) * ((i + 1),1)) `1
by A40, A33, A37, A92, GOBOARD5:2;
A99:
(G * (i2,j2)) `1 = (G * (i2,1)) `1
by A14, A13, A16, A11, GOBOARD5:2;
consider i19,
j19 being
Nat such that A100:
[i19,j19] in Indices G
and A101:
f /. l = G * (
i19,
j19)
by A2, A93, GOBOARD1:def 9;
A102:
1
<= i19
by A100, MATRIX_0:32;
A103:
( 1
<= j19 &
j19 <= width G )
by A100, MATRIX_0:32;
A104:
i19 <= len G
by A100, MATRIX_0:32;
then A105:
(G * (i19,j19)) `1 = (G * (i19,1)) `1
by A102, A103, GOBOARD5:2;
A106:
(G * (i19,j1)) `1 = (G * (i19,1)) `1
by A8, A12, A102, A104, GOBOARD5:2;
A107:
now not i1 <= i19assume
i1 <= i19
;
contradictionthen
(G * (i19,j19)) `1 >= (G * (i1,j1)) `1
by A25, A8, A12, A104, A105, A106, SPRECT_3:13;
hence
contradiction
by A21, A28, A45, A39, A4, A91, A95, A97, A96, A101, GOBOARD5:3;
verum end; A108:
(G * (i2,j19)) `1 = (G * (i2,1)) `1
by A14, A13, A103, GOBOARD5:2;
now not i2 >= i19assume
i2 >= i19
;
contradictionthen
(G * (i2,j2)) `1 >= (G * (i19,j19)) `1
by A13, A102, A103, A99, A108, SPRECT_3:13;
hence
contradiction
by A23, A42, A40, A33, A6, A34, A92, A95, A97, A98, A101, GOBOARD5:3;
verum end; hence
contradiction
by A89, A107, NAT_1:13;
verum end; now not m <= iassume
m <= i
;
contradictionthen A109:
((GoB f) * (i,j)) `1 >= ((GoB f) * (m,k)) `1
by A24, A45, A39, A36, A43, A46, SPRECT_3:13;
i1 > i2
by A89, NAT_1:13;
hence
contradiction
by A21, A23, A4, A6, A18, A8, A12, A14, A89, A109, GOBOARD5:3;
verum end; then
i + 1
<= m
by NAT_1:13;
then
i + 1
= m
by A90, XXREAL_0:1;
then A110:
(
right_cell (
f,
n)
= cell (
(GoB f),
i,
j) &
left_cell (
f,
n)
= cell (
(GoB f),
i,
(j -' 1)) )
by A1, A20, A21, A22, A23, A35, A34, GOBOARD5:def 6, GOBOARD5:def 7;
(
right_cell (
f,
n,
G)
= cell (
G,
i2,
j2) &
left_cell (
f,
n,
G)
= cell (
G,
i2,
(j2 -' 1)) )
by A1, A2, A3, A4, A5, A6, A10, A89, Def1, Def2;
hence
(
left_cell (
f,
n,
G)
c= left_cell (
f,
n) &
right_cell (
f,
n,
G)
c= right_cell (
f,
n) )
by A19, A22, A23, A5, A6, A110, Th10, Th12;
verum end; suppose A111:
(
i1 = i2 &
j1 = j2 + 1 )
;
( left_cell (f,n,G) c= left_cell (f,n) & right_cell (f,n,G) c= right_cell (f,n) )A112:
now not j + 1 < kA113:
(G * (i2,j2)) `2 = (G * (1,j2)) `2
by A14, A13, A16, A11, GOBOARD5:1;
assume A114:
j + 1
< k
;
contradictionthen A115:
j + 1
< width (GoB f)
by A39, XXREAL_0:2;
then consider l,
i9 being
Nat such that A116:
l in dom f
and A117:
[i9,(j + 1)] in Indices (GoB f)
and A118:
f /. l = (GoB f) * (
i9,
(j + 1))
by JORDAN5D:8, NAT_1:12;
A119:
((GoB f) * (m,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2
by A24, A28, A32, A115, GOBOARD5:1;
( 1
<= i9 &
i9 <= len (GoB f) )
by A117, MATRIX_0:32;
then A120:
((GoB f) * (i9,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2
by A32, A115, GOBOARD5:1;
consider i19,
j19 being
Nat such that A121:
[i19,j19] in Indices G
and A122:
f /. l = G * (
i19,
j19)
by A2, A116, GOBOARD1:def 9;
A123:
j19 <= width G
by A121, MATRIX_0:32;
A124:
( 1
<= i19 &
i19 <= len G )
by A121, MATRIX_0:32;
then A125:
(G * (i19,j1)) `2 = (G * (1,j1)) `2
by A8, A12, GOBOARD5:1;
A126:
now not j1 <= j19assume
j1 <= j19
;
contradictionthen
(G * (i19,j19)) `2 >= (G * (i1,j1)) `2
by A8, A27, A124, A123, A125, SPRECT_3:12;
hence
contradiction
by A21, A24, A28, A39, A4, A32, A114, A118, A120, A119, A122, GOBOARD5:4;
verum end; A127:
((GoB f) * (i,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2
by A42, A36, A32, A115, GOBOARD5:1;
A128:
1
<= j19
by A121, MATRIX_0:32;
A129:
(G * (i19,j2)) `2 = (G * (1,j2)) `2
by A16, A11, A124, GOBOARD5:1;
now not j2 >= j19assume
j2 >= j19
;
contradictionthen
(G * (i2,j2)) `2 >= (G * (i19,j19)) `2
by A11, A124, A128, A113, A129, SPRECT_3:12;
hence
contradiction
by A23, A42, A36, A40, A6, A29, A115, A118, A120, A127, A122, GOBOARD5:4;
verum end; hence
contradiction
by A111, A126, NAT_1:13;
verum end; now not j >= kassume
j >= k
;
contradictionthen A130:
((GoB f) * (i,j)) `2 >= ((GoB f) * (m,k)) `2
by A24, A28, A45, A33, A44, A41, SPRECT_3:12;
j1 > j2
by A111, NAT_1:13;
hence
contradiction
by A21, A23, A4, A6, A12, A14, A13, A16, A27, A15, A130, GOBOARD5:4;
verum end; then
j + 1
<= k
by NAT_1:13;
then
j + 1
= k
by A112, XXREAL_0:1;
then A131:
(
right_cell (
f,
n)
= cell (
(GoB f),
(m -' 1),
j) &
left_cell (
f,
n)
= cell (
(GoB f),
m,
j) )
by A1, A20, A21, A22, A23, A30, A29, GOBOARD5:def 6, GOBOARD5:def 7;
A132:
now not m <> iassume A133:
m <> i
;
contradictionper cases
( m < i or m > i )
by A133, XXREAL_0:1;
suppose
m < i
;
contradictionhence
contradiction
by A21, A23, A24, A45, A39, A36, A43, A46, A4, A6, A26, A17, A111, GOBOARD5:3;
verum end; suppose
m > i
;
contradictionhence
contradiction
by A21, A23, A28, A45, A39, A42, A43, A46, A4, A6, A26, A17, A111, GOBOARD5:3;
verum end; end; end;
(
right_cell (
f,
n,
G)
= cell (
G,
(i1 -' 1),
j2) &
left_cell (
f,
n,
G)
= cell (
G,
i1,
j2) )
by A1, A2, A3, A4, A5, A6, A9, A111, Def1, Def2;
hence
(
left_cell (
f,
n,
G)
c= left_cell (
f,
n) &
right_cell (
f,
n,
G)
c= right_cell (
f,
n) )
by A19, A22, A23, A5, A6, A111, A132, A131, Th10, Th11;
verum end; end;