begin
Lm1:
for n being Element of NAT st 1 <= n holds
(n -' 1) + 2 = n + 1
begin
Lm2:
for k being Element of NAT
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & 1 <= k & k <= len f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. k = G * (i,j) )
theorem Th20:
for
i,
j being
Element of
NAT for
G being
Go-board st 1
<= i &
i + 1
<= len G & 1
<= j &
j + 1
<= width G holds
(
G * (
i,
j)
in cell (
G,
i,
j) &
G * (
i,
(j + 1))
in cell (
G,
i,
j) &
G * (
(i + 1),
(j + 1))
in cell (
G,
i,
j) &
G * (
(i + 1),
j)
in cell (
G,
i,
j) )
begin
theorem Th29:
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n,
i1,
i2 being
Nat st 1
<= i1 &
i1 + 1
<= len (Gauge (C,n)) &
N-min C in cell (
(Gauge (C,n)),
i1,
((width (Gauge (C,n))) -' 1)) &
N-min C <> (Gauge (C,n)) * (
i1,
((width (Gauge (C,n))) -' 1)) & 1
<= i2 &
i2 + 1
<= len (Gauge (C,n)) &
N-min C in cell (
(Gauge (C,n)),
i2,
((width (Gauge (C,n))) -' 1)) &
N-min C <> (Gauge (C,n)) * (
i2,
((width (Gauge (C,n))) -' 1)) holds
i1 = i2
theorem Th30:
for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat for
f being non
constant standard special_circular_sequence st
f is_sequence_on Gauge (
C,
n) & ( for
k being
Element of
NAT st 1
<= k &
k + 1
<= len f holds
(
left_cell (
f,
k,
(Gauge (C,n)))
misses C &
right_cell (
f,
k,
(Gauge (C,n)))
meets C ) ) & ex
i being
Element of
NAT st
( 1
<= i &
i + 1
<= len (Gauge (C,n)) &
f /. 1
= (Gauge (C,n)) * (
i,
(width (Gauge (C,n)))) &
f /. 2
= (Gauge (C,n)) * (
(i + 1),
(width (Gauge (C,n)))) &
N-min C in cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1)) &
N-min C <> (Gauge (C,n)) * (
i,
((width (Gauge (C,n))) -' 1)) ) holds
N-min (L~ f) = f /. 1
definition
let C be non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2);
let n be
Nat;
assume A1:
C is
connected
;
func Cage (
C,
n)
-> non
constant standard clockwise_oriented special_circular_sequence means :
Def1:
(
it is_sequence_on Gauge (
C,
n) & ex
i being
Element of
NAT st
( 1
<= i &
i + 1
<= len (Gauge (C,n)) &
it /. 1
= (Gauge (C,n)) * (
i,
(width (Gauge (C,n)))) &
it /. 2
= (Gauge (C,n)) * (
(i + 1),
(width (Gauge (C,n)))) &
N-min C in cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1)) &
N-min C <> (Gauge (C,n)) * (
i,
((width (Gauge (C,n))) -' 1)) ) & ( for
k being
Element of
NAT st 1
<= k &
k + 2
<= len it holds
( (
front_left_cell (
it,
k,
(Gauge (C,n)))
misses C &
front_right_cell (
it,
k,
(Gauge (C,n)))
misses C implies
it turns_right k,
Gauge (
C,
n) ) & (
front_left_cell (
it,
k,
(Gauge (C,n)))
misses C &
front_right_cell (
it,
k,
(Gauge (C,n)))
meets C implies
it goes_straight k,
Gauge (
C,
n) ) & (
front_left_cell (
it,
k,
(Gauge (C,n)))
meets C implies
it turns_left k,
Gauge (
C,
n) ) ) ) );
existence
ex b1 being non constant standard clockwise_oriented special_circular_sequence st
( b1 is_sequence_on Gauge (C,n) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & b1 /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & b1 /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b1 holds
( ( front_left_cell (b1,k,(Gauge (C,n))) misses C & front_right_cell (b1,k,(Gauge (C,n))) misses C implies b1 turns_right k, Gauge (C,n) ) & ( front_left_cell (b1,k,(Gauge (C,n))) misses C & front_right_cell (b1,k,(Gauge (C,n))) meets C implies b1 goes_straight k, Gauge (C,n) ) & ( front_left_cell (b1,k,(Gauge (C,n))) meets C implies b1 turns_left k, Gauge (C,n) ) ) ) )
uniqueness
for b1, b2 being non constant standard clockwise_oriented special_circular_sequence st b1 is_sequence_on Gauge (C,n) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & b1 /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & b1 /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b1 holds
( ( front_left_cell (b1,k,(Gauge (C,n))) misses C & front_right_cell (b1,k,(Gauge (C,n))) misses C implies b1 turns_right k, Gauge (C,n) ) & ( front_left_cell (b1,k,(Gauge (C,n))) misses C & front_right_cell (b1,k,(Gauge (C,n))) meets C implies b1 goes_straight k, Gauge (C,n) ) & ( front_left_cell (b1,k,(Gauge (C,n))) meets C implies b1 turns_left k, Gauge (C,n) ) ) ) & b2 is_sequence_on Gauge (C,n) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & b2 /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & b2 /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b2 holds
( ( front_left_cell (b2,k,(Gauge (C,n))) misses C & front_right_cell (b2,k,(Gauge (C,n))) misses C implies b2 turns_right k, Gauge (C,n) ) & ( front_left_cell (b2,k,(Gauge (C,n))) misses C & front_right_cell (b2,k,(Gauge (C,n))) meets C implies b2 goes_straight k, Gauge (C,n) ) & ( front_left_cell (b2,k,(Gauge (C,n))) meets C implies b2 turns_left k, Gauge (C,n) ) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
Cage JORDAN9:def 1 :
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st C is connected holds
for b3 being non constant standard clockwise_oriented special_circular_sequence holds
( b3 = Cage (C,n) iff ( b3 is_sequence_on Gauge (C,n) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & b3 /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & b3 /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b3 holds
( ( front_left_cell (b3,k,(Gauge (C,n))) misses C & front_right_cell (b3,k,(Gauge (C,n))) misses C implies b3 turns_right k, Gauge (C,n) ) & ( front_left_cell (b3,k,(Gauge (C,n))) misses C & front_right_cell (b3,k,(Gauge (C,n))) meets C implies b3 goes_straight k, Gauge (C,n) ) & ( front_left_cell (b3,k,(Gauge (C,n))) meets C implies b3 turns_left k, Gauge (C,n) ) ) ) ) );
theorem Th31:
for
k,
n being
Element of
NAT for
C being non
empty compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
C is
connected & 1
<= k &
k + 1
<= len (Cage (C,n)) holds
(
left_cell (
(Cage (C,n)),
k,
(Gauge (C,n)))
misses C &
right_cell (
(Cage (C,n)),
k,
(Gauge (C,n)))
meets C )