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 15, 1995
- MML identifier: GOBOARD7
- [
Mizar article,
MML identifier index
]
environ
vocabulary FINSEQ_1, EUCLID, PRE_TOPC, GOBOARD1, ABSVALUE, ARYTM_1, TOPREAL1,
MCART_1, ARYTM_3, MATRIX_1, TREES_1, RELAT_1, SPPOL_1, GOBOARD2, BOOLE,
TOPS_1, GOBOARD5, TARSKI, SEQM_3, FUNCT_1, FINSET_1, CARD_1, FINSEQ_6,
FINSEQ_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, REAL_1, NAT_1,
ABSVALUE, BINARITH, CARD_1, FUNCT_1, FINSEQ_1, FINSET_1, FINSEQ_4,
MATRIX_1, PRE_TOPC, TOPS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
SPPOL_1, FINSEQ_6, GOBOARD5, GROUP_1;
constructors REAL_1, TOPS_1, SPPOL_1, GOBOARD2, GOBOARD5, SEQM_3, BINARITH,
FINSEQ_4, GROUP_1, MEMBERED, XBOOLE_0;
clusters STRUCT_0, GOBOARD5, RELSET_1, GOBOARD2, INT_1, EUCLID, FINSEQ_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve f for non empty FinSequence of TOP-REAL 2,
i,j,k,k1,k2,n,i1,i2,j1,j2 for Nat,
r,s,r1,r2 for Real,
p,q,p1,q1 for Point of TOP-REAL 2,
G for Go-board,
x for set;
theorem :: GOBOARD7:1
abs(r1-r2) > s implies r1+s < r2 or r2+s < r1;
theorem :: GOBOARD7:2
abs(r - s) = 0 iff r = s;
theorem :: GOBOARD7:3
for p,p1,q being Point of TOP-REAL n st p + p1 = q + p1
holds p = q;
theorem :: GOBOARD7:4
for p,p1,q being Point of TOP-REAL n st p1 + p = p1 + q
holds p = q;
theorem :: GOBOARD7:5
p1 in LSeg(p,q) & p`1 = q`1 implies p1`1 = q`1;
theorem :: GOBOARD7:6
p1 in LSeg(p,q) & p`2 = q`2 implies p1`2 = q`2;
theorem :: GOBOARD7:7
1/2*(p+q) in LSeg(p,q);
theorem :: GOBOARD7:8
p`1 = q`1 & q`1 = p1`1 & p`2 <= q`2 & q`2 <= p1`2 implies q in LSeg(p,p1);
theorem :: GOBOARD7:9
p`1 <= q`1 & q`1 <= p1`1 & p`2 = q`2 & q`2 = p1`2 implies q in LSeg(p,p1);
theorem :: GOBOARD7:10
for D being non empty set
for i,j for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M
holds [i,j] in Indices M;
theorem :: GOBOARD7:11
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
1/2*(G*(i,j)+G*(i+1,j+1)) = 1/2*(G*(i,j+1)+G*(i+1,j));
theorem :: GOBOARD7:12
LSeg(f,k) is horizontal implies
ex j st 1 <= j & j <= width GoB f &
for p st p in LSeg(f,k) holds p`2 = (GoB f)*(1,j)`2;
theorem :: GOBOARD7:13
LSeg(f,k) is vertical implies
ex i st 1 <= i & i <= len GoB f &
for p st p in LSeg(f,k) holds p`1 = (GoB f)*(i,1)`1;
theorem :: GOBOARD7:14
f is special & i <= len GoB f & j <= width GoB f implies
Int cell(GoB f,i,j) misses L~f;
begin :: Segments on a Go Board
theorem :: GOBOARD7:15
1 <= i & i <= len G & 1 <= j & j+2 <= width G implies
LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i,j+2)) = { G*(i,j+1) };
theorem :: GOBOARD7:16
1 <= i & i+2 <= len G & 1 <= j & j <= width G implies
LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+2,j)) = { G*(i+1,j) };
theorem :: GOBOARD7:17
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
LSeg(G*(i,j),G*(i,j+1)) /\ LSeg(G*(i,j+1),G*(i+1,j+1)) = { G*(i,j+1) };
theorem :: GOBOARD7:18
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
LSeg(G*(i,j+1),G*(i+1,j+1)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G*
(i+1,j+1) };
theorem :: GOBOARD7:19
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i,j),G*(i,j+1)) = { G*(i,j) };
theorem :: GOBOARD7:20
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
LSeg(G*(i,j),G*(i+1,j)) /\ LSeg(G*(i+1,j),G*(i+1,j+1)) = { G*(i+1,j) };
theorem :: GOBOARD7:21
for i1,j1,i2,j2 being Nat st
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1))
holds i1 = i2 & abs(j1-j2) <= 1;
theorem :: GOBOARD7:22
for i1,j1,i2,j2 being Nat st
1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G &
1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
holds j1 = j2 & abs(i1-i2) <= 1;
theorem :: GOBOARD7:23
for i1,j1,i2,j2 being Nat st
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
holds (i1 = i2 or i1 = i2+1) & (j1 = j2 or j1+1 = j2);
theorem :: GOBOARD7:24
for i1,j1,i2,j2 being Nat st
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2,j2+1))
holds
j1 = j2 &
LSeg(G*(i1,j1),G*(i1,j1+1)) = LSeg(G*(i2,j2),G*(i2,j2+1)) or
j1 = j2+1 &
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G*
(i1,j1) }
or j1+1 = j2 &
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2,j2+1)) = { G*
(i2,j2) };
theorem :: GOBOARD7:25
for i1,j1,i2,j2 being Nat st
1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G &
1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
LSeg(G*(i1,j1),G*(i1+1,j1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
holds
i1 = i2 &
LSeg(G*(i1,j1),G*(i1+1,j1)) = LSeg(G*(i2,j2),G*(i2+1,j2)) or
i1 = i2+1 &
LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i1,j1) }
or i1+1 = i2 &
LSeg(G*(i1,j1),G*(i1+1,j1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i2,j2) };
theorem :: GOBOARD7:26
for i1,j1,i2,j2 being Nat st
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
LSeg(G*(i1,j1),G*(i1,j1+1)) meets LSeg(G*(i2,j2),G*(i2+1,j2))
holds
j1 = j2 &
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i1,j1) }
or j1+1 = j2 &
LSeg(G*(i1,j1),G*(i1,j1+1)) /\ LSeg(G*(i2,j2),G*(i2+1,j2)) = { G*
(i1,j1+1) };
theorem :: GOBOARD7:27
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G &
1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
1/2*(G*(i1,j1)+G*(i1,j1+1)) in LSeg(G*(i2,j2),G*(i2,j2+1)) implies
i1 = i2 & j1 = j2;
theorem :: GOBOARD7:28
1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G &
1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
1/2*(G*(i1,j1)+G*(i1+1,j1)) in LSeg(G*(i2,j2),G*(i2+1,j2)) implies
i1 = i2 & j1 = j2;
theorem :: GOBOARD7:29
1 <= i1 & i1+1 <= len G & 1 <= j1 & j1 <= width G implies
not ex i2,j2 st
1 <= i2 & i2 <= len G & 1 <= j2 & j2+1 <= width G &
1/2*(G*(i1,j1)+G*(i1+1,j1)) in LSeg(G*(i2,j2),G*(i2,j2+1));
theorem :: GOBOARD7:30
1 <= i1 & i1 <= len G & 1 <= j1 & j1+1 <= width G implies
not ex i2,j2 st
1 <= i2 & i2+1 <= len G & 1 <= j2 & j2 <= width G &
1/2*(G*(i1,j1)+G*(i1,j1+1)) in LSeg(G*(i2,j2),G*(i2+1,j2));
begin :: Standard special circular sequences
reserve f for non constant standard special_circular_sequence;
theorem :: GOBOARD7:31
for f being standard (non empty FinSequence of TOP-REAL 2)
st i in dom f & i+1 in dom f holds f/.i <> f/.(i+1);
theorem :: GOBOARD7:32
ex i st i in dom f & (f/.i)`1 <> (f/.1)`1;
theorem :: GOBOARD7:33
ex i st i in dom f & (f/.i)`2 <> (f/.1)`2;
theorem :: GOBOARD7:34
len GoB f > 1;
theorem :: GOBOARD7:35
width GoB f > 1;
theorem :: GOBOARD7:36
len f > 4;
theorem :: GOBOARD7:37
for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f > 4
for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j;
theorem :: GOBOARD7:38
for i,j being Nat st 1 <= i & i < j & j < len f holds f/.i <> f/.j;
theorem :: GOBOARD7:39
for i,j being Nat st 1 < i & i < j & j <= len f holds f/.i <> f/.j;
theorem :: GOBOARD7:40
for i being Nat st 1 < i & i <= len f & f/.i = f/.1 holds i = len f;
theorem :: GOBOARD7:41
1 <= i & i <= len GoB f & 1 <= j & j+1 <= width GoB f &
1/2*((GoB f)*(i,j)+(GoB f)*(i,j+1)) in L~f implies
ex k st 1 <= k & k+1 <= len f &
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k);
theorem :: GOBOARD7:42
1 <= i & i+1 <= len GoB f & 1 <= j & j <= width GoB f &
1/2*((GoB f)*(i,j)+(GoB f)*(i+1,j)) in L~f implies
ex k st 1 <= k & k+1 <= len f &
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k);
theorem :: GOBOARD7:43
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i,j+1) & f/.(k+1) = (GoB f)*(i+1,j+1) &
f/.(k+2) = (GoB f)*(i+1,j);
theorem :: GOBOARD7:44
1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 < len f
&
LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k) &
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i,j+2) & f/.(k+1) = (GoB f)*(i,j+1) &
f/.(k+2) = (GoB f)*(i,j);
theorem :: GOBOARD7:45
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i,j+1) &
f/.(k+2) = (GoB f)*(i,j);
theorem :: GOBOARD7:46
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i+1,j) & f/.(k+1) = (GoB f)*(i+1,j+1) &
f/.(k+2) = (GoB f)*(i,j+1);
theorem :: GOBOARD7:47
1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 < len f
&
LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k) &
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i+2,j) & f/.(k+1) = (GoB f)*(i+1,j) &
f/.(k+2) = (GoB f)*(i,j);
theorem :: GOBOARD7:48
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i+1,j+1) & f/.(k+1) = (GoB f)*(i+1,j) &
f/.(k+2) = (GoB f)*(i,j);
theorem :: GOBOARD7:49
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i+1,j) & f/.(k+1) = (GoB f)*(i+1,j+1) &
f/.(k+2) = (GoB f)*(i,j+1);
theorem :: GOBOARD7:50
1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f & 1 <= k & k+1 < len f
&
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i,j+1) &
f/.(k+2) = (GoB f)*(i,j+2);
theorem :: GOBOARD7:51
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i,j+1) &
f/.(k+2) = (GoB f)*(i+1,j+1);
theorem :: GOBOARD7:52
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) = LSeg(f,k) &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i,j+1) & f/.(k+1) = (GoB f)*(i+1,j+1) &
f/.(k+2) = (GoB f)*(i+1,j);
theorem :: GOBOARD7:53
1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f & 1 <= k & k+1 < len f
&
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i+1,j) &
f/.(k+2) = (GoB f)*(i+2,j);
theorem :: GOBOARD7:54
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f & 1 <=
k & k+1 < len f &
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) = LSeg(f,k) &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) = LSeg(f,k+1) implies
f/.k = (GoB f)*(i,j) & f/.(k+1) = (GoB f)*(i+1,j) &
f/.(k+2) = (GoB f)*(i+1,j+1);
theorem :: GOBOARD7:55
1 <= i & i <= len GoB f & 1 <= j & j+1 < width GoB f &
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f implies
f/.1 = (GoB f)*(i,j+1) &
(f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i,j+2) or
f/.2 = (GoB f)*(i,j+2) & f/.(len f-'1) = (GoB f)*(i,j))
or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i,j+2) & f/.(k+2) = (GoB f)*(i,j));
theorem :: GOBOARD7:56
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f implies
f/.1 = (GoB f)*(i,j+1) &
(f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+1,j+1) or
f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j))
or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i,j+1) &
(f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or
f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j));
theorem :: GOBOARD7:57
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f &
LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+1,j)) c= L~f implies
f/.1 = (GoB f)*(i+1,j+1) &
(f/.2 = (GoB f)*(i,j+1) & f/.(len f-'1) = (GoB f)*(i+1,j) or
f/.2 = (GoB f)*(i+1,j) & f/.(len f-'1) = (GoB f)*(i,j+1))
or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i+1,j) & f/.(k+2) = (GoB f)*(i,j+1));
theorem :: GOBOARD7:58
1 <= i & i+1 < len GoB f & 1 <= j & j <= width GoB f &
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f implies
f/.1 = (GoB f)*(i+1,j) &
(f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+2,j) or
f/.2 = (GoB f)*(i+2,j) & f/.(len f-'1) = (GoB f)*(i,j))
or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i+2,j) & f/.(k+2) = (GoB f)*(i,j));
theorem :: GOBOARD7:59
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f implies
f/.1 = (GoB f)*(i+1,j) &
(f/.2 = (GoB f)*(i,j) & f/.(len f-'1) = (GoB f)*(i+1,j+1) or
f/.2 = (GoB f)*(i+1,j+1) & f/.(len f-'1) = (GoB f)*(i,j))
or ex k st 1 <= k & k+1 < len f & f/.(k+1) = (GoB f)*(i+1,j) &
(f/.k = (GoB f)*(i,j) & f/.(k+2) = (GoB f)*(i+1,j+1) or
f/.k = (GoB f)*(i+1,j+1) & f/.(k+2) = (GoB f)*(i,j));
theorem :: GOBOARD7:60
1 <= i & i+1 <= len GoB f & 1 <= j & j+1 <= width GoB f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f &
LSeg((GoB f)*(i+1,j+1),(GoB f)*(i,j+1)) c= L~f implies
f/.1 = (GoB f)*(i+1,j+1) &
(f/.2 = (GoB f)*(i+1,j) & f/.(len f-'1) = (GoB f)*(i,j+1) or
f/.2 = (GoB f)*(i,j+1) & f/.(len f-'1) = (GoB f)*(i+1,j))
or ex k st 1 <= k & k+1 < len 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 = (GoB f)*(i,j+1) & f/.(k+2) = (GoB f)*(i+1,j));
theorem :: GOBOARD7:61
1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies
not ( LSeg((GoB f)*(i,j),(GoB f)*(i,j+1)) c= L~f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i,j+2)) c= L~f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f);
theorem :: GOBOARD7:62
1 <= i & i < len GoB f & 1 <= j & j+1 < width GoB f implies
not ( LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f &
LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+1,j+2)) c= L~f &
LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f);
theorem :: GOBOARD7:63
1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies
not ( LSeg((GoB f)*(i,j),(GoB f)*(i+1,j)) c= L~f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+2,j)) c= L~f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f);
theorem :: GOBOARD7:64
1 <= j & j < width GoB f & 1 <= i & i+1 < len GoB f implies
not ( LSeg((GoB f)*(i,j+1),(GoB f)*(i+1,j+1)) c= L~f &
LSeg((GoB f)*(i+1,j+1),(GoB f)*(i+2,j+1)) c= L~f &
LSeg((GoB f)*(i+1,j),(GoB f)*(i+1,j+1)) c= L~f);
Back to top