begin
definition
let C be non
empty non
horizontal non
vertical being_simple_closed_curve Subset of
(TOP-REAL 2);
let n be
Element of
NAT ;
assume A1:
n is_sufficiently_large_for C
;
func Span (
C,
n)
-> non
constant standard clockwise_oriented special_circular_sequence means
(
it is_sequence_on Gauge (
C,
n) &
it /. 1
= (Gauge (C,n)) * (
(X-SpanStart (C,n)),
(Y-SpanStart (C,n))) &
it /. 2
= (Gauge (C,n)) * (
((X-SpanStart (C,n)) -' 1),
(Y-SpanStart (C,n))) & ( for
k being
Element of
NAT st 1
<= k &
k + 2
<= len it holds
( (
front_right_cell (
it,
k,
(Gauge (C,n)))
misses C &
front_left_cell (
it,
k,
(Gauge (C,n)))
misses C implies
it turns_left k,
Gauge (
C,
n) ) & (
front_right_cell (
it,
k,
(Gauge (C,n)))
misses C &
front_left_cell (
it,
k,
(Gauge (C,n)))
meets C implies
it goes_straight k,
Gauge (
C,
n) ) & (
front_right_cell (
it,
k,
(Gauge (C,n)))
meets C implies
it turns_right k,
Gauge (
C,
n) ) ) ) );
existence
ex b1 being non constant standard clockwise_oriented special_circular_sequence st
( b1 is_sequence_on Gauge (C,n) & b1 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b1 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b1 holds
( ( front_right_cell (b1,k,(Gauge (C,n))) misses C & front_left_cell (b1,k,(Gauge (C,n))) misses C implies b1 turns_left k, Gauge (C,n) ) & ( front_right_cell (b1,k,(Gauge (C,n))) misses C & front_left_cell (b1,k,(Gauge (C,n))) meets C implies b1 goes_straight k, Gauge (C,n) ) & ( front_right_cell (b1,k,(Gauge (C,n))) meets C implies b1 turns_right 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) & b1 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b1 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b1 holds
( ( front_right_cell (b1,k,(Gauge (C,n))) misses C & front_left_cell (b1,k,(Gauge (C,n))) misses C implies b1 turns_left k, Gauge (C,n) ) & ( front_right_cell (b1,k,(Gauge (C,n))) misses C & front_left_cell (b1,k,(Gauge (C,n))) meets C implies b1 goes_straight k, Gauge (C,n) ) & ( front_right_cell (b1,k,(Gauge (C,n))) meets C implies b1 turns_right k, Gauge (C,n) ) ) ) & b2 is_sequence_on Gauge (C,n) & b2 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b2 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b2 holds
( ( front_right_cell (b2,k,(Gauge (C,n))) misses C & front_left_cell (b2,k,(Gauge (C,n))) misses C implies b2 turns_left k, Gauge (C,n) ) & ( front_right_cell (b2,k,(Gauge (C,n))) misses C & front_left_cell (b2,k,(Gauge (C,n))) meets C implies b2 goes_straight k, Gauge (C,n) ) & ( front_right_cell (b2,k,(Gauge (C,n))) meets C implies b2 turns_right k, Gauge (C,n) ) ) ) holds
b1 = b2
end;
::
deftheorem defines
Span JORDAN13:def 1 :
for C being non empty non horizontal non vertical being_simple_closed_curve Subset of (TOP-REAL 2)
for n being Element of NAT st n is_sufficiently_large_for C holds
for b3 being non constant standard clockwise_oriented special_circular_sequence holds
( b3 = Span (C,n) iff ( b3 is_sequence_on Gauge (C,n) & b3 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b3 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Element of NAT st 1 <= k & k + 2 <= len b3 holds
( ( front_right_cell (b3,k,(Gauge (C,n))) misses C & front_left_cell (b3,k,(Gauge (C,n))) misses C implies b3 turns_left k, Gauge (C,n) ) & ( front_right_cell (b3,k,(Gauge (C,n))) misses C & front_left_cell (b3,k,(Gauge (C,n))) meets C implies b3 goes_straight k, Gauge (C,n) ) & ( front_right_cell (b3,k,(Gauge (C,n))) meets C implies b3 turns_right k, Gauge (C,n) ) ) ) ) );