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