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