:: JORDAN13 semantic presentation

definition
let c1 be non empty being_simple_closed_curve non horizontal non vertical Subset of (TOP-REAL 2);
let c2 be Nat;
assume E1: c2 is_sufficiently_large_for c1 ;
func Span c1,c2 -> clockwise_oriented non constant standard special_circular_sequence means :: JORDAN13:def 1
( a3 is_sequence_on Gauge a1,a2 & a3 /. 1 = (Gauge a1,a2) * (X-SpanStart a1,a2),(Y-SpanStart a1,a2) & a3 /. 2 = (Gauge a1,a2) * ((X-SpanStart a1,a2) -' 1),(Y-SpanStart a1,a2) & ( for b1 being Nat st 1 <= b1 & b1 + 2 <= len a3 holds
( ( front_right_cell a3,b1,(Gauge a1,a2) misses a1 & front_left_cell a3,b1,(Gauge a1,a2) misses a1 implies a3 turns_left b1, Gauge a1,a2 ) & ( front_right_cell a3,b1,(Gauge a1,a2) misses a1 & front_left_cell a3,b1,(Gauge a1,a2) meets a1 implies a3 goes_straight b1, Gauge a1,a2 ) & ( front_right_cell a3,b1,(Gauge a1,a2) meets a1 implies a3 turns_right b1, Gauge a1,a2 ) ) ) );
existence
ex b1 being clockwise_oriented non constant standard special_circular_sequence st
( b1 is_sequence_on Gauge c1,c2 & b1 /. 1 = (Gauge c1,c2) * (X-SpanStart c1,c2),(Y-SpanStart c1,c2) & b1 /. 2 = (Gauge c1,c2) * ((X-SpanStart c1,c2) -' 1),(Y-SpanStart c1,c2) & ( for b2 being Nat st 1 <= b2 & b2 + 2 <= len b1 holds
( ( front_right_cell b1,b2,(Gauge c1,c2) misses c1 & front_left_cell b1,b2,(Gauge c1,c2) misses c1 implies b1 turns_left b2, Gauge c1,c2 ) & ( front_right_cell b1,b2,(Gauge c1,c2) misses c1 & front_left_cell b1,b2,(Gauge c1,c2) meets c1 implies b1 goes_straight b2, Gauge c1,c2 ) & ( front_right_cell b1,b2,(Gauge c1,c2) meets c1 implies b1 turns_right b2, Gauge c1,c2 ) ) ) )
proof end;
uniqueness
for b1, b2 being clockwise_oriented non constant standard special_circular_sequence st b1 is_sequence_on Gauge c1,c2 & b1 /. 1 = (Gauge c1,c2) * (X-SpanStart c1,c2),(Y-SpanStart c1,c2) & b1 /. 2 = (Gauge c1,c2) * ((X-SpanStart c1,c2) -' 1),(Y-SpanStart c1,c2) & ( for b3 being Nat st 1 <= b3 & b3 + 2 <= len b1 holds
( ( front_right_cell b1,b3,(Gauge c1,c2) misses c1 & front_left_cell b1,b3,(Gauge c1,c2) misses c1 implies b1 turns_left b3, Gauge c1,c2 ) & ( front_right_cell b1,b3,(Gauge c1,c2) misses c1 & front_left_cell b1,b3,(Gauge c1,c2) meets c1 implies b1 goes_straight b3, Gauge c1,c2 ) & ( front_right_cell b1,b3,(Gauge c1,c2) meets c1 implies b1 turns_right b3, Gauge c1,c2 ) ) ) & b2 is_sequence_on Gauge c1,c2 & b2 /. 1 = (Gauge c1,c2) * (X-SpanStart c1,c2),(Y-SpanStart c1,c2) & b2 /. 2 = (Gauge c1,c2) * ((X-SpanStart c1,c2) -' 1),(Y-SpanStart c1,c2) & ( for b3 being Nat st 1 <= b3 & b3 + 2 <= len b2 holds
( ( front_right_cell b2,b3,(Gauge c1,c2) misses c1 & front_left_cell b2,b3,(Gauge c1,c2) misses c1 implies b2 turns_left b3, Gauge c1,c2 ) & ( front_right_cell b2,b3,(Gauge c1,c2) misses c1 & front_left_cell b2,b3,(Gauge c1,c2) meets c1 implies b2 goes_straight b3, Gauge c1,c2 ) & ( front_right_cell b2,b3,(Gauge c1,c2) meets c1 implies b2 turns_right b3, Gauge c1,c2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Span JORDAN13:def 1 :
for b1 being non empty being_simple_closed_curve non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 is_sufficiently_large_for b1 holds
for b3 being clockwise_oriented non constant standard special_circular_sequence holds
( b3 = Span b1,b2 iff ( b3 is_sequence_on Gauge b1,b2 & b3 /. 1 = (Gauge b1,b2) * (X-SpanStart b1,b2),(Y-SpanStart b1,b2) & b3 /. 2 = (Gauge b1,b2) * ((X-SpanStart b1,b2) -' 1),(Y-SpanStart b1,b2) & ( for b4 being Nat st 1 <= b4 & b4 + 2 <= len b3 holds
( ( front_right_cell b3,b4,(Gauge b1,b2) misses b1 & front_left_cell b3,b4,(Gauge b1,b2) misses b1 implies b3 turns_left b4, Gauge b1,b2 ) & ( front_right_cell b3,b4,(Gauge b1,b2) misses b1 & front_left_cell b3,b4,(Gauge b1,b2) meets b1 implies b3 goes_straight b4, Gauge b1,b2 ) & ( front_right_cell b3,b4,(Gauge b1,b2) meets b1 implies b3 turns_right b4, Gauge b1,b2 ) ) ) ) );