begin
theorem Th1:
for
r1,
r2,
s being
Real holds
( not
abs (r1 - r2) > s or
r1 + s < r2 or
r2 + s < r1 )
theorem Th2:
for
r,
s being
Real holds
(
abs (r - s) = 0 iff
r = s )
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem
canceled;
theorem Th8:
theorem Th9:
theorem
canceled;
theorem
theorem Th12:
theorem Th13:
theorem
begin
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
for
G being
Go-board for
i1,
j1,
i2,
j2 being
Element of
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)) & not (
j1 = j2 &
LSeg (G * i1,j1),
(G * i1,(j1 + 1)) = LSeg (G * i2,j2),
(G * i2,(j2 + 1)) ) & not (
j1 = j2 + 1 &
(LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * i2,(j2 + 1))) = {(G * i1,j1)} ) holds
(
j1 + 1
= j2 &
(LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * i2,(j2 + 1))) = {(G * i2,j2)} )
theorem
for
G being
Go-board for
i1,
j1,
i2,
j2 being
Element of
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) & not (
i1 = i2 &
LSeg (G * i1,j1),
(G * (i1 + 1),j1) = LSeg (G * i2,j2),
(G * (i2 + 1),j2) ) & not (
i1 = i2 + 1 &
(LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) holds
(
i1 + 1
= i2 &
(LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i2,j2)} )
theorem
for
G being
Go-board for
i1,
j1,
i2,
j2 being
Element of
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) & not (
j1 = j2 &
(LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) holds
(
j1 + 1
= j2 &
(LSeg (G * i1,j1),(G * i1,(j1 + 1))) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,(j1 + 1))} )
Lm1:
1 - (1 / 2) = 1 / 2
;
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
begin
Lm2:
for f being non constant standard special_circular_sequence holds len f > 1
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
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
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * i,
(j + 2) &
f /. (k + 1) = (GoB f) * i,
(j + 1) &
f /. (k + 2) = (GoB f) * i,
j )
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * (i + 1),
(j + 1) &
f /. (k + 1) = (GoB f) * i,
(j + 1) &
f /. (k + 2) = (GoB f) * i,
j )
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
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
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * (i + 2),
j &
f /. (k + 1) = (GoB f) * (i + 1),
j &
f /. (k + 2) = (GoB f) * i,
j )
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * (i + 1),
(j + 1) &
f /. (k + 1) = (GoB f) * (i + 1),
j &
f /. (k + 2) = (GoB f) * i,
j )
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
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
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * i,
j &
f /. (k + 1) = (GoB f) * i,
(j + 1) &
f /. (k + 2) = (GoB f) * i,
(j + 2) )
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * i,
j &
f /. (k + 1) = (GoB f) * i,
(j + 1) &
f /. (k + 2) = (GoB f) * (i + 1),
(j + 1) )
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
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
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * i,
j &
f /. (k + 1) = (GoB f) * (i + 1),
j &
f /. (k + 2) = (GoB f) * (i + 2),
j )
theorem
for
i,
j,
k being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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) holds
(
f /. k = (GoB f) * i,
j &
f /. (k + 1) = (GoB f) * (i + 1),
j &
f /. (k + 2) = (GoB f) * (i + 1),
(j + 1) )
theorem Th55:
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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 & not (
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 ) ) ) holds
ex
k being
Element of
NAT 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 Th56:
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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 & not (
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 ) ) ) holds
ex
k being
Element of
NAT 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 Th57:
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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 & not (
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) ) ) ) holds
ex
k being
Element of
NAT 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 Th58:
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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 & not (
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 ) ) ) holds
ex
k being
Element of
NAT 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 Th59:
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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 & not (
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 ) ) ) holds
ex
k being
Element of
NAT 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 Th60:
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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 & not (
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 ) ) ) holds
ex
k being
Element of
NAT 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
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 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 holds
not
LSeg ((GoB f) * i,(j + 1)),
((GoB f) * (i + 1),(j + 1)) c= L~ f
theorem
for
i,
j being
Element of
NAT for
f being non
constant standard special_circular_sequence st 1
<= i &
i < 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 + 1),(j + 2)) c= L~ f holds
not
LSeg ((GoB f) * i,(j + 1)),
((GoB f) * (i + 1),(j + 1)) c= L~ f
theorem
for
j,
i being
Element of
NAT for
f being non
constant standard special_circular_sequence st 1
<= j &
j < width (GoB f) & 1
<= i &
i + 1
< len (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 holds
not
LSeg ((GoB f) * (i + 1),j),
((GoB f) * (i + 1),(j + 1)) c= L~ f
theorem
for
j,
i being
Element of
NAT for
f being non
constant standard special_circular_sequence st 1
<= j &
j < width (GoB f) & 1
<= i &
i + 1
< len (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 + 2),(j + 1)) c= L~ f holds
not
LSeg ((GoB f) * (i + 1),j),
((GoB f) * (i + 1),(j + 1)) c= L~ f
theorem
theorem