let i1, j1, i2, j2 be Element of NAT ; :: thesis: for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * i1,j1 = G2 * i2,j2 holds
cell G2,(i2 -' 1),j2 c= cell G1,(i1 -' 1),j1
let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * i1,j1 = G2 * i2,j2 implies cell G2,(i2 -' 1),j2 c= cell G1,(i1 -' 1),j1 )
assume that
A1:
Values G1 c= Values G2
and
A2:
[i1,j1] in Indices G1
and
A3:
[i2,j2] in Indices G2
and
A4:
G1 * i1,j1 = G2 * i2,j2
; :: thesis: cell G2,(i2 -' 1),j2 c= cell G1,(i1 -' 1),j1
let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in cell G2,(i2 -' 1),j2 or p in cell G1,(i1 -' 1),j1 )
assume A5:
p in cell G2,(i2 -' 1),j2
; :: thesis: p in cell G1,(i1 -' 1),j1
A6:
( 1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 )
by A2, MATRIX_1:39;
A7:
( 1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 )
by A3, MATRIX_1:39;
then A8:
( (G2 * i2,j2) `1 = (G2 * i2,1) `1 & (G2 * i2,j2) `2 = (G2 * 1,j2) `2 )
by GOBOARD5:2, GOBOARD5:3;
per cases
( ( i1 = 1 & i2 = 1 ) or ( i1 = 1 & 1 < i2 ) or ( 1 < i1 & i2 = 1 ) or ( 1 < i1 & 1 < i2 ) )
by A6, A7, XXREAL_0:1;
suppose A9:
(
i1 = 1 &
i2 = 1 )
;
:: thesis: p in cell G1,(i1 -' 1),j1then A10:
(
i1 -' 1
= 0 &
i2 -' 1
= 0 )
by XREAL_1:234;
now per cases
( j2 = width G2 or j2 < width G2 )
by A7, XXREAL_0:1;
suppose A11:
j2 = width G2
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( r <= (G2 * 1,1) `1 & (G2 * 1,(width G2)) `2 <= s ) }
by A5, A10, GOBRD11:25;
then consider r',
s' being
Real such that A12:
p = |[r',s']|
and A13:
r' <= (G2 * 1,1) `1
and A14:
(G2 * 1,(width G2)) `2 <= s'
;
A15:
j1 = width G1
by A1, A2, A4, A7, A11, Th13;
(G2 * 1,1) `1 = (G2 * i1,j2) `1
by A7, A9, GOBOARD5:3;
then
r' <= (G1 * 1,1) `1
by A4, A6, A9, A13, GOBOARD5:3;
then
p in { |[r,s]| where r, s is Real : ( r <= (G1 * 1,1) `1 & (G1 * 1,(width G1)) `2 <= s ) }
by A4, A9, A11, A12, A14, A15;
hence
p in cell G1,
(i1 -' 1),
j1
by A10, A15, GOBRD11:25;
:: thesis: verum end; suppose A16:
j2 < width G2
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( r <= (G2 * 1,1) `1 & (G2 * 1,j2) `2 <= s & s <= (G2 * 1,(j2 + 1)) `2 ) }
by A5, A7, A10, GOBRD11:26;
then consider r',
s' being
Real such that A17:
p = |[r',s']|
and A18:
r' <= (G2 * 1,1) `1
and A19:
(G2 * 1,j2) `2 <= s'
and A20:
s' <= (G2 * 1,(j2 + 1)) `2
;
(G2 * 1,1) `1 = (G2 * i1,j2) `1
by A7, A9, GOBOARD5:3;
then A21:
r' <= (G1 * 1,1) `1
by A4, A6, A9, A18, GOBOARD5:3;
now per cases
( j1 = width G1 or j1 < width G1 )
by A6, XXREAL_0:1;
suppose A22:
j1 = width G1
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( r <= (G1 * 1,1) `1 & (G1 * 1,(width G1)) `2 <= s ) }
by A4, A9, A17, A19, A21;
hence
p in cell G1,
(i1 -' 1),
j1
by A10, A22, GOBRD11:25;
:: thesis: verum end; suppose A23:
j1 < width G1
;
:: thesis: p in cell G1,(i1 -' 1),j1then
( 1
<= j1 + 1 &
j1 + 1
<= width G1 )
by NAT_1:11, NAT_1:13;
then
G1 * i1,
(j1 + 1) in Values G1
by A6, Lm1;
then
(G2 * 1,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2
by A1, A4, A6, A7, A9, A16, A23, Th16;
then
s' <= (G1 * 1,(j1 + 1)) `2
by A20, XXREAL_0:2;
then
p in { |[r,s]| where r, s is Real : ( r <= (G1 * 1,1) `1 & (G1 * 1,j1) `2 <= s & s <= (G1 * 1,(j1 + 1)) `2 ) }
by A4, A9, A17, A19, A21;
hence
p in cell G1,
(i1 -' 1),
j1
by A6, A10, A23, GOBRD11:26;
:: thesis: verum end; hence
p in cell G1,
(i1 -' 1),
j1
;
:: thesis: verum end; hence
p in cell G1,
(i1 -' 1),
j1
;
:: thesis: verum end; suppose that A24:
i1 = 1
and A25:
1
< i2
;
:: thesis: p in cell G1,(i1 -' 1),j1A26:
i1 -' 1
= 0
by A24, XREAL_1:234;
A27:
1
<= i2 -' 1
by A25, NAT_D:49;
then
i2 -' 1
< i2
by NAT_D:51;
then A28:
i2 -' 1
< len G2
by A7, XXREAL_0:2;
A29:
(i2 -' 1) + 1
= i2
by A25, XREAL_1:237;
now per cases
( j2 = width G2 or j2 < width G2 )
by A7, XXREAL_0:1;
suppose A30:
j2 = width G2
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2 -' 1),1) `1 <= r & r <= (G2 * i2,1) `1 & (G2 * 1,j2) `2 <= s ) }
by A5, A27, A28, A29, GOBRD11:31;
then consider r',
s' being
Real such that A31:
p = |[r',s']|
and
(G2 * (i2 -' 1),1) `1 <= r'
and A32:
r' <= (G2 * i2,1) `1
and A33:
(G2 * 1,j2) `2 <= s'
;
A34:
j1 = width G1
by A1, A2, A4, A7, A30, Th13;
A35:
r' <= (G1 * 1,1) `1
by A4, A6, A8, A24, A32, GOBOARD5:3;
(G1 * 1,j1) `2 <= s'
by A4, A6, A8, A33, GOBOARD5:2;
then
p in { |[r,s]| where r, s is Real : ( r <= (G1 * 1,1) `1 & (G1 * 1,j1) `2 <= s ) }
by A31, A35;
hence
p in cell G1,
(i1 -' 1),
j1
by A26, A34, GOBRD11:25;
:: thesis: verum end; suppose A36:
j2 < width G2
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2 -' 1),1) `1 <= r & r <= (G2 * i2,1) `1 & (G2 * 1,j2) `2 <= s & s <= (G2 * 1,(j2 + 1)) `2 ) }
by A5, A7, A27, A28, A29, GOBRD11:32;
then consider r',
s' being
Real such that A37:
p = |[r',s']|
and
(G2 * (i2 -' 1),1) `1 <= r'
and A38:
r' <= (G2 * i2,1) `1
and A39:
(G2 * 1,j2) `2 <= s'
and A40:
s' <= (G2 * 1,(j2 + 1)) `2
;
A41:
r' <= (G1 * 1,1) `1
by A4, A6, A8, A24, A38, GOBOARD5:3;
A42:
(G1 * 1,j1) `2 <= s'
by A4, A6, A8, A39, GOBOARD5:2;
now per cases
( j1 = width G1 or j1 < width G1 )
by A6, XXREAL_0:1;
suppose A43:
j1 = width G1
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( r <= (G1 * 1,1) `1 & (G1 * 1,(width G1)) `2 <= s ) }
by A37, A41, A42;
hence
p in cell G1,
(i1 -' 1),
j1
by A26, A43, GOBRD11:25;
:: thesis: verum end; suppose A44:
j1 < width G1
;
:: thesis: p in cell G1,(i1 -' 1),j1then A45:
( 1
<= j1 + 1 &
j1 + 1
<= width G1 & 1
<= j2 + 1 &
j2 + 1
<= width G2 )
by A36, NAT_1:12, NAT_1:13;
then A46:
G1 * i1,
(j1 + 1) in Values G1
by A6, Lm1;
(
(G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 &
(G2 * i2,(j2 + 1)) `2 = (G2 * 1,(j2 + 1)) `2 )
by A6, A7, A45, GOBOARD5:2;
then
(G2 * 1,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2
by A1, A4, A6, A7, A36, A44, A46, Th16;
then
s' <= (G1 * 1,(j1 + 1)) `2
by A40, XXREAL_0:2;
then
p in { |[r,s]| where r, s is Real : ( r <= (G1 * 1,1) `1 & (G1 * 1,j1) `2 <= s & s <= (G1 * 1,(j1 + 1)) `2 ) }
by A37, A41, A42;
hence
p in cell G1,
(i1 -' 1),
j1
by A6, A26, A44, GOBRD11:26;
:: thesis: verum end; hence
p in cell G1,
(i1 -' 1),
j1
;
:: thesis: verum end; hence
p in cell G1,
(i1 -' 1),
j1
;
:: thesis: verum end; suppose A47:
( 1
< i1 & 1
< i2 )
;
:: thesis: p in cell G1,(i1 -' 1),j1then A48:
( 1
<= i1 -' 1 & 1
<= i2 -' 1 )
by NAT_D:49;
then
(
i1 -' 1
< i1 &
i2 -' 1
< i2 )
by NAT_D:51;
then A49:
(
i1 -' 1
< len G1 &
i2 -' 1
< len G2 )
by A6, A7, XXREAL_0:2;
A50:
(
(i1 -' 1) + 1
= i1 &
(i2 -' 1) + 1
= i2 )
by A48, NAT_D:43;
A51:
G1 * (i1 -' 1),
j1 in Values G1
by A6, A48, A49, Lm1;
(
(G1 * (i1 -' 1),1) `1 = (G1 * (i1 -' 1),j1) `1 &
(G2 * (i2 -' 1),1) `1 = (G2 * (i2 -' 1),j2) `1 )
by A6, A7, A48, A49, GOBOARD5:3;
then A52:
(G1 * (i1 -' 1),1) `1 <= (G2 * (i2 -' 1),1) `1
by A1, A4, A6, A7, A47, A51, Th15;
now per cases
( j2 = width G2 or j2 < width G2 )
by A7, XXREAL_0:1;
suppose A53:
j2 = width G2
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2 -' 1),1) `1 <= r & r <= (G2 * i2,1) `1 & (G2 * 1,j2) `2 <= s ) }
by A5, A48, A49, A50, GOBRD11:31;
then consider r',
s' being
Real such that A54:
p = |[r',s']|
and A55:
(G2 * (i2 -' 1),1) `1 <= r'
and A56:
r' <= (G2 * i2,1) `1
and A57:
(G2 * 1,j2) `2 <= s'
;
A58:
j1 = width G1
by A1, A2, A4, A7, A53, Th13;
A59:
(G1 * (i1 -' 1),1) `1 <= r'
by A52, A55, XXREAL_0:2;
A60:
r' <= (G1 * i1,1) `1
by A4, A6, A8, A56, GOBOARD5:3;
(G1 * 1,j1) `2 <= s'
by A4, A6, A8, A57, GOBOARD5:2;
then
p in { |[r,s]| where r, s is Real : ( (G1 * (i1 -' 1),1) `1 <= r & r <= (G1 * i1,1) `1 & (G1 * 1,j1) `2 <= s ) }
by A54, A59, A60;
hence
p in cell G1,
(i1 -' 1),
j1
by A48, A49, A50, A58, GOBRD11:31;
:: thesis: verum end; suppose A61:
j2 < width G2
;
:: thesis: p in cell G1,(i1 -' 1),j1then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2 -' 1),1) `1 <= r & r <= (G2 * i2,1) `1 & (G2 * 1,j2) `2 <= s & s <= (G2 * 1,(j2 + 1)) `2 ) }
by A5, A7, A48, A49, A50, GOBRD11:32;
then consider r',
s' being
Real such that A62:
p = |[r',s']|
and A63:
(G2 * (i2 -' 1),1) `1 <= r'
and A64:
r' <= (G2 * i2,1) `1
and A65:
(G2 * 1,j2) `2 <= s'
and A66:
s' <= (G2 * 1,(j2 + 1)) `2
;
A67:
(G1 * (i1 -' 1),1) `1 <= r'
by A52, A63, XXREAL_0:2;
A68:
r' <= (G1 * i1,1) `1
by A4, A6, A8, A64, GOBOARD5:3;
A69:
(G1 * 1,j1) `2 <= s'
by A4, A6, A8, A65, GOBOARD5:2;
now per cases
( j1 = width G1 or j1 < width G1 )
by A6, XXREAL_0:1;
suppose A70:
j1 = width G1
;
:: thesis: p in cell G1,(i1 -' 1),j1
p in { |[r,s]| where r, s is Real : ( (G1 * (i1 -' 1),1) `1 <= r & r <= (G1 * i1,1) `1 & (G1 * 1,j1) `2 <= s ) }
by A62, A67, A68, A69;
hence
p in cell G1,
(i1 -' 1),
j1
by A48, A49, A50, A70, GOBRD11:31;
:: thesis: verum end; suppose A71:
j1 < width G1
;
:: thesis: p in cell G1,(i1 -' 1),j1then A72:
( 1
<= j1 + 1 &
j1 + 1
<= width G1 & 1
<= j2 + 1 &
j2 + 1
<= width G2 )
by A61, NAT_1:12, NAT_1:13;
then A73:
G1 * i1,
(j1 + 1) in Values G1
by A6, Lm1;
(
(G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 &
(G2 * i2,(j2 + 1)) `2 = (G2 * 1,(j2 + 1)) `2 )
by A6, A7, A72, GOBOARD5:2;
then
(G2 * 1,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2
by A1, A4, A6, A7, A61, A71, A73, Th16;
then
s' <= (G1 * 1,(j1 + 1)) `2
by A66, XXREAL_0:2;
then
p in { |[r,s]| where r, s is Real : ( (G1 * (i1 -' 1),1) `1 <= r & r <= (G1 * i1,1) `1 & (G1 * 1,j1) `2 <= s & s <= (G1 * 1,(j1 + 1)) `2 ) }
by A62, A67, A68, A69;
hence
p in cell G1,
(i1 -' 1),
j1
by A6, A48, A49, A50, A71, GOBRD11:32;
:: thesis: verum end; hence
p in cell G1,
(i1 -' 1),
j1
;
:: thesis: verum end; hence
p in cell G1,
(i1 -' 1),
j1
;
:: thesis: verum end;