let G be Go-board; ( 1 < width G & 1 < len G implies 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]|)} )
assume that
A1:
1 < width G
and
A2:
1 < len G
; 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]|)}
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);
A3:
((len G) -' 1) + 1 = len G
by A2, XREAL_1:237;
then A4:
(len G) -' 1 >= 1
by A2, NAT_1:13;
A5:
(len G) -' 1 < len G
by A3, NAT_1:13;
then
(G * ((len G) -' 1),(width G)) `1 < (G * (len G),(width G)) `1
by A1, A4, GOBOARD5:4;
then A6:
((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ) > 0
by XREAL_1:52;
then
1 < ((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1
by XREAL_1:31, XREAL_1:131;
then A7:
1 / (((1 / 2) * (((G * (len G),(width G)) `1 ) - ((G * ((len G) -' 1),(width G)) `1 ))) + 1) < 1
by XREAL_1:214;
A8: (G * (len G),(width G)) `2 =
(G * 1,(width G)) `2
by A1, A2, GOBOARD5:2
.=
(G * ((len G) -' 1),(width G)) `2
by A1, A4, A5, GOBOARD5:2
;
A9: (((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 A8, Lm1
.=
((G * (len G),(width G)) `2 ) + (|[0 ,1]| `2 )
by EUCLID:56
.=
((G * (len G),(width G)) + |[0 ,1]|) `2
by Lm1
;
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 A6, XCMPLX_1:107
;
(((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
;
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 A9, 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 A6, A7;
then A11:
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 TOPREAL1:11;
set I1 = Int (cell G,(len G),(width G));
set I2 = Int (cell G,((len G) -' 1),(width G));
A12: ((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
;
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;
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 A3, A4, A5, Th58;
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 A11, A13, A12, XBOOLE_1:13; verum