:: Subsequences of Standard Special Circular Sequences in $ { \cal E :: } ^2_ { \rm T } $ :: by Yatsuka Nakamura , Roman Matuszewski and Adam Grabowski :: :: Received May 12, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, NAT_1, ARYTM_3, INT_1, CARD_1, ARYTM_1, XXREAL_0, RELAT_1, XBOOLE_0, FINSEQ_1, FINSEQ_6, FUNCT_1, PARTFUN1, RFINSEQ, EUCLID, TOPREAL1, JORDAN3, FINSEQ_5, RLTOPSP1, GOBOARD5, ORDINAL4, TARSKI, PRE_TOPC, SUPINF_2, TOPREAL4, TOPREAL2, MCART_1, JORDAN4; notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, REAL_1, ORDINAL1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_5, STRUCT_0, TOPREAL1, TOPREAL2, TOPREAL4, GOBOARD5, PRE_TOPC, RLVECT_1, RLTOPSP1, EUCLID, FINSEQ_6, RFINSEQ, XXREAL_0; constructors REAL_1, NAT_D, RFINSEQ, BINARITH, FINSEQ_5, TOPREAL2, TOPREAL4, GOBOARD5, RELSET_1; registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, EUCLID, SPPOL_2, GOBOARD5, NAT_1, FINSEQ_1, CARD_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, RLTOPSP1; theorems TARSKI, JORDAN3, TOPREAL4, EUCLID, TOPREAL1, TOPREAL2, FUNCT_1, SPPOL_1, GOBOARD5, FINSEQ_1, GOBOARD7, NAT_1, SPPOL_2, FINSEQ_3, FINSEQ_2, FINSEQ_4, FINSEQ_5, RFINSEQ, FINSEQ_6, ENUMSET1, ZFMISC_1, TOPREAL3, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, NAT_D, ORDINAL1, CARD_1, XREAL_0, RLTOPSP1; begin :: Preliminaries reserve i, i1, i2, j, k for Element of NAT, r, s for Real; theorem Th1: for i, j being Nat holds j0 proof let i, j be Nat; assume that A1: j= j by A1,A3,NAT_D:24; hence thesis by A2,XXREAL_0:1; end; begin :: Some facts about cutting of finite sequences reserve D for non empty set, f1 for FinSequence of D; theorem Th5: for f1 st f1 is circular & 1<=len f1 holds f1.1=f1.len f1 proof let f1; assume that A1: f1 is circular and A2: 1<=len f1; A3: f1.1=f1/.1 by A2,FINSEQ_4:15; f1/.1=f1/.len f1 by A1,FINSEQ_6:def 1; hence thesis by A2,A3,FINSEQ_4:15; end; theorem Th6: for f1,k st ki2; 0<=i2-1 by A3,XREAL_1:48; then i1-0>=i1-(i2-1) by XREAL_1:10; then i1>=i1-i2+1; then i1-'i2+1<=i1 by A5,XREAL_1:233; then A6: i1-'(i1-'i2+1)+1=i1-(i1-'i2+1)+1 by XREAL_1:233 .=i1-(i1-'i2) .=i1-(i1-i2) by A5,XREAL_1:233 .=i2; len mid(f1,i1,i2)=i1-'i2+1 by A1,A2,A3,A4,A5,FINSEQ_6:118; then 1<=len mid(f1,i1,i2) by NAT_1:11; then mid(f1,i1,i2).(len mid(f1,i1,i2)) =f1.(i1-'len mid(f1,i1,i2)+1) by A1,A2,A3 ,A4,A5,FINSEQ_6:118 .=f1.(i1-'(i1-'i2+1)+1) by A1,A2,A3,A4,A5,FINSEQ_6:118; hence thesis by A6; end; end; theorem Th12: for f1,i1,i2,j st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j & j<=i1-'i2 +1 holds mid(f1,i1,i2).j=f1.(i1-'j+1) proof let f1,i1,i2,j; assume that A1: 1<= i2 and A2: i2<=i1 and A3: i1<= len f1 and A4: 1<=j and A5: j<=i1-'i2+1; A6: j<=len mid(f1,i1,i2) by A1,A2,A3,A5,Th9; per cases by A2,XXREAL_0:1; suppose A7: i1=i2; then A8: i1-'i2+1=0+1 by XREAL_1:232 .=1; then j+i1-'1=1+i1-'1 by A4,A5,XXREAL_0:1 .=1+i1-1 by NAT_D:37 .=i1-1+1 .=i1-'1+1 by A1,A7,XREAL_1:233 .=i1-'j+1 by A4,A5,A8,XXREAL_0:1; hence thesis by A1,A3,A4,A6,A7,FINSEQ_6:118; end; suppose A9: i2=0 by A1,XREAL_1:48; then A7: i1-(i2-1)<=i1-0 by XREAL_1:10; A8: i2<=len f1 by A2,A3,XXREAL_0:2; 1-j<=j-j by A4,XREAL_1:9; then A9: i1-'i2+(1-j)<=i1-'i2+0 by XREAL_1:7; j-j<=i1-'i2+1-j by A5,XREAL_1:9; then i1-'i2+1-'j<=i1-'i2 by A9,XREAL_0:def 2; then A10: i1-'i2+1-'j+1<=i1-'i2+1 by XREAL_1:6; A11: 1<=(i1-'i2+1-'j+1) by NAT_1:11; A12: (i1-'i2+1-'j+1) =i1-'i2+1-j+1 by A5,XREAL_1:233 .=i1-i2+1-j+1 by A2,XREAL_1:233; A13: i1-'i2+1=i1-i2+1 by A2,XREAL_1:233; now per cases by A2,XXREAL_0:1; case A14: i1>i2; len mid(f1,i2,i1)=i1-'i2+1 by A1,A2,A3,A6,A8,FINSEQ_6:118; then A15: mid(f1,i2,i1).(i1-'i2+1-'j+1)=f1.((i1-'i2+1-'j+1)+i2-'1) by A1,A2,A3,A6 ,A8,A10,A11,FINSEQ_6:118; A16: len mid(f1,i1,i2)=i1-'i2+1 by A1,A3,A6,A8,A14,FINSEQ_6:118; (i1-'i2+1-'j+1)+i2-'1 =(i1-'i2+1-'j+1)+i2-1 by A1,NAT_D:37 .=i1-j+1 by A12 .=i1-'j+1 by A5,A13,A7,XREAL_1:233,XXREAL_0:2; hence thesis by A1,A3,A4,A5,A6,A8,A12,A14,A15,A16,FINSEQ_6:118; end; case A17: i1=i2; then i1-'i2+1=0+1 by XREAL_1:232 .=1; then i1-i2+1-j+1=0+1-1+1 by A4,A5,A17,XXREAL_0:1 .=1; hence thesis by A12,A17; end; end; hence thesis; end; theorem for f1,i1,i2 st 1<=i1 & i1<=i2 & i2<=len f1 & 1<=j & j<=i2-'i1+1 holds mid(f1,i1,i2).j=mid(f1,i2,i1).(i2-i1+1-j+1) & i2-i1+1-j+1=i2-'i1+1-'j+1 proof let f1,i1,i2; assume that A1: 1<=i1 and A2: i1<=i2 and A3: i2<=len f1 and A4: 1<=j and A5: j<=i2-'i1+1; set k=i2-'i1+1-'j+1; i2-i1+1-j+1=i2-'i1+1-j+1 by A2,XREAL_1:233 .=i2-'i1+1-'j+1 by A5,XREAL_1:233; then A6: i2-i1+1-k+1=j; j-1>=0 by A4,XREAL_1:48; then A7: k+0<=k+(j-1) by XREAL_1:7; A8: 1<=k by NAT_1:11; i2-'i1+1-j=i2-'i1+1-'j by A5,XREAL_1:233; hence thesis by A1,A2,A3,A8,A7,A6,Th13; end; theorem Th15: for f1,k st 1<=k & k<=len f1 holds mid(f1,k,k)=<*f1/.k*> & len mid(f1,k,k)=1 proof let f1,k; assume that A1: 1<=k and A2: k<=len f1; A3: f1/.k=f1.k by A1,A2,FINSEQ_4:15; k-'1+1<=len f1 by A1,A2,XREAL_1:235; then A4: k-'1+1-(k-'1)<=len f1-(k-'1) by XREAL_1:9; len (f1/^(k-'1))=len f1-'(k-'1) by RFINSEQ:29; then A5: 1<=len (f1/^(k-'1)) by A4,NAT_D:39; k-'1+1=k by A1,XREAL_1:235; then A6: (f1/^(k-'1)).1=f1.k by A2,FINSEQ_6:114; k-'k+1=k-k+1 by XREAL_1:233 .=1; then mid(f1,k,k)=(f1/^(k-'1))|1 by FINSEQ_6:def 3 .=<*(f1/^(k-'1))/.1*> by A5,CARD_1:27,FINSEQ_5:20; hence thesis by A6,A3,A5,FINSEQ_1:39,FINSEQ_4:15; end; theorem Th16: mid(f1,0,0)=f1|1 proof 0-1<0; then A1: 0-'1=0 by XREAL_0:def 2; 0-'0+1=0-0+1 by XREAL_1:233 .=1; then mid(f1,0,0)=(f1/^(0-'1))|1 by FINSEQ_6:def 3; hence thesis by A1,FINSEQ_5:28; end; theorem Th17: for f1,k st len f1D proof let f1,k; assume A1: len f1D by FINSEQ_5:32; k-'k+1=k-k+1 by XREAL_1:233 .=1; then mid(f1,k,k)=(f1/^(k-'1))|1 by FINSEQ_6:def 3; hence thesis by A3,FINSEQ_5:78; end; theorem Th18: for f1,i1,i2 holds mid(f1,i1,i2)=Rev mid(f1,i2,i1) proof let f1; let k1,k2 be Element of NAT; now per cases; case A1: k1<=k2; then A2: mid(f1,k1,k2)=(f1/^(k1-'1))|(k2-'k1+1) by FINSEQ_6:def 3; now per cases by A1,XXREAL_0:1; case k1D; then f1|1=<*>D by FINSEQ_5:78; hence thesis by A3,A5,FINSEQ_5:79; end; case len f1<>0; then f1 <> <*>D; then f1|1=<*f1/.1*> by FINSEQ_5:20; hence thesis by A3,A5,FINSEQ_5:60; end; end; hence thesis; end; case 1<=k1 & k1<= len f1; then mid(f1,k1,k1)=<*f1/.k1*> by Th15; hence thesis by A3,FINSEQ_5:60; end; case len f1D by Th17; hence thesis by A3,FINSEQ_5:79; end; end; hence thesis; end; end; hence thesis; end; case A6: k1>k2; then mid(f1,k1,k2)=Rev ((f1/^(k2-'1))|(k1-'k2+1)) by FINSEQ_6:def 3; hence thesis by A6,FINSEQ_6:def 3; end; end; hence thesis; end; theorem Th19: for f being FinSequence of TOP-REAL 2,i1,i2,i st 1<=i1 & i1 Element of NAT equals :Def1: (n mod (len f -'1)) if n mod (len f -'1)<>0 otherwise len f -'1; correctness; end; theorem Th21: for f being FinSequence holds S_Drop(len f-'1,f)=len f-'1 proof let f be FinSequence; (len f-'1) mod (len f-'1)=0 by NAT_D:25; hence thesis by Def1; end; theorem Th22: for n being Element of NAT, f being FinSequence st 1<=n & n<=len f-'1 holds S_Drop(n,f)=n proof let n be Element of NAT,f be FinSequence; assume that A1: 1<=n and A2: n<=len f-'1; per cases by A2,XXREAL_0:1; suppose n0; then S_Drop(n,f)=n mod (len f-'1) by Def1; hence thesis by A1,A2,Def1; end; suppose A3: n mod (len f-'1)=0; then S_Drop(n,f)=len f-'1 by Def1; hence thesis by A1,A3,Def1; end; end; definition let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; pred g is_a_part>_of f,i1,i2 means :Def2: 1<=i1 & i1+1<=len f & 1<=i2 & i2+1 <=len f & g.len g=f.i2 & 1<=len g & len g_of f,i1,i2 or g is_a_part<_of f,i1,i2; end; theorem for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part_of f,i1,i2 holds 1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g_of f,i1,i2; hence thesis by Def2; end; case g is_a_part<_of f,i1,i2; hence thesis by Def3; end; end; hence thesis; end; theorem Th25: for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part>_of f ,i1,i2 & i1<=i2 holds len g=i2-'i1+1 & g=mid(f,i1,i2) proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part>_of f,i1,i2 and A2: i1<=i2; A3: 1<=len g by A1,Def2; A4: 1<=i1 by A1,Def2; A5: i1+1<=len f by A1,Def2; then A6: i1+1-1<=len f-1 by XREAL_1:9; then A7: 1<=len f-1 by A4,XXREAL_0:2; then A8: len f-1=len f-'1 by NAT_D:39; A9: now per cases; case A10: (i1+len g)-'1 mod (len f -'1)<>0; A11: i1<=len f -'1 by A5,NAT_D:49; then A12: ((i1+len g)-'1 mod (len f -'1)) 0; then 0+1<=(i1+len g)-'1 mod (len f -'1) by NAT_1:13; hence 1<=S_Drop((i1+len g)-'1,f) by Def1; end; case A19: (i1+len g)-'1 mod (len f -'1)=0; A20: i1<=len f -'1 by A5,NAT_D:49; S_Drop((i1+len g)-'1,f)=len f -'1 by A19,Def1; hence 1<=S_Drop((i1+len g)-'1,f) by A4,A20,XXREAL_0:2; end; end; i1<=i1+1 by NAT_1:11; then A21: i1<=len f by A5,XXREAL_0:2; A22: 0<>len f-'1 by A7,NAT_D:39; A23: len gf/.(S_Drop((i1+len g)-'1,f)) by A24,A9,A28,GOBOARD7:36; hence contradiction by A16,A9,A29,A30,FINSEQ_4:15; end; case A31: i2>S_Drop((i1+len g)-'1,f); i2<=len f by A17,NAT_D:46; then A32: f/.i2=f.i2 by A24,FINSEQ_4:15; f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A18,A27,A31,GOBOARD7:36; hence contradiction by A16,A18,A9,A32,FINSEQ_4:15; end; case A33: i2=S_Drop((i1+len g)-'1,f); now per cases; case A34: (i1+len g)-'1 mod (len f -'1)<>0; ex n being Nat st i1+len g -'1 =(len f-'1)*n+((i1+len g-'1) mod (len f -'1)) & ((i1+len g-'1) mod (len f -'1))=1+1 by A4,A45,XREAL_1:7; then A47: i1+j-'1<>0 by A46; A48: j<=len g by A38,A44,FINSEQ_1:1; then j+i1<=i2-i1+1+i1 by A40,A39,XREAL_1:6; then A49: i1+j<=len f by A17,XXREAL_0:2; A50: now per cases; case A51: i1+j=len f; then (i1+j-'1) mod (len f-'1)=0 by NAT_D:25; hence S_Drop(i1+j-'1,f)=i1+j-'1 by A51,Def1; end; case i1+j<>len f; then i1+j0; then 0+1<=n by NAT_1:13; then A53: (len f-'1)*n>=(len f-'1)*1 by XREAL_1:64; len g+1<=len f by A23,NAT_1:13; then len g+1-1<=len f-1 by XREAL_1:9; then len g<=len f-'1 by XREAL_0:def 2; then len g+i1<=len f-'1+i2 by A2,XREAL_1:7; then i1+len g1; then n>=1+1 by NAT_1:13; then A58: i1+len g -'1>=(len f-'1)*(1+1) by A55,A56,NAT_1:4; len g -1=1+1 by A4,A3,XREAL_1:7; hence contradiction by A59,XXREAL_0:2; end; then n>=0+1 by NAT_1:13; then A60: n=1 by A57,XXREAL_0:1; i1+len g -'1=i2*n by A33,A55,A56,Def1; then A61: i1+len g-1=i2 by A24,A60,NAT_D:39; A62: i2-i1=i2-'i1 by A2,XREAL_1:233; then A63: len g=i2-'i1+1 by A61; A64: dom g = Seg len g by FINSEQ_1:def 3; A65: for j be Nat st j in dom g holds g.j = mid(f,i1,i2).j proof let j be Nat; A66: j in NAT by ORDINAL1:def 12; assume A67: j in dom g; then A68: 1<=j by A64,FINSEQ_1:1; then A69: i1+j-'1=i1+j-1 by NAT_D:37; A70: j<=len g by A64,A67,FINSEQ_1:1; then j+i1<=i2-i1+1+i1 by A61,XREAL_1:6; then A71: i1+j<=len f by A17,XXREAL_0:2; i1+j>=1+1 by A4,A68,XREAL_1:7; then A72: i1+j-'1<>0 by A69; A73: now per cases; case A74: i1+j=len f; then (i1+j-'1) mod (len f-'1)=0 by NAT_D:25; hence S_Drop(i1+j-'1,f)=i1+j-'1 by A74,Def1; end; case i1+j<>len f; then i1+j0 by A72,NAT_D:24; then S_Drop((i1+j)-'1,f)=(i1+j-'1) mod (len f-'1) by Def1; hence S_Drop((i1+j)-'1,f)=i1+j-'1 by A75,NAT_D:24; end; end; g.j=f.S_Drop((i1+j)-'1,f) by A1,A68,A70,Def2; hence thesis by A2,A4,A25,A63,A68,A70,A66,A73,FINSEQ_6:122; end; len mid(f,i1,i2) = len g by A2,A4,A24,A21,A25,A63,FINSEQ_6:118; hence thesis by A61,A62,A65,FINSEQ_2:9; end; end; hence thesis; end; end; hence thesis; end; theorem Th26: for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part>_of f ,i1,i2 & i1>i2 holds len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2) & g=mid(f ,i1,len f-'1)^mid(f,1,i2) proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part>_of f,i1,i2 and A2: i1>i2; A3: 1<=len g by A1,Def2; g.len g=f.i2 by A1,Def2; then A4: f.i2=f.S_Drop((i1+len g)-'1,f) by A1,A3,Def2; A5: i2<=i2+1 by NAT_1:11; A6: i1<=i1+1 by NAT_1:12; A7: 1<=i1 by A1,Def2; A8: i1+1<=len f by A1,Def2; then A9: i1+1-1<=len f-1 by XREAL_1:9; then A10: 1<=len f-1 by A7,XXREAL_0:2; then A11: len f-1=len f-'1 by NAT_D:39; A12: now per cases; case A13: (i1+len g)-'1 mod (len f -'1)<>0; A14: i1<=len f -'1 by A8,NAT_D:49; then A15: ((i1+len g)-'1 mod (len f -'1)) 0; then 0+1<=(i1+len g)-'1 mod (len f -'1) by NAT_1:13; hence 1<=S_Drop((i1+len g)-'1,f) by Def1; end; case A21: (i1+len g)-'1 mod (len f -'1)=0; A22: i1<=len f -'1 by A8,NAT_D:49; S_Drop((i1+len g)-'1,f)=len f -'1 by A21,Def1; hence 1<=S_Drop((i1+len g)-'1,f) by A7,A22,XXREAL_0:2; end; end; A23: 1<=i2 by A1,Def2; A24: i2+1<=len f by A1,Def2; then A25: i2<=len f -'1 by NAT_D:49; then A26: 1<=len f -'1 by A23,XXREAL_0:2; then len f -'1len f-'1 by A10,NAT_D:39; now per cases by XXREAL_0:1; case A30: i2f/.(S_Drop((i1+len g)-'1,f)) by A23,A12,A30,GOBOARD7:36; hence contradiction by A4,A12,A31,A32,FINSEQ_4:15; end; case A33: i2>S_Drop((i1+len g)-'1,f); i2<=len f by A24,NAT_D:46; then A34: f/.i2=f.i2 by A23,FINSEQ_4:15; f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A20,A27,A33,GOBOARD7:36; hence contradiction by A4,A20,A12,A34,FINSEQ_4:15; end; case A35: i2=S_Drop((i1+len g)-'1,f); now per cases; case A36: (i1+len g)-'1 mod (len f -'1)<>0; (ex n being Nat st i1+len g -'1 =(len f-'1)*n+((i1+len g-'1) mod (len f -'1)) & ((i1+len g-'1) mod (len f -'1))0; then A39: 0+1<=n by NAT_1:13; now per cases by A39,XXREAL_0:1; case A40: 1=n; len f-'1=len f-1 by A26,NAT_D:39; then A41: i1+len g-1=len f-1+i2 by A7,A38,A40,NAT_D:37; then A42: len g=len f+i2-i1; A43: len f-'1<=len f by NAT_D:50; A44: dom g = Seg len g by FINSEQ_1:def 3; A45: i1<=len f by A8,A6,XXREAL_0:2; A46: 1<=len f-'1 by A10,NAT_D:39; A47: i1<=len f-'1 by A9,A10,NAT_D:39; then A48: len (mid(f,i1,len f-'1))=len f-'1-'i1+ 1 by A7,A45,A46,A43, FINSEQ_6:118; A49: len f-'1-'i1+1 =len f-1-i1+1 by A9,A11,XREAL_1:233 .=len f-i1; len (mid(f,i1,len f-'1)^(f|i2)) = len (mid(f,i1,len f-' 1))+ len(f|i2) by FINSEQ_1:22; then len (mid(f,i1,len f-'1)^(f|i2))=len f-i1+i2 by A24,A5 ,A48,A49,FINSEQ_1:59,XXREAL_0:2 .=len f+i2-i1 .=len f+i2-'i1 by A8,A6,NAT_D:37,XXREAL_0:2; then A50: len (mid(f,i1,len f-'1 )^(f|i2))=len g by A8,A6,A42,NAT_D:37 ,XXREAL_0:2; A51: len f-'1-'i1=len f-'1-i1 by A9,A11,XREAL_1:233; for j be Nat st j in dom g holds g.j =(mid(f,i1,len f-' 1)^(f|i2)).j proof let j be Nat; assume A52: j in dom g; then A53: 1<=j by A44,FINSEQ_1:1; then A54: i1+j-'1=i1+j-1 by NAT_D:37; i1+j>=1+1 by A7,A53,XREAL_1:7; then A55: i1+j-'1<>0 by A54; A56: j<=len g by A44,A52,FINSEQ_1:1; then A57: g.j=f.S_Drop((i1+j)-'1,f) by A1,A53,Def2; A58: j in NAT by ORDINAL1:def 12; now per cases; case A59: j<=len mid(f,i1,len f-'1); then A60: j+i1<=len f-'1-i1+1+i1 by A48,A51,XREAL_1:6; A61: now per cases; case A62: i1+j=len f; then (i1+j-'1) mod (len f-'1)=0 by NAT_D:25; hence S_Drop(i1+j-'1,f)=i1+j-'1 by A62,Def1; end; case i1+j<>len f; then i1+j0 by A55,NAT_D:24; then S_Drop((i1+j)-'1,f)=(i1+j-'1) mod (len f-'1) by Def1; hence S_Drop((i1+j)-'1,f)=i1+j-'1 by A63,NAT_D:24; end; end; A64: len f-'1<=len f by NAT_D:50; j in dom mid(f,i1,len f-'1) by A53,A59,FINSEQ_3:25; then A65: (mid(f,i1,len f-'1)^(f|i2) ).j =mid(f,i1,len f-'1 ).j by FINSEQ_1:def 7; A66: 1<=j by A44,A52,FINSEQ_1:1; i1<=len f-'1 by A9,A10,NAT_D:39; hence thesis by A7,A45,A46,A57,A58,A59,A65,A64,A66,A61, FINSEQ_6:118; end; case A67: j>len mid(f,i1,len f-'1); j<=len f+i2-i1 by A41,A44,A52,FINSEQ_1:1; then j+i1<=len f+i2-i1+i1 by XREAL_1:6; then A68: j+i1-len f<=len f+i2-len f by XREAL_1:9; jlen f-i1+i1 by A48,A49,A67,XREAL_1:6; then A74: i1+j-len f>len f-len f by XREAL_1:9; then A75: i1+j-'len f=i1+j-len f by XREAL_0:def 2; j -len mid(f,i1,len f-'1)=j-(len f-i1) by A7,A45,A46 ,A43,A47,A49,FINSEQ_6:118 .=j+i1-len f; then A76: (f|i2).(j-len mid(f,i1,len f-'1)) =f.(i1+j-'len f) by A75,A68,FINSEQ_3:112; i1+j0; i1+j-'len f+(len f-'1)=i1+j-'len f+(len f-1) by A10,NAT_D:39 .=i1+j-len f+(len f-1) by A74,XREAL_0:def 2 .=i1+j-1 .=i1+j-'1 by A53,NAT_D:37; then A79: (i1+j-'1) mod (len f-'1) =(i1+j-'len f+((len f-'1)mod (len f-'1))) mod (len f-'1) by NAT_D:23 .=(i1+j-'len f+0) mod (len f-'1) by NAT_D:25 .=(i1+j-'len f) mod (len f-'1); i1+j-(len f-'1)<=(len f-'1)+(len f-'1)-(len f-'1) by A70,XREAL_1:9; then i1+j-(len f-1)<=(len f-'1) by A10,NAT_D:39; then i1+j-'len f+1<=(len f-'1) by A75; then A80: i1+j-'len f<(len f-'1) by NAT_1:13; S_Drop (i1+j-'1,f)= (i1+j-'1) mod (len f -'1 ) by A78,Def1; hence thesis by A57,A71,A76,A79,A80,NAT_D:24; end; end; hence thesis; end; end; hence thesis; end; hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2) by A8,A6,A42 ,A50,FINSEQ_2:9,NAT_D:37,XXREAL_0:2; end; case 1=(len f-'1)*(1+1) by XREAL_1:64; then A81: i1+len g-'1>=(len f-'1)*(1+1)+i2 by A38,XREAL_1:6; A82: (len f-'1)*(1+1)<=(len f-'1)*(1+1)+i2 by NAT_1:11; A83: i1+1-1<=len f-1 by A8,XREAL_1:9; len g-11; then n>=1+1 by NAT_1:13; then A88: i1+len g -'1>=(len f-'1)*(1+1) by A85,A86,NAT_1:4; len g -1=1+1 by A7,A3,XREAL_1:7; hence contradiction by A89,XXREAL_0:2; end; then n>=0+1 by NAT_1:13; then n=1 by A87,XXREAL_0:1; then i1+len g-'1=i2 by A35,A85,A86,Def1; then A90: i1+len g-1=i2 by A23,NAT_D:39; i2-i2-(i1-i2) by XREAL_1:24; 1-1<=len g-1 by A3,XREAL_1:9; hence contradiction by A90,A91; end; end; hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2); end; end; hence thesis by A23,FINSEQ_6:116; end; theorem Th27: for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part<_of f ,i1,i2 & i1>=i2 holds len g=i1-'i2+1 & g=mid(f,i1,i2) proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part<_of f,i1,i2 and A2: i1>=i2; A3: 1<=len g by A1,Def3; g.len g=f.i2 by A1,Def3; then A4: f.i2=f.S_Drop((len f+i1-'len g),f) by A1,A3,Def3; A5: i1+1<=len f by A1,Def3; i1<=i1+1 by NAT_1:11; then A6: i1<=len f by A5,XXREAL_0:2; A7: 1<=i2 by A1,Def3; A8: i2+1<=len f by A1,Def3; then i2+1-1<=len f-1 by XREAL_1:9; then A9: 1<=len f-1 by A7,XXREAL_0:2; then A10: len f-1=len f-'1 by NAT_D:39; A11: now per cases; case A12: (len f+i1-'len g) mod (len f -'1)<>0; A13: i2<=len f -'1 by A8,NAT_D:49; then A14: ((len f+i1-'len g) mod (len f -'1)) len f-'1 by A9,NAT_D:39; A21: now per cases; case (len f+i1-'len g) mod (len f -'1)<>0; then 0+1<=(len f+i1-'len g) mod (len f -'1) by NAT_1:13; hence 1<=S_Drop((len f+i1-'len g),f) by Def1; end; case A22: (len f+i1-'len g) mod (len f -'1)=0; A23: i2<=len f -'1 by A8,NAT_D:49; S_Drop((len f+i1-'len g),f)=len f -'1 by A22,Def1; hence 1<=S_Drop((len f+i1-'len g),f) by A7,A23,XXREAL_0:2; end; end; A24: len gf/.(S_Drop((len f+i1-'len g),f)) by A7,A11,A26,GOBOARD7:36; hence contradiction by A4,A11,A27,A28,FINSEQ_4:15; end; case A29: i2>S_Drop((len f+i1-'len g),f); i2<=len f by A8,NAT_1:13; then A30: f/.i2=f.i2 by A7,FINSEQ_4:15; f/.i2<>f/.(S_Drop((len f+i1-'len g),f)) by A21,A19,A29,GOBOARD7:36; hence contradiction by A4,A21,A11,A30,FINSEQ_4:15; end; case A31: i2=S_Drop((len f+i1-'len g),f); now per cases; case A32: (len f+i1-'len g) mod (len f -'1)<>0; ex n being Nat st len f+i1-'len g =(len f-'1)*n+((len f+i1-'len g) mod (len f -'1)) & ((len f+i1-'len g) mod (len f -'1))=0+1 by NAT_1:13; A35: len f+i1-'len g=(len f-'1)*n+i2 by A31,A32,A33,Def1; now per cases by A34,XXREAL_0:1; case n=0; then i2=len f+i1-'len g by A31,A32,A33,Def1; then i2=len f+i1-len g by A24,NAT_D:37; then i2+len g=i1+len f; hence contradiction by A2,A24,XREAL_1:8; end; case A36: n=1; A37: len f+i1-'len g=len f+i1-len g by A24,NAT_D:37; A38: len f-1+i2=len f+i1-'len g by A10,A31,A32,A33,A36,Def1; then A39: len g=i1-i2+1 by A37; then A40: len g=i1-'i2+1 by A2,XREAL_1:233; A41: dom g = Seg len g by FINSEQ_1:def 3; A42: for j be Nat st j in dom g holds g.j =mid(f,i1,i2).j proof let j be Nat; A43: j in NAT by ORDINAL1:def 12; assume A44: j in dom g; then A45: 1<=j by A41,FINSEQ_1:1; A46: j<=len g by A41,A44,FINSEQ_1:1; 1-1<=i2-1 by A7,XREAL_1:9; then A47: i1-0>=i1-(i2-1) by XREAL_1:10; then A48: i1-'j+1=i1-j+1 by A38,A37,A46,XREAL_1:233,XXREAL_0:2; A49: j<=i1 by A38,A37,A46,A47,XXREAL_0:2; A50: now per cases; case len f+i1-'j=len f-'1; then len f+i1-j=len f-'1 by A24,A46,NAT_D:37,XXREAL_0:2 .=len f-1 by A9,NAT_D:39; then i1-j=-1; hence contradiction by A49,XREAL_1:48; end; case len f+i1-'j<>len f-'1; i1+1+01; then 1+1<=n by NAT_1:13; then A58: len f+i1-'len g-i2>=(len f-'1)*(1+1) by A35,XREAL_1:64; A59: len f-i2<=len f-1 by A7,XREAL_1:10; i1+1+0=len f+i1 by A61,A62,NAT_D:36; len f<=len f +i1 by NAT_1:11; hence contradiction by A24,A64,XXREAL_0:2; end; then A65: n>=0+1 by NAT_1:13; A66: now per cases by A65,XXREAL_0:1; case A67: n>1; A68: len f-'1+(len f-'1)=(len f-'1)*(1+1); i1+1+1<=len f+len g by A5,A3,XREAL_1:7; then 1+(i1+1)-len g<=len f+len g-len g by XREAL_1:9; then 1+((i1+1)-len g)-1<=len f-1 by XREAL_1:9; then len f-1+((i1+1)-len g)<=len f-1+(len f-1) by XREAL_1:6; then len f+i1-len g<=len f-1+(len f-1); then A69: len f+i1-'len g<=len f-'1+(len f-'1) by A24,A10,NAT_D:37; A70: n>=1+1 by A67,NAT_1:13; now per cases by A70,XXREAL_0:1; case n>1+1; hence contradiction by A25,A61,A62,A69,A68,XREAL_1:68; end; case A71: n=1+1; then A72: len f-1+(1+i1)-len g=len f-'1+(len f-' 1) by A24,A61,A62, NAT_D:37; then 1+(len f-'1)<=(1+i1)-(len f-'1)+(len f-'1) by A3,A10, XREAL_1:6; then 1+(len f-1)<=(1+i1) by A9,NAT_D:39; then A73: len f=i1+1 by A5,XXREAL_0:1; then i2=i1 by A61,A62,A63,A71,NAT_D:34; then i1-'i2=0 by XREAL_1:232; hence len g=i1-'i2+1 by A10,A72,A73; end; end; hence len g=i1-'i2+1; end; case A74: n=1; len f+i1-'len g=len f+i1-len g by A24,NAT_D:37; then len f+i1=i2+len g by A63,A74; hence contradiction by A2,A24,XREAL_1:8; end; end; A75: dom g = Seg len g by FINSEQ_1:def 3; A76: for j be Nat st j in dom g holds g.j =mid(f,i1,i2).j proof let j be Nat; A77: j in NAT by ORDINAL1:def 12; assume A78: j in dom g; then A79: 1<=j by A75,FINSEQ_1:1; A80: j<=len g by A75,A78,FINSEQ_1:1; 1-1<=i2-1 by A7,XREAL_1:9; then A81: i1-0>=i1-(i2-1) by XREAL_1:10; A82: i1-'i2+1=i1-i2+1 by A2,XREAL_1:233 .=i1-(i2-1); then A83: i1-'j+1=i1-j+1 by A66,A80,A81,XREAL_1:233,XXREAL_0:2; A84: j<=i1 by A66,A80,A82,A81,XXREAL_0:2; A85: now per cases; case len f+i1-'j=len f-'1; then len f+i1-j=len f-'1 by A66,A80,A82,A81,NAT_D:37,XXREAL_0:2 .=len f-1 by A9,NAT_D:39; then i1-j=-1; hence contradiction by A84,XREAL_1:48; end; case len f+i1-'j<>len f-'1; i1+1+00; A14: i1<=len f -'1 by A9,NAT_D:49; then A15: (len f+i1-'len g mod (len f -'1)) 0; then 0+1<=len f+i1-'len g mod (len f -'1) by NAT_1:13; hence 1<=S_Drop(len f+i1-'len g,f) by Def1; end; case A21: len f+i1-'len g mod (len f -'1)=0; A22: i1<=len f -'1 by A9,NAT_D:49; S_Drop(len f+i1-'len g,f)=len f -'1 by A21,Def1; hence 1<=S_Drop(len f+i1-'len g,f) by A4,A22,XXREAL_0:2; end; end; i1<=i1+1 by NAT_1:11; then A23: i1<=len f by A9,XXREAL_0:2; i1<=i1+1 by NAT_1:12; then A24: i1<=len f by A9,XXREAL_0:2; A25: 0<>len f-'1 by A10,NAT_D:39; i1<=len f -'1 by A9,NAT_D:49; then 1<=len f -'1 by A4,XXREAL_0:2; then A26: len f -'1f/.(S_Drop(len f+i1-'len g,f)) by A19,A12,A30,GOBOARD7:36; hence contradiction by A5,A12,A31,A32,FINSEQ_4:15; end; case A33: i2>S_Drop(len f+i1-'len g,f); i2<=len f by A7,NAT_1:13; then A34: f/.i2=f.i2 by A19,FINSEQ_4:15; f/.i2<>f/.(S_Drop(len f+i1-'len g,f)) by A20,A29,A33,GOBOARD7:36; hence contradiction by A5,A20,A12,A34,FINSEQ_4:15; end; case A35: i2=S_Drop(len f+i1-'len g,f); now per cases; case A36: len f+i1-'len g mod (len f -'1)<>0; ex n being Nat st len f+i1-'len g =(len f-'1)*n+((len f+i1-'len g) mod (len f -'1)) & ((len f+i1-'len g) mod (len f -'1))len f-'1; A56: j-1>=0 by A46,XREAL_1:48; then j-1=j-'1 by XREAL_0:def 2; then A57: len f<=len f+(j-1) by NAT_1:11; A58: len f+i1-'j>len f-'1 by A11,A49,A52,A55,XXREAL_0:1; now per cases; case A59: i1+1=len f & j-1=0; then len f+i1-'j=len f-1+len f-1 by A4,NAT_D:37 .=len f-'1+(len f-'1) by A11; then (len f+i1-'j)mod (len f-'1)=0 by Th3; then S_Drop(len f+i1-'j,f) =j+i1-'1 by A59,Def1; then A60: S_Drop(len f+i1-'j,f) =1+i1-1 by A59,NAT_D:37 .=i1-j+1 by A59; A61: 1<=i1-'j+1 by NAT_1:11; i1<=i1+(j-'1) by NAT_1:11; then A62: i1-(j-'1)<=i1 by XREAL_1:20; A63: i1-j+1=i1-'j+1 by A41,A51,XREAL_1:233; A64: j-1=j-'1 by A46,XREAL_1:233; mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23 ,A46,A50,A51,A54,Th13 .=f.(i1-'j+1) by A23,A63,A61,A64,A62,FINSEQ_6:123 ; hence thesis by A41,A48,A51,A53,A60,XREAL_1:233; end; case A65: i1+1<>len f or j-1<>0; now per cases by A65; case i1+1<>len f; then i1+10; then len f0 by A11,A49,A58 ,Th1; then A67: S_Drop(len f+i1-'j,f) =(len f+i1-'j) mod ( len f-'1) by Def1 .=len f+i1-j-(len f-1) by A11,A49,A52,A66,Th2 .=(i1-j)+1; A68: 1<=i1-'j+1 by NAT_1:11; i1<=i1+(j-'1) by NAT_1:11; then A69: i1-(j-'1)<=i1 by XREAL_1:20; A70: i1-j+1=i1-'j+1 by A41,A51,XREAL_1:233; A71: j-1=j-'1 by A46,XREAL_1:233; mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23 ,A46,A50,A51,A54,Th13 .=f.(i1-'j+1) by A23,A70,A68,A71,A69,FINSEQ_6:123 ; hence thesis by A41,A48,A51,A53,A67,XREAL_1:233; end; end; hence thesis; end; end; hence thesis; end; case A72: j>len mid(f,i1,1); i2+1-1<=len f-1 by A7,XREAL_1:9; then A73: i2-i2<=len f-1-i2 by XREAL_1:9; A74: len f-i2=len f-1-i2+1 .=len f-'1-'i2+1 by A11,A73,XREAL_0:def 2; A75: len f+0=0 by A2,XREAL_1:48; then len f+0<=len f+(i2-i1) by XREAL_1:7; then A80: len f-(i2-i1)<=len f+(i2-i1)-(i2- i1) by XREAL_1:9; A81: j<=len f+i1-i2 by A39,A43,A45,FINSEQ_1:1; then j<=len f by A80,XXREAL_0:2; then j=len f+i1-'j by A11,A81,A80,NAT_D:37,XXREAL_0:2; now per cases; case A87: (len f+i1-'j) mod (len f -'1)=0; then len f+i1-'j=len f-'1 by A82,A86,Th4; hence thesis by A48,A83,A87,Def1; end; case A88: (len f+i1-'j) mod (len f -'1)<>0; len f+(i1+1)<=len f+j by A84,XREAL_1:7; then len f+i1+1-j<=len f+j-j by XREAL_1:9; then A89: len f+i1+1-j-1<=len f-1 by XREAL_1:9; A90: S_Drop(len f+i1-'j,f) = (len f+i1-'j) mod (len f -'1) by A88,Def1; len f+i1-j=len f-'1 implies contradiction by A85,A88, NAT_D:25; then len f+i1-'j<(len f-'1) by A11,A85,A89,XXREAL_0:1; hence thesis by A48,A83,A90,NAT_D:24; end; end; hence thesis; end; end; hence thesis; end; hence thesis by A7,A6,A40,A44,FINSEQ_2:9,NAT_D:37,XXREAL_0:2; end; case n<>0; then A91: 0+1<=n by NAT_1:13; now per cases by A91,XXREAL_0:1; case A92: 1=n; A93: len f+i1-'len g=len f+i1-len g by A27,NAT_D:37; i1+1+0=(len f-'1)*(1+1) by XREAL_1:64; then A94: len f+i1-'len g>=(len f-'1)*(1+1)+i2 by A38,XREAL_1:6; A95: (len f-'1)*(1+1)<(len f-'1)*(1+1)+i2 by A2,XREAL_1:29; i1+1-1<=len f-1 by A9,XREAL_1:9; then 1+i1<=len g+(len f-'1) by A3,A11,XREAL_1:7; then len f-1+(1+i1)<=len f-1+(len g+(len f-'1)) by XREAL_1:6; then A96: len f+i1-len g<=len f-1+len g+(len f-' 1)-len g by XREAL_1:9 ; len f+i1-len g=len f+i1-'len g by A27,NAT_D:37; hence contradiction by A11,A94,A96,A95,XXREAL_0:2; end; end; hence contradiction; end; end; hence thesis; end; case A97: len f+i1-'len g mod (len f -'1)=0; ex n being Nat st len f+i1-'len g =(len f-'1)*n+((len f+i1-' len g) mod (len f -'1)) & ((len f+i1-'len g) mod (len f -'1))1; then n>=1+1 by NAT_1:13; then A100: len f+i1-'len g>=(len f-'1)*(1+1) by A97,A98,NAT_1:4; now assume i1+1len f-1+1 by A2,XREAL_1:6; hence contradiction by A1,Def3; end; now assume n=0; then A101: len f+i1<=len g by A97,A98,NAT_D:36; len f<=len f+i1 by NAT_1:11; hence contradiction by A27,A101,XXREAL_0:2; end; then n>=0+1 by NAT_1:13; then A102: n=1 by A99,XXREAL_0:1; len f+i1-'len g=i2*n by A35,A97,A98,Def1; then A103: len f+i1-len g=i2 by A27,A102,NAT_D:37; then A104: len f+i1-i2=len g; A105: dom g = Seg len g by FINSEQ_1:def 3; A106: len (mid(f,i1,1))=i1-'1+1 by A4,A24,Th9 .=i1 by A4,XREAL_1:235; len (mid(f,len f-'1,i2))=len f-'1-'i2+1 by A19,A11,A8,A26,Th9; then len (mid(f,len f-'1,i2))=len f-1-i2+1 by A11,A8,XREAL_1:233; then len (mid(f,i1,1)^mid(f,len f-'1,i2))=i1+(len f-i2) by A106, FINSEQ_1:22 .=i1+len f-i2 .=len f+i1-'i2 by A7,A6,NAT_D:37,XXREAL_0:2; then A107: len (mid(f,i1,1)^mid(f,len f-'1,i2))=len g by A7,A6,A104,NAT_D:37 ,XXREAL_0:2; for j be Nat st j in dom g holds g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j proof let j be Nat; assume A108: j in dom g; then A109: 1<=j by A105,FINSEQ_1:1; A110: j<=len g by A105,A108,FINSEQ_1:1; then A111: g.j=f.S_Drop(len f+i1-'j,f) by A1,A109,Def3; A112: len f+i1-'j=len f+i1-j by A27,A110,NAT_D:37,XXREAL_0:2; A113: j in NAT by ORDINAL1:def 12; now per cases; case A114: j<=len mid(f,i1,1); len f-'1<=len f by NAT_D:50; then len f-1+j<=len f+i1 by A11,A106,A114,XREAL_1:7; then A115: len f-1+j-j<=len f+i1-j by XREAL_1:9; j in dom mid(f,i1,1) by A109,A114,FINSEQ_3:25; then A116: (mid(f,i1,1)^mid(f,len f-'1,i2)).j =mid(f, i1,1).j by FINSEQ_1:def 7; A117: len mid(f,i1,1)=i1-'1+1 by A4,A23,Th9; now per cases; case len f+i1-'j=len f-'1; then len f+i1-j=len f-1 by A11,A106,A114,NAT_D:37; then i1+1=j; hence thesis by A106,A114,NAT_1:13; end; case A118: len f+i1-'j<>len f-'1; A119: j-1>=0 by A109,XREAL_1:48; then j-1=j-'1 by XREAL_0:def 2; then A120: len f<=len f+(j-1) by NAT_1:11; A121: len f+i1-'j>len f-'1 by A11,A112,A115,A118,XXREAL_0:1; now per cases; case A122: i1+1=len f & j-1=0; then len f+i1-'j=len f-1+len f-1 by A4,NAT_D:37 .=len f-'1+(len f-'1) by A11; then (len f+i1-'j)mod (len f-'1)=0 by Th3; then S_Drop(len f+i1-'j,f) =j+i1-'1 by A122,Def1; then S_Drop(len f+i1-'j,f) =i1+ 1-1 by A122,NAT_D:37 .=i1-j+1 by A122; then A123: f.S_Drop(len f+i1-'j,f)=f.(i1-'j+1) by A106,A114, XREAL_1:233; A124: 1<=i1-'j+1 by NAT_1:11; i1<=i1+(j-'1) by NAT_1:11; then A125: i1-(j-'1)<=i1 by XREAL_1:20; A126: i1-j+1=i1-'j+1 by A106,A114,XREAL_1:233; A127: j-1=j-'1 by A109,XREAL_1:233; mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23,A109 ,A113,A114,A117,Th13 .=f.(i1-'j+1) by A23,A126,A124,A127,A125,FINSEQ_6:123 ; hence thesis by A1,A109,A110,A116,A123,Def3; end; case A128: i1+1<>len f or j-1<>0; now per cases by A128; case i1+1<>len f; then i1+10; then len f0 by A11,A112,A121 ,Th1; then A130: S_Drop(len f+i1-'j,f) =(len f+i1-'j) mod (len f -'1) by Def1 .=len f+(i1-j)-(len f-1) by A11,A112,A115,A129,Th2 .=(i1-j)+1; A131: 1<=i1-'j+1 by NAT_1:11; i1<=i1+(j-'1) by NAT_1:11; then A132: i1-(j-'1)<=i1 by XREAL_1:20; A133: i1-j+1=i1-'j+1 by A106,A114,XREAL_1:233; A134: j-1=j-'1 by A109,XREAL_1:233; mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1) by A4,A23,A109 ,A113,A114,A117,Th13 .=f.(i1-'j+1) by A23,A133,A131,A134,A132,FINSEQ_6:123 ; hence thesis by A106,A111,A114,A116,A130,XREAL_1:233; end; end; hence thesis; end; end; hence thesis; end; case A135: j>len mid(f,i1,1); i2+1-1<=len f-1 by A7,XREAL_1:9; then A136: i2-i2<=len f-1-i2 by XREAL_1:9; A137: len f-i2=len f-1-i2+1 .=len f-'1-'i2+1 by A11,A136,XREAL_0:def 2; A138: len f+0=0 by A2,XREAL_1:48; then len f+0<=len f+(i2-i1) by XREAL_1:7; then A143: len f-(i2-i1)<=len f+(i2-i1)-(i2-i1) by XREAL_1:9; A144: j<=len f+i1-i2 by A103,A105,A108,FINSEQ_1:1; then j<=len f by A143,XXREAL_0:2; then j=len f+i1-'j by A11,A144,A143,NAT_D:37,XXREAL_0:2; now per cases; case A150: (len f+i1-'j) mod (len f -'1)=0; then len f+i1-'j=len f-'1 by A145,A149,Th4; hence thesis by A111,A146,A150,Def1; end; case A151: (len f+i1-'j) mod (len f -'1)<>0; len f+(i1+1)<=len f+j by A147,XREAL_1:7; then len f+i1+1-j<=len f+j-j by XREAL_1:9; then A152: len f+i1+1-j-1<=len f-1 by XREAL_1:9; A153: S_Drop(len f+i1-'j,f) = (len f+i1-'j) mod (len f -'1 ) by A151,Def1; len f+i1-j=len f-'1 implies contradiction by A148,A151, NAT_D:25; then len f+i1-'j<(len f-'1) by A11,A148,A152,XXREAL_0:1; hence thesis by A111,A146,A153,NAT_D:24; end; end; hence thesis; end; end; hence thesis; end; hence thesis by A7,A6,A104,A107,FINSEQ_2:9,NAT_D:37,XXREAL_0:2; end; end; hence thesis; end; end; hence thesis; end; theorem Th29: for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part>_of f ,i1,i2 holds Rev g is_a_part<_of f,i2,i1 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; A1: len g=len (Rev g) by FINSEQ_5:def 3; assume A2: g is_a_part>_of f,i1,i2; then A3: 1<=len g by Def2; A4: len gi2; then len g=len f+i2-'i1 by A2,Th26; then len g+i1=len f+i2-i1+i1 by A7,NAT_D:37; then len f+i2-'i=i1+len g-i by A1,A10,NAT_D:37; then len f+i2-'i=i1+(len g-i); then len f+i2-'i=i1+(len g-'i)+1-1 by A1,A10,XREAL_1:233; hence thesis by A13,NAT_D:37; end; end; hence thesis; end; A15: i2+1<=len f by A2,Def2; A16: 1<=i1 by A2,Def2; A17: (Rev g).len (Rev g)=(Rev g).len g by FINSEQ_5:def 3 .=g.(len g-len g+1) by A3,FINSEQ_6:115 .=f.S_Drop((i1+1-'1),f) by A2,A3,Def2 .=f.S_Drop(i1,f) by NAT_D:34; A18: now per cases; case A19: i1 mod (len f-'1)<>0; then i1 <> len f-'1 by NAT_D:25; then A20: i1_of f,i2,i1 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; A1: len g=len (Rev g) by FINSEQ_5:def 3; assume A2: g is_a_part<_of f,i1,i2; then A3: 1<=len g by Def3; A4: 1<=i2 by A2,Def3; A5: len g=i2; then len g=i1-'i2+1 by A2,Th27; then len g=i1-i2+1 by A18,XREAL_1:233; then i1-(len g-i)=(i2+i)-1; then i1-(len g-i)=(i2+i)-'1 by A9,NAT_D:37; then i1-(len g-'i)=(i2+i)-'1 by A1,A10,XREAL_1:233; then len f-1+(i1-(len g-'i))=(i2+i)-'1+(len f-'1) by A3,A5,XREAL_1:233 ,XXREAL_0:2; then len f+i1-(len g-'i+1)=(i2+i)-'1+(len f-'1); then (Rev g).i=f.S_Drop((i2+i)-'1+(len f-'1),f) by A13,A15,A14,NAT_D:37 ,XXREAL_0:2 .=f.S_Drop((i2+i)-'1,f) by Th23; hence thesis; end; end; hence thesis; end; A19: S_Drop(len f-'1+i1,f)=S_Drop(i1,f) by Th23; A20: i1+1<=len f by A2,Def3; then i1+1-1<=len f-1 by XREAL_1:9; then A21: i1<=len f-'1 by A3,A5,XREAL_1:233,XXREAL_0:2; A22: 1<=i1 by A2,Def3; A23: (Rev g).len (Rev g)=(Rev g).len g by FINSEQ_5:def 3 .=g.(len g-len g+1) by A3,FINSEQ_6:115 .=f.S_Drop(len f+i1-'1,f) by A2,A3,Def3 .=f.S_Drop(len f-'1+i1,f) by A3,A5,NAT_D:38,XXREAL_0:2; now per cases; case A24: i1 mod (len f-'1)<>0; then i1 <> len f-'1 by NAT_D:25; then A25: i1_of f,i1,i2 proof let f be non constant standard special_circular_sequence, i1,i2 be Element of NAT; assume that A1: 1<=i1 and A2: i1<=i2 and A3: i2i2 & i1_of f,i1,i2 proof let f be non constant standard special_circular_sequence, i1,i2 be Element of NAT; assume that A1: 1<=i2 and A2: i1>i2 and A3: i1len mid(f,i1,len f-'1); then i>=len f-'i1+1 by A20,A19,A18,NAT_1:13; then A27: i-(len f-'i1)>=len f-'i1+1-(len f-'i1) by XREAL_1:9; then A28: 1<=i-'(len f-'i1) by NAT_D:39; A29: len f-i1=len f-'i1 by A3,XREAL_1:233; i-(len f-i1)<=len f-i1+i2-(len f-i1) by A10,A16,XREAL_1:9; then A30: i-'(len f-'i1)<=i2 by A29,A27,NAT_D:39; then A31: i-'(len f-'i1)<=len f-'1 by A13,XXREAL_0:2; len f-'1+(i-'(len f-'i1))=len f-'1+(i-(len f-'i1)) by A20,A19,A18,A26, XREAL_1:233 .=len f-'1+i-(len f-'i1) .=len f-1+i-(len f-'i1) by A3,A5,XREAL_1:233,XXREAL_0:2 .=len f-1+i-(len f-i1) by A3,XREAL_1:233 .=(i+i1)-1 .=i1+i-'1 by A15,NAT_D:37; then A32: S_Drop((i1+i)-'1,f) =S_Drop(i-'(len f-'i1),f) by Th23 .=i-'(len f-'i1) by A28,A31,Th22; (mid(f,i1,len f-'1)^mid(f,1,i2)).i =mid(f,1,i2).(i-len mid(f,i1, len f-'1)) by A16,A26,FINSEQ_6:108 .=mid(f,1,i2).(i-'(len f-'i1)) by A20,A19,A18,A26,XREAL_1:233 .=f.(i-'(len f-'i1)) by A11,A28,A30,FINSEQ_6:123; hence thesis by A32; end; end; hence thesis; end; i1-i2>0 by A2,XREAL_1:50; then len fi2; mid(h,i1,i2)=Rev mid(h,i2,i1) by Th18; then x in L~mid(h,i2,i1) by A5,SPPOL_2:22; then x in union { LSeg(mid(h,i2,i1),i) : 1 <= i & i+1 <= len mid(h,i2, i1) } by TOPREAL1:def 4; then consider Y being set such that A26: x in Y & Y in { LSeg(mid(h,i2,i1),i) : 1 <= i & i+1 <= len mid(h,i2,i1) } by TARSKI:def 4; consider i such that A27: Y=LSeg(mid(h,i2,i1),i) and A28: 1 <= i and A29: i+1 <= len mid(h,i2,i1) by A26; A30: LSeg(mid(h,i2,i1),i)=LSeg(mid(h,i2,i1)/.i,mid(h,i2,i1)/.(i+1)) by A28 ,A29,TOPREAL1:def 3; i<=i+1 by NAT_1:11; then A31: i<=len mid(h,i2,i1) by A29,XXREAL_0:2; then A32: mid(h,i2,i1).i=h.(i+i2-'1) by A1,A2,A3,A4,A25,A28,FINSEQ_6:118; A33: mid(h,i2,i1)/.i=mid(h,i2,i1).i by A28,A31,FINSEQ_4:15; A34: mid(h,i2,i1)/.(i+1)=mid(h,i2,i1).(i+1) by A29,FINSEQ_4:15,NAT_1:11; 1+1<=i+i2 by A3,A28,XREAL_1:7; then A35: 1+1-1<=i+i2-1 by XREAL_1:9; then A36: 1<=i+i2-'1 by A3,NAT_D:37; i+i2-'1<=i+i2-'1+1 by NAT_1:11; then i+i2-'1<=i+i2-1+1 by A3,NAT_D:37; then A37: 1<=i+i2 by A36,XXREAL_0:2; 1<=i+1 by NAT_1:11; then A38: mid(h,i2,i1).(i+1)=h.(i+1+i2-'1) by A1,A2,A3,A4,A25,A29,FINSEQ_6:118; A39: i+1+i2-'1=i+1+i2-1 by A3,NAT_D:37 .=i+i2; then A40: i+1+i2-'1=i+i2-1+1 .=i+i2-'1+1 by A3,NAT_D:37; len mid(h,i2,i1)=i1-'i2+1 by A1,A2,A3,A4,A25,FINSEQ_6:118; then i+1-1<=i1-'i2+1-1 by A29,XREAL_1:9; then i<=i1-i2 by A25,XREAL_1:233; then A41: i+i2<=i1-i2+i2 by XREAL_1:6; then A42: i+i2<=len h by A2,XXREAL_0:2; A43: i+i2<=len h by A2,A41,XXREAL_0:2; then h/.(i+i2-'1)=h.(i+i2-'1) by A36,FINSEQ_4:15,NAT_D:44; then LSeg(mid(h,i2,i1),i)=LSeg(h/.(i+i2-'1),h/.(i+1+i2-'1)) by A30,A32,A38 ,A33,A34,A39,A37,A42,FINSEQ_4:15 .=LSeg(h,i+i2-'1) by A35,A43,A39,A40,TOPREAL1:def 3; then LSeg(mid(h,i2,i1),i) in { LSeg(h,j) : 1 <= j & j+1 <= len h} by A35,A39,A40,A42; then x in union { LSeg(h,j) : 1 <= j & j+1 <= len h} by A26,A27, TARSKI:def 4; hence thesis by TOPREAL1:def 4; end; end; hence thesis; end; end; theorem Th36: for g being FinSequence of D holds g is one-to-one iff for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g/.i1=g/.i2) holds i1= i2 proof let g be FinSequence of D; A1: (for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g/. i1=g/.i2) holds i1=i2) implies g is one-to-one proof assume A2: for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g/.i1=g/.i2) holds i1=i2; for x1,x2 being set st x1 in dom g & x2 in dom g & g.x1=g.x2 holds x1 = x2 proof let x1,x2 be set; assume that A3: x1 in dom g and A4: x2 in dom g and A5: g.x1=g.x2; reconsider n2=x2 as Element of NAT by A4; A6: 1<=n2 by A4,FINSEQ_3:25; reconsider n1=x1 as Element of NAT by A3; A7: n1<=len g by A3,FINSEQ_3:25; A8: n2<=len g by A4,FINSEQ_3:25; 1<=n1 by A3,FINSEQ_3:25; hence thesis by A2,A5,A7,A6,A8; end; hence thesis by FUNCT_1:def 4; end; g is one-to-one implies for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g/.i1=g/.i2) holds i1=i2 proof assume A9: g is one-to-one; thus for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g & (g.i1=g.i2 or g /.i1=g/.i2) holds i1=i2 proof let i1,i2; assume that A10: 1<=i1 and A11: i1<=len g and A12: 1<=i2 and A13: i2<=len g and A14: g.i1=g.i2 or g/.i1=g/.i2; A15: i2 in dom g by A12,A13,FINSEQ_3:25; A16: g/.i2=g.i2 by A12,A13,FINSEQ_4:15; A17: g/.i1=g.i1 by A10,A11,FINSEQ_4:15; i1 in dom g by A10,A11,FINSEQ_3:25; hence thesis by A9,A14,A15,A17,A16,FUNCT_1:def 4; end; end; hence thesis by A1; end; theorem Th37: for f being non constant standard special_circular_sequence, i2 st 14 by GOBOARD7:34; then A13: f/.n1<>f/.n2 by A4,A11,A12,GOBOARD7:35; A14: (f|i2)/.n1=f/.n1 by A10,FINSEQ_4:70; A15: (f|i2)/.n2=f/.n2 by A9,FINSEQ_4:70; (f|i2)/.n1=(f|i2).n1 by A4,A5,FINSEQ_4:15; hence contradiction by A6,A7,A8,A13,A14,A15,FINSEQ_4:15; end; case n1=n2; hence thesis; end; case A16: n24 by GOBOARD7:34; then A18: f/.n2<>f/.n1 by A6,A16,A17,GOBOARD7:35; A19: (f|i2)/.n2=f/.n2 by A9,FINSEQ_4:70; A20: (f|i2)/.n1=f/.n1 by A10,FINSEQ_4:70; (f|i2)/.n2=(f|i2).n2 by A6,A7,FINSEQ_4:15; hence contradiction by A4,A5,A8,A18,A19,A20,FINSEQ_4:15; end; end; hence thesis; end; then A21: f|i2 is one-to-one by Th36; for i,j be Nat st i+1 < j holds LSeg(f|i2,i) misses LSeg(f|i2,j) proof let i,j be Nat; assume A22: i+1 < j; A23: j in NAT by ORDINAL1:def 12; A24: i in NAT by ORDINAL1:def 12; now per cases; case A25: 1<=i & j+1<=len (f|i2); i2<=len f by A2,NAT_1:13; then len (f|i2)=i2 by FINSEQ_1:59; then j+1i or j+1>len (f|i2); now per cases by A28; case 1>i; then LSeg(f|i2,i)={} by TOPREAL1:def 3; then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {}; hence thesis by XBOOLE_0:def 7; end; case j+1>len (f|i2); then LSeg(f|i2,j)={} by TOPREAL1:def 3; then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {}; hence thesis by XBOOLE_0:def 7; end; end; hence thesis; end; end; hence thesis; end; then A29: f|i2 is s.n.c. by TOPREAL1:def 7; 1+1<=len (f|i2) by A1,A3,NAT_1:13; hence thesis by A29,A21,TOPREAL1:def 8; end; theorem Th38: for f being non constant standard special_circular_sequence, i2 st 1<=i2 & i2+1i or j>=len (f/^i2); now per cases by A10; case 1>i; then LSeg(f/^i2,i)={} by TOPREAL1:def 3; then LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = {}; hence thesis by XBOOLE_0:def 7; end; case j>=len (f/^i2); then j+1>len (f/^i2) by NAT_1:13; then LSeg(f/^i2,j)={} by TOPREAL1:def 3; then LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = {}; hence thesis by XBOOLE_0:def 7; end; end; hence thesis; end; end; hence thesis; end; then A11: f/^i2 is s.n.c. by TOPREAL1:def 7; A12: len (f/^i2)=len f-i2 by A3,RFINSEQ:def 1; for n1,n2 being Element of NAT st 1<=n1 & n1<=len (f/^i2) & 1<=n2 & n2 <=len (f/^i2) &((f/^i2).n1=(f/^i2).n2 or (f/^i2)/.n1=(f/^i2)/.n2) holds n1=n2 proof let n1,n2 be Element of NAT; assume that A13: 1<=n1 and A14: n1<=len (f/^i2) and A15: 1<=n2 and A16: n2<=len (f/^i2) and A17: (f/^i2).n1=(f/^i2).n2 or (f/^i2)/.n1=(f/^i2)/.n2; A18: n2 in dom (f/^i2) by A15,A16,FINSEQ_3:25; A19: n1 in dom (f/^i2) by A13,A14,FINSEQ_3:25; now per cases by XXREAL_0:1; case n1f/.(i2+n2) by A22,A20,GOBOARD7:37; A24: (f/^i2)/.n1=f/.(i2+n1) by A19,FINSEQ_5:27; A25: (f/^i2)/.n2=f/.(i2+n2) by A18,FINSEQ_5:27; (f/^i2)/.n1=(f/^i2).(n1) by A13,A14,FINSEQ_4:15; hence contradiction by A15,A16,A17,A23,A24,A25,FINSEQ_4:15; end; case n1=n2; hence thesis; end; case n2f/.(i2+n1) by A28,A26,GOBOARD7:37; n2 in dom (f/^i2) by A15,A16,FINSEQ_3:25; then A30: (f/^i2)/.n2=f/.(i2+n2) by FINSEQ_5:27; n1 in dom (f/^i2) by A13,A14,FINSEQ_3:25; then A31: (f/^i2)/.n1=f/.(i2+n1) by FINSEQ_5:27; (f/^i2)/.n2=(f/^i2).n2 by A15,A16,FINSEQ_4:15; hence contradiction by A13,A14,A17,A29,A30,A31,FINSEQ_4:15; end; end; hence thesis; end; then A32: f/^i2 is one-to-one by Th36; i2+1-i20 by A2,XREAL_1:50; then A8: 1<>i2-'i1+1 by XREAL_0:def 2; i2-'i1>0 by A7,XREAL_0:def 2; then A9: i2-'i1>=0+1 by NAT_1:13; then A10: 1<=i2-'i1+1 by NAT_1:13; i1p0 holds q1 in LSeg(p,q2) or q2 in LSeg(p,q1) proof let p0,p,q1,q2 be Point of TOP-REAL 2; assume that A1: p0 in LSeg(p,q1) and A2: p0 in LSeg(p,q2) and A3: p<>p0; consider r such that A4: p0=(1-r)*p + r*q1 and A5: 0 <= r and A6: r <= 1 by A1; A7: 1-r>=0 by A6,XREAL_1:48; A8: p0-r*q1=(1-r)*p by A4,EUCLID:48; consider s such that A9: p0=(1-s)*p + s*q2 and A10: 0 <= s and A11: s <= 1 by A2; A12: 1-s>=0 by A11,XREAL_1:48; A13: p0-s*q2=(1-s)*p by A9,EUCLID:48; A14: p0-(1-s)*p=s*q2 by A9,EUCLID:48; A15: p0-(1-r)*p=r*q1 by A4,EUCLID:48; A16: now assume A17: r<>s; now per cases by A17,XXREAL_0:1; case A18: r0; hence thesis by A32,A33,EUCLID:34; end; case r=0; then p0=(1-0)*p+0.TOP-REAL 2 by A4,EUCLID:29; then p0=(1-0)*p by EUCLID:27; hence contradiction by A3,EUCLID:29; end; end; hence thesis; end; hence thesis by A16; end; theorem Th42: for f being non constant standard special_circular_sequence holds LSeg(f,1)/\ LSeg(f,len f-'1)={f.1} proof let f be non constant standard special_circular_sequence; A1: 34 by GOBOARD7:34; then A3: len f-1=len f-'1 by XREAL_1:233,XXREAL_0:2; A4: 2f/.1; now per cases by A13,A18,A22,Th41; case A23: f/.(1+1) in LSeg(f/.1,f/.(len f-'1)); len f-'1+1=len f-1+1 by A2,XREAL_1:233,XXREAL_0:2 .=len f; then A24: f/.(len f-'1+1)=f/.1 by FINSEQ_6:def 1; f/.(1+1) in LSeg(f/.(1+1),f/.(1+1+1)) by RLTOPSP1:68; then LSeg(f/.(1+1),f/.(1+1+1))/\ LSeg(f/.(len f-'1),f/.(len f-'1+1 )) <>{} by A23,A24,XBOOLE_0:def 4; then LSeg(f/.(1+1),f/.(1+1+1)) meets LSeg(f/.(len f-'1),f/.(len f -'1+1)) by XBOOLE_0:def 7; hence contradiction by A9,A3,A17,A19,A21,GOBOARD5:def 4; end; case A25: f/.(len f-'1) in LSeg(f/.1,f/.(1+1)); f/.(len f-'1) in LSeg(f/.(len f-'1-'1),f/.(len f-'1)) by RLTOPSP1:68; then LSeg(f,1)/\ LSeg(f,len f-'1-'1)<>{} by A15,A20,A25, XBOOLE_0:def 4; then A26: LSeg(f,1) meets LSeg(f,len f-'1-'1) by XBOOLE_0:def 7; 3+1-1<*>(TOP-REAL 2) by A20; mid(f,len f-'1,i2)<><*>(TOP-REAL 2) by A24; then A32: L~(mid(f,i1,1)^mid(f,len f-'1,i2)) = L~mid(f,i1,1) \/ LSeg(mid(f,i1,1) /.len mid(f,i1,1),mid(f,len f-'1,i2)/.1) \/ L~mid(f,len f-'1,i2) by A31, SPPOL_2:23; A33: L~f c= (L~g1) \/ (L~g2) proof let x be set; assume A34: x in L~f; then reconsider p=x as Point of TOP-REAL 2; consider i such that A35: 1 <= i and A36: i+1 <= len f and A37: p in LSeg(f,i) by A34,SPPOL_2:13; now per cases; case A38: i1<=i & i1; then A70: 1i3; then A81: k3+11; then 11; then 1len f-'1; then A120: i2i2-'i1; then ilen f-'1-'i2; then k_of f ,i1,i2 & i1_of f,i1,i2 and A2: i1_of f,i1,i2 & i1>i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part>_of f,i1,i2 and A2: i1>i2; A3: g=mid(f,i1,len f-'1)^(f|i2) by A1,A2,Th26; set f1=mid(f,i1,len f); A4: 1<=i1 by A1,Def2; then A5: i1-1=i1-'1 by XREAL_1:233; A6: 1<=len g by A1,Def2; then A7: g/.len g=g.len g by FINSEQ_4:15; A8: len g1; union { LSeg((f/^(i1-'1)),i) : 1 <= i & i+1 <= len (f/^(i1-'1)) } /\ union { LSeg((f|i2),j) : 1 <= j & j+1 <= len (f|i2) } ={f.1} proof A40: (f|2).(1+1)=f.(1+1) by FINSEQ_3:112; A41: (f|2).1=f.1 by FINSEQ_3:112; A42: len (f|2)=2 by A36,FINSEQ_1:59; then A43: (f|2)/.1=(f|2).1 by FINSEQ_4:15; len (f|2)-'1=2-1 by A42,NAT_D:39 .=1; then A44: LSeg((f|2),len (f|2)-'1) = LSeg((f|2)/.(len (f|2)-'1) ,(f|2)/.( len (f|2)-'1+1)) by A42,TOPREAL1:def 3; A45: len (f|i2)=i2 by A17,FINSEQ_1:59; then A46: 1+1<=len (f|i2) by A39,NAT_1:13; then A47: LSeg(f|i2,1)=LSeg((f|i2)/.1,(f|i2)/.(1+1)) by TOPREAL1:def 3; (f|i2).1=f.1 by A14,FINSEQ_3:112; then A48: (f|2)/.1=(f|i2)/.1 by A14,A43,A41,A45,FINSEQ_4:15; A49: f.1=f/.1 by A9,FINSEQ_4:15; A50: len (f|2)-'1=1+1-'1 by A36,FINSEQ_1:59 .=1 by NAT_D:34; then (f|2)/.(len (f|2)-'1)=f/.1 by A49,A43,FINSEQ_3:112; then A51: f.1 in LSeg((f|2),len (f|2)-'1) by A49,A44,RLTOPSP1:68; A52: (f|2)/.(1+1)=(f|2).(1+1) by A42,FINSEQ_4:15; A53: f/.len f in LSeg((f/^(i1-'1))/.(len (f/^(i1-'1))-'1), f/.len f) by RLTOPSP1:68; (f|i2).(1+1)=f.(1+1) by A45,A46,FINSEQ_3:112; then A54: (f|2)/.(1+1)=(f|i2)/.(1+1) by A46,A40,A52,FINSEQ_4:15; A55: len (f/^(i1-'1))=len f-'(i1-'1) by RFINSEQ:29; i1-i11; then LSeg(f,(i1-'1)+j1) misses LSeg(f,j2) by A99,A94, GOBOARD5:def 4; hence LSeg(f,(i1-'1)+j1) /\ LSeg(f,j2)={} by XBOOLE_0:def 7; end; case (i1-'1)+j1 < len f-'1; then (i1-'1)+j1+1 < len f-'1+1 by XREAL_1:6; then LSeg(f,(i1-'1)+j1) misses LSeg(f,j2) by A28,A99, GOBOARD5:def 4; hence LSeg(f,(i1-'1)+j1) /\ LSeg(f,j2)={} by XBOOLE_0:def 7; end; end; hence contradiction by A67,A68,A80,A81,A79,A91,XBOOLE_0:def 4; end; then A101: LSeg((f|i2),j2) = LSeg(f,1) by A46,SPPOL_2:3; len f-'1-(i1-'1)+(i1-'1)<=len f by A28,A27; then A102: len f-'1-'(i1-'1)+(i1-'1)<=len f by A64,XREAL_1:233; A103: len f-'1-'(i1-'1)+1+(i1-'1)= len f-'1-(i1-'1)+1+(i1-'1) by A64, XREAL_1:233 .=len f-'1+1 .=len f-1+1 by A6,A8,XREAL_1:233,XXREAL_0:2 .=len f; A104: len (f/^(i1-'1))=len f-(i1-'1) by A12,A55,NAT_D:44,XREAL_1:233; len f-'1-(i1-'1) by FINSEQ_5:20; A115: mid(f1,1,len f1-'1)=f1|(len f1-'1) by A23,FINSEQ_6:116; A116: len f1-'1+1=len f1 by A20,NAT_D:34; <*f/.1*>=<*f1/.len f1*> by A13,A10,A35,A37,FINSEQ_4:15; hence mid(f1,1,len f1-'1)^mid(f,1,i2) is being_S-Seq by A15,A114,A115 ,A116,FINSEQ_5:21; end; end; A117: 1<=len f1 by A20,NAT_1:11; then len mid(f1,1,len f1-'1)=len f1-'1-'1+1 by A23,A22,FINSEQ_6:118 .=len f-'i1+1-'1-'1+1 by A4,A9,A12,FINSEQ_6:118; then A118: len mid(f1,1,len f1-'1)=len mid(f,i1,len f-'1) by A25,A32,NAT_D:34; for k be Nat st 1<=k & k<=len mid(f,i1,len f-'1) holds mid(f1,1,len f1 -'1).k=mid(f,i1,len f-'1).k proof A119: len mid(f,i1,len f)=len f-'i1+1 by A4,A9,A12,FINSEQ_6:118; let k be Nat; assume that A120: 1<=k and A121: k<=len mid(f,i1,len f-'1); k<=len f-'i1 by A12,A32,A121,XREAL_1:233; then A122: ki2 holds L~g is_S-P_arc_joining f/.i1,f/.i2 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part<_of f,i1,i2 and A2: i1>i2; reconsider P=L~g as Subset of TOP-REAL 2; reconsider p2=f/.i2,p1=f/.i1 as Point of TOP-REAL 2; L~Rev g is_S-P_arc_joining f/.i2,f/.i1 by A1,A2,Th30,Th44; then P is_S-P_arc_joining p2,p1 by SPPOL_2:22; hence thesis by SPPOL_2:49; end; theorem Th46: for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part>_of f ,i1,i2 & i1<>i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part>_of f,i1,i2 and A2: i1<>i2; now per cases; case i1=i2; then i1>i2 by A2,XXREAL_0:1; hence thesis by A1,Lm1; end; end; hence thesis; end; theorem Th47: for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part<_of f ,i1,i2 & i1<>i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part<_of f,i1,i2 and A2: i1<>i2; now per cases; case A3: i1>i2; reconsider P=L~g as Subset of TOP-REAL 2; reconsider p2=f/.i2,p1=f/.i1 as Point of TOP-REAL 2; L~Rev g is_S-P_arc_joining f/.i2,f/.i1 by A1,A3,Th30,Th44; then P is_S-P_arc_joining p2,p1 by SPPOL_2:22; hence thesis by SPPOL_2:49; end; case A4: i1<=i2; reconsider P=L~g as Subset of TOP-REAL 2; reconsider p2=f/.i2,p1=f/.i1 as Point of TOP-REAL 2; i1i2 holds L~g is_S-P_arc_joining f/.i1,f/.i2 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part_of f,i1,i2 and A2: i1<>i2; now per cases by A1,Def4; case g is_a_part>_of f,i1,i2; hence thesis by A2,Th46; end; case g is_a_part<_of f,i1,i2; hence thesis by A2,Th47; end; end; hence thesis; end; theorem for f being non constant standard special_circular_sequence, g being FinSequence of TOP-REAL 2,i1,i2 being Element of NAT st g is_a_part_of f,i1,i2 & g.1<>g.len g holds L~g is_S-P_arc_joining f/.i1,f/.i2 proof let f be non constant standard special_circular_sequence, g be FinSequence of TOP-REAL 2,i1,i2 be Element of NAT; assume that A1: g is_a_part_of f,i1,i2 and A2: g.1<>g.len g; now per cases by A1,Def4; case A3: g is_a_part>_of f,i1,i2; then i1+1<=len f by Def2; then A4: i1+1-1<=len f-1 by XREAL_1:9; A5: 1<=i1 by A3,Def2; A6: 1<=len g by A3,Def2; len gi2 holds ex g1,g2 being FinSequence of TOP-REAL 2 st g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f & L~g1 is_S-P_arc_joining f/.i1,f/.i2 & L~g2 is_S-P_arc_joining f/.i1,f/.i2 & for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds g=g1 or g=g2 proof let f be non constant standard special_circular_sequence, i1,i2 be Element of NAT; assume that A1: 1<=i1 and A2: i1+1<=len f and A3: 1<=i2 and A4: i2+1<=len f and A5: i1<>i2; now per cases; case A6: i1<=i2; set h1=mid(f,i1,i2),h2=mid(f,i1,1)^mid(f,len f-'1,i2); A7: i2_of f,i1,i2 by A1,A6,Th31; then A9: h1 is_a_part_of f,i1,i2 by Def4; A10: i1_of f,i1,i2; hence thesis by A6,Th25; end; case g is_a_part<_of f,i1,i2; hence thesis by A10,Th28; end; end; hence thesis; end; A14: (L~h1) \/ (L~h2)=L~f by A1,A10,A7,Th43; A15: (L~h1)/\(L~h2)={f.i1,f.i2} by A1,A10,A7,Th43; mid(f,i1,1)^mid(f,len f-'1,i2) is_a_part<_of f,i1,i2 by A1,A10,A7,Th34; then A16: h2 is_a_part_of f,i1,i2 by Def4; then L~h2 is_S-P_arc_joining f/.i1,f/.i2 by A5,Th48; hence thesis by A9,A16,A15,A14,A11,A12; end; case A17: i1>i2; set h1=mid(f,i2,i1),h2=mid(f,i2,1)^mid(f,len f-'1,i1); set h3=Rev h1,h4=Rev h2; A18: L~h1=L~h3 by SPPOL_2:22; A19: for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds g=h3 or g=h4 proof let g be FinSequence of TOP-REAL 2; assume A20: g is_a_part_of f,i1,i2; now per cases by A20,Def4; case g is_a_part>_of f,i1,i2; then Rev g is_a_part<_of f,i2,i1 by Th29; then Rev g= mid(f,i2,1)^mid(f,len f-'1,i1) by A17,Th28; hence thesis; end; case g is_a_part<_of f,i1,i2; then Rev g is_a_part>_of f,i2,i1 by Th30; then Rev g= mid(f,i2,i1) by A17,Th25; hence thesis; end; end; hence thesis; end; A21: i1_of f,i2,i1 by A3,A17,Th31; then A22: L~h3 is_S-P_arc_joining f/.i1,f/.i2 by A17,Th29,Th47; (L~h1) \/ (L~h2)=L~f by A3,A17,A21,Th43; then A23: (L~h3) \/ (L~h4)=L~f by A18,SPPOL_2:22; (L~h1)/\(L~h2)={f.i2,f.i1} by A3,A17,A21,Th43; then A24: (L~h3)/\(L~h4)={f.i1,f.i2} by A18,SPPOL_2:22; Rev mid(f,i2,i1) is_a_part<_of f,i1,i2 by A3,A17,A21,Th29,Th31; then A25: h3 is_a_part_of f,i1,i2 by Def4; Rev (mid(f,i2,1)^mid(f,len f-'1,i1)) is_a_part>_of f,i1,i2 by A3,A17,A21 ,Th30,Th34; then A26: h4 is_a_part_of f,i1,i2 by Def4; then L~h4 is_S-P_arc_joining f/.i1,f/.i2 by A5,Th48; hence thesis by A25,A26,A24,A23,A22,A19; end; end; hence thesis; end; reserve g, g1, g2 for FinSequence of TOP-REAL 2; theorem for f being non constant standard special_circular_sequence, P being non empty Subset of TOP-REAL 2 st P = L~f holds P is being_simple_closed_curve proof set i1=1,i2=1+1; let f be non constant standard special_circular_sequence, P be non empty Subset of TOP-REAL 2 such that A1: P = L~f; A2: 1+1f/.i2 by GOBOARD7:36; 1+1+1<=len f by GOBOARD7:34,XXREAL_0:2; then consider g1,g2 being FinSequence of TOP-REAL 2 such that g1 is_a_part_of f,i1,i2 and g2 is_a_part_of f,i1,i2 and A4: (L~g1)/\(L~g2)={f.i1,f.i2} and A5: (L~g1) \/ (L~g2)=L~f and A6: L~g1 is_S-P_arc_joining f/.i1,f/.i2 and A7: L~g2 is_S-P_arc_joining f/.i1,f/.i2 and for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds g= g1 or g=g2 by A2,Th50; reconsider L1 = L~g1, L2 = L~g2 as non empty Subset of TOP-REAL 2 by A4; A8: L2 is_an_arc_of f/.i1,f/.i2 by A7,TOPREAL4:2; 1<=len f by GOBOARD7:34,XXREAL_0:2; then A9: f.i1=f/.i1 by FINSEQ_4:15; then f/.i1 in (L~g1)/\(L~g2) by A4,TARSKI:def 2; then f/.i1 in (L~g1) by XBOOLE_0:def 4; then A10: f/.i1 in P by A1,A5,XBOOLE_0:def 3; A11: f.i2=f/.i2 by A2,FINSEQ_4:15; then f/.i2 in (L~g1)/\(L~g2) by A4,TARSKI:def 2; then f/.i2 in (L~g2) by XBOOLE_0:def 4; then A12: f/.i2 in P by A1,A5,XBOOLE_0:def 3; L1 is_an_arc_of f/.i1,f/.i2 by A6,TOPREAL4:2; hence thesis by A1,A4,A5,A8,A9,A11,A3,A10,A12,TOPREAL2:6; end; theorem Th52: for f being non constant standard special_circular_sequence, g1, g2 st g1 is_a_part>_of f,i1,i2 & g2 is_a_part>_of f,i1,i2 holds g1=g2 proof let f be non constant standard special_circular_sequence, g1,g2; assume that A1: g1 is_a_part>_of f,i1,i2 and A2: g2 is_a_part>_of f,i1,i2; now per cases; case A3: i1<=i2; then g1=mid(f,i1,i2) by A1,Th25; hence thesis by A2,A3,Th25; end; case A4: i1>i2; then g1=mid(f,i1,len f-'1)^mid(f,1,i2) by A1,Th26; hence thesis by A2,A4,Th26; end; end; hence thesis; end; theorem Th53: for f being non constant standard special_circular_sequence, g1, g2 st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds g1=g2 proof let f be non constant standard special_circular_sequence, g1,g2; assume that A1: g1 is_a_part<_of f,i1,i2 and A2: g2 is_a_part<_of f,i1,i2; per cases; suppose A3: i1>=i2; then g1=mid(f,i1,i2) by A1,Th27; hence thesis by A2,A3,Th27; end; suppose A4: i1i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds g1.2<> g2.2 proof let f be non constant standard special_circular_sequence, g1,g2; assume that A1: i1<>i2 and A2: g1 is_a_part>_of f,i1,i2 and A3: g2 is_a_part<_of f,i1,i2; A4: 1<=i1 by A2,Def2; A5: i2+1<=len f by A2,Def2; then A6: i2i1-'1; A31: 1f/.(i1+1) by A32,A33,GOBOARD7:37; hence thesis by A9,A22,A26,A34,A31,FINSEQ_4:15; end; case A35: i1+1<>len f; A36: 1<=i1-'1 by A23,NAT_D:39; i1-'1f/.(i1+1) by A36,A37,GOBOARD7:36; hence thesis by A9,A22,A26,A38,A39,FINSEQ_4:15; end; end; hence thesis; end; case A40: 1=i1; len f>4 by GOBOARD7:34; then len f-1>3+1-1 by XREAL_1:9; then i1+1f/.(len f-'1) by A12,A7,A40,GOBOARD7:37; i1+1<=i2 by A15,NAT_1:13; then 1+i1-i1<=i2-i1 by XREAL_1:9; then 1<=i2-'i1 by NAT_D:39; then 1+1<=i2-'i1+1 by XREAL_1:6; then A42: 2<=len mid(f,i1,i2) by A4,A8,A6,A10,A15,FINSEQ_6:118; A43: f.(len f-'1)=f/.(len f-'1) by A12,A7,A17,FINSEQ_4:15; A44: len mid(f,i1,1)=i1-'1+1 by A4,A10,Th9 .=0+1 by A40,XREAL_1:232 .=1; i2+1+1<=len f+1 by A5,XREAL_1:6; then A45: 1+i2+1-i2<=len f+1-i2 by XREAL_1:9; A46: len mid(f,i1,1)=i1-'1+1 by A4,A10,Th9 .=0+1 by A40,XREAL_1:232 .=1; len g2=len f+i1-'i2 by A3,A15,Th28 .=len f+1-i2 by A6,A40,NAT_D:37; then A47: g2 .2 =mid(f,len f-'1,i2).(2-len mid(f,i1,1)) by A18,A44,A45,FINSEQ_6:108 .=f.(len f-'1) by A8,A12,A7,A6,A17,A46,FINSEQ_6:118; A48: 1i2; then i2+1<=i1 by NAT_1:13; then 1+i2-i2<=i1-i2 by XREAL_1:9; then 1<=i1-'i2 by NAT_D:39; then 1+1<=i1-'i2+1 by XREAL_1:6; then A50: 2<=len mid(f,i1,i2) by A4,A8,A6,A10,A49,FINSEQ_6:118; 1i1-'1; A71: 1f/.(i1+1) by A72,A73,GOBOARD7:37; hence thesis by A9,A59,A52,A74,A71,FINSEQ_4:15; end; case A75: i1+1<>len f; A76: 1<=i1-'1 by A53,NAT_D:39; i1-'1f/.(i1+1) by A76,A77,GOBOARD7:36; hence thesis by A9,A59,A52,A78,A79,FINSEQ_4:15; end; end; hence thesis; end; end; hence thesis; end; theorem Th55: for f being non constant standard special_circular_sequence, g1, g2 st i1<>i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1.2=g2.2 holds g1=g2 proof let f be non constant standard special_circular_sequence, g1,g2; assume that A1: i1<>i2 and A2: g1 is_a_part_of f,i1,i2 and A3: g2 is_a_part_of f,i1,i2 and A4: g1.2=g2.2; per cases by A2,Def4; suppose A5: g1 is_a_part>_of f,i1,i2; now per cases by A3,Def4; case g2 is_a_part>_of f,i1,i2; hence thesis by A5,Th52; end; case g2 is_a_part<_of f,i1,i2; hence contradiction by A1,A4,A5,Th54; end; end; hence thesis; end; suppose A6: g1 is_a_part<_of f,i1,i2; now per cases by A3,Def4; case g2 is_a_part>_of f,i1,i2; hence contradiction by A1,A4,A6,Th54; end; case g2 is_a_part<_of f,i1,i2; hence thesis by A6,Th53; end; end; hence thesis; end; end; definition let f be non constant standard special_circular_sequence, i1,i2 be Element of NAT; assume that A1: 1<=i1 and A2: i1+1<=len f and A3: 1<=i2 and A4: i2+1<=len f and A5: i1<>i2; func Lower (f,i1,i2) -> FinSequence of TOP-REAL 2 means it is_a_part_of f,i1 ,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2 implies it.2=f.(i1+1) )& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2 implies it.2=f.S_Drop( i1-'1,f)); correctness proof A6: i1+1-1<=len f-1 by A2,XREAL_1:9; A7: i1-'1=i1-1 by A1,XREAL_1:233; A8: i2+1-1<=len f-1 by A4,XREAL_1:9; A9: i2_of f,i1,i2 by A1,A9,A16,Th31; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+ 1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1)) `2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A18,A20,Def4; end; case A21: (f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2; set g=mid(f,i1,1)^mid(f,len f-'1,i2); A22: len mid(f,i1,1)=i1-'1+1 by A1,A11,Th9; A23: g is_a_part<_of f,i1,i2 by A1,A9,A17,Th34; now per cases; case A24: 1=(f/.i1)`1 & (f/.(i1+ 1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A7,A21,A23,A29,A28,A26,Def4 ,Th22; end; case A30: 1>=i1; then i1=1 by A1,XXREAL_0:1; then A31: i1-'1=0 by XREAL_1:232; A32: S_Drop(i1-'1,f)=S_Drop(i1-'1+(len f-'1),f) by Th23 .=len f-'1 by A15,A31,Th22; A33: 1<=len f-'1-'i2+1 by NAT_1:11; A34: len f-i2>=i2+1-i2 by A4,XREAL_1:9; A35: len mid(f,i1,1)=len mid(f,1,1) by A1,A30,XXREAL_0:1 .=1 by A13,Th15; len mid(f,len f-'1,i2)=len f-'1-'i2+1 by A3,A12,A8,A10,Th9 .=len f-1-i2+1 by A12,A8,XREAL_1:233 .=len f-i2; then 1+1<=len mid(f,i1,1)+len mid(f,len f-'1,i2 ) by A35,A34, XREAL_1:6; then g .2 =mid(f,len f-'1,i2).(2-len mid(f,i1,1)) by A35, FINSEQ_6:108 .=mid(f,len f-'1,i2).(2-(i1-'1+1)) by A1,A11,Th9 .=mid(f,len f-'1,i2).(1+1-(1-'1+1)) by A1,A30,XXREAL_0:1 .=mid(f,len f-'1,i2).(1+1-(0+1)) by XREAL_1:232 .=f.(len f-'1-'1+1) by A3,A12,A8,A10,A33,Th12 .=f.(len f-'1) by A15,XREAL_1:235; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/. (i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+ 1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A21,A23,A32,Def4; end; end; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+ 1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1)) `2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; end; hence ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/. (i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+ 1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; case A36: i1>i2; then i1>1 by A3,XXREAL_0:2; then A37: 1+1<=i1 by NAT_1:13; then A38: 1+1-1<=i1-1 by XREAL_1:9; now per cases; case A39: (f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2; set g=mid(f,i1,i2); A40: i1-1=(f/.i1)`1 & (f/.(i1+1)) `2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A7,A12,A38,A39,A42,A40,Def4 ,Th22; end; case A43: (f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2; set g=mid(f,i1,len f-'1)^mid(f,1,i2); A44: g is_a_part>_of f,i1,i2 by A3,A11,A36,Th33; A45: len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A1,A11,A14,A12,A6,A10, FINSEQ_6:118 .=len f-1-i1+1 by A12,A6,XREAL_1:233 .=len f-i1; now per cases; case i1+1=(f/.i1)`1 & (f/.(i1+ 1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A43,A44,Def4; end; case A47: i1+1>=len f; then i1+1=len f by A2,XXREAL_0:1; then A48: len mid(f,i1,len f-'1)=1 by A14,A12,A10,Th15; len mid(f,1,i2)=i2-'1+1 by A3,A13,A9,FINSEQ_6:118 .=i2-1+1 by A3,XREAL_1:233 .=i2; then 1+1<=len mid(f,i1,len f-'1)+len mid(f,1,i2) by A3,A48,XREAL_1:6; then g.2 =mid(f,1,i2).(2-(i1+1-i1)) by A48,FINSEQ_6:108 .=f.1 by A3,A13,A9,FINSEQ_6:118 .=f/.1 by A13,FINSEQ_4:15 .=f/.len f by FINSEQ_6:def 1 .=f.len f by A13,FINSEQ_4:15; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/. (i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+ 1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A2,A43,A44,A47,Def4, XXREAL_0:1; end; end; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+ 1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1)) `2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; end; hence ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/. (i1+1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+ 1))`2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; end; hence ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+ 1))`2<(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1)) `2>=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); thus thesis by A5,Th55; end; func Upper (f,i1,i2) -> FinSequence of TOP-REAL 2 means it is_a_part_of f,i1 ,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2 implies it.2=f.(i1+1) )& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2 implies it.2=f.S_Drop( i1-'1,f)); correctness proof len f(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2; set g=mid(f,i1,i2); i1+1<=i2 by A60,NAT_1:13; then (1+i1)+1<=i2+1 by XREAL_1:6; then 2+i1-i1<=i2+1-i1 by XREAL_1:9; then A62: 2+i1-i1<=i2-i1+1; len mid(f,i1,i2)=i2-'i1+1 by A1,A3,A54,A51,A59,FINSEQ_6:118; then 2<=len mid(f,i1,i2) by A59,A62,XREAL_1:233; then A63: g.2=f.(2+i1-'1) by A1,A3,A54,A51,A59,FINSEQ_6:118 .=f.(i1+1+1-1) by NAT_D:37 .=f.(i1+1); g is_a_part>_of f,i1,i2 by A1,A51,A59,Th31; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+ 1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1)) `2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A61,A63,Def4; end; case A64: (f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2; set g=mid(f,i1,1)^mid(f,len f-'1,i2); A65: len mid(f,i1,1)=i1-'1+1 by A1,A54,Th9; A66: g is_a_part<_of f,i1,i2 by A1,A51,A60,Th34; now per cases; case A67: 1(f/.i1)`1 or (f/. (i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+ 1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A53,A64,A66,A72,A71,A69,Def4 ,Th22; end; case A73: 1>=i1; then i1=1 by A1,XXREAL_0:1; then A74: i1-'1=0 by XREAL_1:232; A75: S_Drop(i1-'1,f)=S_Drop(i1-'1+(len f-'1),f) by Th23 .=len f-'1 by A58,A74,Th22; A76: 1<=len f-'1-'i2+1 by NAT_1:11; A77: i2+1-1<=len f-1 by A4,XREAL_1:9; A78: len f-i2>=i2+1-i2 by A4,XREAL_1:9; A79: len mid(f,i1,1)=len mid(f,1,1) by A1,A73,XXREAL_0:1 .=1 by A56,Th15; len mid(f,len f-'1,i2)=len f-'1-'i2+1 by A3,A55,A50,A49,Th9 .=len f-1-i2+1 by A55,A50,XREAL_1:233 .=len f-i2; then 1+1<=len mid(f,i1,1)+len mid(f,len f-'1,i2 ) by A79,A78, XREAL_1:6; then g .2 =mid(f,len f-'1,i2).(2-len mid(f,i1,1)) by A79, FINSEQ_6:108 .=mid(f,len f-'1,i2).(2-(i1-'1+1)) by A1,A54,Th9 .=mid(f,len f-'1,i2).(1+1-(1-'1+1)) by A1,A73,XXREAL_0:1 .=mid(f,len f-'1,i2).(1+1-(0+1)) by XREAL_1:232 .=f.(len f-'1-'1+1) by A3,A55,A49,A77,A76,Th12 .=f.(len f-'1) by A58,XREAL_1:235; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/. (i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+ 1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A64,A66,A75,Def4; end; end; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+ 1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1)) `2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; end; hence ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/. (i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+ 1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; case A80: i1>i2; then i1>1 by A3,XXREAL_0:2; then A81: 1+1<=i1 by NAT_1:13; then A82: 1+1-1<=i1-1 by XREAL_1:9; now per cases; case A83: (f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2; set g=mid(f,i1,i2); A84: i1-'1<=len f-'1 by A54,A53,A55,XREAL_1:9; i2+1<=i1 by A80,NAT_1:13; then (1+i2)+1<=i1+1 by XREAL_1:6; then 2+i2-i2<=i1+1-i2 by XREAL_1:9; then A85: 2+i2-i2<=i1-i2+1; len mid(f,i1,i2)=i1-'i2+1 by A1,A3,A54,A51,A80,FINSEQ_6:118; then 2<=len mid(f,i1,i2) by A80,A85,XREAL_1:233; then A86: g.2=f.(i1-'2+1) by A1,A3,A54,A51,A80,FINSEQ_6:118 .=f.(i1-(1+1)+1) by A81,XREAL_1:233 .=f.(i1-1) .=f.(i1-'1) by A1,XREAL_1:233; g is_a_part<_of f,i1,i2 by A3,A54,A80,Th32; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+ 1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1)) `2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A53,A82,A83,A86,A84,Def4,Th22; end; case A87: (f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2; set g=mid(f,i1,len f-'1)^mid(f,1,i2); A88: g is_a_part>_of f,i1,i2 by A3,A54,A80,Th33; A89: len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A1,A54,A57,A55,A52,A49, FINSEQ_6:118 .=len f-1-i1+1 by A55,A52,XREAL_1:233 .=len f-i1; now per cases; case i1+1(f/.i1)`1 or (f/. (i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1)) & ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1 +1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A87,A88,Def4; end; case A91: i1+1>=len f; then i1+1=len f by A2,XXREAL_0:1; then A92: len mid(f,i1,len f-'1)=1 by A57,A55,A49,Th15; len mid(f,1,i2)=i2-'1+1 by A3,A56,A51,FINSEQ_6:118 .=i2-1+1 by A3,XREAL_1:233 .=i2; then 1+1<=len mid(f,i1,len f-'1)+len mid(f,1,i2) by A3,A92, XREAL_1:6; then g.2 =mid(f,1,i2).(2-(i1+1-i1)) by A92,FINSEQ_6:108 .=f.1 by A3,A56,A51,FINSEQ_6:118 .=f/.1 by A56,FINSEQ_4:15 .=f/.len f by FINSEQ_6:def 1 .=f.len f by A56,FINSEQ_4:15; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/. (i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1)) & ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1 +1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)) by A2,A87,A88,A91,Def4, XXREAL_0:1; end; end; hence g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+ 1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1)) `2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; end; hence ex g st g is_a_part_of f,i1,i2 & ((f/.(i1+1))`1>(f/.i1)`1 or (f/. (i1+1))`2>(f/.i1)`2 implies g.2=f.(i1+1))& ((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+ 1))`2<=(f/.i1)`2 implies g.2=f.S_Drop(i1-'1,f)); end; end; hence thesis by A5,Th55; end; end;