let j, i be Element of NAT ; :: thesis:
let G be Go-board; :: thesis:
assume A1: ( 1 <= j & j < width G & 1 <= i & i + 1 < len G ) ; :: thesis:
set p1 = G * i,j;
set p2 = G * (i + 1),j;
set q2 = G * (i + 1),(j + 1);
set q3 = G * (i + 2),(j + 1);
set r = (((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ));
A2: i + 1 >= 1 by NAT_1:11;
i <= i + 1 by NAT_1:11;
then A3: i < len G by A1, XXREAL_0:2;
then A4: (G * i,j) `2 = (G * 1,j) `2 by A1, GOBOARD5:2
.= (G * (i + 1),j) `2 by A1, A2, GOBOARD5:2 ;
A5: j + 1 >= 1 by NAT_1:11;
A6: (i + 1) + 1 = i + (1 + 1) ;
then A7: i + (1 + 1) <= len G by A1, NAT_1:13;
A8: i + 2 >= 1 by A6, NAT_1:11;
A9: j + 1 <= width G by A1, NAT_1:13;
then A10: (G * (i + 1),(j + 1)) `2 = (G * 1,(j + 1)) `2 by A1, A2, A5, GOBOARD5:2
.= (G * (i + 2),(j + 1)) `2 by A5, A7, A8, A9, GOBOARD5:2 ;
A11: (G * (i + 1),(j + 1)) `1 = (G * (i + 1),1) `1 by A1, A2, A5, A9, GOBOARD5:3
.= (G * (i + 1),j) `1 by A1, A2, GOBOARD5:3 ;
i + 1 < i + 2 by XREAL_1:8;
then (G * (i + 1),(j + 1)) `1 < (G * (i + 2),(j + 1)) `1 by A2, A5, A7, A9, GOBOARD5:4;
then A12: ((G * (i + 1),j) `1 ) - ((G * i,j) `1 ) < ((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ) by A11, XREAL_1:11;
i < i + 1 by XREAL_1:31;
then (G * i,j) `1 < (G * (i + 1),j) `1 by A1, GOBOARD5:4;
then A13: ((G * (i + 1),j) `1 ) - ((G * i,j) `1 ) > 0 by XREAL_1:52;
then A14: 0 < (((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )) by A12, XREAL_1:141;
A15: (((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )) < 1 by A12, A13, XREAL_1:191;
A16: ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )) = ((G * (i + 1),j) `1 ) - ((G * i,j) `1 ) by A12, A13, XCMPLX_1:88;
A17: ((G * (i + 1),j) + (G * (i + 1),(j + 1))) `2 = ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) `2 ) + ((G * (i + 1),(j + 1)) `2 ))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) `2 ) + ((G * (i + 2),(j + 1)) `2 ))) by A4, A10, Lm1
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `2 )) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) `2 ) + ((G * (i + 2),(j + 1)) `2 ))) by Lm1
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `2 )) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) + (G * (i + 2),(j + 1))) `2 )) by Lm1
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `2 )) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `2 ) by Lm3
.= (((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) `2 ) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `2 ) by Lm3
.= (((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) `2 by Lm1 ;
((G * (i + 1),j) + (G * (i + 1),(j + 1))) `1 = ((G * (i + 1),j) `1 ) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) + (1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))))) * ((G * (i + 1),(j + 1)) `1 )) by Lm1
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 ))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) `1 ) + ((G * (i + 2),(j + 1)) `1 ))) by A11, A16
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) `1 ) + ((G * (i + 1),(j + 1)) `1 ))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) + (G * (i + 2),(j + 1))) `1 )) by Lm1
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `1 )) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * (((G * (i + 1),j) + (G * (i + 2),(j + 1))) `1 )) by Lm1
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * (((G * i,j) + (G * (i + 1),(j + 1))) `1 )) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `1 ) by Lm3
.= (((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) `1 ) + ((((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) `1 ) by Lm3
.= (((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) `1 by Lm1 ;
then ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) = |[(((G * (i + 1),j) + (G * (i + 1),(j + 1))) `1 ),(((G * (i + 1),j) + (G * (i + 1),(j + 1))) `2 )]| by A17, EUCLID:57
.= (G * (i + 1),j) + (G * (i + 1),(j + 1)) by EUCLID:57 ;
then (1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))) = ((1 / 2) * ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * i,j) + (G * (i + 1),(j + 1))))) + ((1 / 2) * (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) by EUCLID:36
.= (((1 / 2) * (1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))))) * ((G * i,j) + (G * (i + 1),(j + 1)))) + ((1 / 2) * (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) by EUCLID:34
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))))) + ((1 / 2) * (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) by EUCLID:34
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))))) + (((1 / 2) * ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) by EUCLID:34
.= ((1 - ((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 )))) * ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))))) + (((((G * (i + 1),j) `1 ) - ((G * i,j) `1 )) / (((G * (i + 2),(j + 1)) `1 ) - ((G * i,j) `1 ))) * ((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) by EUCLID:34 ;
then (1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))) in LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) by A14, A15;
then A18: LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) = (LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))) \/ (LSeg ((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1))))) by A14, A15, TOPREAL1:11;
set I1 = Int (cell G,i,j);
set I2 = Int (cell G,(i + 1),j);
A19: LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} by A1, A3, Th45;
A20: LSeg ((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) c= (Int (cell G,(i + 1),j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} by A1, A2, A6, Th43;
((Int (cell G,i,j)) \/ (Int (cell G,(i + 1),j))) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} = (Int (cell G,i,j)) \/ ((Int (cell G,(i + 1),j)) \/ ({((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))})) by XBOOLE_1:4
.= (Int (cell G,i,j)) \/ (((Int (cell G,(i + 1),j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}) by XBOOLE_1:4
.= ((Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}) \/ ((Int (cell G,(i + 1),j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}) by XBOOLE_1:4 ;
hence LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 2),(j + 1)))) c= ((Int (cell G,i,j)) \/ (Int (cell G,(i + 1),j))) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} by A18, A19, A20, XBOOLE_1:13; :: thesis: