let i1, i2, j1, j2 be Nat; 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,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1))
let G1, G2 be Go-board; ( 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,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1)) )
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)
; cell (G2,i2,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1))
A5:
1 <= i1
by A2, MATRIX_0:32;
A6:
1 <= j2
by A3, MATRIX_0:32;
A7:
1 <= i2
by A3, MATRIX_0:32;
A8:
j1 <= width G1
by A2, MATRIX_0:32;
A9:
j2 <= width G2
by A3, MATRIX_0:32;
A10:
i2 <= len G2
by A3, MATRIX_0:32;
then A11:
(G2 * (i2,j2)) `1 = (G2 * (i2,1)) `1
by A7, A6, A9, GOBOARD5:2;
A12:
i1 <= len G1
by A2, MATRIX_0:32;
A13:
1 <= j1
by A2, MATRIX_0:32;
then A14:
(G1 * (i1,j1)) `2 = (G1 * (1,j1)) `2
by A5, A12, A8, GOBOARD5:1;
let p be object ; TARSKI:def 3 ( not p in cell (G2,i2,(j2 -' 1)) or p in cell (G1,i1,(j1 -' 1)) )
assume A15:
p in cell (G2,i2,(j2 -' 1))
; p in cell (G1,i1,(j1 -' 1))
A16:
(G2 * (i2,j2)) `2 = (G2 * (1,j2)) `2
by A7, A10, A6, A9, GOBOARD5:1;
per cases
( ( j1 = 1 & j2 = 1 ) or ( j1 = 1 & 1 < j2 ) or ( 1 < j1 & j2 = 1 ) or ( 1 < j1 & 1 < j2 ) )
by A13, A6, XXREAL_0:1;
suppose A17:
(
j1 = 1 &
j2 = 1 )
;
p in cell (G1,i1,(j1 -' 1))then A18:
j1 -' 1
= 0
by XREAL_1:232;
A19:
j2 -' 1
= 0
by A17, XREAL_1:232;
now p in cell (G1,i1,(j1 -' 1))per cases
( i2 = len G2 or i2 < len G2 )
by A10, XXREAL_0:1;
suppose A20:
i2 = len G2
;
p in cell (G1,i1,(j1 -' 1))then
p in { |[r,s]| where r, s is Real : ( (G2 * ((len G2),1)) `1 <= r & s <= (G2 * (1,1)) `2 ) }
by A15, A19, GOBRD11:27;
then consider r9,
s9 being
Real such that A21:
(
p = |[r9,s9]| &
(G2 * ((len G2),1)) `1 <= r9 )
and A22:
s9 <= (G2 * (1,1)) `2
;
A23:
i1 = len G1
by A1, A2, A4, A6, A9, A20, Th3;
(G2 * (1,1)) `2 = (G2 * (i2,j2)) `2
by A7, A10, A9, A17, GOBOARD5:1;
then
s9 <= (G1 * (1,1)) `2
by A4, A5, A12, A8, A17, A22, GOBOARD5:1;
then
p in { |[r,s]| where r, s is Real : ( (G1 * ((len G1),1)) `1 <= r & s <= (G1 * (1,1)) `2 ) }
by A4, A17, A20, A21, A23;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A18, A23, GOBRD11:27;
verum end; suppose A24:
i2 < len G2
;
p in cell (G1,i1,(j1 -' 1))then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & s <= (G2 * (1,1)) `2 ) }
by A15, A7, A19, GOBRD11:30;
then consider r9,
s9 being
Real such that A25:
(
p = |[r9,s9]| &
(G2 * (i2,1)) `1 <= r9 )
and A26:
r9 <= (G2 * ((i2 + 1),1)) `1
and A27:
s9 <= (G2 * (1,1)) `2
;
(G2 * (1,1)) `2 = (G2 * (i2,j1)) `2
by A7, A10, A9, A17, GOBOARD5:1;
then A28:
s9 <= (G1 * (1,1)) `2
by A4, A5, A12, A8, A17, A27, GOBOARD5:1;
now p in cell (G1,i1,(j1 -' 1))per cases
( i1 = len G1 or i1 < len G1 )
by A12, XXREAL_0:1;
suppose A29:
i1 = len G1
;
p in cell (G1,i1,(j1 -' 1))then
p in { |[r,s]| where r, s is Real : ( (G1 * ((len G1),1)) `1 <= r & s <= (G1 * (1,1)) `2 ) }
by A4, A17, A25, A28;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A18, A29, GOBRD11:27;
verum end; suppose A30:
i1 < len G1
;
p in cell (G1,i1,(j1 -' 1))then
(G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1
by A1, A4, A5, A8, A7, A9, A17, A24, Th6;
then
r9 <= (G1 * ((i1 + 1),1)) `1
by A26, XXREAL_0:2;
then
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & s <= (G1 * (1,1)) `2 ) }
by A4, A17, A25, A28;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A5, A18, A30, GOBRD11:30;
verum end; end; end; hence
p in cell (
G1,
i1,
(j1 -' 1))
;
verum end; end; end; hence
p in cell (
G1,
i1,
(j1 -' 1))
;
verum end; suppose that A31:
j1 = 1
and A32:
1
< j2
;
p in cell (G1,i1,(j1 -' 1))A33:
j1 -' 1
= 0
by A31, XREAL_1:232;
A34:
1
<= j2 -' 1
by A32, NAT_D:49;
then
j2 -' 1
< j2
by NAT_D:51;
then A35:
j2 -' 1
< width G2
by A9, XXREAL_0:2;
A36:
(j2 -' 1) + 1
= j2
by A32, XREAL_1:235;
now p in cell (G1,i1,(j1 -' 1))per cases
( i2 = len G2 or i2 < len G2 )
by A10, XXREAL_0:1;
suppose A37:
i2 = len G2
;
p in cell (G1,i1,(j1 -' 1))then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) }
by A15, A34, A35, A36, GOBRD11:29;
then
ex
r9,
s9 being
Real st
(
p = |[r9,s9]| &
(G2 * (i2,1)) `1 <= r9 &
(G2 * (1,(j2 -' 1))) `2 <= s9 &
s9 <= (G2 * (1,j2)) `2 )
;
then A38:
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & s <= (G1 * (1,1)) `2 ) }
by A4, A14, A11, A16, A31;
i1 = len G1
by A1, A2, A4, A6, A9, A37, Th3;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A33, A38, GOBRD11:27;
verum end; suppose A39:
i2 < len G2
;
p in cell (G1,i1,(j1 -' 1))then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) }
by A15, A7, A34, A35, A36, GOBRD11:32;
then consider r9,
s9 being
Real such that A40:
p = |[r9,s9]|
and A41:
(G2 * (i2,1)) `1 <= r9
and A42:
r9 <= (G2 * ((i2 + 1),1)) `1
and
(G2 * (1,(j2 -' 1))) `2 <= s9
and A43:
s9 <= (G2 * (1,j2)) `2
;
A44:
(
s9 <= (G1 * (1,1)) `2 &
(G1 * (i1,1)) `1 <= r9 )
by A4, A7, A10, A6, A9, A14, A31, A41, A43, GOBOARD5:1, GOBOARD5:2;
now p in cell (G1,i1,(j1 -' 1))per cases
( i1 = len G1 or i1 < len G1 )
by A12, XXREAL_0:1;
suppose A46:
i1 < len G1
;
p in cell (G1,i1,(j1 -' 1))
( 1
<= i2 + 1 &
i2 + 1
<= len G2 )
by A39, NAT_1:12, NAT_1:13;
then A47:
(G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1
by A6, A9, GOBOARD5:2;
( 1
<= i1 + 1 &
i1 + 1
<= len G1 )
by A46, NAT_1:12, NAT_1:13;
then
(G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1
by A13, A8, GOBOARD5:2;
then
(G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1
by A1, A4, A5, A13, A8, A7, A6, A9, A39, A46, A47, Th6;
then
r9 <= (G1 * ((i1 + 1),1)) `1
by A42, XXREAL_0:2;
then
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & s <= (G1 * (1,1)) `2 ) }
by A40, A44;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A5, A33, A46, GOBRD11:30;
verum end; end; end; hence
p in cell (
G1,
i1,
(j1 -' 1))
;
verum end; end; end; hence
p in cell (
G1,
i1,
(j1 -' 1))
;
verum end; suppose A48:
( 1
< j1 & 1
< j2 )
;
p in cell (G1,i1,(j1 -' 1))then A49:
1
<= j2 -' 1
by NAT_D:49;
then A50:
(j2 -' 1) + 1
= j2
by NAT_D:43;
j2 -' 1
< j2
by A49, NAT_D:51;
then A51:
j2 -' 1
< width G2
by A9, XXREAL_0:2;
then A52:
(G2 * (1,(j2 -' 1))) `2 = (G2 * (i2,(j2 -' 1))) `2
by A7, A10, A49, GOBOARD5:1;
A53:
1
<= j1 -' 1
by A48, NAT_D:49;
then A54:
(j1 -' 1) + 1
= j1
by NAT_D:43;
j1 -' 1
< j1
by A53, NAT_D:51;
then A55:
j1 -' 1
< width G1
by A8, XXREAL_0:2;
then
(G1 * (1,(j1 -' 1))) `2 = (G1 * (i1,(j1 -' 1))) `2
by A5, A12, A53, GOBOARD5:1;
then A56:
(G1 * (1,(j1 -' 1))) `2 <= (G2 * (1,(j2 -' 1))) `2
by A1, A4, A5, A12, A8, A7, A10, A9, A48, A52, Th9;
now p in cell (G1,i1,(j1 -' 1))per cases
( i2 = len G2 or i2 < len G2 )
by A10, XXREAL_0:1;
suppose A57:
i2 = len G2
;
p in cell (G1,i1,(j1 -' 1))then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) }
by A15, A49, A51, A50, GOBRD11:29;
then consider r9,
s9 being
Real such that A58:
p = |[r9,s9]|
and A59:
(G2 * (i2,1)) `1 <= r9
and A60:
(
(G2 * (1,(j2 -' 1))) `2 <= s9 &
s9 <= (G2 * (1,j2)) `2 )
;
A61:
(G1 * (i1,1)) `1 <= r9
by A4, A5, A12, A13, A8, A11, A59, GOBOARD5:2;
(
(G1 * (1,(j1 -' 1))) `2 <= s9 &
s9 <= (G1 * (1,j1)) `2 )
by A4, A5, A12, A13, A8, A16, A56, A60, GOBOARD5:1, XXREAL_0:2;
then A62:
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & (G1 * (1,(j1 -' 1))) `2 <= s & s <= (G1 * (1,j1)) `2 ) }
by A58, A61;
i1 = len G1
by A1, A2, A4, A6, A9, A57, Th3;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A53, A55, A54, A62, GOBRD11:29;
verum end; suppose A63:
i2 < len G2
;
p in cell (G1,i1,(j1 -' 1))then
p in { |[r,s]| where r, s is Real : ( (G2 * (i2,1)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & (G2 * (1,(j2 -' 1))) `2 <= s & s <= (G2 * (1,j2)) `2 ) }
by A15, A7, A49, A51, A50, GOBRD11:32;
then consider r9,
s9 being
Real such that A64:
p = |[r9,s9]|
and A65:
(G2 * (i2,1)) `1 <= r9
and A66:
r9 <= (G2 * ((i2 + 1),1)) `1
and A67:
(
(G2 * (1,(j2 -' 1))) `2 <= s9 &
s9 <= (G2 * (1,j2)) `2 )
;
A68:
(G1 * (i1,1)) `1 <= r9
by A4, A5, A12, A13, A8, A11, A65, GOBOARD5:2;
A69:
(
(G1 * (1,(j1 -' 1))) `2 <= s9 &
s9 <= (G1 * (1,j1)) `2 )
by A4, A5, A12, A13, A8, A16, A56, A67, GOBOARD5:1, XXREAL_0:2;
now p in cell (G1,i1,(j1 -' 1))per cases
( i1 = len G1 or i1 < len G1 )
by A12, XXREAL_0:1;
suppose A70:
i1 = len G1
;
p in cell (G1,i1,(j1 -' 1))
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & (G1 * (1,(j1 -' 1))) `2 <= s & s <= (G1 * (1,j1)) `2 ) }
by A64, A69, A68;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A53, A55, A54, A70, GOBRD11:29;
verum end; suppose A71:
i1 < len G1
;
p in cell (G1,i1,(j1 -' 1))
( 1
<= i2 + 1 &
i2 + 1
<= len G2 )
by A63, NAT_1:12, NAT_1:13;
then A72:
(G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1
by A6, A9, GOBOARD5:2;
( 1
<= i1 + 1 &
i1 + 1
<= len G1 )
by A71, NAT_1:12, NAT_1:13;
then
(G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1
by A13, A8, GOBOARD5:2;
then
(G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1
by A1, A4, A5, A13, A8, A7, A6, A9, A63, A71, A72, Th6;
then
r9 <= (G1 * ((i1 + 1),1)) `1
by A66, XXREAL_0:2;
then
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & (G1 * (1,(j1 -' 1))) `2 <= s & s <= (G1 * (1,j1)) `2 ) }
by A64, A69, A68;
hence
p in cell (
G1,
i1,
(j1 -' 1))
by A5, A53, A55, A54, A71, GOBRD11:32;
verum end; end; end; hence
p in cell (
G1,
i1,
(j1 -' 1))
;
verum end; end; end; hence
p in cell (
G1,
i1,
(j1 -' 1))
;
verum end; end;