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;

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;

end;

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;( 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

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;

end;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)end;

hence
p in cell (G1,i1,j1)
; :: thesis: verumper cases
( j1 = width G1 or j1 < width G1 )
by A6, XXREAL_0:1;

end;

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;hence p in cell (G1,i1,j1) by A15, A21, A22, GOBRD11:28; :: thesis: verum

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;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

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;

end;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)end;

hence
p in cell (G1,i1,j1)
; :: thesis: verumper cases
( i1 = len G1 or i1 < len G1 )
by A14, XXREAL_0:1;

end;

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;hence p in cell (G1,i1,j1) by A15, A29, A30, GOBRD11:28; :: thesis: verum

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;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

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 ;

end;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)end;

hence
p in cell (G1,i1,j1)
; :: thesis: verumper 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;

end;

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;hence p in cell (G1,i1,j1) by A15, A39, GOBRD11:28; :: thesis: verum

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;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

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;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

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;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