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,(j2 -' 1)) c= cell (G1,i1,(j1 -' 1))
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,(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) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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 ) ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A24: i2 < len G2 ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A30: i1 < len G1 ; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum
end;
suppose that A31: j1 = 1 and
A32: 1 < j2 ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A39: i2 < len G2 ; :: thesis: 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 :: thesis: p in cell (G1,i1,(j1 -' 1))
per cases ( i1 = len G1 or i1 < len G1 ) by A12, XXREAL_0:1;
suppose A45: i1 = len G1 ; :: thesis: 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 A40, A44;
hence p in cell (G1,i1,(j1 -' 1)) by A33, A45, GOBRD11:27; :: thesis: verum
end;
suppose A46: i1 < len G1 ; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum
end;
suppose ( 1 < j1 & j2 = 1 ) ; :: thesis: p in cell (G1,i1,(j1 -' 1))
hence p in cell (G1,i1,(j1 -' 1)) by A1, A2, A4, A7, A10, Th4; :: thesis: verum
end;
suppose A48: ( 1 < j1 & 1 < j2 ) ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A63: i2 < len G2 ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A71: i1 < len G1 ; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,(j1 -' 1)) ; :: thesis: verum
end;
end;