environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SPPOL_1, XBOOLE_0, TOPREAL2, EUCLID, JORDAN1H, SPRECT_2, GOBOARD5, FUNCT_1, GOBOARD1, JORDAN8, PARTFUN1, RELAT_1, JORDAN11, ARYTM_1, XXREAL_0, ARYTM_3, FINSEQ_1, GOBRD13, NEWTON, CARD_1, ORDINAL4, PRE_TOPC, PCOMPS_1, MATRIX_1, TREES_1, STRUCT_0, TARSKI, COMPLEX1, NAT_1, TOPREAL1, RLTOPSP1, RFINSEQ, CONNSP_1, TOPS_1, RELAT_2, GOBOARD9, RCOMP_1, METRIC_1, REAL_1, FINSEQ_5, JORDAN2C, JORDAN13, CONVEX1, XXREAL_2;
notations HIDDEN, TARSKI, GOBOARD5, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, COMPLEX1, NEWTON, FINSEQ_1, FINSEQ_2, FINSEQ_4, STRUCT_0, RFINSEQ, MATRIX_0, METRIC_1, PRE_TOPC, TOPS_1, CONNSP_1, PCOMPS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, SPRECT_2, GOBOARD9, JORDAN8, GOBRD13, JORDAN2C, JORDAN1H, JORDAN11;
definitions TARSKI, XBOOLE_0, GOBOARD5, SEQM_3;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, JORDAN3, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, XBOOLE_0, XBOOLE_1, ABSVALUE, FUNCT_1, FUNCT_2, GOBOARD9, FINSEQ_2, UNIFORM1, SUBSET_1, GOBRD11, SPRECT_3, CARD_1, RFINSEQ, GOBOARD6, TOPREAL3, TOPMETR, TOPS_1, JORDAN8, GOBRD13, SPRECT_4, CONNSP_1, GOBRD14, JORDAN9, JORDAN5B, JORDAN2C, PARTFUN2, RELSET_1, TBSP_1, JORDAN1H, JORDAN11, XREAL_0, ZFMISC_1, XREAL_1, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, SEQ_4, RLTOPSP1;
schemes NAT_1, RECDEF_1;
registrations RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, TOPREAL2, SPPOL_2, GOBOARD9, SPRECT_2, SPRECT_3, TOPREAL6, JORDAN8, MATRIX_0, JORDAN1A, FINSET_1, SPPOL_1, JORDAN1, JORDAN2C, NEWTON;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, TOPREAL4, PSCOMP_1, GOBOARD9, SPRECT_2, JORDAN2C, JORDAN8, JORDAN1H, JORDAN11, RELSET_1, PCOMPS_1, FUNCSDOM, CONVEX1, GOBRD13, JORDAN9, DOMAIN_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities XBOOLE_0;
expansions TARSKI;
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
(
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 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 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 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 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 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 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) ) ) ) ) );