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) c= cell (G1,i1,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,j2) c= cell (G1,i1,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,j2) c= cell (G1,i1,j1)
A5: 1 <= i1 by A2, MATRIX_0:32;
A6: j1 <= width G1 by A2, MATRIX_0:32;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in cell (G2,i2,j2) or p in cell (G1,i1,j1) )
assume A7: p in cell (G2,i2,j2) ; :: thesis: p in cell (G1,i1,j1)
A8: 1 <= i2 by A3, MATRIX_0:32;
A9: j2 <= width G2 by A3, MATRIX_0:32;
A10: 1 <= j2 by A3, MATRIX_0:32;
A11: i2 <= len G2 by A3, MATRIX_0:32;
then A12: ( (G2 * (i2,j2)) `1 = (G2 * (i2,1)) `1 & (G2 * (i2,j2)) `2 = (G2 * (1,j2)) `2 ) by A8, A10, A9, GOBOARD5:1, GOBOARD5:2;
A13: 1 <= j1 by A2, MATRIX_0:32;
A14: i1 <= len G1 by A2, MATRIX_0:32;
then A15: ( (G1 * (i1,j1)) `1 = (G1 * (i1,1)) `1 & (G1 * (i1,j1)) `2 = (G1 * (1,j1)) `2 ) by A5, A13, A6, GOBOARD5:1, GOBOARD5:2;
per cases ( ( i2 = len G2 & j2 = width G2 ) or ( i2 = len G2 & j2 < width G2 ) or ( i2 < len G2 & j2 = width G2 ) or ( i2 < len G2 & j2 < width G2 ) ) by A11, A9, XXREAL_0:1;
suppose A16: ( i2 = len G2 & j2 = width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then A17: p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & (G2 * (i2,j2)) `2 <= s ) } by A7, A12, GOBRD11:28;
( i1 = len G1 & j1 = width G1 ) by A1, A2, A4, A8, A10, A16, Th3, Th5;
hence p in cell (G1,i1,j1) by A4, A15, A17, GOBRD11:28; :: thesis: verum
end;
suppose A18: ( i2 = len G2 & j2 < width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & (G2 * (i2,j2)) `2 <= s & s <= (G2 * (1,(j2 + 1))) `2 ) } by A7, A10, A12, GOBRD11:29;
then consider r9, s9 being Real such that
A19: ( p = |[r9,s9]| & (G2 * (i2,j2)) `1 <= r9 & (G2 * (i2,j2)) `2 <= s9 ) and
A20: s9 <= (G2 * (1,(j2 + 1))) `2 ;
A21: i1 = len G1 by A1, A2, A4, A10, A18, Th3;
now :: thesis: p in cell (G1,i1,j1)
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,j1)
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s ) } by A4, A19;
hence p in cell (G1,i1,j1) by A15, A21, A22, GOBRD11:28; :: thesis: verum
end;
suppose A23: j1 < width G1 ; :: thesis: p in cell (G1,i1,j1)
( 1 <= j2 + 1 & j2 + 1 <= width G2 ) by A18, NAT_1:12, NAT_1:13;
then A24: (G2 * (i2,(j2 + 1))) `2 = (G2 * (1,(j2 + 1))) `2 by A8, A11, GOBOARD5:1;
( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by A23, 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 A5, A14, GOBOARD5:1, MATRIX_0:41;
then (G2 * (1,(j2 + 1))) `2 <= (G1 * (1,(j1 + 1))) `2 by A1, A4, A5, A14, A13, A8, A10, A18, A23, A24, Th8;
then s9 <= (G1 * (1,(j1 + 1))) `2 by A20, XXREAL_0:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s & s <= (G1 * (1,(j1 + 1))) `2 ) } by A4, A19;
hence p in cell (G1,i1,j1) by A13, A15, A21, A23, GOBRD11:29; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,j1) ; :: thesis: verum
end;
suppose A25: ( i2 < len G2 & j2 = width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & (G2 * (i2,j2)) `2 <= s ) } by A7, A8, A12, GOBRD11:31;
then consider r9, s9 being Real such that
A26: ( p = |[r9,s9]| & (G2 * (i2,j2)) `1 <= r9 ) and
A27: r9 <= (G2 * ((i2 + 1),1)) `1 and
A28: (G2 * (i2,j2)) `2 <= s9 ;
A29: j1 = width G1 by A1, A2, A4, A8, A25, Th5;
now :: thesis: p in cell (G1,i1,j1)
per cases ( i1 = len G1 or i1 < len G1 ) by A14, XXREAL_0:1;
suppose A30: i1 = len G1 ; :: thesis: p in cell (G1,i1,j1)
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s ) } by A4, A26, A28;
hence p in cell (G1,i1,j1) by A15, A29, A30, GOBRD11:28; :: thesis: verum
end;
suppose A31: i1 < len G1 ; :: thesis: p in cell (G1,i1,j1)
( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by A25, NAT_1:12, NAT_1:13;
then A32: (G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1 by A10, A9, GOBOARD5:2;
( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by A31, NAT_1:12, NAT_1:13;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by A13, A6, GOBOARD5:2;
then (G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A6, A8, A10, A25, A31, A32, Th6;
then r9 <= (G1 * ((i1 + 1),1)) `1 by A27, XXREAL_0:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & (G1 * (i1,j1)) `2 <= s ) } by A4, A26, A28;
hence p in cell (G1,i1,j1) by A5, A15, A29, A31, GOBRD11:31; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,j1) ; :: thesis: verum
end;
suppose A33: ( i2 < len G2 & j2 < width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= j2 + 1 & j2 + 1 <= width G2 ) by NAT_1:12, NAT_1:13;
then A34: (G2 * (i2,(j2 + 1))) `2 = (G2 * (1,(j2 + 1))) `2 by A8, A11, GOBOARD5:1;
( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by A33, NAT_1:12, NAT_1:13;
then (G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1 by A10, A9, GOBOARD5:2;
then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & r <= (G2 * ((i2 + 1),j2)) `1 & (G2 * (i2,j2)) `2 <= s & s <= (G2 * (i2,(j2 + 1))) `2 ) } by A7, A8, A10, A12, A33, A34, GOBRD11:32;
then consider r9, s9 being Real such that
A35: ( p = |[r9,s9]| & (G2 * (i2,j2)) `1 <= r9 ) and
A36: r9 <= (G2 * ((i2 + 1),j2)) `1 and
A37: (G2 * (i2,j2)) `2 <= s9 and
A38: s9 <= (G2 * (i2,(j2 + 1))) `2 ;
now :: thesis: p in cell (G1,i1,j1)
per cases ( ( i1 = len G1 & j1 = width G1 ) or ( i1 = len G1 & j1 < width G1 ) or ( i1 < len G1 & j1 = width G1 ) or ( i1 < len G1 & j1 < width G1 ) ) by A14, A6, XXREAL_0:1;
suppose A39: ( i1 = len G1 & j1 = width G1 ) ; :: thesis: p in cell (G1,i1,j1)
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s ) } by A4, A35, A37;
hence p in cell (G1,i1,j1) by A15, A39, GOBRD11:28; :: thesis: verum
end;
suppose A40: ( i1 = len G1 & j1 < width G1 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by 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 A5, A14, GOBOARD5:1, MATRIX_0:41;
then (G2 * (i2,(j2 + 1))) `2 <= (G1 * (1,(j1 + 1))) `2 by A1, A4, A5, A13, A8, A10, A33, A40, Th8;
then s9 <= (G1 * (1,(j1 + 1))) `2 by A38, XXREAL_0:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s & s <= (G1 * (1,(j1 + 1))) `2 ) } by A4, A35, A37;
hence p in cell (G1,i1,j1) by A13, A15, A40, GOBRD11:29; :: thesis: verum
end;
suppose A41: ( i1 < len G1 & j1 = width G1 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by NAT_1:12, NAT_1:13;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by A13, A6, GOBOARD5:2;
then (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A8, A10, A33, A41, Th6;
then r9 <= (G1 * ((i1 + 1),1)) `1 by A36, XXREAL_0:2;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & (G1 * (i1,j1)) `2 <= s ) } by A4, A35, A37;
hence p in cell (G1,i1,j1) by A5, A15, A41, GOBRD11:31; :: thesis: verum
end;
suppose A42: ( i1 < len G1 & j1 < width G1 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by NAT_1:12, NAT_1:13;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by A13, A6, GOBOARD5:2;
then (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A8, A10, A33, A42, Th6;
then A43: r9 <= (G1 * ((i1 + 1),1)) `1 by A36, XXREAL_0:2;
( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by A42, 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 A5, A14, GOBOARD5:1, MATRIX_0:41;
then (G2 * (i2,(j2 + 1))) `2 <= (G1 * (1,(j1 + 1))) `2 by A1, A4, A5, A13, A8, A10, A33, A42, Th8;
then s9 <= (G1 * (1,(j1 + 1))) `2 by A38, 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)) `2 <= s & s <= (G1 * (1,(j1 + 1))) `2 ) } by A4, A15, A35, A37, A43;
hence p in cell (G1,i1,j1) by A5, A13, A42, GOBRD11:32; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,j1) ; :: thesis: verum
end;
end;