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

definition

let C be non empty non horizontal non vertical being_simple_closed_curve Subset of (TOP-REAL 2);
let n be 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) & 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 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 b₁ being non constant standard clockwise_oriented special_circular_sequence st
( b₁ is_sequence_on Gauge (C,n) & b₁ /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b₁ /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Nat st 1 <= k & k + 2 <= len b₁ holds
( ( front_right_cell (b₁,k,(Gauge (C,n))) misses C & front_left_cell (b₁,k,(Gauge (C,n))) misses C implies b₁ turns_left k, Gauge (C,n) ) & ( front_right_cell (b₁,k,(Gauge (C,n))) misses C & front_left_cell (b₁,k,(Gauge (C,n))) meets C implies b₁ goes_straight k, Gauge (C,n) ) & ( front_right_cell (b₁,k,(Gauge (C,n))) meets C implies b₁ turns_right k, Gauge (C,n) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being non constant standard clockwise_oriented special_circular_sequence st b₁ is_sequence_on Gauge (C,n) & b₁ /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b₁ /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Nat st 1 <= k & k + 2 <= len b₁ holds
( ( front_right_cell (b₁,k,(Gauge (C,n))) misses C & front_left_cell (b₁,k,(Gauge (C,n))) misses C implies b₁ turns_left k, Gauge (C,n) ) & ( front_right_cell (b₁,k,(Gauge (C,n))) misses C & front_left_cell (b₁,k,(Gauge (C,n))) meets C implies b₁ goes_straight k, Gauge (C,n) ) & ( front_right_cell (b₁,k,(Gauge (C,n))) meets C implies b₁ turns_right k, Gauge (C,n) ) ) ) & b₂ is_sequence_on Gauge (C,n) & b₂ /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b₂ /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Nat st 1 <= k & k + 2 <= len b₂ holds
( ( front_right_cell (b₂,k,(Gauge (C,n))) misses C & front_left_cell (b₂,k,(Gauge (C,n))) misses C implies b₂ turns_left k, Gauge (C,n) ) & ( front_right_cell (b₂,k,(Gauge (C,n))) misses C & front_left_cell (b₂,k,(Gauge (C,n))) meets C implies b₂ goes_straight k, Gauge (C,n) ) & ( front_right_cell (b₂,k,(Gauge (C,n))) meets C implies b₂ turns_right k, Gauge (C,n) ) ) ) holds
b₁ = b₂

proof end;

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 Nat st n is_sufficiently_large_for C holds
for b₃ being non constant standard clockwise_oriented special_circular_sequence holds
( b₃ = Span (C,n) iff ( b₃ is_sequence_on Gauge (C,n) & b₃ /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & b₃ /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Nat st 1 <= k & k + 2 <= len b₃ holds
( ( front_right_cell (b₃,k,(Gauge (C,n))) misses C & front_left_cell (b₃,k,(Gauge (C,n))) misses C implies b₃ turns_left k, Gauge (C,n) ) & ( front_right_cell (b₃,k,(Gauge (C,n))) misses C & front_left_cell (b₃,k,(Gauge (C,n))) meets C implies b₃ goes_straight k, Gauge (C,n) ) & ( front_right_cell (b₃,k,(Gauge (C,n))) meets C implies b₃ turns_right k, Gauge (C,n) ) ) ) ) );