begin
begin
Lm1:
for D being non empty set
for M being Matrix of D holds
( M is V3() iff ( 0 < len M & 0 < width M ) )
begin
definition
let D be
set ;
let f be
FinSequence of
D;
let M be
Matrix of
D;
pred f is_sequence_on M means :
Def9:
( ( for
n being
Element of
NAT st
n in dom f holds
ex
i,
j being
Element of
NAT st
(
[i,j] in Indices M &
f /. n = M * (
i,
j) ) ) & ( for
n being
Element of
NAT st
n in dom f &
n + 1
in dom f holds
for
m,
k,
i,
j being
Element of
NAT st
[m,k] in Indices M &
[i,j] in Indices M &
f /. n = M * (
m,
k) &
f /. (n + 1) = M * (
i,
j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) );
end;
::
deftheorem Def9 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 Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices M & f /. n = M * (i,j) ) ) & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f /. n = M * (m,k) & f /. (n + 1) = M * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) ) );
Lm2:
for D being set
for M being Matrix of D holds <*> D is_sequence_on M
theorem
for
f1,
f2 being
FinSequence of
(TOP-REAL 2) for
D being
set for
M being
Matrix of
D st ( for
n being
Element of
NAT st
n in dom f1 holds
ex
i,
j being
Element of
NAT st
(
[i,j] in Indices M &
f1 /. n = M * (
i,
j) ) ) & ( for
n being
Element of
NAT st
n in dom f2 holds
ex
i,
j being
Element of
NAT st
(
[i,j] in Indices M &
f2 /. n = M * (
i,
j) ) ) holds
for
n being
Element of
NAT st
n in dom (f1 ^ f2) holds
ex
i,
j being
Element of
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
Element of
NAT st
n in dom f1 &
n + 1
in dom f1 holds
for
m,
k,
i,
j being
Element of
NAT st
[m,k] in Indices M &
[i,j] in Indices M &
f1 /. n = M * (
m,
k) &
f1 /. (n + 1) = M * (
i,
j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for
n being
Element of
NAT st
n in dom f2 &
n + 1
in dom f2 holds
for
m,
k,
i,
j being
Element of
NAT st
[m,k] in Indices M &
[i,j] in Indices M &
f2 /. n = M * (
m,
k) &
f2 /. (n + 1) = M * (
i,
j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for
m,
k,
i,
j being
Element of
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
(abs (m - i)) + (abs (k - j)) = 1 ) holds
for
n being
Element of
NAT st
n in dom (f1 ^ f2) &
n + 1
in dom (f1 ^ f2) holds
for
m,
k,
i,
j being
Element of
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
(abs (m - i)) + (abs (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
Element of
NAT st 1
<= i &
i <= len G holds
ex
k being
Element of
NAT st
(
k in dom f &
f /. k in rng (Line (G,i)) ) ) & ( for
i being
Element of
NAT st 1
<= i &
i <= len G & 2
<= len f holds
L~ f meets rng (Line (G,i)) ) & ( for
i,
j,
k,
m being
Element of
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
Element of
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 Th33:
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
Element of
NAT st 1
<= i &
i <= width G holds
ex
k being
Element of
NAT st
(
k in dom f &
f /. k in rng (Col (G,i)) ) ) & ( for
i being
Element of
NAT st 1
<= i &
i <= width G & 2
<= len f holds
L~ f meets rng (Col (G,i)) ) & ( for
i,
j,
k,
m being
Element of
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
Element of
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 ) )