:: Introducing Spans
:: by Andrzej Trybulec
::
:: Received May 27, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


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 :: JORDAN13:def 1
( it is_sequence_on Gauge (C,n) &amp; it /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) &amp; it /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) &amp; ( for k being Element of NAT st 1 <= k &amp; k + 2 <= len it holds
( ( front_right_cell (it,k,(Gauge (C,n))) misses C &amp; front_left_cell (it,k,(Gauge (C,n))) misses C implies it turns_left k, Gauge (C,n) ) &amp; ( front_right_cell (it,k,(Gauge (C,n))) misses C &amp; front_left_cell (it,k,(Gauge (C,n))) meets C implies it goes_straight k, Gauge (C,n) ) &amp; ( 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) &amp; b1 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) &amp; b1 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) &amp; ( for k being Element of NAT st 1 <= k &amp; k + 2 <= len b1 holds
( ( front_right_cell (b1,k,(Gauge (C,n))) misses C &amp; front_left_cell (b1,k,(Gauge (C,n))) misses C implies b1 turns_left k, Gauge (C,n) ) &amp; ( front_right_cell (b1,k,(Gauge (C,n))) misses C &amp; front_left_cell (b1,k,(Gauge (C,n))) meets C implies b1 goes_straight k, Gauge (C,n) ) &amp; ( front_right_cell (b1,k,(Gauge (C,n))) meets C implies b1 turns_right k, Gauge (C,n) ) ) ) )
proofend;
uniqueness
 for b1, b2 being non constant standard clockwise_oriented special_circular_sequence st b1 is_sequence_on Gauge (C,n) &amp; b1 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) &amp; b1 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) &amp; ( for k being Element of NAT st 1 <= k &amp; k + 2 <= len b1 holds
( ( front_right_cell (b1,k,(Gauge (C,n))) misses C &amp; front_left_cell (b1,k,(Gauge (C,n))) misses C implies b1 turns_left k, Gauge (C,n) ) &amp; ( front_right_cell (b1,k,(Gauge (C,n))) misses C &amp; front_left_cell (b1,k,(Gauge (C,n))) meets C implies b1 goes_straight k, Gauge (C,n) ) &amp; ( front_right_cell (b1,k,(Gauge (C,n))) meets C implies b1 turns_right k, Gauge (C,n) ) ) ) &amp; b2 is_sequence_on Gauge (C,n) &amp; b2 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) &amp; b2 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) &amp; ( for k being Element of NAT st 1 <= k &amp; k + 2 <= len b2 holds
( ( front_right_cell (b2,k,(Gauge (C,n))) misses C &amp; front_left_cell (b2,k,(Gauge (C,n))) misses C implies b2 turns_left k, Gauge (C,n) ) &amp; ( front_right_cell (b2,k,(Gauge (C,n))) misses C &amp; front_left_cell (b2,k,(Gauge (C,n))) meets C implies b2 goes_straight k, Gauge (C,n) ) &amp; ( front_right_cell (b2,k,(Gauge (C,n))) meets C implies b2 turns_right k, Gauge (C,n) ) ) ) holds
b1 = b2
proofend;
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) &amp; b3 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) &amp; b3 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) &amp; ( for k being Element of NAT st 1 <= k &amp; k + 2 <= len b3 holds
( ( front_right_cell (b3,k,(Gauge (C,n))) misses C &amp; front_left_cell (b3,k,(Gauge (C,n))) misses C implies b3 turns_left k, Gauge (C,n) ) &amp; ( front_right_cell (b3,k,(Gauge (C,n))) misses C &amp; front_left_cell (b3,k,(Gauge (C,n))) meets C implies b3 goes_straight k, Gauge (C,n) ) &amp; ( front_right_cell (b3,k,(Gauge (C,n))) meets C implies b3 turns_right k, Gauge (C,n) ) ) ) ) );