begin
theorem Th1:
for
r,
s being
Real holds
(
abs (r - s) = 1 iff ( (
r > s &
r = s + 1 ) or (
r < s &
s = r + 1 ) ) )
theorem Th2:
theorem Th3:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem
canceled;
theorem
canceled;
:: deftheorem GOBOARD1:def 1 :
canceled;
:: deftheorem Def2 defines constant GOBOARD1:def 2 :
:: deftheorem Def3 defines X_axis GOBOARD1:def 3 :
:: deftheorem Def4 defines Y_axis GOBOARD1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th14:
theorem
theorem Th16:
begin
theorem Th17:
:: deftheorem Def5 defines empty-yielding GOBOARD1:def 5 :
:: deftheorem Def6 defines X_equal-in-line GOBOARD1:def 6 :
:: deftheorem Def7 defines Y_equal-in-column GOBOARD1:def 7 :
:: deftheorem Def8 defines Y_increasing-in-line GOBOARD1:def 8 :
:: deftheorem Def9 defines X_increasing-in-column GOBOARD1:def 9 :
Lm1:
for D being non empty set
for M being Matrix of holds
( not M is empty-yielding iff ( 0 < len M & 0 < width M ) )
theorem
canceled;
theorem Th19:
theorem Th20:
begin
theorem
theorem
theorem
theorem Th24:
definition
let G be
Go-board;
let i be
Element of
NAT ;
assume A1:
(
i in Seg (width G) &
width G > 1 )
;
func DelCol G,
i -> Go-board means :
Def10:
(
len it = len G & ( for
k being
Element of
NAT st
k in dom G holds
it . k = Del (Line G,k),
i ) );
existence
ex b1 being Go-board st
( len b1 = len G & ( for k being Element of NAT st k in dom G holds
b1 . k = Del (Line G,k),i ) )
uniqueness
for b1, b2 being Go-board st len b1 = len G & ( for k being Element of NAT st k in dom G holds
b1 . k = Del (Line G,k),i ) & len b2 = len G & ( for k being Element of NAT st k in dom G holds
b2 . k = Del (Line G,k),i ) holds
b1 = b2
end;
:: deftheorem Def10 defines DelCol GOBOARD1:def 10 :
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem
theorem
theorem Th36:
theorem
definition
let D be
set ;
let f be
FinSequence of
D;
let M be
Matrix of ;
pred f is_sequence_on M means :
Def11:
( ( 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 Def11 defines is_sequence_on GOBOARD1:def 11 :
for
D being
set for
f being
FinSequence of
D for
M being
Matrix of 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 holds <*> D is_sequence_on M
theorem
theorem
for
f1,
f2 being
FinSequence of
for
D being
set for
M being
Matrix of 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
for
D being
set for
M being
Matrix of 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
theorem Th42:
theorem Th43:
theorem Th44:
theorem
for
G being
Go-board for
f being
FinSequence of 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 Th46:
theorem Th47:
theorem Th48:
theorem Th49:
for
G being
Go-board for
f being
FinSequence of 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 ) )
theorem Th50:
theorem
theorem
theorem