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