begin
Lm1:
for n being Element of NAT st 1 <= n holds
(n -' 1) + 2 = n + 1
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
theorem Th7:
theorem Th8:
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 Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
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 )
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem
theorem Th28:
theorem Th29:
begin
theorem Th30:
theorem Th31:
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 Th32:
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 Th33:
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 )
theorem