environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, RELAT_1, JORDAN3, ARYTM_3, ARYTM_1, CARD_1, PARTFUN1, FUNCT_1, RCOMP_1, EUCLID, PRE_TOPC, MCART_1, PSCOMP_1, RLTOPSP1, TOPREAL1, TARSKI, GOBOARD1, REAL_1, SUPINF_2, ZFMISC_1, ORDINAL4, NAT_1, GOBOARD4, FINSEQ_6, GOBOARD5, STRUCT_0, SPPOL_1, SPRECT_1, SPPOL_2, FINSEQ_5, FINSEQ_4, TOPREAL2, SPRECT_2, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, STRUCT_0, FINSEQ_4, FINSEQ_5, ZFMISC_1, FINSEQ_6, NAT_1, NAT_D, PRE_TOPC, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, GOBOARD4, SPPOL_1, SPPOL_2, GOBOARD5, PSCOMP_1, SPRECT_1, XXREAL_0;
definitions TARSKI, GOBOARD4, XBOOLE_0;
theorems FINSEQ_6, FINSEQ_4, FINSEQ_5, GOBOARD4, GOBOARD1, PSCOMP_1, FINSEQ_3, JORDAN3, NAT_1, SPPOL_1, FINSEQ_1, JORDAN4, ZFMISC_1, SPPOL_2, TOPREAL3, TARSKI, FUNCT_1, TOPREAL1, GOBOARD2, GOBOARD7, PARTFUN2, GOBOARD5, EUCLID, TOPREAL2, FUNCT_2, PRE_TOPC, RELAT_1, SPRECT_1, TOPREAL5, XBOOLE_0, XBOOLE_1, XCMPLX_1, SEQ_4, XREAL_1, XXREAL_0, PARTFUN1, CARD_1, NAT_D, RLTOPSP1, RLVECT_1;
schemes ;
registrations RELSET_1, NUMBERS, XREAL_0, FINSEQ_1, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, SPPOL_2, SPRECT_1, XBOOLE_0, VALUED_0, FUNCT_1, RLTOPSP1, MEASURE6, NAT_1, ORDINAL1;
constructors HIDDEN, REAL_1, FINSEQ_4, NAT_D, FINSEQ_5, COMPTS_1, TOPREAL2, GOBOARD1, GOBOARD4, SPPOL_1, GOBOARD5, PSCOMP_1, SPRECT_1, SEQ_4, RELSET_1, CONVEX1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities TOPREAL1, PSCOMP_1, STRUCT_0, RLTOPSP1;
expansions XBOOLE_0;
Lm1:
for f being non constant standard special_circular_sequence
for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) holds
(<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2
Lm2:
for f being non constant standard special_circular_sequence holds LSeg ((S-max (L~ f)),(SE-corner (L~ f))) misses LSeg ((NW-corner (L~ f)),(N-min (L~ f)))
Lm3:
for f being non constant standard special_circular_sequence
for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds
(<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2
Lm4:
for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds
(N-min (L~ f)) .. f < (E-max (L~ f)) .. f
Lm5:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm6:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-min (L~ z)) .. z
Lm7:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm8:
for f being non constant standard special_circular_sequence holds (LSeg ((N-min (L~ f)),(NW-corner (L~ f)))) /\ (LSeg ((NE-corner (L~ f)),(E-max (L~ f)))) = {}
Lm9:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (S-min (L~ z)) .. z
Lm10:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) & N-min (L~ z) <> W-max (L~ z) holds
(E-min (L~ z)) .. z < (W-max (L~ z)) .. z
Lm11:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (W-min (L~ z)) .. z