let i1, i2, j1, j2 be Nat; :: thesis: for G1, G2 being Go-board st G1 * (i1,(j1 + 1)) in 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,(j2 + 1))) `2 <= (G1 * (i1,(j1 + 1))) `2

let G1, G2 be Go-board; :: thesis: ( G1 * (i1,(j1 + 1)) in 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,(j2 + 1))) `2 <= (G1 * (i1,(j1 + 1))) `2 )

assume that

A1: G1 * (i1,(j1 + 1)) in Values G2 and

A2: ( 1 <= i1 & i1 <= len G1 & 1 <= j1 ) and

A3: j1 < width G1 and

A4: ( 1 <= i2 & i2 <= len G2 ) and

A5: 1 <= j2 and

A6: j2 < width G2 and

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

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

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

then consider i, j being Nat such that

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

A9: [i,j] in Indices G2 ;

A10: 1 <= j by A9, MATRIX_0:32;

A11: j <= width G2 by A9, MATRIX_0:32;

( 1 <= i & i <= len G2 ) by A9, MATRIX_0:32;

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

.= (G2 * (i2,j)) `2 by A4, A10, A11, GOBOARD5:1 ;

( j1 < j1 + 1 & j1 + 1 <= width G1 ) by A3, NAT_1:13;

then A13: (G2 * (i2,j2)) `2 < (G2 * (i2,j)) `2 by A2, A7, A8, A12, GOBOARD5:4;

A16: 1 <= j2 + 1 by A5, NAT_1:13;

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

let G1, G2 be Go-board; :: thesis: ( G1 * (i1,(j1 + 1)) in 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,(j2 + 1))) `2 <= (G1 * (i1,(j1 + 1))) `2 )

assume that

A1: G1 * (i1,(j1 + 1)) in Values G2 and

A2: ( 1 <= i1 & i1 <= len G1 & 1 <= j1 ) and

A3: j1 < width G1 and

A4: ( 1 <= i2 & i2 <= len G2 ) and

A5: 1 <= j2 and

A6: j2 < width G2 and

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

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

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

then consider i, j being Nat such that

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

A9: [i,j] in Indices G2 ;

A10: 1 <= j by A9, MATRIX_0:32;

A11: j <= width G2 by A9, MATRIX_0:32;

( 1 <= i & i <= len G2 ) by A9, MATRIX_0:32;

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

.= (G2 * (i2,j)) `2 by A4, A10, A11, GOBOARD5:1 ;

( j1 < j1 + 1 & j1 + 1 <= width G1 ) by A3, NAT_1:13;

then A13: (G2 * (i2,j2)) `2 < (G2 * (i2,j)) `2 by A2, A7, A8, A12, GOBOARD5:4;

A14: now :: thesis: not j <= j2

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

then ( j = j2 or j < j2 ) by XXREAL_0:1;

hence contradiction by A4, A6, A10, A13, GOBOARD5:4; :: thesis: verum

end;then ( j = j2 or j < j2 ) by XXREAL_0:1;

hence contradiction by A4, A6, A10, A13, GOBOARD5:4; :: thesis: verum

A16: 1 <= j2 + 1 by A5, NAT_1:13;

now :: thesis: not j2 + 1 <= j

hence
contradiction
by A14, NAT_1:13; :: thesis: verumassume
j2 + 1 <= j
; :: thesis: contradiction

then ( j2 + 1 = j or j2 + 1 < j ) by XXREAL_0:1;

hence contradiction by A4, A15, A8, A11, A12, A16, GOBOARD5:4; :: thesis: verum

end;then ( j2 + 1 = j or j2 + 1 < j ) by XXREAL_0:1;

hence contradiction by A4, A15, A8, A11, A12, A16, GOBOARD5:4; :: thesis: verum