:: More on Segments on a Go Board
:: by Andrzej Trybulec
::
:: Received October 17, 1995
:: Copyright (c) 1995-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, FUNCT_1, GOBOARD5, XXREAL_0,
ARYTM_3, FINSEQ_1, GOBOARD2, TREES_1, PARTFUN1, RELAT_1, RLTOPSP1,
XBOOLE_0, TOPREAL1, TARSKI, TOPS_1, ARYTM_1, CARD_1, MCART_1, GOBOARD1,
MATRIX_1, NAT_1, COMPLEX1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1,
NAT_1, NAT_D, PARTFUN1, FINSEQ_1, MATRIX_0, SEQM_3, STRUCT_0, PRE_TOPC,
TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
GOBOARD5, XXREAL_0;
constructors REAL_1, NAT_D, TOPS_1, GOBOARD2, GOBOARD5, GOBOARD1, RELSET_1;
registrations RELSET_1, XREAL_0, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5,
ORDINAL1, NAT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
begin
reserve i,j,k,i1,j1 for Nat,
p for Point of TOP-REAL 2,
x for set;
reserve f for non constant standard special_circular_sequence;
theorem :: GOBOARD8:1
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+1 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) = (GoB f)*(i+1,j) & f/.k = (
GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f
)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f;
theorem :: GOBOARD8:2
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) = (GoB f)*(i+2,j+1) & f/.k =
(GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB
f)*(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f;
theorem :: GOBOARD8:3
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+2,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.(k+2) = (GoB f)*(i+2,j+1) & f/.k = (
GoB f)*(i+1,j)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*
(i,j+1)+(GoB f)*(i+1,j+2))) misses L~f;
theorem :: GOBOARD8:4
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+1 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i,j+1) & (f/.k = (GoB f)*(i,j
) & f/.(k+2) = (GoB f)*(i,j+2) or f/.(k+2) = (GoB f)*(i,j) & f/.k = (GoB f)*(i,
j+2)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i,j+1)+(
GoB f)*(i+1,j+2))) misses L~f;
theorem :: GOBOARD8:5
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
,j+1) & f/.(k+2) = (GoB f)*(i+1,j+2) or f/.(k+2) = (GoB f)*(i,j+1) & f/.k = (
GoB f)*(i+1,j+2)) holds LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB
f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f;
theorem :: GOBOARD8:6
for k st 1 <= k & k+2 <= len f for i,j st 1 <= i & i+2 <= len GoB f &
1 <= j & j+2 <= width GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
,j+1) & f/.(k+2) = (GoB f)*(i+1,j) or f/.(k+2) = (GoB f)*(i,j+1) & f/.k = (GoB
f)*(i+1,j)) holds LSeg(1/2*((GoB f)*(i+1,j)+(GoB f)*(i+2,j+1)), 1/2*((GoB f)*(i
+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f;
theorem :: GOBOARD8:7
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,1) & (f/.k = (GoB f)*(i+2,1) & f/.(k+2) = (GoB f)*(i+1,2
) or f/.(k+2) = (GoB f)*(i+2,1) & f/.k = (GoB f)*(i+1,2)) holds LSeg(1/2*((GoB
f)*(i,1)+(GoB f)*(i+1,1))- |[0,1]|, 1/2*((GoB f)*(i,1)+(GoB f)*(i+1,2))) misses
L~f;
theorem :: GOBOARD8:8
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,1) & (f/.k = (GoB f)*(i,1) & f/.(k+2) = (GoB f)*(i+1,2)
or f/.(k+2) = (GoB f)*(i,1) & f/.k = (GoB f)*(i+1,2)) holds LSeg(1/2*((GoB f)*(
i+1,1)+(GoB f)*(i+2,1))- |[0,1]|, 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,2))) misses
L~f;
theorem :: GOBOARD8:9
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,width GoB f) & (f/.k = (GoB f)*(i+2,width GoB f) & f/.(k
+2) = (GoB f)*(i+1,width GoB f -' 1) or f/.(k+2) = (GoB f)*(i+2,width GoB f) &
f/.k = (GoB f)*(i+1,width GoB f -' 1)) holds LSeg(1/2*((GoB f)*(i,width GoB f
-' 1)+(GoB f)*(i+1,width GoB f)), 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,
width GoB f))+|[0,1]|) misses L~f;
theorem :: GOBOARD8:10
for k st 1 <= k & k+2 <= len f for i st 1 <= i & i+2 <= len GoB f & f
/.(k+1) = (GoB f)*(i+1,width GoB f) & (f/.k = (GoB f)*(i,width GoB f) & f/.(k+2
) = (GoB f)*(i+1,width GoB f -' 1) or f/.(k+2) = (GoB f)*(i,width GoB f) & f/.k
= (GoB f)*(i+1,width GoB f -' 1)) holds LSeg(1/2*((GoB f)*(i+1,width GoB f -' 1
)+(GoB f)*(i+2,width GoB f)), 1/2*((GoB f)*(i+1,width GoB f)+(GoB f)*(i+2,width
GoB f))+|[0,1]|) misses L~f;
theorem :: GOBOARD8:11
for k st 1 <= k & k+2 <= len f for i,j st 1 <= j & j+1 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
,j+1) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i,j+1) & f/.k = (
GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f
)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f;
theorem :: GOBOARD8:12
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j+2) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i+1,j+2) & f/.k =
(GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB
f)*(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f;
theorem :: GOBOARD8:13
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j+2) & f/.(k+2) = (GoB f)*(i,j+1) or f/.(k+2) = (GoB f)*(i+1,j+2) & f/.k = (
GoB f)*(i,j+1)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*
(i+1,j)+(GoB f)*(i+2,j+1))) misses L~f;
theorem :: GOBOARD8:14
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+1 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j) & (f/.k = (GoB f)*(i,j
) & f/.(k+2) = (GoB f)*(i+2,j) or f/.(k+2) = (GoB f)*(i,j) & f/.k = (GoB f)*(i+
2,j)) holds LSeg(1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j+1)), 1/2*((GoB f)*(i+1,j)+(
GoB f)*(i+2,j+1))) misses L~f;
theorem :: GOBOARD8:15
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j) & f/.(k+2) = (GoB f)*(i+2,j+1) or f/.(k+2) = (GoB f)*(i+1,j) & f/.k = (
GoB f)*(i+2,j+1)) holds LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB
f)*(i+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f;
theorem :: GOBOARD8:16
for k st 1 <= k & k+2 <= len f for j,i st 1 <= j & j+2 <= width GoB f
& 1 <= i & i+2 <= len GoB f & f/.(k+1) = (GoB f)*(i+1,j+1) & (f/.k = (GoB f)*(i
+1,j) & f/.(k+2) = (GoB f)*(i,j+1) or f/.(k+2) = (GoB f)*(i+1,j) & f/.k = (GoB
f)*(i,j+1)) holds LSeg(1/2*((GoB f)*(i,j+1)+(GoB f)*(i+1,j+2)), 1/2*((GoB f)*(i
+1,j+1)+(GoB f)*(i+2,j+2))) misses L~f;
theorem :: GOBOARD8:17
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(1,j+1) & (f/.k = (GoB f)*(1,j+2) & f/.(k+2) = (GoB f)*(2,j+
1) or f/.(k+2) = (GoB f)*(1,j+2) & f/.k = (GoB f)*(2,j+1)) holds LSeg(1/2*((GoB
f)*(1,j)+(GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB f)*(1,j)+(GoB f)*(2,j+1))) misses
L~f;
theorem :: GOBOARD8:18
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(1,j+1) & (f/.k = (GoB f)*(1,j) & f/.(k+2) = (GoB f)*(2,j+1)
or f/.(k+2) = (GoB f)*(1,j) & f/.k = (GoB f)*(2,j+1)) holds LSeg(1/2*((GoB f)*(
1,j+1)+(GoB f)*(1,j+2))- |[1,0]|, 1/2*((GoB f)*(1,j+1)+(GoB f)*(2,j+2))) misses
L~f;
theorem :: GOBOARD8:19
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(len GoB f,j+1) & (f/.k = (GoB f)*(len GoB f,j+2) & f/.(k+2)
= (GoB f)*(len GoB f -' 1,j+1) or f/.(k+2) = (GoB f)*(len GoB f,j+2) & f/.k = (
GoB f)*(len GoB f -' 1,j+1)) holds LSeg(1/2*((GoB f)*(len GoB f -' 1,j)+(GoB f)
*(len GoB f,j+1)), 1/2*((GoB f)*(len GoB f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|)
misses L~f;
theorem :: GOBOARD8:20
for k st 1 <= k & k+2 <= len f for j st 1 <= j & j+2 <= width GoB f &
f/.(k+1) = (GoB f)*(len GoB f,j+1) & (f/.k = (GoB f)*(len GoB f,j) & f/.(k+2) =
(GoB f)*(len GoB f -' 1,j+1) or f/.(k+2) = (GoB f)*(len GoB f,j) & f/.k = (GoB
f)*(len GoB f -' 1,j+1)) holds LSeg(1/2*((GoB f)*(len GoB f -' 1,j+1)+(GoB f)*(
len GoB f,j+2)), 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(len GoB f,j+2))+|[1,0]|)
misses L~f;
reserve P for Subset of TOP-REAL 2;
theorem :: GOBOARD8:21
(for p st p in P holds p`1 < (GoB f)*(1,1)`1) implies P misses L~f;
theorem :: GOBOARD8:22
(for p st p in P holds p`1 > (GoB f)*(len GoB f,1)`1) implies P misses L~f;
theorem :: GOBOARD8:23
(for p st p in P holds p`2 < (GoB f)*(1,1)`2) implies P misses L~f;
theorem :: GOBOARD8:24
(for p st p in P holds p`2 > (GoB f)*(1,width GoB f)`2) implies P misses L~f;
theorem :: GOBOARD8:25
for i st 1 <= i & i+2 <= len GoB f holds LSeg(1/2*((GoB f)*(i,1)+(GoB
f)*(i+1,1))- |[0,1]|, 1/2*((GoB f)*(i+1,1)+(GoB f)*(i+2,1))- |[0,1]|) misses L~
f;
theorem :: GOBOARD8:26
LSeg((GoB f)*(1,1)- |[1,1]|,1/2*((GoB f)*(1,1)+(GoB f)*(2,1))- |[0,1]|
) misses L~f;
theorem :: GOBOARD8:27
LSeg(1/2*((GoB f)*(len GoB f -' 1,1)+(GoB f)*(len GoB f,1))- |[0,1]|,
(GoB f)*(len GoB f,1)+|[1,-1]|) misses L~f;
theorem :: GOBOARD8:28
for i st 1 <= i & i+2 <= len GoB f holds LSeg(1/2*((GoB f)*(i,width
GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|, 1/2*((GoB f)*(i+1,width GoB f)+(GoB
f)*(i+2,width GoB f))+|[0,1]|) misses L~f;
theorem :: GOBOARD8:29
LSeg((GoB f)*(1,width GoB f)+|[-1,1]|, 1/2*((GoB f)*(1,width GoB f)+(
GoB f)*(2,width GoB f))+|[0,1]|) misses L~f;
theorem :: GOBOARD8:30
LSeg(1/2*((GoB f)*(len GoB f -' 1,width GoB f)+ (GoB f)*(len GoB f,
width GoB f))+|[0,1]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|) misses L~f;
theorem :: GOBOARD8:31
for j st 1 <= j & j+2 <= width GoB f holds LSeg(1/2*((GoB f)*(1,j)+(
GoB f)*(1,j+1))- |[1,0]|, 1/2*((GoB f)*(1,j+1)+(GoB f)*(1,j+2))- |[1,0]|)
misses L~f;
theorem :: GOBOARD8:32
LSeg((GoB f)*(1,1)- |[1,1]|,1/2*((GoB f)*(1,1)+(GoB f)*(1,2))- |[1,0]|
) misses L~f;
theorem :: GOBOARD8:33
LSeg(1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*(1,width GoB f))- |[1,0
]| , (GoB f)*(1,width GoB f)+|[-1,1]|) misses L~f;
theorem :: GOBOARD8:34
for j st 1 <= j & j+2 <= width GoB f holds LSeg(1/2*((GoB f)*(len GoB
f,j)+(GoB f)*(len GoB f,j+1))+|[1,0]|, 1/2*((GoB f)*(len GoB f,j+1)+(GoB f)*(
len GoB f,j+2))+|[1,0]|) misses L~f;
theorem :: GOBOARD8:35
LSeg((GoB f)*(len GoB f,1)+|[1,-1]|, 1/2*((GoB f)*(len GoB f,1)+(GoB f
)*(len GoB f,2))+|[1,0]|) misses L~f;
theorem :: GOBOARD8:36
LSeg(1/2*((GoB f)*(len GoB f,width GoB f -' 1)+ (GoB f)*(len GoB f,
width GoB f))+|[1,0]|, (GoB f)*(len GoB f,width GoB f)+|[1,1]|) misses L~f;
theorem :: GOBOARD8:37
1 <= k & k+1 <= len f implies Int left_cell(f,k) misses L~f;
theorem :: GOBOARD8:38
1 <= k & k+1 <= len f implies Int right_cell(f,k) misses L~f;