let G be Go-board; :: thesis:
assume A1: ( 1 < width G & 1 < len G ) ; :: thesis:
set q2 = G * (len G),(width G);
set q3 = G * ((len G) -' 1),(width G);
set r = 1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1);
A2: ((len G) -' 1) + 1 = len G by A1, XREAL_1:237;
then A3: (len G) -' 1 >= 1 by A1, NAT_1:13;
A4: (len G) -' 1 < len G by A2, NAT_1:13;
A5: (G * (len G),(width G)) `2 = (G * 1,(width G)) `2 by A1, GOBOARD5:2
.= (G * ((len G) -' 1),(width G)) `2 by A1, A3, A4, GOBOARD5:2 ;
(G * ((len G) -' 1),(width G)) `1 < (G * (len G),(width G)) `1 by A1, A3, A4, GOBOARD5:4;
then ((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ) > 0 by XREAL_1:52;
then (1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 )) > 0 by XREAL_1:131;
then A7: 1 < ((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1 by XREAL_1:31;
then A8: 0 < 1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1) ;
A9: 1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1) < 1 by A7, XREAL_1:214;
A10: (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((1 / 2) * ((G * (len G),(width G)) `1 ))) - ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((1 / 2) * ((G * ((len G) -' 1),(width G)) `1 )))) + (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) = (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)
.= 1 by A7, XCMPLX_1:107 ;
A11: (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) + |[1,1]|)) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|))) `1 = (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) + |[1,1]|)) `1 ) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `1 ) by Lm1
.= ((((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (G * (len G),(width G))) + ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * |[1,1]|)) `1 ) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `1 ) by EUCLID:36
.= ((((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (G * (len G),(width G))) `1 ) + (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * |[1,1]|) `1 )) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `1 ) by Lm1
.= ((((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (G * (len G),(width G))) `1 ) + ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (|[1,1]| `1 ))) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `1 ) by Lm3
.= ((((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (G * (len G),(width G))) `1 ) + ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * 1)) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `1 ) by EUCLID:56
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `1 )) + (1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)))) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `1 ) by Lm3
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `1 )) + (1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)))) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|) `1 )) by Lm3
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `1 )) + (1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)))) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) `1 ) + (|[0 ,1]| `1 ))) by Lm1
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `1 )) + (1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)))) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) `1 ) + 0 )) by EUCLID:56
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `1 )) + (1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)))) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((1 / 2) * (((G * (len G),(width G)) + (G * ((len G) -' 1),(width G))) `1 ))) by Lm3
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `1 )) + (1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)))) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((1 / 2) * (((G * (len G),(width G)) `1 ) + ((G * ((len G) -' 1),(width G)) `1 )))) by Lm1
.= ((G * (len G),(width G)) `1 ) + 0 by A10
.= ((G * (len G),(width G)) `1 ) + (|[0 ,1]| `1 ) by EUCLID:56
.= ((G * (len G),(width G)) + |[0 ,1]|) `1 by Lm1 ;
(((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) + |[1,1]|)) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|))) `2 = (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) + |[1,1]|)) `2 ) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `2 ) by Lm1
.= ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (((G * (len G),(width G)) + |[1,1]|) `2 )) + (((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) `2 ) by Lm3
.= ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (((G * (len G),(width G)) + |[1,1]|) `2 )) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|) `2 )) by Lm3
.= ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (((G * (len G),(width G)) `2 ) + (|[1,1]| `2 ))) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|) `2 )) by Lm1
.= ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (((G * (len G),(width G)) `2 ) + (|[1,1]| `2 ))) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) `2 ) + (|[0 ,1]| `2 ))) by Lm1
.= ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * (((G * (len G),(width G)) `2 ) + 1)) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) `2 ) + (|[0 ,1]| `2 ))) by EUCLID:56
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `2 )) + ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * 1)) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) `2 ) + 1)) by EUCLID:56
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `2 )) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) `2 ))) + ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) + (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)))
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `2 )) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((1 / 2) * (((G * (len G),(width G)) + (G * ((len G) -' 1),(width G))) `2 )))) + 1 by Lm3
.= (((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) `2 )) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * ((1 / 2) * (((G * (len G),(width G)) `2 ) + ((G * (len G),(width G)) `2 ))))) + 1 by A5, Lm1
.= ((G * (len G),(width G)) `2 ) + (|[0 ,1]| `2 ) by EUCLID:56
.= ((G * (len G),(width G)) + |[0 ,1]|) `2 by Lm1 ;
then ((1 - (1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1))) * ((G * (len G),(width G)) + |[1,1]|)) + ((1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1)) * (((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) = |[(((G * (len G),(width G)) + |[0 ,1]|) `1 ),(((G * (len G),(width G)) + |[0 ,1]|) `2 )]| by A11, EUCLID:57
.= (G * (len G),(width G)) + |[0 ,1]| by EUCLID:57 ;
then (G * (len G),(width G)) + |[0 ,1]| in LSeg ((G * (len G),(width G)) + |[1,1]|),(((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|) by A8, A9;
then A12: LSeg ((G * (len G),(width G)) + |[1,1]|),(((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|) = (LSeg ((G * (len G),(width G)) + |[1,1]|),((G * (len G),(width G)) + |[0 ,1]|)) \/ (LSeg ((G * (len G),(width G)) + |[0 ,1]|),(((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|)) by A8, A9, TOPREAL1:11;
set I1 = Int (cell G,(len G),(width G));
set I2 = Int (cell G,((len G) -' 1),(width G));
A13: LSeg ((G * (len G),(width G)) + |[1,1]|),((G * (len G),(width G)) + |[0 ,1]|) c= (Int (cell G,(len G),(width G))) \/ {((G * (len G),(width G)) + |[0 ,1]|)} by Th66;
A14: LSeg ((G * (len G),(width G)) + |[0 ,1]|),(((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|) c= (Int (cell G,((len G) -' 1),(width G))) \/ {((G * (len G),(width G)) + |[0 ,1]|)} by A2, A3, A4, Th58;
((Int (cell G,(len G),(width G))) \/ (Int (cell G,((len G) -' 1),(width G)))) \/ {((G * (len G),(width G)) + |[0 ,1]|)} = (Int (cell G,(len G),(width G))) \/ ((Int (cell G,((len G) -' 1),(width G))) \/ ({((G * (len G),(width G)) + |[0 ,1]|)} \/ {((G * (len G),(width G)) + |[0 ,1]|)})) by XBOOLE_1:4
.= (Int (cell G,(len G),(width G))) \/ (((Int (cell G,((len G) -' 1),(width G))) \/ {((G * (len G),(width G)) + |[0 ,1]|)}) \/ {((G * (len G),(width G)) + |[0 ,1]|)}) by XBOOLE_1:4
.= ((Int (cell G,(len G),(width G))) \/ {((G * (len G),(width G)) + |[0 ,1]|)}) \/ ((Int (cell G,((len G) -' 1),(width G))) \/ {((G * (len G),(width G)) + |[0 ,1]|)}) by XBOOLE_1:4 ;
hence LSeg ((G * (len G),(width G)) + |[1,1]|),(((1 / 2) * ((G * (len G),(width G)) + (G * ((len G) -' 1),(width G)))) + |[0 ,1]|) c= ((Int (cell G,(len G),(width G))) \/ (Int (cell G,((len G) -' 1),(width G)))) \/ {((G * (len G),(width G)) + |[0 ,1]|)} by A12, A13, A14, XBOOLE_1:13; :: thesis: