environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, EUCLID, FINSEQ_1, REAL_1, SUBSET_1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, CARD_1, NAT_1, RELAT_1, FINSEQ_3, FUNCT_1, XBOOLE_0, TARSKI, ORDINAL2, PARTFUN1, MCART_1, TOPREAL1, RLTOPSP1, MATRIX_1, TREES_1, INCSP_1, ZFMISC_1, ORDINAL4, GOBOARD1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, XXREAL_0, COMPLEX1, NAT_1, VALUED_0, FINSEQ_1, FINSEQ_3, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, MATRIX_0, MATRIX_1;
definitions TARSKI, SEQM_3;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, FINSEQ_2, FINSEQ_3, MATRIX_0, TOPREAL1, TOPREAL3, FINSEQ_4, RELAT_1, INT_1, PARTFUN2, XBOOLE_0, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, PARTFUN1, SEQM_3, XREAL_0;
schemes NAT_1, FINSEQ_1, FINSEQ_4;
registrations RELAT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, VALUED_0, INT_1;
constructors HIDDEN, PARTFUN1, XXREAL_0, NAT_1, COMPLEX1, MATRIX_1, TOPREAL1, SEQM_3, RELSET_1, REAL_1, MATRIX_0;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0;
expansions XBOOLE_0, SEQM_3;
definition
let D be
set ;
let f be
FinSequence of
D;
let M be
Matrix of
D;
pred f is_sequence_on M means
( ( for
n being
Nat st
n in dom f holds
ex
i,
j being
Nat st
(
[i,j] in Indices M &
f /. n = M * (
i,
j) ) ) & ( for
n being
Nat st
n in dom f &
n + 1
in dom f holds
for
m,
k,
i,
j being
Nat st
[m,k] in Indices M &
[i,j] in Indices M &
f /. n = M * (
m,
k) &
f /. (n + 1) = M * (
i,
j) holds
|.(m - i).| + |.(k - j).| = 1 ) );
end;
::
deftheorem defines
is_sequence_on GOBOARD1:def 9 :
for D being set
for f being FinSequence of D
for M being Matrix of D holds
( f is_sequence_on M iff ( ( for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) ) );
theorem
for
f1,
f2 being
FinSequence of
(TOP-REAL 2) for
D being
set for
M being
Matrix of
D st ( for
n being
Nat st
n in dom f1 holds
ex
i,
j being
Nat st
(
[i,j] in Indices M &
f1 /. n = M * (
i,
j) ) ) & ( for
n being
Nat st
n in dom f2 holds
ex
i,
j being
Nat st
(
[i,j] in Indices M &
f2 /. n = M * (
i,
j) ) ) holds
for
n being
Nat st
n in dom (f1 ^ f2) holds
ex
i,
j being
Nat st
(
[i,j] in Indices M &
(f1 ^ f2) /. n = M * (
i,
j) )
theorem
for
f1,
f2 being
FinSequence of
(TOP-REAL 2) for
D being
set for
M being
Matrix of
D st ( for
n being
Nat st
n in dom f1 &
n + 1
in dom f1 holds
for
m,
k,
i,
j being
Nat st
[m,k] in Indices M &
[i,j] in Indices M &
f1 /. n = M * (
m,
k) &
f1 /. (n + 1) = M * (
i,
j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for
n being
Nat st
n in dom f2 &
n + 1
in dom f2 holds
for
m,
k,
i,
j being
Nat st
[m,k] in Indices M &
[i,j] in Indices M &
f2 /. n = M * (
m,
k) &
f2 /. (n + 1) = M * (
i,
j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for
m,
k,
i,
j being
Nat st
[m,k] in Indices M &
[i,j] in Indices M &
f1 /. (len f1) = M * (
m,
k) &
f2 /. 1
= M * (
i,
j) &
len f1 in dom f1 & 1
in dom f2 holds
|.(m - i).| + |.(k - j).| = 1 ) holds
for
n being
Nat st
n in dom (f1 ^ f2) &
n + 1
in dom (f1 ^ f2) holds
for
m,
k,
i,
j being
Nat st
[m,k] in Indices M &
[i,j] in Indices M &
(f1 ^ f2) /. n = M * (
m,
k) &
(f1 ^ f2) /. (n + 1) = M * (
i,
j) holds
|.(m - i).| + |.(k - j).| = 1
theorem
for
G being
Go-board for
f being
FinSequence of
(TOP-REAL 2) st 1
<= len f &
f /. 1
in rng (Line (G,1)) &
f /. (len f) in rng (Line (G,(len G))) &
f is_sequence_on G holds
( ( for
i being
Nat st 1
<= i &
i <= len G holds
ex
k being
Nat st
(
k in dom f &
f /. k in rng (Line (G,i)) ) ) & ( for
i being
Nat st 1
<= i &
i <= len G & 2
<= len f holds
L~ f meets rng (Line (G,i)) ) & ( for
i,
j,
k,
m being
Nat st 1
<= i &
i <= len G & 1
<= j &
j <= len G &
k in dom f &
m in dom f &
f /. k in rng (Line (G,i)) & ( for
n being
Nat st
n in dom f &
f /. n in rng (Line (G,i)) holds
n <= k ) &
k < m &
f /. m in rng (Line (G,j)) holds
i < j ) )
theorem Th26:
for
G being
Go-board for
f being
FinSequence of
(TOP-REAL 2) st 1
<= len f &
f /. 1
in rng (Col (G,1)) &
f /. (len f) in rng (Col (G,(width G))) &
f is_sequence_on G holds
( ( for
i being
Nat st 1
<= i &
i <= width G holds
ex
k being
Nat st
(
k in dom f &
f /. k in rng (Col (G,i)) ) ) & ( for
i being
Nat st 1
<= i &
i <= width G & 2
<= len f holds
L~ f meets rng (Col (G,i)) ) & ( for
i,
j,
k,
m being
Nat st 1
<= i &
i <= width G & 1
<= j &
j <= width G &
k in dom f &
m in dom f &
f /. k in rng (Col (G,i)) & ( for
n being
Nat st
n in dom f &
f /. n in rng (Col (G,i)) holds
n <= k ) &
k < m &
f /. m in rng (Col (G,j)) holds
i < j ) )