Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Andrzej Trybulec
- Received October 17, 1995
- MML identifier: GOBOARD8
- [
Mizar article,
MML identifier index
]
environ
vocabulary PRE_TOPC, EUCLID, SEQM_3, GOBOARD5, FINSEQ_1, GOBOARD2, TREES_1,
TOPREAL1, ARYTM_3, BOOLE, TOPS_1, ARYTM_1, MCART_1, GOBOARD1, RELAT_1,
MATRIX_1, ABSVALUE, FINSEQ_4;
notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, ABSVALUE, BINARITH,
FINSEQ_1, FINSEQ_4, MATRIX_1, STRUCT_0, PRE_TOPC, TOPS_1, EUCLID,
TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5;
constructors TOPS_1, GROUP_1, GOBOARD5, GOBOARD2, SEQM_3, REAL_1, BINARITH,
FINSEQ_4, MEMBERED;
clusters STRUCT_0, GOBOARD5, RELSET_1, GOBOARD2, EUCLID, ARYTM_3, MEMBERED;
requirements REAL, NUMERALS, SUBSET, ARITHM;
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;
Back to top