let i1, i2, j1, j2 be Nat; :: thesis: for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 < len G1 & 1 <= j1 & j1 <= width G1 & 1 <= i2 & i2 < len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds

(G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1

let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & 1 <= i1 & i1 < len G1 & 1 <= j1 & j1 <= width G1 & 1 <= i2 & i2 < len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) implies (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1 )

assume that

A1: Values G1 c= Values G2 and

A2: 1 <= i1 and

A3: i1 < len G1 and

A4: ( 1 <= j1 & j1 <= width G1 ) and

A5: 1 <= i2 and

A6: i2 < len G2 and

A7: ( 1 <= j2 & j2 <= width G2 ) and

A8: G1 * (i1,j1) = G2 * (i2,j2) ; :: thesis: (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1

set p = G1 * ((i1 + 1),j1);

A9: i1 + 1 <= len G1 by A3, NAT_1:13;

1 <= i1 + 1 by A2, NAT_1:13;

then [(i1 + 1),j1] in Indices G1 by A4, A9, MATRIX_0:30;

then G1 * ((i1 + 1),j1) in { (G1 * (i,j)) where i, j is Nat : [i,j] in Indices G1 } ;

then G1 * ((i1 + 1),j1) in Values G1 by MATRIX_0:39;

then G1 * ((i1 + 1),j1) in Values G2 by A1;

then G1 * ((i1 + 1),j1) in { (G2 * (i,j)) where i, j is Nat : [i,j] in Indices G2 } by MATRIX_0:39;

then consider i, j being Nat such that

A10: G1 * ((i1 + 1),j1) = G2 * (i,j) and

A11: [i,j] in Indices G2 ;

A12: 1 <= i by A11, MATRIX_0:32;

A13: i <= len G2 by A11, MATRIX_0:32;

( 1 <= j & j <= width G2 ) by A11, MATRIX_0:32;

then A14: (G2 * (i,j)) `1 = (G2 * (i,1)) `1 by A12, A13, GOBOARD5:2

.= (G2 * (i,j2)) `1 by A7, A12, A13, GOBOARD5:2 ;

i1 < i1 + 1 by NAT_1:13;

then A15: (G2 * (i2,j2)) `1 < (G2 * (i,j2)) `1 by A2, A4, A8, A9, A10, A14, GOBOARD5:3;

A18: 1 <= i2 + 1 by A5, NAT_1:13;

(G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1

let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & 1 <= i1 & i1 < len G1 & 1 <= j1 & j1 <= width G1 & 1 <= i2 & i2 < len G2 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) implies (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1 )

assume that

A1: Values G1 c= Values G2 and

A2: 1 <= i1 and

A3: i1 < len G1 and

A4: ( 1 <= j1 & j1 <= width G1 ) and

A5: 1 <= i2 and

A6: i2 < len G2 and

A7: ( 1 <= j2 & j2 <= width G2 ) and

A8: G1 * (i1,j1) = G2 * (i2,j2) ; :: thesis: (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),j1)) `1

set p = G1 * ((i1 + 1),j1);

A9: i1 + 1 <= len G1 by A3, NAT_1:13;

1 <= i1 + 1 by A2, NAT_1:13;

then [(i1 + 1),j1] in Indices G1 by A4, A9, MATRIX_0:30;

then G1 * ((i1 + 1),j1) in { (G1 * (i,j)) where i, j is Nat : [i,j] in Indices G1 } ;

then G1 * ((i1 + 1),j1) in Values G1 by MATRIX_0:39;

then G1 * ((i1 + 1),j1) in Values G2 by A1;

then G1 * ((i1 + 1),j1) in { (G2 * (i,j)) where i, j is Nat : [i,j] in Indices G2 } by MATRIX_0:39;

then consider i, j being Nat such that

A10: G1 * ((i1 + 1),j1) = G2 * (i,j) and

A11: [i,j] in Indices G2 ;

A12: 1 <= i by A11, MATRIX_0:32;

A13: i <= len G2 by A11, MATRIX_0:32;

( 1 <= j & j <= width G2 ) by A11, MATRIX_0:32;

then A14: (G2 * (i,j)) `1 = (G2 * (i,1)) `1 by A12, A13, GOBOARD5:2

.= (G2 * (i,j2)) `1 by A7, A12, A13, GOBOARD5:2 ;

i1 < i1 + 1 by NAT_1:13;

then A15: (G2 * (i2,j2)) `1 < (G2 * (i,j2)) `1 by A2, A4, A8, A9, A10, A14, GOBOARD5:3;

A16: now :: thesis: not i <= i2

assume A17:
(G1 * ((i1 + 1),j1)) `1 < (G2 * ((i2 + 1),j2)) `1
; :: thesis: contradictionassume
i <= i2
; :: thesis: contradiction

then ( i = i2 or i < i2 ) by XXREAL_0:1;

hence contradiction by A6, A7, A12, A15, GOBOARD5:3; :: thesis: verum

end;then ( i = i2 or i < i2 ) by XXREAL_0:1;

hence contradiction by A6, A7, A12, A15, GOBOARD5:3; :: thesis: verum

A18: 1 <= i2 + 1 by A5, NAT_1:13;

now :: thesis: not i2 + 1 <= i

hence
contradiction
by A16, NAT_1:13; :: thesis: verumassume
i2 + 1 <= i
; :: thesis: contradiction

then ( i2 + 1 = i or i2 + 1 < i ) by XXREAL_0:1;

hence contradiction by A7, A17, A10, A13, A14, A18, GOBOARD5:3; :: thesis: verum

end;then ( i2 + 1 = i or i2 + 1 < i ) by XXREAL_0:1;

hence contradiction by A7, A17, A10, A13, A14, A18, GOBOARD5:3; :: thesis: verum