let G be Go-board; ( 1 < len G & 1 < width G implies LSeg (((G * ((len G),(width G))) + |[1,1]|),(((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) c= ((Int (cell (G,(len G),(width G)))) \/ (Int (cell (G,(len G),((width G) -' 1))))) \/ {((G * ((len G),(width G))) + |[1,0]|)} )
assume that
A1:
1 < len G
and
A2:
1 < width G
; LSeg (((G * ((len G),(width G))) + |[1,1]|),(((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) c= ((Int (cell (G,(len G),(width G)))) \/ (Int (cell (G,(len G),((width G) -' 1))))) \/ {((G * ((len G),(width G))) + |[1,0]|)}
set q2 = G * ((len G),(width G));
set q3 = G * ((len G),((width G) -' 1));
set r = 1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1);
A3:
((width G) -' 1) + 1 = width G
by A2, XREAL_1:235;
then A4:
(width G) -' 1 >= 1
by A2, NAT_1:13;
A5:
(width G) -' 1 < width G
by A3, NAT_1:13;
then
(G * ((len G),((width G) -' 1))) `2 < (G * ((len G),(width G))) `2
by A1, A4, GOBOARD5:4;
then A6:
((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2) > 0
by XREAL_1:50;
then
1 < ((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1
by XREAL_1:29, XREAL_1:129;
then A7:
1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1) < 1
by XREAL_1:212;
A8: (G * ((len G),(width G))) `1 =
(G * ((len G),1)) `1
by A1, A2, GOBOARD5:2
.=
(G * ((len G),((width G) -' 1))) `1
by A1, A4, A5, GOBOARD5:2
;
A9: (((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) + |[1,1]|)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|))) `1 =
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) + |[1,1]|)) `1) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `1)
by Lm1
.=
((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (((G * ((len G),(width G))) + |[1,1]|) `1)) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `1)
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (((G * ((len G),(width G))) + |[1,1]|) `1)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|) `1))
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (((G * ((len G),(width G))) `1) + (|[1,1]| `1))) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|) `1))
by Lm1
.=
((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (((G * ((len G),(width G))) `1) + (|[1,1]| `1))) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) `1) + (|[1,0]| `1)))
by Lm1
.=
((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (((G * ((len G),(width G))) `1) + 1)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) `1) + (|[1,0]| `1)))
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `1)) + ((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * 1)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) `1) + 1))
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `1)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) `1))) + ((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) + (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)))
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `1)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1)))) `1)))) + 1
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `1)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (((G * ((len G),(width G))) `1) + ((G * ((len G),(width G))) `1))))) + 1
by A8, Lm1
.=
((G * ((len G),(width G))) `1) + (|[1,0]| `1)
by EUCLID:52
.=
((G * ((len G),(width G))) + |[1,0]|) `1
by Lm1
;
A10: (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * ((len G),(width G))) `2))) - ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * ((len G),((width G) -' 1))) `2)))) + (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) =
(1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)
.=
1
by A6, XCMPLX_1:106
;
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) + |[1,1]|)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|))) `2 =
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) + |[1,1]|)) `2) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `2)
by Lm1
.=
((((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (G * ((len G),(width G)))) + ((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * |[1,1]|)) `2) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `2)
by RLVECT_1:def 5
.=
((((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (G * ((len G),(width G)))) `2) + (((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * |[1,1]|) `2)) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `2)
by Lm1
.=
((((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (G * ((len G),(width G)))) `2) + ((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (|[1,1]| `2))) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `2)
by Lm3
.=
((((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * (G * ((len G),(width G)))) `2) + ((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * 1)) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `2)
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `2)) + (1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)))) + (((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) `2)
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `2)) + (1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)))) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|) `2))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `2)) + (1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)))) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) `2) + (|[1,0]| `2)))
by Lm1
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `2)) + (1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)))) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) `2) + 0))
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `2)) + (1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)))) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1)))) `2)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) `2)) + (1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)))) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (((G * ((len G),(width G))) `2) + ((G * ((len G),((width G) -' 1))) `2))))
by Lm1
.=
((G * ((len G),(width G))) `2) + 0
by A10
.=
((G * ((len G),(width G))) `2) + (|[1,0]| `2)
by EUCLID:52
.=
((G * ((len G),(width G))) + |[1,0]|) `2
by Lm1
;
then ((1 - (1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1))) * ((G * ((len G),(width G))) + |[1,1]|)) + ((1 / (((1 / 2) * (((G * ((len G),(width G))) `2) - ((G * ((len G),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) =
|[(((G * ((len G),(width G))) + |[1,0]|) `1),(((G * ((len G),(width G))) + |[1,0]|) `2)]|
by A9, EUCLID:53
.=
(G * ((len G),(width G))) + |[1,0]|
by EUCLID:53
;
then
(G * ((len G),(width G))) + |[1,0]| in LSeg (((G * ((len G),(width G))) + |[1,1]|),(((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|))
by A6, A7;
then A11:
LSeg (((G * ((len G),(width G))) + |[1,1]|),(((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) = (LSeg (((G * ((len G),(width G))) + |[1,1]|),((G * ((len G),(width G))) + |[1,0]|))) \/ (LSeg (((G * ((len G),(width G))) + |[1,0]|),(((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)))
by TOPREAL1:5;
set I1 = Int (cell (G,(len G),(width G)));
set I2 = Int (cell (G,(len G),((width G) -' 1)));
A12: ((Int (cell (G,(len G),(width G)))) \/ (Int (cell (G,(len G),((width G) -' 1))))) \/ {((G * ((len G),(width G))) + |[1,0]|)} =
(Int (cell (G,(len G),(width G)))) \/ ((Int (cell (G,(len G),((width G) -' 1)))) \/ ({((G * ((len G),(width G))) + |[1,0]|)} \/ {((G * ((len G),(width G))) + |[1,0]|)}))
by XBOOLE_1:4
.=
(Int (cell (G,(len G),(width G)))) \/ (((Int (cell (G,(len G),((width G) -' 1)))) \/ {((G * ((len G),(width G))) + |[1,0]|)}) \/ {((G * ((len G),(width G))) + |[1,0]|)})
by XBOOLE_1:4
.=
((Int (cell (G,(len G),(width G)))) \/ {((G * ((len G),(width G))) + |[1,0]|)}) \/ ((Int (cell (G,(len G),((width G) -' 1)))) \/ {((G * ((len G),(width G))) + |[1,0]|)})
by XBOOLE_1:4
;
A13:
LSeg (((G * ((len G),(width G))) + |[1,1]|),((G * ((len G),(width G))) + |[1,0]|)) c= (Int (cell (G,(len G),(width G)))) \/ {((G * ((len G),(width G))) + |[1,0]|)}
by Th59;
LSeg (((G * ((len G),(width G))) + |[1,0]|),(((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) c= (Int (cell (G,(len G),((width G) -' 1)))) \/ {((G * ((len G),(width G))) + |[1,0]|)}
by A3, A4, A5, Th51;
hence
LSeg (((G * ((len G),(width G))) + |[1,1]|),(((1 / 2) * ((G * ((len G),(width G))) + (G * ((len G),((width G) -' 1))))) + |[1,0]|)) c= ((Int (cell (G,(len G),(width G)))) \/ (Int (cell (G,(len G),((width G) -' 1))))) \/ {((G * ((len G),(width G))) + |[1,0]|)}
by A11, A13, A12, XBOOLE_1:13; verum