Copyright (c) 1997 Association of Mizar Users
environ
vocabulary ARYTM_1, NAT_1, RELAT_1, ARYTM_3, FINSEQ_1, FINSEQ_6, FUNCT_1,
FINSEQ_5, RFINSEQ, EUCLID, TOPREAL1, JORDAN3, SEQM_3, GOBOARD5, TARSKI,
BOOLE, PRE_TOPC, TOPREAL4, TOPREAL2, MCART_1, JORDAN4, FINSEQ_4;
notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, BINARITH, RELAT_1,
FINSEQ_1, FUNCT_1, FINSEQ_4, FINSEQ_5, STRUCT_0, TOPREAL1, TOPREAL2,
TOPREAL4, GOBOARD1, GOBOARD5, PRE_TOPC, EUCLID, FINSEQ_6, RFINSEQ,
JORDAN3;
constructors GOBOARD9, BINARITH, TOPREAL4, TOPREAL2, REAL_1, RFINSEQ, JORDAN3,
FINSEQ_4, MEMBERED;
clusters STRUCT_0, GOBOARD5, RELSET_1, EUCLID, SPPOL_2, XREAL_0, ARYTM_3,
MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
theorems TARSKI, AXIOMS, JORDAN3, TOPREAL4, EUCLID, TOPREAL1, TOPREAL2,
FUNCT_1, SPPOL_1, GOBOARD5, FINSEQ_1, GOBOARD7, NAT_1, SPPOL_2, REAL_1,
BINARITH, REAL_2, SQUARE_1, FINSEQ_3, GR_CY_1, FINSEQ_2, FINSEQ_4,
GOBOARD9, FINSEQ_5, RFINSEQ, FINSEQ_6, ENUMSET1, SCMFSA_7, ZFMISC_1,
TOPREAL3, GROUP_4, AMI_5, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
begin :: Preliminaries
reserve i, i1, i2, i3, j, k, n for Nat,
r, r1, r2, s, s1 for Real;
theorem Th1: n-'i=0 implies n<=i
proof assume A1:n-'i=0;
assume i<n; then i+1<=n by NAT_1:38; then i+1-i<=n-i by REAL_1:49;
then 1<=n-i by XCMPLX_1:26;
then 0<n-i by AXIOMS:22;
hence contradiction by A1,BINARITH:def 3;
end;
theorem Th2:i<=j implies j+k-'i=j+k-i
proof assume i<=j; then i<=j+k by NAT_1:37;
hence thesis by SCMFSA_7:3;
end;
theorem Th3:i<=j implies j+k-'i=j-'i+k
proof assume A1:i<=j; then i<=j+k by NAT_1:37;
hence j+k-'i=j+k-i by SCMFSA_7:3 .=j-i+k by XCMPLX_1:29
.=j-'i+k by A1,SCMFSA_7:3;
end;
theorem Th4:i1<>0 & i2=i3*i1 implies i3<=i2
proof assume A1:i1<>0 & i2=i3*i1; then i1>0 by NAT_1:19;
then i1>=0+1 by NAT_1:38;
then i1-'1+1=i1 by AMI_5:4;
then i2=i3*(i1-'1)+i3*1 by A1,XCMPLX_1:8;
hence i3<=i2 by NAT_1:29;
end;
theorem i1<i2 implies i1 div i2=0
proof assume A1: i1<i2;
now per cases by NAT_1:def 1;
case (ex j1 be Nat st i1=i2*(i1 div i2)+j1 & j1<i2);
then consider j1 be Nat such that A2:i1=i2*(i1 div i2)+j1 & j1<i2;
A3:i1-'j1=i2*(i1 div i2) by A2,BINARITH:39;
now assume i1 div i2<>0;
then A4:i1-'j1>=i2 by A3,Th4;
i1>=i1-'j1 by JORDAN3:13;
hence contradiction by A1,A4,AXIOMS:22;
end;
hence i1 div i2=0;
case (i1 div i2)=0 & i2=0;
hence i1 div i2=0;
end;
hence thesis;
end;
theorem Th6: 0<j & j<i & i<j+j implies i mod j<>0
proof assume A1:0<j & j<i & i<j+j;
assume A2:i mod j=0;
A3:i-j=i-'j by A1,SCMFSA_7:3;
i=i-j+j by XCMPLX_1:27;
then A4:i mod j=(i-'j+j) mod j by A1,SCMFSA_7:3
.=((i-'j)+ (j mod j)) mod j by GR_CY_1:3
.=(i-'j+0)mod j by GR_CY_1:5
.=(i-'j)mod j;
i-j<j+j-j by A1,REAL_1:54;
then i-j<j by XCMPLX_1:26;
then (i-'j) mod j=i-'j by A3,GR_CY_1:4;
hence contradiction by A1,A2,A4,Th1;
end;
theorem Th7: 0<j & j<=i & i<j+j implies i mod j=i-j & i mod j=i-'j
proof assume A1:0<j & j<=i & i<j+j;
then A2:i-j=i-'j by SCMFSA_7:3;
i=i-j+j by XCMPLX_1:27;
then A3:i mod j=(i-'j+j) mod j by A1,SCMFSA_7:3
.=((i-'j)+(j mod j))mod j by GR_CY_1:3
.=((i-'j)+0)mod j by GR_CY_1:5 .=(i-'j)mod j;
i-j<j+j-j by A1,REAL_1:54;
then i-j<j by XCMPLX_1:26;
hence thesis by A2,A3,GR_CY_1:4;
end;
theorem Th8: (j+j)mod j=0
proof thus (j+j)mod j= (2*j) mod j by XCMPLX_1:11
.= 0 by GROUP_4:101;
end;
theorem Th9: 0<k & k<=j & k mod j=0 implies k=j
proof assume A1:0<k & k<=j & k mod j=0;
then k >= j by GR_CY_1:4;
hence k=j by A1,REAL_1:def 5;
end;
begin :: Some facts about cutting of finite sequences
reserve D for non empty set,
f1 for FinSequence of D;
canceled 4;
theorem Th14: for f1 st f1 is circular & 1<=len f1 holds f1.1=f1.len f1
proof let f1;assume A1:f1 is circular & 1<=len f1;
then A2:f1/.1=f1/.len f1 by FINSEQ_6:def 1;
f1.1=f1/.1 by A1,FINSEQ_4:24;
hence thesis by A1,A2,FINSEQ_4:24;
end;
theorem for f1,i1,i2 st i1<=i2 holds
(f1|i1)|i2=f1|i1 & (f1|i2)|i1=f1|i1
proof let f1,i1,i2;assume A1:i1<=i2;
len (f1|i1)<=i1 by FINSEQ_5:19;
then len (f1|i1)<=i2 by A1,AXIOMS:22;
hence (f1|i1)|i2=f1|i1 by TOPREAL1:2;
A2:f1|i2=f1|(Seg i2) by TOPREAL1:def 1;
A3:f1|i1=f1|(Seg i1) by TOPREAL1:def 1;
A4:(f1|i2)|i1=(f1|i2)|Seg i1 by TOPREAL1:def 1;
Seg i1 c= Seg i2 by A1,FINSEQ_1:7;
hence thesis by A2,A3,A4,FUNCT_1:82;
end;
theorem Th16: (<*>D)|i=<*>D
proof len (<*>D)=0 by FINSEQ_1:32;
then len (<*>D)<=i by NAT_1:18;
hence thesis by TOPREAL1:2;
end;
theorem Th17: Rev (<*>D)=<*>D
proof len (Rev(<*>D))=len (<*>D) by FINSEQ_5:def 3 .=0 by FINSEQ_1:32;
hence thesis by FINSEQ_1:32;
end;
theorem Th18: for f1,k st k<len f1 holds
(f1/^k).len (f1/^k)=f1.len f1 & (f1/^k)/.len (f1/^k)=f1/.len f1
proof let f1,k;assume A1:k<len f1;
then k+1<=len f1 by NAT_1:38;
then k+1-k<=len f1-k by REAL_1:49;
then A2:1<=len f1-k by XCMPLX_1:26;
0<=k by NAT_1:18;
then A3: 0+1<=len f1 by A1,NAT_1:38;
A4:1<=len (f1/^k) by A1,A2,RFINSEQ:def 2;
then len (f1/^k) in Seg len (f1/^k) by FINSEQ_1:3;
then A5: len (f1/^k) in dom (f1/^k) & k<=len f1 by A1,FINSEQ_1:def 3;
len (f1/^k)+k=len f1-k+k by A1,RFINSEQ:def 2 .=len f1 by XCMPLX_1:27;
hence A6:(f1/^k).len (f1/^k)=f1.len f1 by A5,RFINSEQ:def 2;
(f1/^k)/.len (f1/^k)=(f1/^k).len (f1/^k) by A4,FINSEQ_4:24;
hence thesis by A3,A6,FINSEQ_4:24;
end;
theorem Th19: for g being FinSequence of TOP-REAL 2,i
st g is_S-Seq & i+1<len g holds g/^i is_S-Seq
proof let g be FinSequence of TOP-REAL 2,i;
assume A1:g is_S-Seq & i+1<len g;
A2:1<=i+1 by NAT_1:29;
then A3:1<len g by A1,AXIOMS:22;
mid(g,i+1,len g)=g/^(i+1-'1) by A1,JORDAN3:26
.=g/^i by BINARITH:39;
hence thesis by A1,A2,A3,JORDAN3:39;
end;
theorem Th20: for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1
holds len mid(f1,i2,i1)=i1-'i2+1
proof let f1,i1,i2;assume A1:1<= i2 & i2<=i1 & i1<= len f1;
then A2:1<=i1 by AXIOMS:22;
i2<=len f1 by A1,AXIOMS:22;
hence thesis by A1,A2,JORDAN3:27;
end;
theorem Th21: for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1
holds len mid(f1,i1,i2)=i1-'i2+1
proof let f1,i1,i2;assume A1:1<= i2 & i2<=i1 & i1<= len f1;
per cases by A1,REAL_1:def 5;
suppose i1=i2;
hence len mid(f1,i1,i2)=i1-'i2+1 by A1,JORDAN3:27;
suppose A2:i2<i1; A3:1<=i1 by A1,AXIOMS:22;
i2<=len f1 by A1,AXIOMS:22;
hence len mid(f1,i1,i2)=i1-'i2+1 by A1,A2,A3,JORDAN3:27;
end;
theorem Th22: for f1,i1,i2,j st 1<=i1 & i1<=i2 & i2<=len f1
holds mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2
proof let f1,i1,i2,j;assume A1:1<=i1 & i1<=i2 & i2<=len f1;
then A2:1<=i2 by AXIOMS:22;
A3:i1<=len f1 by A1,AXIOMS:22;
then len mid(f1,i1,i2)=i2-'i1+1 by A1,A2,JORDAN3:27;
then 1<=len mid(f1,i1,i2) by NAT_1:29;
then A4:mid(f1,i1,i2).(len mid(f1,i1,i2))
=f1.(len mid(f1,i1,i2)+i1-'1) by A1,A2,A3,JORDAN3:27
.=f1.(i2-'i1+1+i1-'1) by A1,A2,A3,JORDAN3:27;
i2-'i1+1+i1=i2-i1+1+i1 by A1,SCMFSA_7:3 .=i2+1 by XCMPLX_1:227;
hence thesis by A4,BINARITH:39;
end;
theorem Th23: for f1,i1,i2,j st 1<=i1 & i1<=len f1 & 1<=i2 & i2<=len f1
holds mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2
proof let f1,i1,i2,j;assume A1:1<=i1 & i1<=len f1 & 1<=i2 & i2<=len f1;
per cases;
suppose i1<=i2;
hence mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2 by A1,Th22;
suppose A2:i1>i2;
then len mid(f1,i1,i2)=i1-'i2+1 by A1,JORDAN3:27;
then 1<=len mid(f1,i1,i2) by NAT_1:29;
then A3:mid(f1,i1,i2).(len mid(f1,i1,i2))
=f1.(i1-'len mid(f1,i1,i2)+1) by A1,A2,JORDAN3:27
.=f1.(i1-'(i1-'i2+1)+1) by A1,A2,JORDAN3:27;
0<=i2-1 by A1,SQUARE_1:12;
then i1-0>=i1-(i2-1) by REAL_2:106;
then i1>=i1-i2+1 by XCMPLX_1:37;
then i1-'i2+1<=i1 by A2,SCMFSA_7:3;
then i1-'(i1-'i2+1)+1=i1-(i1-'i2+1)+1 by SCMFSA_7:3
.=i1-(i1-'i2)-1+1 by XCMPLX_1:36
.=i1-(i1-'i2) by XCMPLX_1:27
.=i1-(i1-i2) by A2,SCMFSA_7:3
.=i2 by XCMPLX_1:18;
hence thesis by A3;
end;
theorem Th24: 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
A1:1<= i2 & i2<=i1 & i1<= len f1 & 1<=j
& j<=i1-'i2+1;
then A2:j<=len mid(f1,i1,i2) by Th21;
per cases by A1,REAL_1:def 5;
suppose A3:i1=i2;
then A4: i1-'i2+1=0+1 by GOBOARD9:1 .=1;
then j+i1-'1=1+i1-'1 by A1,AXIOMS:21
.=1+i1-1 by Th2 .=i1-1+1 by XCMPLX_1:29
.=i1-'1+1 by A1,A3,SCMFSA_7:3 .=i1-'j+1 by A1,A4,AXIOMS:21;
hence mid(f1,i1,i2).j=f1.(i1-'j+1) by A1,A2,A3,JORDAN3:27;
suppose A5:i2<i1; A6:1<=i1 by A1,AXIOMS:22;
i2<=len f1 by A1,AXIOMS:22;
hence mid(f1,i1,i2).j=f1.(i1-'j+1) by A1,A2,A5,A6,JORDAN3:27;
end;
theorem Th25:for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j & j<=i1-'i2+1
holds mid(f1,i1,i2).j=mid(f1,i2,i1).(i1-i2+1-j+1)
& i1-i2+1-j+1=i1-'i2+1-'j+1
proof let f1,i1,i2;assume A1: 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j & j<=i1-'i2+1;
then A2:1<=i1 by AXIOMS:22;
A3:i2<=len f1 by A1,AXIOMS:22;
j-j<=i1-'i2+1-j by A1,REAL_1:49;
then 0<=i1-'i2+1-j by XCMPLX_1:14;
then A4:i1-'i2+1-j=i1-'i2+1-'j by BINARITH:def 3;
1-j<=j-j by A1,REAL_1:49;
then 1-j<=0 by XCMPLX_1:14;
then i1-'i2+(1-j)<=i1-'i2+0 by REAL_1:55;
then i1-'i2+1-'j<=i1-'i2 by A4,XCMPLX_1:29;
then A5:i1-'i2+1-'j+1<=i1-'i2+1 by AXIOMS:24;
i1-'i2+1=i1-i2+1 by A1,SCMFSA_7:3;
then A6:i1-'i2+1=i1-(i2-1) by XCMPLX_1:37;
i2-1>=0 by A1,SQUARE_1:12;
then i1-(i2-1)<=i1-0 by REAL_2:106;
then A7: j<=i1 by A1,A6,AXIOMS:22;
A8:(i1-'i2+1-'j+1)
=i1-'i2+1-j+1 by A1,SCMFSA_7:3
.=i1-i2+1-j+1 by A1,SCMFSA_7:3;
A9:1<=(i1-'i2+1-'j+1) by NAT_1:29;
now per cases by A1,REAL_1:def 5;
case A10:i1>i2;
len mid(f1,i2,i1)=i1-'i2+1 by A1,A2,A3,JORDAN3:27;
then A11:mid(f1,i2,i1).(i1-'i2+1-'j+1)=f1.((i1-'i2+1-'j+1)+i2-'1)
by A1,A2,A3,A5,A9,JORDAN3:27;
A12:(i1-'i2+1-'j+1)+i2-'1
=(i1-'i2+1-'j+1)+i2-1 by A1,Th2
.=i1-i2+1-j+i2 by A8,XCMPLX_1:226
.=i1-i2+(1-j)+i2 by XCMPLX_1:29
.=i1+(1-j) by XCMPLX_1:227
.=i1+1-j by XCMPLX_1:29 .=i1-j+1 by XCMPLX_1:29
.=i1-'j+1 by A7,SCMFSA_7:3;
len mid(f1,i1,i2)=i1-'i2+1 by A1,A2,A3,A10,JORDAN3:27;
hence mid(f1,i1,i2).j=mid(f1,i2,i1).(i1-i2+1-j+1)
& i1-i2+1-j+1=i1-'i2+1-'j+1 by A1,A2,A3,A8,A10,A11,A12,JORDAN3:27;
case A13:i1=i2;
then A14: i1-'i2+1=0+1 by GOBOARD9:1 .=1;
then j=1 by A1,AXIOMS:21;
then i1-i2+1-j+1=0+1-1+1 by A13,XCMPLX_1:14 .=1;
hence mid(f1,i1,i2).j=mid(f1,i2,i1).(i1-i2+1-j+1)
& i1-i2+1-j+1=i1-'i2+1-'j+1 by A1,A8,A13,A14,AXIOMS:21;
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 A1:1<=i1 & i1<=i2 & i2<=len f1 & 1<=j & j<=i2-'i1+1;
set k=i2-'i1+1-'j+1;
A2:1<=k by NAT_1:29;
j-1>=0 by A1,SQUARE_1:12;
then A3: k+0<=k+(j-1) by REAL_1:55;
i2-'i1+1-j=i2-'i1+1-'j by A1,SCMFSA_7:3;
then A4: i2-'i1+1-'j+1+(j-1)=i2-'i1+1-(j-1)+(j-1) by XCMPLX_1:37
.=i2-'i1+1 by XCMPLX_1:27;
A5:i2-i1+1-j+1=i2-'i1+1-j+1 by A1,SCMFSA_7:3
.=i2-'i1+1-'j+1 by A1,SCMFSA_7:3;
then i2-i1+1-k+1=i2-i1+1-((i2-i1+1)-(j-1))+1 by XCMPLX_1:37
.=j-1+1 by XCMPLX_1:18
.=j by XCMPLX_1:27;
hence thesis by A1,A2,A3,A4,A5,Th25;
end;
theorem Th27: 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 A1:1<=k & k<=len f1;
A2:len (f1/^(k-'1))=len f1-'(k-'1) by JORDAN3:19;
k-'1+1=k by A1,AMI_5:4;
then A3:(f1/^(k-'1)).1=f1.k by A1,JORDAN3:23;
A4:f1/.k=f1.k by A1,FINSEQ_4:24;
k-'1+1<=len f1 by A1,AMI_5:4;
then k-'1+1-(k-'1)<=len f1-(k-'1) by REAL_1:49;
then 1<=len f1-(k-'1) by XCMPLX_1:26;
then A5:1<=1 & 1<=len (f1/^(k-'1)) by A2,JORDAN3:1;
then 0<len (f1/^(k-'1)) by AXIOMS:22;
then A6:f1/^(k-'1) is non empty by FINSEQ_1:25;
k-'k+1=k-k+1 by SCMFSA_7:3 .=1 by XCMPLX_1:25;
then mid(f1,k,k)=(f1/^(k-'1))|1 by JORDAN3:def 1
.=<*(f1/^(k-'1))/.1*> by A6,FINSEQ_5:23;
hence thesis by A3,A4,A5,FINSEQ_1:56,FINSEQ_4:24;
end;
theorem Th28: mid(f1,0,0)=f1|1
proof
0-'0+1=0-0+1 by SCMFSA_7:3 .=1;
then A1:mid(f1,0,0)=(f1/^(0-'1))|1 by JORDAN3:def 1; 0-1<0;
then 0-'1=0 by BINARITH:def 3;
hence thesis by A1,FINSEQ_5:31;
end;
theorem Th29: for f1,k st len f1<k
holds mid(f1,k,k)=<*>D
proof let f1,k;assume A1:len f1<k;
0<=len f1 by NAT_1:18;
then A2: 0+1<=k by A1,NAT_1:38;
k-'k+1=k-k+1 by SCMFSA_7:3 .=1 by XCMPLX_1:25;
then A3:mid(f1,k,k)=(f1/^(k-'1))|1 by JORDAN3:def 1;
len f1+1<=k by A1,NAT_1:38;
then len f1+1-1<=k-1 by REAL_1:49;
then len f1<=k-1 by XCMPLX_1:26;
then len f1<=k-'1 by A2,SCMFSA_7:3;
then f1/^(k-'1)=<*>D by FINSEQ_5:35;
hence thesis by A3,Th16;
end;
theorem Th30: for f1,i1,i2 holds mid(f1,i1,i2)=Rev mid(f1,i2,i1)
proof let f1; let k1,k2 be Nat;
now per cases;
case A1:k1<=k2;
then A2:mid(f1,k1,k2)=(f1/^(k1-'1))|(k2-'k1+1)
by JORDAN3:def 1;
now per cases by A1,REAL_1:def 5;
case k1<k2;
then mid(f1,k2,k1)=Rev mid(f1,k1,k2) by A2,JORDAN3:def 1;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1) by FINSEQ_6:29;
case A3:k1=k2;
k1=0 or k1>0 by NAT_1:19;
then A4: k1=0 or 0+1<=k1 by NAT_1:38;
now per cases by A4;
case k1=0;
then A5:mid(f1,k1,k2)=f1|1 by A3,Th28;
now per cases;
case len f1=0; then f1=<*>D by FINSEQ_1:32;
then f1|1=<*>D by Th16;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1) by A3,A5,Th17;
case len f1<>0;
then f1 <> <*>D by FINSEQ_1:32;
then f1|1=<*f1/.1*> by FINSEQ_5:23;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1)
by A3,A5,FINSEQ_5:63;
end;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1);
case 1<=k1 & k1<= len f1;
then mid(f1,k1,k1)=<*f1/.k1*> by Th27;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1) by A3,FINSEQ_5:63;
case len f1<k1; then mid(f1,k1,k1)=<*>D by Th29;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1) by A3,Th17;
end;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1);
end;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1);
case A6:k1>k2;
then mid(f1,k1,k2)=Rev ((f1/^(k2-'1))|(k1-'k2+1)) by JORDAN3:def 1;
hence mid(f1,k1,k2)=Rev mid(f1,k2,k1) by A6,JORDAN3:def 1;
end;
hence thesis;
end;
theorem Th31: for f being FinSequence of TOP-REAL 2,i1,i2,i
st 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1
holds LSeg(mid(f,i1,i2),i)=LSeg(f,i+i1-'1)
proof let f be FinSequence of TOP-REAL 2,i1,i2,i;
assume A1: 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1;
then A2: i<len mid(f,i1,i2) by Th20;
then A3:i+1<=len mid(f,i1,i2) by NAT_1:38;
i2-i1+1=i2-'i1+1 by A1,SCMFSA_7:3;
then i+i1<i2-i1+1+i1 by A1,REAL_1:53;
then i+i1<i2+1 by XCMPLX_1:227;
then i+i1+1<=i2+1 by NAT_1:38;
then i+i1+1-1<=i2+1-1 by REAL_1:49;
then i+i1-1+1<=i2+1-1 by XCMPLX_1:29;
then i+i1-1+1<=i2 by XCMPLX_1:26;
then A4: i+i1-1+1<=len f by A1,AXIOMS:22;
1+1<=i+i1 by A1,REAL_1:55;
then 1+1-1<=i+i1-1 by REAL_1:49;
then A5:1<=i+i1-'1 & i+i1-'1+1<=len f by A1,A4,Th2;
then A6:LSeg(f,i+i1-'1)=LSeg(f/.(i+i1-'1),f/.(i+i1-'1+1)) by TOPREAL1:def 5;
A7:1<=i & i+1<=len mid(f,i1,i2) by A1,A2,NAT_1:38;
A8:1<i+i1-'1+1 by A5,NAT_1:38;
A9:i+i1-'1<len f by A5,NAT_1:38;
A10:i+i1-'1+1<=len f by A1,A4,Th2;
A11:i+i1-'1+1=i+i1-1+1 by A1,Th2 .=i+i1 by XCMPLX_1:27 .=i+1-1+i1 by XCMPLX_1
:26
.=i+1+i1-1 by XCMPLX_1:29 .=i+1+i1-'1 by A1,Th2;
A12:mid(f,i1,i2)/.i=mid(f,i1,i2).i by A1,A2,FINSEQ_4:24
.=f.(i+i1-'1) by A1,JORDAN3:31
.=f/.(i+i1-'1) by A5,A9,FINSEQ_4:24;
A13:i+1<=i2-'i1+1 by A1,NAT_1:38;
A14:1<=1+i by NAT_1:29;
then mid(f,i1,i2)/.(i+1)=mid(f,i1,i2).(i+1) by A7,FINSEQ_4:24
.=f.(i+1+i1-'1) by A1,A13,A14,JORDAN3:31
.=f/.(i+1+i1-'1) by A8,A10,A11,FINSEQ_4:24;
hence thesis by A1,A3,A6,A11,A12,TOPREAL1:def 5;
end;
theorem Th32: for f being FinSequence of TOP-REAL 2,i1,i2,i
st 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1
holds LSeg(mid(f,i2,i1),i)=LSeg(f,i2-'i)
proof let f be FinSequence of TOP-REAL 2,i1,i2,i;
assume A1: 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1;
then A2:len mid(f,i2,i1)=i2-'i1+1 by Th21;
A3:i<len mid(f,i2,i1) by A1,Th21;
A4:i+(len mid(f,i2,i1)-'i)
=len mid(f,i2,i1) by A1,A2,AMI_5:4;
i+1<=len mid(f,i2,i1) by A3,NAT_1:38;
then i+1-i<=len mid(f,i2,i1)-i by REAL_1:49;
then A5: 1<=len mid(f,i2,i1)-i by XCMPLX_1:26;
len mid(f,i2,i1)+1<=len mid(f,i2,i1)+i by A1,AXIOMS:24;
then len mid(f,i2,i1)<len mid(f,i2,i1)+i by NAT_1:38;
then len mid(f,i2,i1)-i<len mid(f,i2,i1)+i-i by REAL_1:54;
then len mid(f,i2,i1)-i<len mid(f,i2,i1) by XCMPLX_1:26;
then A6:1<=len mid(f,i2,i1)-'i & len mid(f,i2,i1)-'i<i2-'i1+1
by A2,A5,JORDAN3:1;
i2<=i2+(i1-'1) by NAT_1:29;
then i2<=i2+(i1-1) by A1,SCMFSA_7:3;
then i2-(i1-1)<=i2+(i1-1)-(i1-1) by REAL_1:49;
then i2-(i1-1)<=i2 by XCMPLX_1:26;
then i2-i1+1<=i2 by XCMPLX_1:37;
then i2-'i1+1<=i2 by A1,SCMFSA_7:3;
then A7:i<i2 by A1,AXIOMS:22;
A8:i2-'i1+1-'i+i1-'1
=i2-'i1+1-'i+i1-1 by A1,Th2
.=i2-'i1+1-i+i1-1 by A1,SCMFSA_7:3
.=i2-'i1+1-i-1+i1 by XCMPLX_1:29
.=i2-'i1-i+i1 by XCMPLX_1:228
.=i2-i1-i+i1 by A1,SCMFSA_7:3
.=i2-i by XCMPLX_1:229
.=i2-'i by A7,SCMFSA_7:3;
thus LSeg(mid(f,i2,i1),i)
=LSeg(Rev mid(f,i2,i1),len mid(f,i2,i1)-'i) by A4,SPPOL_2:2
.=LSeg(mid(f,i1,i2),len mid(f,i2,i1)-'i) by Th30
.=LSeg(f,len mid(f,i2,i1)-'i+i1-'1) by A1,A6,Th31
.=LSeg(f,i2-'i) by A1,A8,Th21;
end;
begin :: Dividing of special circular sequences into parts
definition let n be Nat, f be FinSequence;
func S_Drop(n,f) -> Nat equals
:Def1: (n mod (len f -'1)) if n mod (len f -'1)<>0
otherwise len f -'1;
correctness;
end;
theorem Th33: 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 GR_CY_1:5;
hence thesis by Def1;
end;
theorem Th34: for n being Nat, f being FinSequence
st 1<=n & n<=len f-'1 holds S_Drop(n,f)=n
proof let n be Nat,f be FinSequence;
assume A1: 1<=n & n<=len f-'1;
then A2:n<>0;
per cases by A1,REAL_1:def 5;
suppose n<len f-'1;
then n mod (len f-'1)=n by GR_CY_1:4;
hence thesis by A2,Def1;
suppose n=len f-'1;
hence thesis by Th33;
end;
theorem Th35: for n being Nat,f being FinSequence holds
S_Drop(n,f)=S_Drop(n+(len f-'1),f) &
S_Drop(n,f)=S_Drop(len f-'1+n,f)
proof let n be Nat,f be FinSequence;
A1:(n+(len f-'1))mod (len f-'1)
= (n+(len f-'1)*1)mod (len f-'1)
.=n mod (len f-'1) by GR_CY_1:1;
per cases;
suppose A2:n mod (len f-'1)<>0;
then S_Drop(n,f)=n mod (len f-'1) by Def1;
hence thesis by A1,A2,Def1;
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;
definition let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be 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<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f));
end;
definition let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part<_of f,i1,i2 means
:Def3: 1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f));
end;
definition let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part_of f,i1,i2 means
:Def4: g is_a_part>_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 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<len f &
((for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))or
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f)))
proof let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;assume
A1: g is_a_part_of f,i1,i2;
now per cases by A1,Def4;
case g is_a_part>_of f,i1,i2;
hence
1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
((for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))or
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f)))
by Def2;
case g is_a_part<_of f,i1,i2;
hence
1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
((for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))or
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f)))
by Def3;
end;
hence thesis;
end;
theorem Th37:for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being 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 Nat;
assume A1:g is_a_part>_of f,i1,i2 & i1<=i2;
then A2:1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))
by Def2;
then i1+1-1<=len f-1 by REAL_1:49;
then A3:i1<=len f-1 by XCMPLX_1:26;
then 1<=len f-1 by A2,AXIOMS:22;
then A4:len f-1=len f-'1 by JORDAN3:1;
then A5:0<>len f-'1 by A2,A3,AXIOMS:22;
i1<=i1+1 by NAT_1:29; then A6:i1<=len f by A2,AXIOMS:22;
i2<=i2+1 by NAT_1:29; then A7:i2<=len f by A2,AXIOMS:22;
A8:f.i2=f.S_Drop((i1+len g)-'1,f) by A2;
A9: now per cases;
case A10:(i1+len g)-'1 mod (len f -'1)<>0;
then 0<(i1+len g)-'1 mod (len f -'1) by NAT_1:19;
then 0+1<=(i1+len g)-'1 mod (len f -'1) by NAT_1:38;
hence 1<=S_Drop((i1+len g)-'1,f) by A10,Def1;
case (i1+len g)-'1 mod (len f -'1)=0;
then A11:S_Drop((i1+len g)-'1,f)=len f -'1 by Def1;
i1<=len f -'1 by A2,JORDAN3:12;
hence 1<=S_Drop((i1+len g)-'1,f) by A2,A11,AXIOMS:22;
end;
A12: now per cases;
case (i1+len g)-'1 mod (len f -'1)<>0;
then A13:S_Drop((i1+len g)-'1,f)=((i1+len g)-'1 mod (len f -'1)) by
Def1;
A14: i1<=len f -'1 by A2,JORDAN3:12;
then A15:1<=len f -'1 by A2,AXIOMS:22;
0<len f -'1 by A2,A14,AXIOMS:22;
then A16:((i1+len g)-'1 mod (len f -'1)) <len f-'1 by NAT_1:46;
len f -'1<len f by A15,JORDAN3:14;
hence S_Drop((i1+len g)-'1,f)< len f by A13,A16,AXIOMS:22;
case (i1+len g)-'1 mod (len f -'1)=0;
then A17:S_Drop((i1+len g)-'1,f)=len f -'1 by Def1;
i1<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
hence S_Drop((i1+len g)-'1,f)< len f by A17,JORDAN3:14;
end;
A18:i2<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
then len f -'1<len f by JORDAN3:14;
then A19:i2<len f by A18,AXIOMS:22;
now per cases by REAL_1:def 5;
case A20:i2<S_Drop((i1+len g)-'1,f);
then A21:f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A2,A12,GOBOARD7:38;
i2<=len f by A2,JORDAN3:9;
then A22:f/.i2=f.i2 by A2,FINSEQ_4:24;
1<=S_Drop((i1+len g)-'1,f) by A2,A20,AXIOMS:22;
hence contradiction by A8,A12,A21,A22,FINSEQ_4:24;
case i2>S_Drop((i1+len g)-'1,f);
then A23:f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A9,A19,GOBOARD7:38;
i2<=len f by A2,JORDAN3:9;
then f/.i2=f.i2 by A2,FINSEQ_4:24;
hence contradiction by A8,A9,A12,A23,FINSEQ_4:24;
case A24:i2=S_Drop((i1+len g)-'1,f);
now per cases;
case A25: (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))<len f -'1) by A5,NAT_1:def 2;
then consider n being Nat such that A26: i1+len g -'1
=(len f-'1)*n+((i1+len g)-'1 mod (len f -'1));
A27:i1+len g -'1=(len f-'1)*n+i2 by A24,A25,A26,Def1;
now per cases;
case n=0;
then A28:i2=i1+len g -'1 by A24,A25,A26,Def1;
1<=i1+len g by A2,NAT_1:37;
then i1+len g-'1=i1+len g-1 by SCMFSA_7:3;
then A29: i2+1-i1 = i1+len g-i1 by A28,XCMPLX_1:27
.= len g by XCMPLX_1:26;
then A30: i2-i1+1=len g by XCMPLX_1:29;
then len g=i2-'i1+1 by A1,SCMFSA_7:3;
then A31:len g = len g & len mid(f,i1,i2) = len g
by A1,A2,A6,A7,JORDAN3:27;
for j st j in Seg len g holds g.j = mid(f,i1,i2).j
proof let j;assume j in Seg len g;
then A32:1<=j & j<=len g by FINSEQ_1:3;
then A33:g.j=f.S_Drop((i1+j)-'1,f) by A1,Def2;
A34:i1+j-'1=i1+j-1 by A32,Th2;
i1+j>=1+1 by A2,A32,REAL_1:55;
then i1+j-1>=1+1-1 by REAL_1:49;
then A35:i1+j-'1<>0 by A34;
j+i1<=i2-i1+1+i1 by A30,A32,AXIOMS:24;
then j+i1<=i2+1 by XCMPLX_1:227;
then A36:i1+j<=len f by A2,AXIOMS:22;
now per cases;
case A37:i1+j=len f;
then (i1+j-'1) mod (len f-'1)=0 by GR_CY_1:5;
hence S_Drop(i1+j-'1,f)=i1+j-'1 by A37,Def1;
case i1+j<>len f; then i1+j<len f by A36,REAL_1:def 5;
then i1+j-1<len f-1 by REAL_1:54;
then i1+j-'1<len f-'1 by A2,A4,Th2;
then (i1+j-'1)mod (len f-'1)=i1+j-'1 by GR_CY_1:4;
hence S_Drop((i1+j)-'1,f)=i1+j-'1 by A35,Def1;
end;
hence g.j = mid(f,i1,i2).j
by A1,A2,A7,A29,A32,A33,JORDAN3:31;
end;
hence len g=i2-'i1+1 & g=mid(f,i1,i2)
by A1,A30,A31,FINSEQ_2:10,SCMFSA_7:3;
case n<>0; then 0<n by NAT_1:19; then A38: 0+1<=n by NAT_1:38;
0<=len f-'1 by NAT_1:18;
then (len f-'1)*n>=(len f-'1)*1 by A38,AXIOMS:25;
then A39:i1+len g-'1-i2>=(len f-'1) by A27,XCMPLX_1:26;
len g+1<=len f by A2,NAT_1:38;
then len g+1-1<=len f-1 by REAL_1:49;
then A40:len g<=len f-1 by XCMPLX_1:26;
0<=len g by NAT_1:18;
then len g<=len f-'1 by A40,BINARITH:def 3;
then len g+i1<=len f-'1+i2 by A1,REAL_1:55;
then i1+len g<len f-'1+i2+1 by NAT_1:38;
then i1+len g-1<len f-'1+i2+1-1 by REAL_1:92;
then A41:i1+len g-1<len f-'1+i2 by XCMPLX_1:26;
i1<=i1+len g by NAT_1:29;
then 1<=i1+len g by A2,AXIOMS:22;
then i1+len g-1=i1+len g-'1 by SCMFSA_7:3;
then i1+len g-'1-i2<len f-'1+i2-i2 by A41,REAL_1:92;
hence contradiction by A39,XCMPLX_1:26;
end;
hence len g=i2-'i1+1 & g=mid(f,i1,i2);
case A42:(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))<len f -'1) by A5,NAT_1:def 2;
then consider n being Nat such that A43: i1+len g -'1
=(len f-'1)*n+((i1+len g-'1) mod (len f -'1));
A44:i1+len g -'1=i2*n by A24,A42,A43,Def1;
now assume n=0;
then A45: i1+len g<=1 by A42,A43,Th1;
i1+len g>=1+1 by A2,REAL_1:55;
hence contradiction by A45,AXIOMS:22;
end;
then n>0 by NAT_1:19;
then A46: n>=0+1 by NAT_1:38;
now assume n>1; then n>=1+1 by NAT_1:38;
then A47:i1+len g -'1>=(len f-'1)*(1+1) by A42,A43,NAT_1:20;
len g -1<len f-1 by A2,REAL_1:54;
then i1+(len g -1)<len f-'1+(len f-'1) by A3,A4,REAL_1:67;
then A48:i1+len g -1<len f-'1+(len f-'1) by XCMPLX_1:29;
A49:len f-'1+(len f-'1)=(len f-'1)*1+(len f-'1)
.=(len f-'1)*(1+1) by XCMPLX_1:8;
1<=len g+i1 by A2,NAT_1:37;
hence contradiction by A47,A48,A49,SCMFSA_7:3;
end;
then n=1 by A46,AXIOMS:21;
then i1+len g-1=i2 by A2,A44,JORDAN3:1;
then i1+(len g-1)=i2 by XCMPLX_1:29;
then A50:len g-1=i2-i1 by XCMPLX_1:26;
A51: i2-i1=i2-'i1 by A1,SCMFSA_7:3;
then A52:len g=i2-'i1+1 by A50,XCMPLX_1:27;
then A53:len g = len g & len mid(f,i1,i2) = len g
by A1,A2,A6,A7,JORDAN3:27;
for j st j in Seg len g holds g.j = mid(f,i1,i2).j
proof let j;assume j in Seg len g;
then A54:1<=j & j<=len g by FINSEQ_1:3;
then A55:g.j=f.S_Drop((i1+j)-'1,f) by A1,Def2;
A56:i1+j-'1=i1+j-1 by A54,Th2;
i1+j>=1+1 by A2,A54,REAL_1:55;
then i1+j-1>=1+1-1 by REAL_1:49;
then A57:i1+j-'1<>0 by A56;
j<=i2-i1+1 by A50,A54,XCMPLX_1:27;
then j+i1<=i2-i1+1+i1 by AXIOMS:24;
then j+i1<=i2+1 by XCMPLX_1:227;
then A58:i1+j<=len f by A2,AXIOMS:22;
now per cases;
case A59:i1+j=len f;
then (i1+j-'1) mod (len f-'1)=0 by GR_CY_1:5;
hence S_Drop(i1+j-'1,f)=i1+j-'1 by A59,Def1;
case i1+j<>len f; then i1+j<len f by A58,REAL_1:def 5;
then i1+j-1<len f-1 by REAL_1:54;
then A60:i1+j-'1<len f-'1 by A2,A4,Th2;
then (i1+j-'1) mod (len f-'1)<>0 by A57,GR_CY_1:4;
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 A60,GR_CY_1:4;
end;
hence g.j = mid(f,i1,i2).j by A1,A2,A7,A52,A54,A55,JORDAN3:31;
end;
hence len g=i2-'i1+1 & g=mid(f,i1,i2)
by A50,A51,A53,FINSEQ_2:10,XCMPLX_1:27;
end;
hence len g=i2-'i1+1 & g=mid(f,i1,i2);
end;
hence thesis;
end;
theorem Th38:for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being 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 Nat;
assume A1:g is_a_part>_of f,i1,i2 & i1>i2;
then A2:1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))
by Def2;
A3:i1<=i1+1 by NAT_1:37;
then A4:i1<=len f by A2,AXIOMS:22;
i1+1-1<=len f-1 by A2,REAL_1:49;
then A5:i1<=len f-1 by XCMPLX_1:26;
then A6:1<=len f-1 by A2,AXIOMS:22;
then A7:len f-1=len f-'1 by JORDAN3:1;
then A8:0<len f-'1 by A2,A5,AXIOMS:22;
A9:0<>len f-'1 by A2,A5,A7,AXIOMS:22;
i1<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
then A10:len f -'1<len f by JORDAN3:14;
A11: i2<=i2+1 by NAT_1:29;
then A12:i2<=len f by A2,AXIOMS:22;
A13:f.i2=f.S_Drop((i1+len g)-'1,f) by A2;
A14: now per cases;
case A15:(i1+len g)-'1 mod (len f -'1)<>0;
then 0<(i1+len g)-'1 mod (len f -'1) by NAT_1:19;
then 0+1<=(i1+len g)-'1 mod (len f -'1) by NAT_1:38;
hence 1<=S_Drop((i1+len g)-'1,f) by A15,Def1;
case (i1+len g)-'1 mod (len f -'1)=0;
then A16:S_Drop((i1+len g)-'1,f)=len f -'1 by Def1;
i1<=len f -'1 by A2,JORDAN3:12;
hence 1<=S_Drop((i1+len g)-'1,f) by A2,A16,AXIOMS:22;
end;
A17: now per cases;
case (i1+len g)-'1 mod (len f -'1)<>0;
then A18:S_Drop((i1+len g)-'1,f)=((i1+len g)-'1 mod (len f -'1)) by
Def1;
A19: i1<=len f -'1 by A2,JORDAN3:12;
then A20:1<=len f -'1 by A2,AXIOMS:22;
0<len f -'1 by A2,A19,AXIOMS:22;
then A21:((i1+len g)-'1 mod (len f -'1)) <len f-'1 by NAT_1:46;
len f -'1<len f by A20,JORDAN3:14;
hence S_Drop((i1+len g)-'1,f)< len f by A18,A21,AXIOMS:22;
case (i1+len g)-'1 mod (len f -'1)=0;
then A22:S_Drop((i1+len g)-'1,f)=len f -'1 by Def1;
i1<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
hence S_Drop((i1+len g)-'1,f)< len f by A22,JORDAN3:14;
end;
A23:i2<=len f -'1 by A2,JORDAN3:12;
then A24:1<=len f -'1 by A2,AXIOMS:22;
then len f -'1<len f by JORDAN3:14;
then A25:i2<len f by A23,AXIOMS:22;
now per cases by REAL_1:def 5;
case A26:i2<S_Drop((i1+len g)-'1,f);
then A27:f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A2,A17,GOBOARD7:38;
i2<=len f by A2,JORDAN3:9;
then A28:f/.i2=f.i2 by A2,FINSEQ_4:24;
1<=S_Drop((i1+len g)-'1,f) by A2,A26,AXIOMS:22;
hence contradiction by A13,A17,A27,A28,FINSEQ_4:24;
case i2>S_Drop((i1+len g)-'1,f);
then A29:f/.i2<>f/.(S_Drop((i1+len g)-'1,f)) by A14,A25,GOBOARD7:38;
i2<=len f by A2,JORDAN3:9;
then f/.i2=f.i2 by A2,FINSEQ_4:24;
hence contradiction by A13,A14,A17,A29,FINSEQ_4:24;
case A30:i2=S_Drop((i1+len g)-'1,f);
now per cases;
case A31: (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))<len f -'1)or
((i1+len g-'1) mod (len f -'1))=0 & len f-'1=0
by NAT_1:def 2;
then consider n being Nat such that A32: i1+len g -'1
=(len f-'1)*n+((i1+len g)-'1 mod (len f -'1))
by A2,A5,A7,AXIOMS:22;
A33:i1+len g -'1=(len f-'1)*n+i2 by A30,A31,A32,Def1;
now per cases;
case n=0;
then i2=i1+len g -'1 by A30,A31,A32,Def1;
then A34:i2+1=i1+len g -1+1 by A2,JORDAN3:1
.=i1+len g by XCMPLX_1:27;
A35:i2+1<=i1 by A1,NAT_1:38;
0<len g by A2,AXIOMS:22;
then i2+1+0<i1+len g by A35,REAL_1:67;
hence contradiction by A34;
case n<>0; then 0<n by NAT_1:19;
then A36: 0+1<=n by NAT_1:38;
now per cases by A36,REAL_1:def 5;
case A37:1=n;
len f-'1=len f-1 by A24,JORDAN3:1;
then i1+len g-1=len f-1+i2 by A2,A33,A37,Th2;
then i1+len g=len f-1+i2+1 by XCMPLX_1:27;
then i1+len g-i1=len f+i2-i1 by XCMPLX_1:227;
then A38:len g=len f+i2-i1 by XCMPLX_1:26;
A39:len (mid(f,i1,len f-'1)^(f|i2))
= len (mid(f,i1,len f-'1))+ len(f|i2)
by FINSEQ_1:35;
A40: 1<=i1 & i1<=len f & 1<=len f-'1 & len f-'1<=len f & i1<=len f-'1
by A2,A3,A5,A6,AXIOMS:22,JORDAN3:1,13;
then A41:len (mid(f,i1,len f-'1))=len f-'1-'i1+1 by JORDAN3:27;
A42:len f-'1-'i1=len f-'1-i1 by A5,A7,SCMFSA_7:3;
A43:len f-'1-'i1+1 =len f-1-i1+1 by A5,A7,SCMFSA_7:3
.=len f-i1 by XCMPLX_1:229;
then len (mid(f,i1,len f-'1)^(f|i2))=len f-i1+i2
by A12,A39,A41,TOPREAL1:3
.=len f+i2-i1 by XCMPLX_1:29
.=len f+i2-'i1 by A4,Th2;
then A44:len g = len g & len (mid(f,i1,len f-'1)^(f|i2))=len g
by A4,A38,Th2;
for j st j in Seg len g holds g.j =(mid(f,i1,len f-'1)^(f|i2)).j
proof let j;assume A45: j in Seg len g;
then A46:1<=j & j<=len g by FINSEQ_1:3;
then A47:g.j=f.S_Drop((i1+j)-'1,f) by A1,Def2;
A48:i1+j-'1=i1+j-1 by A46,Th2;
i1+j>=1+1 by A2,A46,REAL_1:55;
then i1+j-1>=1+1-1 by REAL_1:49;
then A49:i1+j-'1<>0 by A48;
now per cases;
case A50:j<=len mid(f,i1,len f-'1);
then j in dom mid(f,i1,len f-'1) by A46,FINSEQ_3:27;
then A51:(mid(f,i1,len f-'1)^(f|i2)).j =mid(f,i1,len f-'1).j
by FINSEQ_1:def 7;
A52:1<=i1 & i1<=len f-'1 & len f-'1<=len f & 1<=j & j<=
len f-'1-i1+1
by A40,A42,A45,A50,FINSEQ_1:3,JORDAN3:27;
j+i1<=len f-'1-i1+1+i1
by A41,A42,A50,AXIOMS:24;
then i1+j<=len f-1+1 by A7,XCMPLX_1:227;
then A53:i1+j<=len f by XCMPLX_1:27;
now per cases;
case A54:i1+j=len f;
then (i1+j-'1) mod (len f-'1)=0 by GR_CY_1:5;
hence S_Drop(i1+j-'1,f)=i1+j-'1 by A54,Def1;
case i1+j<>len f; then i1+j<len f by A53,REAL_1:def 5;
then i1+j-1<len f-1 by REAL_1:54;
then A55:i1+j-'1<len f-'1 by A2,A7,Th2;
then (i1+j-'1) mod (len f-'1)<>0 by A49,GR_CY_1:4;
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 A55,GR_CY_1:4;
end;
hence g.j = (mid(f,i1,len f-'1)^(f|i2)).j
by A47,A51,A52,JORDAN3:31;
case A56:j>len mid(f,i1,len f-'1);
then j+i1>len f-i1+i1 by A41,A43,REAL_1:53;
then j+i1>len f by XCMPLX_1:27;
then i1+j-len f>len f-len f by REAL_1:54;
then A57: i1+j-len f>0 by XCMPLX_1:14;
then A58:i1+j-'len f=i1+j-len f by BINARITH:def 3;
A59:(mid(f,i1,len f-'1)^(f|i2)).j
=(f|i2).(j-len mid(f,i1,len f-'1))
by A44,A46,A56,JORDAN3:15;
A60:j-len mid(f,i1,len f-'1)=j-(len f-i1) by A40,A43,JORDAN3:27
.=j-len f+i1 by XCMPLX_1:37
.=j+i1-len f by XCMPLX_1:29;
j<=len f+i2-i1 by A38,A45,FINSEQ_1:3;
then j+i1<=len f+i2-i1+i1 by AXIOMS:24;
then j+i1<=len f+i2 by XCMPLX_1:27;
then j+i1-len f<=len f+i2-len f by REAL_1:49;
then j+i1-'len f<=i2 by A58,XCMPLX_1:26;
then A61:(f|i2).(j-len mid(f,i1,len f-'1))
=f.(i1+j-'len f) by A58,A60,JORDAN3:20;
A62: j<=len f-i1+i2 by A38,A46,XCMPLX_1:29;
A63:j-len mid(f,i1,len f-'1)=j-'len mid(f,i1,len f-'1)
by A56,SCMFSA_7:3;
len mid(f,i1,len f-'1)+1<=j by A56,NAT_1:38;
then len mid(f,i1,len f-'1)+1-len mid(f,i1,len f-'1)
<=j -len mid(f,i1,len f-'1) by REAL_1:49;
then A64:1 <=j -'len mid(f,i1,len f-'1) &
j-'len mid(f,i1,len f-'1)<=i2 & i2<=len f
by A2,A11,A41,A43,A62,A63,AXIOMS:22,REAL_1:86,XCMPLX_1:26;
A65:j-'len mid(f,i1,len f-'1)=j-len mid(f,i1,len f-'1)
by A56,SCMFSA_7:3
.=j-(len f-i1) by A40,A43,JORDAN3:27
.=j-len f+i1 by XCMPLX_1:37
.=i1+j-len f by XCMPLX_1:29;
A66:i1+j-1=i1+j-'1 by A2,Th2;
1+len f<=i1+j-len f+len f by A64,A65,AXIOMS:24;
then 1+len f<=i1+j by XCMPLX_1:27;
then 1+len f -1<=i1+j-1 by REAL_1:49;
then len f<=i1+j-'1 by A66,XCMPLX_1:26;
then A67:len f-'1<i1+j-'1 by A10,AXIOMS:22;
i1+1-1<=len f-1 by A2,REAL_1:49;
then A68:i1<=len f-'1 by A7,XCMPLX_1:26;
j<len f by A2,A46,AXIOMS:22;
then j<=len f-1 by SPPOL_1:6;
then A69:i1+j<=(len f-'1)+(len f-'1) by A7,A68,REAL_1:55;
i1+j<i1+j+1 by NAT_1:38;
then i1+j-1<i1+j+1-1 by REAL_1:54;
then i1+j-1<i1+j by XCMPLX_1:26;
then A70:i1+j-'1<(len f-'1)+(len f-'1) by A66,A69,AXIOMS:22;
now per cases;
case (i1+j-'1) mod (len f -'1)=0;
hence contradiction by A8,A67,A70,Th6;
case (i1+j-'1) mod (len f -'1)<>0;
then A71:S_Drop(i1+j-'1,f)= (i1+j-'1) mod (len f -'1) by Def1;
i1+j-'len f+(len f-'1)=i1+j-'len f+(len f-1)
by A6,JORDAN3:1
.=i1+j-len f+(len f-1) by A57,BINARITH:def 3
.=i1+j-len f+len f-1 by XCMPLX_1:29
.=i1+j-1 by XCMPLX_1:27
.=i1+j-'1 by A46,Th2;
then A72:(i1+j-'1) mod (len f-'1)
=(i1+j-'len f+((len f-'1)mod (len f-'1)))
mod (len f-'1) by GR_CY_1:3
.=(i1+j-'len f+0)
mod (len f-'1) by GR_CY_1:5
.=(i1+j-'len f) mod (len f-'1);
i1+j-(len f-'1)<=(len f-'1)+(len f-'1)-(len f-'1)
by A69,REAL_1:49;
then i1+j-(len f-1)<=(len f-'1) by A7,XCMPLX_1:26;
then i1+j-'len f+1<=(len f-'1) by A58,XCMPLX_1:37;
then i1+j-'len f<(len f-'1) by NAT_1:38;
hence g.j = (mid(f,i1,len f-'1)^(f|i2)).j
by A47,A59,A61,A71,A72,GR_CY_1:4;
end;
hence g.j = (mid(f,i1,len f-'1)^(f|i2)).j;
end;
hence g.j = (mid(f,i1,len f-'1)^(f|i2)).j;
end;
hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2)
by A4,A38,A44,Th2,FINSEQ_2:10;
case 1<n;
then 1+1<=n by NAT_1:38;
then (len f-'1)*n>=(len f-'1)*(1+1) by A8,AXIOMS:25;
then A73:i1+len g-'1>=(len f-'1)*(1+1)+i2 by A33,AXIOMS:24;
i1+1-1<=len f-1 by A2,REAL_1:49;
then A74:i1<=len f-'1 by A7,XCMPLX_1:26;
len g-1<len f-'1 by A2,A7,REAL_1:54;
then i1+(len g-1)<len f-'1+(len f-'1) by A74,REAL_1:67;
then i1+len g-1<(len f-'1)*1+(len f-'1)*1 by XCMPLX_1:29;
then A75:i1+len g-1<(len f-'1)*(1+1) by XCMPLX_1:8;
A76:i1+len g-1=i1+len g-'1 by A2,Th2;
(len f-'1)*(1+1)<=(len f-'1)*(1+1)+i2 by NAT_1:29;
hence contradiction by A73,A75,A76,AXIOMS:22;
end;
hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2);
end;
hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2);
case A77:(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))<len f -'1) by A9,NAT_1:def 2;
then consider n being Nat such that A78: i1+len g -'1
=(len f-'1)*n+((i1+len g-'1) mod (len f -'1));
now assume n=0;
then A79: i1+len g<=1 by A77,A78,Th1;
i1+len g>=1+1 by A2,REAL_1:55;
hence contradiction by A79,AXIOMS:22;
end;
then n>0 by NAT_1:19;
then A80: n>=0+1 by NAT_1:38;
now assume n>1; then n>=1+1 by NAT_1:38;
then A81:i1+len g -'1>=(len f-'1)*(1+1) by A77,A78,NAT_1:20;
len g -1<len f-1 by A2,REAL_1:54;
then i1+(len g -1)<len f-'1+(len f-'1) by A5,A7,REAL_1:67;
then A82:i1+len g -1<len f-'1+(len f-'1) by XCMPLX_1:29;
A83:len f-'1+(len f-'1)=(len f-'1)*1+(len f-'1)
.=(len f-'1)*(1+1) by XCMPLX_1:8;
1<=len g+i1 by A2,NAT_1:37;
hence contradiction by A81,A82,A83,SCMFSA_7:3;
end;
then n=1 by A80,AXIOMS:21;
then i1+len g-'1=i2 by A30,A77,A78,Def1;
then i1+len g-1=i2 by A2,JORDAN3:1;
then i1+(len g-1)=i2 by XCMPLX_1:29;
then A84:len g-1=i2-i1 by XCMPLX_1:26;
A85: 1-1<=len g-1 by A2,REAL_1:49;
i2-i2<i1-i2 by A1,REAL_1:54;
then 0<i1-i2 by XCMPLX_1:14;
then 0>-(i1-i2) by REAL_1:26,50;
hence contradiction by A84,A85,XCMPLX_1:143;
end;
hence len g=len f+i2-'i1 & g=mid(f,i1,len f-'1)^(f|i2);
end;
hence thesis by A2,JORDAN3:25;
end;
theorem Th39:for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being 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 Nat;
assume A1:g is_a_part<_of f,i1,i2 & i1>=i2;
then A2:1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((len f+i1-'i),f))
by Def3;
then i2+1-1<=len f-1 by REAL_1:49;
then A3:i2<=len f-1 by XCMPLX_1:26;
then A4:1<=len f-1 by A2,AXIOMS:22;
then A5:len f-1=len f-'1 by JORDAN3:1;
then A6:0<len f-'1 by A2,A3,AXIOMS:22;
A7:0<>len f-'1 by A2,A3,A5,AXIOMS:22;
i1<=i1+1 by NAT_1:29; then A8:i1<=len f by A2,AXIOMS:22;
A9:f.i2=f.S_Drop((len f+i1-'len g),f) by A2;
A10: now per cases;
case A11:(len f+i1-'len g) mod (len f -'1)<>0;
then 0<(len f+i1-'len g) mod (len f -'1) by NAT_1:19;
then 0+1<=(len f+i1-'len g) mod (len f -'1) by NAT_1:38;
hence 1<=S_Drop((len f+i1-'len g),f) by A11,Def1;
case (len f+i1-'len g) mod (len f -'1)=0;
then A12:S_Drop((len f+i1-'len g),f)=len f -'1 by Def1;
i2<=len f -'1 by A2,JORDAN3:12;
hence 1<=S_Drop((len f+i1-'len g),f) by A2,A12,AXIOMS:22;
end;
A13: now per cases;
case (len f+i1-'len g) mod (len f -'1)<>0;
then A14:S_Drop((len f+i1-'len g),f)
=((len f+i1-'len g) mod (len f -'1)) by Def1;
A15: i2<=len f -'1 by A2,JORDAN3:12;
then A16:1<=len f -'1 by A2,AXIOMS:22;
0<len f -'1 by A2,A15,AXIOMS:22;
then A17:((len f+i1-'len g) mod (len f -'1)) <len f-'1 by NAT_1:46;
len f -'1<len f by A16,JORDAN3:14;
hence S_Drop((len f+i1-'len g),f)< len f by A14,A17,AXIOMS:22;
case (len f+i1-'len g) mod (len f -'1)=0;
then A18:S_Drop((len f+i1-'len g),f)=len f -'1 by Def1;
i2<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
hence S_Drop((len f+i1-'len g),f)< len f by A18,JORDAN3:14;
end;
A19:i2<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
then len f -'1<len f by JORDAN3:14;
then A20:i2<len f by A19,AXIOMS:22;
now per cases by REAL_1:def 5;
case A21:i2<S_Drop((len f+i1-'len g),f);
then A22:f/.i2<>f/.(S_Drop((len f+i1-'len g),f)) by A2,A13,GOBOARD7:38;
i2<=len f by A2,NAT_1:38;
then A23:f/.i2=f.i2 by A2,FINSEQ_4:24;
1<=S_Drop((len f+i1-'len g),f) by A2,A21,AXIOMS:22;
hence contradiction by A9,A13,A22,A23,FINSEQ_4:24;
case i2>S_Drop((len f+i1-'len g),f);
then A24:f/.i2<>f/.(S_Drop((len f+i1-'len g),f)) by A10,A20,GOBOARD7:38;
i2<=len f by A2,NAT_1:38;
then f/.i2=f.i2 by A2,FINSEQ_4:24;
hence contradiction by A9,A10,A13,A24,FINSEQ_4:24;
case A25:i2=S_Drop((len f+i1-'len g),f);
now per cases;
case A26: (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)
by A7,NAT_1:def 2;
then consider n being Nat such that A27: len f+i1-'len g
=(len f-'1)*n+((len f+i1-'len g) mod (len f -'1));
A28:len f+i1-'len g=(len f-'1)*n+i2 by A25,A26,A27,Def1;
n>=0 by NAT_1:18;
then A29: n=0 or n>=0+1 by NAT_1:38;
now per cases by A29,REAL_1:def 5;
case n=0;
then i2=len f+i1-'len g by A25,A26,A27,Def1;
then i2=len f+i1-len g by A2,Th2;
then i2+len g=i1+len f by XCMPLX_1:27;
hence contradiction by A1,A2,REAL_1:67;
case n=1;
then A30:len f-1+i2=len f+i1-'len g by A5,A25,A26,A27,Def1;
len f+i1-'len g=len f+i1-len g by A2,Th2;
then len f-(1-i2)=len f+i1-len g by A30,XCMPLX_1:37;
then len f-(1-i2)=len f+(i1-len g) by XCMPLX_1:29;
then len f-(1-i2)-len f=(i1-len g) by XCMPLX_1:26;
then len f+-(1-i2)-len f=(i1-len g) by XCMPLX_0:def 8;
then -(1-i2)=(i1-len g) by XCMPLX_1:26;
then -(1-i2)+len g=i1 by XCMPLX_1:27;
then len g=i1+(1-i2) by XCMPLX_1:139;
then len g=i1+1-i2 by XCMPLX_1:29;
then A31: len g=i1-i2+1 by XCMPLX_1:29;
then A32:len g=i1-'i2+1 by A1,SCMFSA_7:3;
then A33:len g = len g & len mid(f,i1,i2) = len g by A1,A2,A8,Th21;
for j st j in Seg len g holds g.j =mid(f,i1,i2).j
proof let j;assume j in Seg len g;
then A34:1<=j & j<=len g by FINSEQ_1:3;
then A35:g.j=f.S_Drop(len f+i1-'j,f) by A1,Def3;
A36:j<=i1-'i2+1 by A1,A31,A34,SCMFSA_7:3;
A37:i1-'i2+1=i1-i2+1 by A1,SCMFSA_7:3
.=i1-(i2-1) by XCMPLX_1:37;
1-1<=i2-1 by A2,REAL_1:49;
then i1-0>=i1-(i2-1) by REAL_2:106;
then A38:j<=i1 by A36,A37,AXIOMS:22;
then A39:i1-'j+1=i1-j+1 by SCMFSA_7:3;
i1-j>=0 by A38,SQUARE_1:12;
then i1-j+1>=0+1 by AXIOMS:24;
then A40:i1-'j+1<>0 by A39;
now per cases;
case len f+i1-'j=len f-'1;
then len f+i1-j=len f-'1 by A38,Th2 .=len f-1 by A4,JORDAN3:1;
then len f+(i1-j)-len f=len f-1 -len f by XCMPLX_1:29;
then i1-j=len f-1-len f by XCMPLX_1:26;
then i1-j=len f +-1-len f by XCMPLX_0:def 8.=-1 by XCMPLX_1:26;
hence contradiction by A38,SQUARE_1:12;
case len f+i1-'j<>len f-'1;
A41:len f+i1-'j=len f+i1-j by A38,Th2;
now
0<j by A34,AXIOMS:22;
then i1+1+0<len f+j by A2,REAL_1:67;
then i1+1-j<len f+j-j by REAL_1:54;
then i1+1-j<len f by XCMPLX_1:26;
then i1+1-j-1<len f-1 by REAL_1:54;
then i1-j<len f-1 by XCMPLX_1:228;
then i1-'j<len f-'1 by A5,A38,SCMFSA_7:3;
then A42: i1-'j+1<=len f-'1 by NAT_1:38;
now per cases by A42,REAL_1:def 5;
case A43:i1-'j+1=len f-'1;
len f+i1-'j=len f+i1-j by A38,Th2
.=len f-1+1+i1-j by XCMPLX_1:27
.=len f-'1+(1+i1)-j by A5,XCMPLX_1:1
.=len f-'1+((1+i1)-j) by XCMPLX_1:29
.=len f-'1+(i1-j+1) by XCMPLX_1:29
.=len f-'1+(len f-'1) by A38,A43,SCMFSA_7:3;
then (len f+i1-'j)mod (len f-'1)=0 by Th8;
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A43,Def1;
case A44:i1-'j+1<len f-'1;
A45: len f=len f-1+1 by XCMPLX_1:27 .=len f-'1+1 by A4,JORDAN3:1;
len f-'1+1+i1-'j=len f-'1+1+i1-j by A38,Th2
.=len f-'1+1+(i1-j) by XCMPLX_1:29
.=len f-'1+(1+(i1-j)) by XCMPLX_1:1
.=len f-'1+(1+(i1-'j)) by A38,SCMFSA_7:3;
then (len f+i1-'j)mod (len f-'1)
=(((len f-'1)mod (len f-'1))+(1+(i1-'j)))mod (len f-'1)
by A45,GR_CY_1:2
.=(0+(1+(i1-'j)))mod (len f-'1) by GR_CY_1:5
.=(i1-'j+1) by A44,GR_CY_1:4;
then A46:S_Drop(len f+i1-'j,f)=(len f+i1-'j)mod (len f-'1)
by A40,Def1;
(1+i1)-j=i1-j+1 by XCMPLX_1:29;
then len f-1+(1+i1)-j=(len f-1)+(i1-j+1) by XCMPLX_1:29;
then len f-1+1+i1-j=(len f-1)+(i1-j+1) by XCMPLX_1:1;
then A47:len f+i1-'j=i1-'j+1+(len f-'1) by A5,A39,A41,
XCMPLX_1:27;
(len f-'1)mod(len f-'1)=0 by GR_CY_1:5;
then S_Drop(len f+i1-'j,f)=(i1-'j+1+0)mod (len f-'1)
by A46,A47,GR_CY_1:2
.=(i1-'j+1)mod (len f-'1);
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A44,GR_CY_1:4;
end;
hence S_Drop(len f+i1-'j,f)=i1-'j+1;
end;
hence S_Drop(len f+i1-'j,f)=i1-'j+1;
end;
hence g.j = mid(f,i1,i2).j by A1,A2,A8,A32,A34,A35,Th24;
end;
hence len g=i1-'i2+1 & g=mid(f,i1,i2) by A1,A31,A33,FINSEQ_2:10,
SCMFSA_7:3;
case n>1;
then A48:1+1<=n by NAT_1:38;
A49:len f-'1>=0 by NAT_1:18;
len f+i1-'len g-i2=(len f-'1)*n by A28,XCMPLX_1:26;
then len f+i1-'len g-i2>=(len f-'1)*(1+1) by A48,A49,AXIOMS:25;
then A50: len f+i1-'len g-i2>=(len f-'1)*1+(len f-'1)*1 by XCMPLX_1:8;
0<len g by A2,AXIOMS:22;
then i1+1+0<i1+1+len g by REAL_1:67;
then i1+1-len g<i1+1+len g-len g by REAL_1:92;
then i1+1-len g<i1+1 by XCMPLX_1:26;
then i1-len g+1<i1+1 by XCMPLX_1:29;
then i1-len g+1-i2<i1+1-i2 by REAL_1:92;
then i1-len g-i2+1<i1+1-i2 by XCMPLX_1:29;
then len f-1+(i1-len g-i2+1)<len f-1+(i1+1-i2) by REAL_1:67;
then len f-1+(i1-len g-i2)+1<len f-1+(i1+1-i2) by XCMPLX_1:1;
then len f+(i1-len g-i2)<len f-1+(i1+1-i2)
by XCMPLX_1:227;
then len f+(i1-len g)-i2<len f-1+(i1+1-i2) by XCMPLX_1:29;
then A51:len f+i1-len g-i2<len f-1+(i1+1-i2) by XCMPLX_1:29;
A52:i1+1-i2<=len f-i2 by A2,REAL_1:49;
len f-i2<=len f-1 by A2,REAL_2:106;
then i1+1-i2<=len f-1 by A52,AXIOMS:22;
then len f-1+(i1+1-i2)<=len f-1+(len f-1) by REAL_1:55;
then len f+i1-len g-i2<len f-1+(len f-1) by A51,AXIOMS:22;
hence contradiction by A2,A5,A50,Th2;
end;
hence len g=i1-'i2+1 & g=mid(f,i1,i2);
case A53:(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)or
((len f+i1-'len g) mod (len f -'1))=0 & len f-'1=0
by NAT_1:def 2;
then consider n being Nat such that A54: len f+i1-'len g
=(len f-'1)*n+((len f+i1-'len g) mod (len f -'1))
by A2,A3,A5,AXIOMS:22;
A55:len f+i1-'len g=i2*n by A25,A53,A54,Def1;
now assume n=0;
then A56: len g>=len f+i1 by A53,A54,Th1;
len f<=len f +i1 by NAT_1:29;
hence contradiction by A2,A56,AXIOMS:22;
end;
then n>0 by NAT_1:19;
then A57: n>=0+1 by NAT_1:38;
A58: now per cases by A57,REAL_1:def 5;
case n>1;
then A59: n>=1+1 by NAT_1:38;
i1+1+1<=len f+len g by A2,REAL_1:55;
then 1+(i1+1)-len g<=len f+len g-len g by REAL_1:49;
then 1+(i1+1)-len g<=len f by XCMPLX_1:26;
then 1+((i1+1)-len g)<=len f by XCMPLX_1:29;
then 1+((i1+1)-len g)-1<=len f-1 by REAL_1:49;
then (i1+1)-len g<=len f-1 by XCMPLX_1:26;
then len f-1+((i1+1)-len g)<=len f-1+(len f-1) by AXIOMS:24;
then len f-1+(i1+1)-len g<=len f-1+(len f-1) by XCMPLX_1:29;
then len f-1+i1+1-len g<=len f-1+(len f-1) by XCMPLX_1:1;
then len f+i1-len g<=len f-1+(len f-1)
by XCMPLX_1:227;
then A60:len f+i1-'len g<=len f-'1+(len f-'1) by A2,A5,Th2;
A61:len f-'1+(len f-'1)=(len f-'1)*1+(len f-'1)
.=(len f-'1)*(1+1) by XCMPLX_1:8;
now per cases by A59,REAL_1:def 5;
case n>1+1;
hence contradiction by A6,A53,A54,A60,A61,REAL_1:70;
case A62:n=1+1;
then len f+i1-len g=len f-'1+(len f-'1) by A2,A53,A54,A61,Th2;
then len f-1+1+i1-len g=len f-'1+(len f-'1) by XCMPLX_1:27;
then len f-1+(1+i1)-len g=len f-'1+(len f-'1) by XCMPLX_1:1;
then len f-1+((1+i1)-len g)=len f-'1+(len f-'1) by XCMPLX_1:29;
then (1+i1)-len g=(len f-'1) by A5,XCMPLX_1:2;
then A63:(1+i1)-(len f-'1)=len g by XCMPLX_1:18;
then 1+(len f-'1)<=(1+i1)-(len f-'1)+(len f-'1) by A2,AXIOMS:24;
then 1+(len f-1)<=(1+i1) by A5,XCMPLX_1:27;
then len f<=i1+1 by XCMPLX_1:27;
then A64:len f=i1+1 by A2,AXIOMS:21;
then A65: i1+1-i1=len g by A63,BINARITH:39;
i2*(1+1)=i1*(1+1) by A53,A54,A55,A62,A64,BINARITH:39;
then i2=i1 by XCMPLX_1:5;
then i1-'i2=0 by GOBOARD9:1;
hence len g=i1-'i2+1 by A65,XCMPLX_1:26;
end;
hence len g=i1-'i2+1;
case A66: n=1;
len f+i1-'len g=len f+i1-len g by A2,Th2;
then len f+i1=i2+len g by A55,A66,XCMPLX_1:27;
hence contradiction by A1,A2,REAL_1:67;
end;
then A67:len g = len g & len mid(f,i1,i2) = len g by A1,A2,A8,Th21;
for j st j in Seg len g holds g.j =mid(f,i1,i2).j
proof let j;assume j in Seg len g;
then A68:1<=j & j<=len g by FINSEQ_1:3;
then A69:g.j=f.S_Drop(len f+i1-'j,f) by A1,Def3;
A70:i1-'i2+1=i1-i2+1 by A1,SCMFSA_7:3
.=i1-(i2-1) by XCMPLX_1:37;
1-1<=i2-1 by A2,REAL_1:49;
then i1-0>=i1-(i2-1) by REAL_2:106;
then A71:j<=i1 by A58,A68,A70,AXIOMS:22;
then A72:i1-'j+1=i1-j+1 by SCMFSA_7:3;
i1-j>=0 by A71,SQUARE_1:12;
then i1-j+1>=0+1 by AXIOMS:24;
then A73:i1-'j+1<>0 by A72;
now per cases;
case len f+i1-'j=len f-'1;
then len f+i1-j=len f-'1 by A71,Th2 .=len f-1 by A4,JORDAN3:1;
then len f+(i1-j)-len f=len f-1 -len f by XCMPLX_1:29;
then i1-j=len f-1-len f by XCMPLX_1:26;
then i1-j=len f +-1-len f by XCMPLX_0:def 8.=-1 by XCMPLX_1:26;
hence contradiction by A71,SQUARE_1:12;
case len f+i1-'j<>len f-'1;
A74:len f+i1-'j=len f+i1-j by A71,Th2;
now
0<j by A68,AXIOMS:22;
then i1+1+0<len f+j by A2,REAL_1:67;
then i1+1-j<len f+j-j by REAL_1:54;
then i1+1-j<len f by XCMPLX_1:26;
then i1+1-j-1<len f-1 by REAL_1:54;
then i1-j<len f-1 by XCMPLX_1:228;
then i1-'j<len f-'1 by A5,A71,SCMFSA_7:3;
then A75: i1-'j+1<=len f-'1 by NAT_1:38;
now per cases by A75,REAL_1:def 5;
case A76:i1-'j+1=len f-'1;
len f+i1-'j=len f+i1-j by A71,Th2
.=len f-1+1+i1-j by XCMPLX_1:27
.=len f-'1+(1+i1)-j by A5,XCMPLX_1:1
.=len f-'1+((1+i1)-j) by XCMPLX_1:29
.=len f-'1+(i1-j+1) by XCMPLX_1:29
.=len f-'1+(len f-'1) by A71,A76,SCMFSA_7:3;
then (len f+i1-'j)mod (len f-'1)=0 by Th8;
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A76,Def1;
case A77:i1-'j+1<len f-'1;
A78: len f=len f-1+1 by XCMPLX_1:27 .=len f-'1+1 by A4,JORDAN3:1;
len f-'1+1+i1-'j=len f-'1+1+i1-j by A71,Th2
.=len f-'1+1+(i1-j) by XCMPLX_1:29
.=len f-'1+(1+(i1-j)) by XCMPLX_1:1
.=len f-'1+(1+(i1-'j)) by A71,SCMFSA_7:3;
then (len f+i1-'j)mod (len f-'1)
=(((len f-'1)mod (len f-'1))+(1+(i1-'j)))mod (len f-'1)
by A78,GR_CY_1:2
.=(0+(1+(i1-'j)))mod (len f-'1) by GR_CY_1:5
.=(i1-'j+1) by A77,GR_CY_1:4;
then A79:S_Drop(len f+i1-'j,f)=(len f+i1-'j)mod (len f-'1)
by A73,Def1;
(1+i1)-j=i1-j+1 by XCMPLX_1:29;
then len f-1+(1+i1)-j=(len f-1)+(i1-j+1) by XCMPLX_1:29;
then len f-1+1+i1-j=(len f-1)+(i1-j+1) by XCMPLX_1:1;
then A80:len f+i1-'j=i1-'j+1+(len f-'1) by A5,A72,A74,
XCMPLX_1:27;
(len f-'1)mod(len f-'1)=0 by GR_CY_1:5;
then S_Drop(len f+i1-'j,f)=(i1-'j+1+0)mod (len f-'1)
by A79,A80,GR_CY_1:2
.=(i1-'j+1)mod (len f-'1);
hence S_Drop(len f+i1-'j,f)=i1-'j+1 by A77,GR_CY_1:4;
end;
hence S_Drop(len f+i1-'j,f)=i1-'j+1;
end;
hence S_Drop(len f+i1-'j,f)=i1-'j+1;
end;
hence g.j = mid(f,i1,i2).j by A1,A2,A8,A58,A68,A69,Th24;
end;
hence len g=i1-'i2+1 & g=mid(f,i1,i2) by A58,A67,FINSEQ_2:10;
end;
hence len g=i1-'i2+1 & g=mid(f,i1,i2);
end;
hence thesis;
end;
theorem Th40:for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1<i2 holds len g=len f+i1-'i2
& g=mid(f,i1,1)^mid(f,len f-'1,i2)
proof let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
assume A1:g is_a_part<_of f,i1,i2 & i1<i2;
then A2:1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((len f+i1-'i),f))
by Def3;
i1<=i1+1 by NAT_1:37;
then A3:i1<=len f by A2,AXIOMS:22;
i1+1-1<=len f-1 by A2,REAL_1:49;
then A4:i1<=len f-1 by XCMPLX_1:26;
then A5:1<=len f-1 by A2,AXIOMS:22;
then A6:len f-1=len f-'1 by JORDAN3:1;
then A7:0<len f-'1 by A2,A4,AXIOMS:22;
A8:0<>len f-'1 by A2,A4,A6,AXIOMS:22;
i2+1-1<=len f-1 by A2,REAL_1:49;
then A9:i2<=len f-'1 by A6,XCMPLX_1:26;
i1<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
then A10:len f -'1<len f by JORDAN3:14;
i1<=i1+1 by NAT_1:29; then A11:i1<=len f by A2,AXIOMS:22;
i2<=i2+1 by NAT_1:29; then A12:i2<=len f by A2,AXIOMS:22;
A13:f.i2=f.S_Drop(len f+i1-'len g,f) by A2;
A14: now per cases;
case A15:len f+i1-'len g mod (len f -'1)<>0;
then 0<len f+i1-'len g mod (len f -'1) by NAT_1:19;
then 0+1<=len f+i1-'len g mod (len f -'1) by NAT_1:38;
hence 1<=S_Drop(len f+i1-'len g,f) by A15,Def1;
case len f+i1-'len g mod (len f -'1)=0;
then A16:S_Drop(len f+i1-'len g,f)=len f -'1 by Def1;
i1<=len f -'1 by A2,JORDAN3:12;
hence 1<=S_Drop(len f+i1-'len g,f) by A2,A16,AXIOMS:22;
end;
A17: now per cases;
case len f+i1-'len g mod (len f -'1)<>0;
then A18:S_Drop(len f+i1-'len g,f)
=(len f+i1-'len g mod (len f -'1)) by Def1;
A19: i1<=len f -'1 by A2,JORDAN3:12;
then A20:1<=len f -'1 by A2,AXIOMS:22;
0<len f -'1 by A2,A19,AXIOMS:22;
then A21:(len f+i1-'len g mod (len f -'1)) <len f-'1 by NAT_1:46;
len f -'1<len f by A20,JORDAN3:14;
hence S_Drop(len f+i1-'len g,f)< len f by A18,A21,AXIOMS:22;
case len f+i1-'len g mod (len f -'1)=0;
then A22:S_Drop(len f+i1-'len g,f)=len f -'1 by Def1;
i1<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
hence S_Drop(len f+i1-'len g,f)< len f by A22,JORDAN3:14;
end;
A23:i2<=len f -'1 by A2,JORDAN3:12;
then 1<=len f -'1 by A2,AXIOMS:22;
then len f -'1<len f by JORDAN3:14;
then A24:i2<len f by A23,AXIOMS:22;
now per cases by REAL_1:def 5;
case A25:i2<S_Drop(len f+i1-'len g,f);
then A26:f/.i2<>f/.(S_Drop(len f+i1-'len g,f)) by A2,A17,GOBOARD7:38;
i2<=len f by A2,NAT_1:38;
then A27:f/.i2=f.i2 by A2,FINSEQ_4:24;
1<=S_Drop(len f+i1-'len g,f) by A2,A25,AXIOMS:22;
hence contradiction by A13,A17,A26,A27,FINSEQ_4:24;
case i2>S_Drop(len f+i1-'len g,f);
then A28:f/.i2<>f/.(S_Drop(len f+i1-'len g,f)) by A14,A24,GOBOARD7:38;
i2<=len f by A2,NAT_1:38;
then f/.i2=f.i2 by A2,FINSEQ_4:24;
hence contradiction by A13,A14,A17,A28,FINSEQ_4:24;
case A29:i2=S_Drop(len f+i1-'len g,f);
now per cases;
case A30: 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)
by A8,NAT_1:def 2;
then consider n being Nat such that A31: len f+i1-'len g
=(len f-'1)*n+(len f+i1-'len g mod (len f -'1));
A32:len f+i1-'len g=(len f-'1)*n+i2 by A29,A30,A31,Def1;
now per cases;
case n=0;
then i2=len f+i1-'len g by A29,A30,A31,Def1 .=len f+i1-len g by A2,
Th2
.=len f-len g+i1 by XCMPLX_1:29;
then i2+len g=len f+i1 by XCMPLX_1:227;
then A33:len g=len f+i1-i2 by XCMPLX_1:26;
A34:len (mid(f,i1,1)^mid(f,len f-'1,i2))
= len (mid(f,i1,1))+ len(mid(f,len f-'1,i2))
by FINSEQ_1:35;
A35:len (mid(f,i1,1))=i1-'1+1 by A2,A3,Th21
.=i1 by A2,AMI_5:4;
len (mid(f,len f-'1,i2))=len f-'1-'i2+1
by A2,A9,A10,Th21;
then len (mid(f,len f-'1,i2))=len f-'1-i2+1 by A9,SCMFSA_7:3;
then len (mid(f,i1,1)^mid(f,len f-'1,i2))=i1+(len f-i2)
by A6,A34,A35,XCMPLX_1:229
.=i1+len f-i2 by XCMPLX_1:29
.=len f+i1-'i2 by A12,Th2;
then A36:len g = len g
& len (mid(f,i1,1)^mid(f,len f-'1,i2))=len g by A12,A33,Th2;
for j st j in Seg len g holds
g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
proof let j;
assume A37: j in Seg len g;
then A38:1<=j & j<=len g by FINSEQ_1:3;
then A39:g.j=f.S_Drop(len f+i1-'j,f) by A1,Def3;
A40:j<len f by A2,A38,AXIOMS:22;
then A41:len f+i1-'j=len f+i1-j by Th2;
now per cases;
case A42:j<=len mid(f,i1,1);
then j in dom mid(f,i1,1) by A38,FINSEQ_3:27;
then A43:(mid(f,i1,1)^mid(f,len f-'1,i2)).j =mid(f,i1,1).j
by FINSEQ_1:def 7;
A44:len mid(f,i1,1)=i1-'1+1 by A2,A11,Th21;
1<=i1 & i1<=len f-'1 & len f-'1<=len f & 1<=j & j<=i1
by A1,A4,A5,A35,A37,A42,Def3,FINSEQ_1:3,JORDAN3:1,13;
then len f-1+j<=len f+i1 by A6,REAL_1:55;
then len f-1+j-j<=len f+i1-j by REAL_1:49;
then A45: len f-1<=len f+i1-j by XCMPLX_1:26;
then A46:len f-'1<=len f+i1-'j by A6,A35,A42,Th2;
now per cases;
case len f+i1-'j=len f-'1;
then len f+i1-j=len f-1 by A6,A35,A42,Th2;
then len f+(i1-j)=len f-1 by XCMPLX_1:29;
then i1-j=len f-1-len f by XCMPLX_1:26;
then i1-j=len f+-1-len f by XCMPLX_0:def 8;
then i1-j=-1 by XCMPLX_1:26;
then i1=-1+j by XCMPLX_1:27;
then i1+1=j by XCMPLX_1:139;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A35,A42,NAT_1:38;
case len f+i1-'j<>len f-'1;
then A47:len f+i1-'j>len f-'1 by A6,A41,A45,REAL_1:def 5;
A48:j-1>=0 by A38,SQUARE_1:12;
then j-1=j-'1 by BINARITH:def 3;
then A49:len f<=len f+(j-1) by NAT_1:29;
now per cases;
case A50:i1+1=len f & j-1=0;
A51:j=j-1+1 by XCMPLX_1:27 .=1 by A50;
len f+i1-'j=len f+i1-j by A40,Th2
.=len f-1+1+i1-j by XCMPLX_1:27
.=len f-1+len f-1 by A50,A51,XCMPLX_1:1
.=len f-'1+(len f-'1) by A6,XCMPLX_1:29;
then (len f+i1-'j)mod (len f-'1)=0 by Th8;
then S_Drop(len f+i1-'j,f) =j+i1-'1 by A50,A51,Def1;
then A52:S_Drop(len f+i1-'j,f)
=1+i1-1 by A51,Th2
.=i1-j+1 by A51,XCMPLX_1:29;
A53: i1-j+1=i1-'j+1 by A35,A42,SCMFSA_7:3;
A54:1<=i1-'j+1 by NAT_1:29;
A55:j-1=j-'1 by A38,SCMFSA_7:3;
i1<=i1+(j-'1) by NAT_1:29;
then i1-(j-'1)<=i1 by REAL_1:86;
then A56:i1-'j+1<=i1 by A53,A55,XCMPLX_1:37;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1)
by A2,A11,A38,A42,A44,Th25
.=mid(f,1,i1).(i1-'j+1) by A53,XCMPLX_1:27
.=f.(i1-'j+1) by A11,A54,A56,JORDAN3:32;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A35,A39,A42,A43,A52,SCMFSA_7:3;
case A57:i1+1<>len f or j-1<>0;
now per cases by A57;
case i1+1<>len f; then i1+1<len f by A2,REAL_1:def 5;
hence i1+1<len f+(j-1) by A49,AXIOMS:22;
case j-1<>0;
then len f<len f+(j-1) by A48,REAL_1:69;
hence i1+1<len f+(j-1) by A2,AXIOMS:22;
end;
then i1+1<len f+j-1 by XCMPLX_1:29;
then i1+1<len f-1+j by XCMPLX_1:29;
then i1+1-j<len f-1+j-j by REAL_1:54;
then i1+1-j<len f-1 by XCMPLX_1:26;
then len f-1+(i1+1-j)<len f-1+(len f-1) by REAL_1:67;
then len f-1+(i1+1)-j<len f-1+(len f-1) by XCMPLX_1:29;
then len f-1+i1+1-j<len f-1+(len f-1) by XCMPLX_1:1;
then
A58:len f+i1-'j<len f-'1+(len f-'1) by A6,A41,XCMPLX_1:227;
then (len f+i1-'j) mod (len f-'1)<>0 by A7,A47,Th6;
then A59: 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 A7,A46,A58,Th7
.=len f+i1-j-(len f-1) by A5,A41,JORDAN3:1
.=len f+(i1-j)-(len f-1) by XCMPLX_1:29
.=len f+(i1-j)-len f+1 by XCMPLX_1:37
.=(i1-j)+1 by XCMPLX_1:26;
A60: i1-j+1=i1-'j+1 by A35,A42,SCMFSA_7:3;
A61:1<=i1-'j+1 by NAT_1:29;
A62:j-1=j-'1 by A38,SCMFSA_7:3;
i1<=i1+(j-'1) by NAT_1:29;
then i1-(j-'1)<=i1 by REAL_1:86;
then A63:i1-'j+1<=i1 by A60,A62,XCMPLX_1:37;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1)
by A2,A11,A38,A42,A44,Th25
.=mid(f,1,i1).(i1-'j+1) by A60,XCMPLX_1:27
.=f.(i1-'j+1) by A11,A61,A63,JORDAN3:32;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A35,A39,A42,A43,A59,SCMFSA_7:3;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
case A64:j>len mid(f,i1,1);
then A65:i1+1<=j by A35,NAT_1:38;
A66:(mid(f,i1,1)^(mid(f,len f-'1,i2))).j
=(mid(f,len f-'1,i2)).(j-len mid(f,i1,1))
by A36,A38,A64,JORDAN3:15;
A67:j<=len f+i1-i2 by A33,A37,FINSEQ_1:3;
i2-i1>=0 by A1,SQUARE_1:12;
then len f+0<=len f+(i2-i1) by REAL_1:55;
then len f-(i2-i1)<=len f+(i2-i1)-(i2-i1) by REAL_1:49
;
then len f-(i2-i1)<=len f by XCMPLX_1:26;
then len f-i2+i1<=len f by XCMPLX_1:37;
then len f+i1-i2<=len f by XCMPLX_1:29;
then A68:j<=len f by A67,AXIOMS:22;
i1+1<=j by A35,A64,NAT_1:38;
then i1+1-i1<=j-i1 by REAL_1:49;
then A69: 1<=j-i1 by XCMPLX_1:26;
i2+1-1<=len f-1 by A2,REAL_1:49;
then i2<=len f-1 by XCMPLX_1:26;
then i2-i2<=len f-1-i2 by REAL_1:49;
then A70: 0<=len f-'1-i2 by A6,XCMPLX_1:14;
A71: j-i1<=len f+i1-i2-i1 by A33,A38,REAL_1:49;
then A72:j-i1<=len f-i2 by XCMPLX_1:228;
len f-i2<=len f-1 by A2,REAL_1:92;
then j-i1<=len f-'1 by A6,A72,AXIOMS:22;
then A73:j-'i1<=len f-'1 by A35,A64,SCMFSA_7:3;
A74: len f-i2=len f-1+1-i2 by XCMPLX_1:27
.=len f-1-i2+1 by XCMPLX_1:29
.=len f-'1-i2+1 by A5,JORDAN3:1
.=len f-'1-'i2+1 by A70,BINARITH:def 3;
0<j-i1 by A69,AXIOMS:22;
then A75: j-i1 =j-'len mid(f,i1,1) by A35,BINARITH:def 3;
A76:j-len mid(f,i1,1)<=len f-'1-'i2+1 by A35,A71,A74,XCMPLX_1:228;
len f-'1-'(j-'i1)+1=len f-'1-(j-'i1)+1
by A73,SCMFSA_7:3
.=len f-1-(j-i1)+1 by A6,A35,A64,SCMFSA_7:3
.=len f-(j-i1) by XCMPLX_1:229
.=len f-j+i1 by XCMPLX_1:37
.=len f+i1-j by XCMPLX_1:29 .=len f+i1-'j by A68,Th2;
then A77:(mid(f,i1,1)^(mid(f,len f-'1,i2))).j
=f.(len f+i1-'j) by A2,A9,A10,A35,A66,A69,A75,A76,Th24;
A78:len f+i1-j=len f+i1-'j by A40,Th2;
0<i1 by A2,AXIOMS:22;
then len f+0<len f+i1 by REAL_1:67;
then j<len f+i1 by A68,AXIOMS:22;
then j-j<len f+i1-j by REAL_1:54;
then 0<len f+i1-j by XCMPLX_1:14;
then A79:0<len f+i1-'j by A68,Th2;
i1+1<=j by A35,A64,NAT_1:38;
then len f+(i1+1)<=len f+j by AXIOMS:24;
then len f+(i1+1)-1<=len f+j-1 by REAL_1:49;
then len f+i1+1-1<=len f+j-1 by XCMPLX_1:1;
then len f+i1<=len f+j-1 by XCMPLX_1:26;
then len f+i1-j<=len f+j-1-j by REAL_1:49;
then len f+i1-j<=len f-1 by XCMPLX_1:228;
then A80:len f-'1>=len f+i1-'j by A6,A68,Th2;
now per cases;
case A81:(len f+i1-'j) mod (len f -'1)=0;
then len f+i1-'j=len f-'1 by A79,A80,Th9;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A39,A77,A81,Def1;
case A82:(len f+i1-'j) mod (len f -'1)<>0;
then A83:S_Drop(len f+i1-'j,f)
= (len f+i1-'j) mod (len f -'1) by Def1;
len f+(i1+1)<=len f+j by A65,REAL_1:55;
then len f+i1+1<=len f+j by XCMPLX_1:1;
then len f+i1+1-j<=len f+j-j by REAL_1:49;
then len f+i1+1-j<=len f by XCMPLX_1:26;
then len f+i1+1-j-1<=len f-1 by REAL_1:49;
then
A84:len f+i1-j<=len f-'1 by A6,XCMPLX_1:228;
len f+i1-j=len f-'1 implies
contradiction by A78,A82,GR_CY_1:5;
then len f+i1-'j<(len f-'1) by A78,A84,REAL_1:def 5;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A39,A77,A83,GR_CY_1:4;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
end;
hence len g=len f+i1-'i2 & g=mid(f,i1,1)^mid(f,len f-'1,i2)
by A12,A33,A36,Th2,FINSEQ_2:10;
case n<>0; then 0<n by NAT_1:19;
then A85: 0+1<=n by NAT_1:38;
now per cases by A85,REAL_1:def 5;
case A86:1=n;
len f+i1-'len g=len f+i1-len g by A2,Th2;
then
A87:i1-len g=i2+(len f-1)-len f by A6,A32,A86,XCMPLX_1:228
.=i2+len f-1-len f by XCMPLX_1:29
.=i2-1 by XCMPLX_1:228;
A88:i1+1<=i2 by A1,NAT_1:38;
0<len g by A2,AXIOMS:22;
then i1+1+0<i2+len g by A88,REAL_1:67;
then i1+1-len g<i2+len g-len g by REAL_1:54;
then i1+1-len g<i2 by XCMPLX_1:26;
then i1+1-len g-1<i2-1 by REAL_1:54;
hence contradiction by A87,XCMPLX_1:228;
case 1<n;
then 1+1<=n by NAT_1:38;
then (len f-'1)*n>=(len f-'1)*(1+1) by A7,AXIOMS:25;
then A89:len f+i1-'len g>=(len f-'1)*(1+1)+i2
by A32,AXIOMS:24;
i1+1-1<=len f-1 by A2,REAL_1:49;
then i1<=len f-'1 by A6,XCMPLX_1:26;
then 1+i1<=len g+(len f-'1) by A2,REAL_1:55;
then len f-1+(1+i1)<=len f-1+(len g+(len f-'1)) by AXIOMS:24
;
then len f-1+1+i1<=len f-1+(len g+(len f-'1)) by XCMPLX_1:1;
then len f+i1<=len f-1+(len g+(len f-'1)) by XCMPLX_1:27;
then len f+i1<=len f-1+len g+(len f-'1) by XCMPLX_1:1;
then len f+i1-len g<=len f-1+len g+(len f-'1)-len g by REAL_1:49;
then len f+i1-len g<=(len f-'1)*1+(len f-'1)*1
by A6,XCMPLX_1:226;
then A90:len f+i1-len g<=(len f-'1)*(1+1) by XCMPLX_1:8;
A91:len f+i1-len g=len f+i1-'len g by A2,Th2;
0<i2 by A2,AXIOMS:22;
then (len f-'1)*(1+1)<(len f-'1)*(1+1)+i2 by REAL_1:69;
hence contradiction by A89,A90,A91,AXIOMS:22;
end;
hence contradiction;
end;
hence len g=len f+i1-'i2 & g=mid(f,i1,1)^mid(f,len f-'1,i2);
case A92: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)
by A8,NAT_1:def 2;
then consider n being Nat such that A93: len f+i1-'len g
=(len f-'1)*n+((len f+i1-'len g) mod (len f -'1));
A94:len f+i1-'len g=i2*n by A29,A92,A93,Def1;
now assume n=0;
then A95: len f+i1<=len g by A92,A93,Th1;
len f<=len f+i1 by NAT_1:29;
hence contradiction by A2,A95,AXIOMS:22;
end;
then n>0 by NAT_1:19;
then A96: n>=0+1 by NAT_1:38;
now assume n>1; then n>=1+1 by NAT_1:38;
then A97:len f+i1-'len g>=(len f-'1)*(1+1) by A92,A93,NAT_1:20;
now assume i1+1<len f;
then i1+1+1<len f+len g by A2,REAL_1:67;
then i1+1+1-1<len f+len g-1 by REAL_1:54;
then i1+1<len f+len g-1 by XCMPLX_1:26;
then i1+1-len g<len f+len g-1-len g by REAL_1:54;
then i1+1-len g<len f-1 by XCMPLX_1:228;
then len f-1+(i1+1-len g)<len f-1+(len f-1) by REAL_1:53;
then len f-1+(i1+1)-len g<len f-1+(len f-1) by XCMPLX_1:29;
then len f-1+i1+1-len g<len f-1+(len f-1) by XCMPLX_1:1;
then A98:len f+i1-len g<len f-1+(len f-1)
by XCMPLX_1:227;
len f-'1+(len f-'1)=(len f-'1)*1+(len f-'1)
.=(len f-'1)*(1+1) by XCMPLX_1:8;
hence contradiction by A2,A6,A97,A98,Th2;
end; then i1+1=len f by A2,REAL_1:def 5;
then i2>len f-1 by A1,XCMPLX_1:26;
then i2+1>len f-1+1 by REAL_1:53;
hence contradiction by A2,XCMPLX_1:27;
end;
then n=1 by A96,AXIOMS:21;
then A99: len f+i1-len g=i2 by A2,A94,Th2;
then A100:len f+i1-i2=len g by XCMPLX_1:18;
A101:len (mid(f,i1,1)^mid(f,len f-'1,i2))
= len (mid(f,i1,1))+ len(mid(f,len f-'1,i2))
by FINSEQ_1:35;
A102:len (mid(f,i1,1))=i1-'1+1 by A2,A3,Th21
.=i1 by A2,AMI_5:4;
len (mid(f,len f-'1,i2))=len f-'1-'i2+1
by A2,A9,A10,Th21;
then len (mid(f,len f-'1,i2))=len f-1-i2+1 by A6,A9,SCMFSA_7:3;
then len (mid(f,i1,1)^mid(f,len f-'1,i2))=i1+(len f-i2) by A101,
A102,XCMPLX_1:229
.=i1+len f-i2 by XCMPLX_1:29
.=len f+i1-'i2 by A12,Th2;
then A103:len g = len g
& len (mid(f,i1,1)^mid(f,len f-'1,i2))=len g by A12,A100,Th2;
for j st j in Seg len g holds
g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
proof let j;assume j in Seg len g;
then A104:1<=j & j<=len g by FINSEQ_1:3;
then A105:g.j=f.S_Drop(len f+i1-'j,f) by A1,Def3;
A106:j<len f by A2,A104,AXIOMS:22;
then A107:len f+i1-'j=len f+i1-j by Th2;
now per cases;
case A108:j<=len mid(f,i1,1);
then j in dom mid(f,i1,1) by A104,FINSEQ_3:27;
then A109:(mid(f,i1,1)^mid(f,len f-'1,i2)).j =mid(f,i1,1).j
by FINSEQ_1:def 7;
A110:len mid(f,i1,1)=i1-'1+1 by A2,A11,Th21;
len f-'1<=len f by JORDAN3:13;
then len f-1+j<=len f+i1 by A6,A102,A108,REAL_1:55;
then len f-1+j-j<=len f+i1-j by REAL_1:49;
then A111: len f-1<=len f+i1-j by XCMPLX_1:26;
then A112:len f-'1<=len f+i1-'j
by A6,A102,A108,Th2;
now per cases;
case len f+i1-'j=len f-'1;
then len f+i1-j=len f-1 by A6,A102,A108,Th2;
then len f+(i1-j)=len f-1 by XCMPLX_1:29;
then i1-j=len f-1-len f by XCMPLX_1:26;
then i1-j=len f+-1-len f by XCMPLX_0:def 8;
then i1-j=-1 by XCMPLX_1:26;
then i1=-1+j by XCMPLX_1:27;
then i1+1=j by XCMPLX_1:139;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A102,A108,NAT_1:38;
case len f+i1-'j<>len f-'1;
then A113:len f+i1-'j>len f-'1
by A6,A107,A111,REAL_1:def 5;
A114:j-1>=0 by A104,SQUARE_1:12;
then j-1=j-'1 by BINARITH:def 3;
then A115:len f<=len f+(j-1) by NAT_1:29;
now per cases;
case A116:i1+1=len f & j-1=0;
A117:j=j-1+1 by XCMPLX_1:27 .=1 by A116;
len f+i1-'j=len f+i1-j by A106,Th2
.=len f-1+1+i1-j by XCMPLX_1:27
.=len f-1+len f-1 by A116,A117,XCMPLX_1:1
.=len f-'1+(len f-'1) by A6,XCMPLX_1:29;
then (len f+i1-'j)mod (len f-'1)=0 by Th8;
then S_Drop(len f+i1-'j,f) =j+i1-'1 by A116,A117,Def1;
then A118:S_Drop(len f+i1-'j,f)
=i1+1-1 by A117,Th2
.=i1-j+1 by A117,XCMPLX_1:29;
A119: i1-j+1=i1-'j+1 by A102,A108,SCMFSA_7:3;
A120:f.S_Drop(len f+i1-'j,f)=f.(i1-'j+1)
by A102,A108,A118,SCMFSA_7:3;
A121:1<=i1-'j+1 by NAT_1:29;
A122:j-1=j-'1 by A104,SCMFSA_7:3;
i1<=i1+(j-'1) by NAT_1:29;
then i1-(j-'1)<=i1 by REAL_1:86;
then A123:i1-'j+1<=i1 by A119,A122,XCMPLX_1:37;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1)
by A2,A11,A104,A108,A110,Th25
.=mid(f,1,i1).(i1-'j+1) by A119,XCMPLX_1:27
.=f.(i1-'j+1) by A11,A121,A123,JORDAN3:32;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A1,A104,A109,A120,Def3;
case A124:i1+1<>len f or j-1<>0;
now per cases by A124;
case i1+1<>len f; then i1+1<len f by A2,REAL_1:def 5;
hence i1+1<len f+(j-1) by A115,AXIOMS:22;
case j-1<>0;
then len f<len f+(j-1) by A114,REAL_1:69;
hence i1+1<len f+(j-1) by A2,AXIOMS:22;
end;
then i1+1<len f+j-1 by XCMPLX_1:29;
then i1+1<len f-1+j by XCMPLX_1:29;
then i1+1-j<len f-1+j-j by REAL_1:54;
then i1+1-j<len f-1 by XCMPLX_1:26;
then len f-1+(i1+1-j)<len f-1+(len f-1) by REAL_1:67;
then len f-1+(i1+1)-j<len f-1+(len f-1) by XCMPLX_1:29;
then len f-1+i1+1-j<len f-1+(len f-1) by XCMPLX_1:1;
then
A125:len f+i1-'j<len f-'1+(len f-'1) by A6,A107,XCMPLX_1:227;
then (len f+i1-'j) mod (len f-'1)<>0 by A7,A113,Th6;
then A126: 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 A7,A112,A125,Th7
.=len f+i1-j-(len f-1) by A5,A107,JORDAN3:1
.=len f+(i1-j)-(len f-1) by XCMPLX_1:29
.=len f+(i1-j)-len f+1 by XCMPLX_1:37
.=(i1-j)+1 by XCMPLX_1:26;
A127: i1-j+1=i1-'j+1 by A102,A108,SCMFSA_7:3;
A128:1<=i1-'j+1 by NAT_1:29;
A129:j-1=j-'1 by A104,SCMFSA_7:3;
i1<=i1+(j-'1) by NAT_1:29;
then i1-(j-'1)<=i1 by REAL_1:86;
then A130:i1-'j+1<=i1 by A127,A129,XCMPLX_1:37;
mid(f,i1,1).j=mid(f,1,i1).(i1-1+1-j+1)
by A2,A11,A104,A108,A110,Th25
.=mid(f,1,i1).(i1-'j+1) by A127,XCMPLX_1:27
.=f.(i1-'j+1) by A11,A128,A130,JORDAN3:32;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A102,A105,A108,A109,A126,SCMFSA_7:3;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
case A131:j>len mid(f,i1,1);
then A132:i1+1<=j by A102,NAT_1:38;
A133:(mid(f,i1,1)^(mid(f,len f-'1,i2))).j
=(mid(f,len f-'1,i2)).(j-len mid(f,i1,1))
by A103,A104,A131,JORDAN3:15;
A134:j<=len f+i1-i2 by A99,A104,XCMPLX_1:18;
i2-i1>=0 by A1,SQUARE_1:12;
then len f+0<=len f+(i2-i1) by REAL_1:55;
then len f-(i2-i1)<=len f+(i2-i1)-(i2-i1) by REAL_1:49;
then len f-(i2-i1)<=len f by XCMPLX_1:26;
then len f-i2+i1<=len f by XCMPLX_1:37;
then len f+i1-i2<=len f by XCMPLX_1:29;
then A135:j<=len f by A134,AXIOMS:22;
i1+1<=j by A102,A131,NAT_1:38;
then i1+1-i1<=j-i1 by REAL_1:49;
then A136: 1<=j-i1 by XCMPLX_1:26;
i2+1-1<=len f-1 by A2,REAL_1:49;
then i2<=len f-1 by XCMPLX_1:26;
then i2-i2<=len f-1-i2 by REAL_1:49;
then A137: 0<=len f-'1-i2 by A6,XCMPLX_1:14;
A138: j-i1<=len f+i1-i2-i1 by A100,A104,REAL_1:49;
then A139:j-i1<=len f-i2 by XCMPLX_1:228;
len f-i2<=len f-1 by A2,REAL_1:92;
then j-i1<=len f-'1 by A6,A139,AXIOMS:22;
then A140:j-'i1<=len f-'1 by A102,A131,SCMFSA_7:3;
A141: len f-i2=len f-1+1-i2 by XCMPLX_1:27
.=len f-1-i2+1 by XCMPLX_1:29
.=len f-'1-i2+1 by A5,JORDAN3:1
.=len f-'1-'i2+1 by A137,BINARITH:def 3;
0<j-i1 by A136,AXIOMS:22;
then A142: j-i1 =j-'len mid(f,i1,1) by A102,BINARITH:def 3;
A143: j-len mid(f,i1,1)<=len f-'1-'i2+1
by A102,A138,A141,XCMPLX_1:228;
len f-'1-'(j-'i1)+1=len f-'1-(j-'i1)+1
by A140,SCMFSA_7:3
.=len f-1-(j-i1)+1 by A6,A102,A131,SCMFSA_7:3
.=len f-(j-i1) by XCMPLX_1:229
.=len f-j+i1 by XCMPLX_1:37
.=len f+i1-j by XCMPLX_1:29 .=len f+i1-'j by A135,Th2;
then A144:(mid(f,i1,1)^(mid(f,len f-'1,i2))).j
=f.(len f+i1-'j) by A2,A9,A10,A102,A133,A136,A142,A143,Th24;
A145:len f+i1-j=len f+i1-'j by A106,Th2;
0<i1 by A2,AXIOMS:22;
then len f+0<len f+i1 by REAL_1:67;
then j<len f+i1 by A135,AXIOMS:22;
then j-j<len f+i1-j by REAL_1:54;
then 0<len f+i1-j by XCMPLX_1:14;
then A146:0<len f+i1-'j by A135,Th2;
i1+1<=j by A102,A131,NAT_1:38;
then len f+(i1+1)<=len f+j by AXIOMS:24;
then len f+(i1+1)-1<=len f+j-1 by REAL_1:49;
then len f+i1+1-1<=len f+j-1 by XCMPLX_1:1;
then len f+i1<=len f+j-1 by XCMPLX_1:26;
then len f+i1-j<=len f+j-1-j by REAL_1:49;
then len f+i1-j<=len f-1 by XCMPLX_1:228;
then A147:len f-'1>=len f+i1-'j by A6,A135,Th2;
now per cases;
case A148:(len f+i1-'j) mod (len f -'1)=0;
then len f+i1-'j=len f-'1 by A146,A147,Th9;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A105,A144,A148,Def1;
case A149:(len f+i1-'j) mod (len f -'1)<>0;
then A150:S_Drop(len f+i1-'j,f)
= (len f+i1-'j) mod (len f -'1) by Def1;
len f+(i1+1)<=len f+j by A132,REAL_1:55;
then len f+i1+1<=len f+j by XCMPLX_1:1;
then len f+i1+1-j<=len f+j-j by REAL_1:49;
then len f+i1+1-j<=len f by XCMPLX_1:26;
then len f+i1+1-j-1<=len f-1 by REAL_1:49;
then
A151:len f+i1-j<=len f-'1 by A6,XCMPLX_1:228;
len f+i1-j=len f-'1 implies
contradiction by A145,A149,GR_CY_1:5;
then len f+i1-'j<(len f-'1) by A145,A151,REAL_1:def 5;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j
by A105,A144,A150,GR_CY_1:4;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
end;
hence g.j = (mid(f,i1,1)^mid(f,len f-'1,i2)).j;
end;
hence len g=len f+i1-'i2 & g=mid(f,i1,1)^mid(f,len f-'1,i2)
by A12,A100,A103,Th2,FINSEQ_2:10;
end;
hence len g=len f+i1-'i2 & g=mid(f,i1,1)^mid(f,len f-'1,i2);
end;
hence thesis;
end;
theorem Th41:for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being 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 Nat;
assume A1:g is_a_part>_of f,i1,i2;
then A2:1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))
by Def2;
then A3:1<len f by AXIOMS:22;
A4:i1<len f by A2,NAT_1:38;
A5:len g=len (Rev g) by FINSEQ_5:def 3;
A6:(Rev g).len (Rev g)=(Rev g).len g by FINSEQ_5:def 3
.=g.(len g-len g+1) by A2,JORDAN3:24
.=g.1 by XCMPLX_1:25 .=f.S_Drop((i1+1-'1),f) by A2
.=f.S_Drop(i1,f) by BINARITH:39;
A7:i1>0 by A2,AXIOMS:22;
i1+1-1<=len f-1 by A2,REAL_1:49;
then i1<=len f-1 by XCMPLX_1:26;
then A8:i1<=len f-'1 by A3,SCMFSA_7:3;
A9:now per cases;
case A10:i1 mod (len f-'1)<>0;
then A11:S_Drop(i1,f)=i1 mod (len f-'1) by Def1;
i1 <> len f-'1 by A10,GR_CY_1:5;
then i1<len f-'1 by A8,REAL_1:def 5;
hence (Rev g).len (Rev g)=f.i1 by A6,A11,GR_CY_1:4;
case A12:i1 mod (len f-'1)=0;
then S_Drop(i1,f)=len f-'1 by Def1;
hence (Rev g).len (Rev g)=f.i1 by A6,A7,A8,A12,Th9;
end;
for i being Nat st 1<=i & i<=len (Rev g) holds
(Rev g).i=f.S_Drop(len f +i2-'i,f)
proof let i be Nat;assume A13:1<=i & i<=len (Rev g);
len g<=len g+(i-'1) by NAT_1:29;
then len g<=len g+(i-1) by A13,SCMFSA_7:3;
then len g-(i-1)<=len g+(i-1)-(i-1) by REAL_1:49;
then len g-(i-1)<=len g by XCMPLX_1:26;
then len g-i+1<=len g by XCMPLX_1:37;
then A14:1<=len g-'i+1 & len g-'i+1<=len g
by A5,A13,NAT_1:29,SCMFSA_7:3;
A15:(Rev g).i=g.(len g-i+1) by A5,A13,JORDAN3:24
.=g.(len g-'i+1) by A5,A13,SCMFSA_7:3
.=f.S_Drop((i1+(len g-'i+1)-'1),f) by A1,A14,Def2;
A16:i<len f by A2,A5,A13,AXIOMS:22;
now per cases;
case A17:i1<=i2;
then len f-1+len g=len f-1+(i2-'i1+1) by A1,Th37;
then len f-1+len g=len f-1+(i2-'i1)+1 by XCMPLX_1:1;
then len f-1+len g=len f+(i2-'i1) by XCMPLX_1:227;
then len f-1+len g=len f+(i2-i1) by A17,SCMFSA_7:3;
then len f-1+len g+i1=len f+i2-i1+i1 by XCMPLX_1:29;
then len f-1+(len g+i1)=len f+i2-i1+i1 by XCMPLX_1:1;
then len f+i2-i=len f-1+(i1+len g)-i by XCMPLX_1:27;
then len f+i2-i=len f-1+(i1+len g-i) by XCMPLX_1:29;
then len f+i2-'i=len f-1+(i1+len g-i) by A16,Th2;
then len f+i2-'i=len f-1+(i1+(len g-i)) by XCMPLX_1:29;
then len f+i2-'i=len f-1+(i1+(len g-'i)) by A5,A13,SCMFSA_7:3;
then len f+i2-'i=len f-1+(i1+(len g-'i)+1-1) by XCMPLX_1:26;
then len f+i2-'i=len f-1+(i1+(len g-'i+1)-1) by XCMPLX_1:1;
then len f+i2-'i=len f-1+(i1+(len g-'i+1)-'1) by A2,Th2;
then len f+i2-'i=(i1+(len g-'i+1)-'1)+(len f-'1) by A3,SCMFSA_7:3;
hence (Rev g).i=f.S_Drop(len f +i2-'i,f) by A15,Th35;
case i1>i2; then len g=len f+i2-'i1 by A1,Th38;
then len g+i1=len f+i2-i1+i1 by A4,Th2;
then len f+i2=i1+len g by XCMPLX_1:27;
then len f+i2-'i=i1+len g-i by A5,A13,Th2;
then len f+i2-'i=i1+(len g-i) by XCMPLX_1:29;
then len f+i2-'i=i1+(len g-'i) by A5,A13,SCMFSA_7:3;
then len f+i2-'i=i1+(len g-'i)+1-1 by XCMPLX_1:26;
then len f+i2-'i=i1+(len g-'i+1)-1 by XCMPLX_1:1;
hence (Rev g).i=f.S_Drop(len f +i2-'i,f) by A2,A15,Th2;
end;
hence (Rev g).i=f.S_Drop(len f +i2-'i,f);
end;
hence thesis by A2,A5,A9,Def3;
end;
theorem Th42:for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being 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 Nat;
assume A1:g is_a_part<_of f,i1,i2;
then A2:1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2
& 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds
g.i=f.S_Drop(len f+i1-'i,f)) by Def3;
then A3:1<len f by AXIOMS:22;
A4:i2<len f by A2,NAT_1:38;
A5:len g=len (Rev g) by FINSEQ_5:def 3;
A6:(Rev g).len (Rev g)=(Rev g).len g by FINSEQ_5:def 3
.=g.(len g-len g+1) by A2,JORDAN3:24
.=g.1 by XCMPLX_1:25 .=f.S_Drop(len f+i1-'1,f) by A2
.=f.S_Drop(len f-'1+i1,f) by A3,Th3;
A7:i1>0 by A2,AXIOMS:22;
i1+1-1<=len f-1 by A2,REAL_1:49;
then i1<=len f-1 by XCMPLX_1:26;
then A8:i1<=len f-'1 by A3,SCMFSA_7:3;
A9:S_Drop(len f-'1+i1,f)=S_Drop(i1,f) by Th35;
A10:now per cases;
case A11:i1 mod (len f-'1)<>0;
then A12:S_Drop(i1,f)=i1 mod (len f-'1) by Def1;
i1 <> len f-'1 by A11,GR_CY_1:5;
then i1<len f-'1 by A8,REAL_1:def 5;
hence (Rev g).len (Rev g)=f.i1 by A6,A9,A12,GR_CY_1:4;
case A13:i1 mod (len f-'1)=0;
then S_Drop(i1,f)=len f-'1 by Def1;
hence (Rev g).len (Rev g)=f.i1 by A6,A7,A8,A9,A13,Th9;
end;
for i being Nat st 1<=i & i<=len (Rev g) holds
(Rev g).i=f.S_Drop((i2+i)-'1,f)
proof let i be Nat;assume A14:1<=i & i<=len (Rev g);
len g<=len g+(i-'1) by NAT_1:29;
then len g<=len g+(i-1) by A14,SCMFSA_7:3;
then len g-(i-1)<=len g+(i-1)-(i-1) by REAL_1:49;
then len g-(i-1)<=len g by XCMPLX_1:26;
then len g-i+1<=len g by XCMPLX_1:37;
then A15:1<=len g-'i+1 & len g-'i+1<=len g
by A5,A14,NAT_1:29,SCMFSA_7:3;
A16:(Rev g).i=g.(len g-i+1) by A5,A14,JORDAN3:24
.=g.(len g-'i+1) by A5,A14,SCMFSA_7:3
.=f.S_Drop(len f+i1-'(len g-'i+1),f) by A1,A15,Def3;
A17:len g+1<=len f by A2,NAT_1:38;
len g+1<=len g+1+i by NAT_1:29;
then len g+1-i<=len g+1+i-i by REAL_1:49;
then len g+1-i<=len g+1 by XCMPLX_1:26;
then len g-i+1<=len g+1 by XCMPLX_1:29;
then len g-'i+1<=len g+1 by A5,A14,SCMFSA_7:3;
then A18:len g-'i+1<=len f by A17,AXIOMS:22;
now per cases;
case i1<i2;
then len g=len f+i1-'i2 by A1,Th40;
then A19:len g=len f+i1-i2 by A4,Th2;
len f=len f-'1+1 by A3,AMI_5:4;
then -len f+i2+i=i2+i-(1+(len f-'1)) by XCMPLX_1:155;
then -len f+i2+i=i2+i-1-(len f-'1) by XCMPLX_1:36;
then -len f+i2+i=i2+i-'1-(len f-'1) by A2,Th2;
then i1+-len f-i1+i2+i=i2+i-'1-(len f-'1) by XCMPLX_1:26;
then i1-len f-i1+i2+i=i2+i-'1-(len f-'1) by XCMPLX_0:def 8;
then i1-(len f+i1)+i2+i=i2+i-'1-(len f-'1) by XCMPLX_1:36;
then i1-len g+i=i2+i-'1-(len f-'1) by A19,XCMPLX_1:37;
then i1-(len g-i)=i2+i-'1-(len f-'1) by XCMPLX_1:37;
then i1-(len g-'i)=i2+i-'1-(len f-'1) by A5,A14,SCMFSA_7:3;
then i1+1-(len g-'i)-1=i2+i-'1-(len f-'1) by XCMPLX_1:228;
then i1+1-(len g-'i+1)=i2+i-'1-(len f-'1) by XCMPLX_1:36;
then 1+(i1-(len g-'i+1))=i2+i-'1-(len f-'1) by XCMPLX_1:29;
then len f-'1+(1+(i1-(len g-'i+1)))=len f-'1+(i2+i-'1)-(len f-'1)
by XCMPLX_1:29;
then len f-'1+1+(i1-(len g-'i+1))=len f-'1+(i2+i-'1)-(len f-'1)
by XCMPLX_1:1;
then len f-'1+1+i1-(len g-'i+1)=len f-'1+(i2+i-'1)-(len f-'1)
by XCMPLX_1:29;
then len f+i1-(len g-'i+1)=len f-'1+(i2+i-'1)-(len f-'1)
by A3,AMI_5:4;
then len f+i1-'(len g-'i+1)=len f-'1+(i2+i-'1)-(len f-'1) by A18,Th2;
hence (Rev g).i=f.S_Drop((i2+i)-'1,f) by A16,XCMPLX_1:26;
case A20:i1>=i2;
then len g=i1-'i2+1 by A1,Th39;
then len g=i1-i2+1 by A20,SCMFSA_7:3;
then i1-len g=i1-(i1-i2)-1 by XCMPLX_1:36;
then i1-len g=i2-1 by XCMPLX_1:18;
then i1-len g+i=(i2+i)-1 by XCMPLX_1:29;
then i1-(len g-i)=(i2+i)-1 by XCMPLX_1:37;
then i1-(len g-i)=(i2+i)-'1 by A14,Th2;
then i1-(len g-'i)=(i2+i)-'1 by A5,A14,SCMFSA_7:3;
then len f-1+(i1-(len g-'i))=(i2+i)-'1+(len f-'1) by A3,SCMFSA_7:3;
then len f-1+i1-(len g-'i)=(i2+i)-'1+(len f-'1) by XCMPLX_1:29;
then len f+i1-1-(len g-'i)=(i2+i)-'1+(len f-'1) by XCMPLX_1:29;
then len f+i1-(len g-'i+1)=(i2+i)-'1+(len f-'1) by XCMPLX_1:36;
then (Rev g).i=f.S_Drop((i2+i)-'1+(len f-'1),f) by A16,A18,Th2
.=f.S_Drop((i2+i)-'1,f) by Th35;
hence (Rev g).i=f.S_Drop((i2+i)-'1,f);
end;
hence (Rev g).i=f.S_Drop((i2+i)-'1,f);
end;
hence thesis by A2,A5,A10,Def2;
end;
theorem Th43:for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<=i2 & i2<len f
holds mid(f,i1,i2) is_a_part>_of f,i1,i2
proof let f be non constant standard special_circular_sequence,
i1,i2 be Nat;
assume A1:1<=i1 & i1<=i2 & i2<len f;
then A2:1<=i2 by AXIOMS:22;
then A3:1<len f by A1,AXIOMS:22;
A4:i1<len f by A1,AXIOMS:22;
then A5:i1+1<=len f by NAT_1:38;
A6:i2+1<=len f by A1,NAT_1:38;
A7:mid(f,i1,i2).len mid(f,i1,i2)=f.i2 by A1,Th22;
A8:len mid(f,i1,i2)=i2-'i1+1 by A1,A2,A4,JORDAN3:27;
then A9:1<=len mid(f,i1,i2) by NAT_1:29;
A10:i2-'i1+1=i2-i1+1 by A1,SCMFSA_7:3;
0<i1 by A1,AXIOMS:22;
then i2+1<i2+1+i1 by REAL_1:69;
then i2+1-i1<i2+1+i1-i1 by REAL_1:54;
then i2+1-i1<i2+1 by XCMPLX_1:26;
then len mid(f,i1,i2)<i2+1 by A8,A10,XCMPLX_1:29;
then A11:len mid(f,i1,i2)<len f by A6,AXIOMS:22;
for i being Nat st 1<=i & i<=len mid(f,i1,i2) holds
mid(f,i1,i2).i=f.S_Drop((i1+i)-'1,f)
proof let i be Nat;assume A12: 1<=i & i<=len mid(f,i1,i2);
then i+i1<=i2-i1+1+i1 by A8,A10,AXIOMS:24;
then i1+i<=i2+1 by XCMPLX_1:227;
then i1+i<=len f by A6,AXIOMS:22;
then i1+i-1<=len f-1 by REAL_1:49;
then i1+i-1<=len f-'1 by A3,SCMFSA_7:3;
then A13:i1+i-'1<=len f-'1 by A1,Th2;
1+1<=i1+i by A1,A12,REAL_1:55;
then 1+1-1<=i1+i-1 by REAL_1:49;
then 1<=i1+i-'1 by A1,Th2;
then S_Drop((i1+i)-'1,f)=(i1+i)-'1 by A13,Th34;
hence mid(f,i1,i2).i=f.S_Drop((i1+i)-'1,f) by A1,A2,A4,A12,JORDAN3:27;
end;
hence thesis by A1,A2,A5,A6,A7,A9,A11,Def2;
end;
theorem Th44:for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<=i2 & i2<len f
holds mid(f,i2,i1) is_a_part<_of f,i2,i1
proof let f be non constant standard special_circular_sequence,
i1,i2 be Nat;
assume 1<=i1 & i1<=i2 & i2<len f;
then mid(f,i1,i2) is_a_part>_of f,i1,i2 by Th43;
then Rev mid(f,i1,i2) is_a_part<_of f,i2,i1 by Th41;
hence thesis by Th30;
end;
theorem Th45:for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i2 & i1>i2 & i1<len f
holds mid(f,i1,len f-'1)^mid(f,1,i2) is_a_part>_of f,i1,i2
proof let f be non constant standard special_circular_sequence,
i1,i2 be Nat;assume A1:1<=i2 & i1>i2 & i1<len f;
then A2:1<=i1 by AXIOMS:22;
then A3:1<len f by A1,AXIOMS:22;
A4:i2<len f by A1,AXIOMS:22;
then A5:i2+1<=len f by NAT_1:38;
A6:i1+1<=len f by A1,NAT_1:38;
then i1+1-1<=len f-1 by REAL_1:49;
then i1<=len f-1 by XCMPLX_1:26;
then A7:i1<=len f-'1 by A3,SCMFSA_7:3;
then A8:1<=len f-'1 by A2,AXIOMS:22;
i2+1-1<=len f-1 by A5,REAL_1:49;
then i2<=len f-1 by XCMPLX_1:26;
then A9:i2<=len f-'1 by A3,SCMFSA_7:3;
len f<len f+1 by NAT_1:38;
then len f-1<len f+1-1 by REAL_1:54;
then len f-1<len f by XCMPLX_1:26;
then A10:len f-'1<len f by A3,SCMFSA_7:3;
A11:len (mid(f,i1,len f-'1)^mid(f,1,i2))
=len mid(f,i1,len f-'1)+ len mid(f,1,i2) by FINSEQ_1:35;
A12:len mid(f,1,i2)=len (f|i2) by A1,JORDAN3:25 .=i2 by A4,TOPREAL1:3;
then 0<len mid(f,1,i2) by A1,AXIOMS:22;
then len mid(f,i1,len f-'1)< len mid(f,i1,len f-'1)+ len mid(f,1,i2)
by REAL_1:69;
then A13:(mid(f,i1,len f-'1)^mid(f,1,i2)).len (mid(f,i1,len f-'1)^mid(f,1,i2)
)
=mid(f,1,i2).(len mid(f,i1,len f-'1)+ len mid(f,1,i2)
-len mid(f,i1,len f-'1)) by A11,JORDAN3:15
.=mid(f,1,i2).(len mid(f,1,i2)) by XCMPLX_1:26
.=f.i2 by A1,A4,Th22;
len mid(f,1,i2)<=len (mid(f,i1,len f-'1)^mid(f,1,i2)) by A11,NAT_1:29;
then A14:1<=len (mid(f,i1,len f-'1)^mid(f,1,i2)) by A1,A12,AXIOMS:22;
len mid(f,i1,len f-'1)=len f-'1-'i1+1 by A1,A2,A7,A8,A10,JORDAN3:27
.=len f-'1-i1+1 by A7,SCMFSA_7:3
.=len f-1-i1+1 by A3,SCMFSA_7:3
.=len f-i1 by XCMPLX_1:229;
then A15:len (mid(f,i1,len f-'1)^mid(f,1,i2))=len f-i1 +i2 by A12,FINSEQ_1:35
.=len f-(i1-i2) by XCMPLX_1:37;
i1-i2>0 by A1,SQUARE_1:11;
then len f<len f+(i1-i2) by REAL_1:69;
then len f-(i1-i2)<len f+(i1-i2)-(i1-i2) by REAL_1:54;
then A16:len (mid(f,i1,len f-'1)^mid(f,1,i2))<len f by A15,XCMPLX_1:26;
for i being Nat st 1<=i & i<=len (mid(f,i1,len f-'1)^mid(f,1,i2)) holds
(mid(f,i1,len f-'1)^mid(f,1,i2)).i
=f.S_Drop((i1+i)-'1,f)
proof let i be Nat;assume
A17: 1<=i & i<=len (mid(f,i1,len f-'1)^mid(f,1,i2));
A18:len mid(f,i1,len f-'1)=len f-'1-'i1+1
by A1,A2,A7,A8,A10,JORDAN3:27;
A19: len f-'1-'i1+1=len f-'1-i1+1 by A7,SCMFSA_7:3
.=len f-1-i1+1 by A3,SCMFSA_7:3
.=len f-i1 by XCMPLX_1:229;
A20:len f-i1=len f-'i1 by A1,SCMFSA_7:3;
A21:i1+i-'1=i1+i-1 by A17,Th2;
now per cases;
case A22:i<=len mid(f,i1,len f-'1);
then i in dom mid(f,i1,len f-'1) by A17,FINSEQ_3:27;
then A23:(mid(f,i1,len f-'1)^mid(f,1,i2)).i=mid(f,i1,len f-'1).i
by FINSEQ_1:def 7;
A24:mid(f,i1,len f-'1).i=f.(i1+i-'1)
by A1,A2,A7,A8,A10,A17,A22,JORDAN3:27;
0<=i-1 by A17,SQUARE_1:12;
then A25: 1+0<=i1+(i-1) by A2,REAL_1:55;
i1+i<=i1+(len f-'1-'i1+1) by A18,A22,AXIOMS:24;
then i1+i<=(len f-'1-i1+1)+i1 by A7,SCMFSA_7:3;
then i1+i<=len f-'1+1 by XCMPLX_1:227;
then i1+i<=len f by A3,AMI_5:4;
then i1+i-'1<=len f-1 by A21,REAL_1:49;
then 1<=i1+i-'1 & i1+i-'1<=len f-'1
by A3,A21,A25,SCMFSA_7:3,XCMPLX_1:29;
hence (mid(f,i1,len f-'1)^mid(f,1,i2)).i=f.S_Drop((i1+i)-'1,f)
by A23,A24,Th34;
case A26:i>len mid(f,i1,len f-'1);
A27:len f-i1=len f-'i1 by A1,SCMFSA_7:3;
i>=len f-'i1+1 by A18,A19,A20,A26,NAT_1:38;
then i-(len f-'i1)>=len f-'i1+1-(len f-'i1) by REAL_1:49;
then A28: i-(len f-'i1)>=1 by XCMPLX_1:26;
i<=len f-i1+i2 by A15,A17,XCMPLX_1:37;
then i-(len f-i1)<=len f-i1+i2-(len f-i1) by REAL_1:49;
then i-(len f-'i1)<=i2 by A27,XCMPLX_1:26;
then A29:1<=i-'(len f-'i1) & i-'(len f-'i1)<=i2 by A28,JORDAN3:1;
then A30:i-'(len f-'i1)<=len f-'1 by A9,AXIOMS:22;
A31:(mid(f,i1,len f-'1)^mid(f,1,i2)).i
=mid(f,1,i2).(i-len mid(f,i1,len f-'1)) by A17,A26,JORDAN3:15
.=mid(f,1,i2).(i-'(len f-'i1))
by A18,A19,A20,A26,SCMFSA_7:3
.=f.(i-'(len f-'i1)) by A4,A29,JORDAN3:32;
len f-'1+(i-'(len f-'i1))=len f-'1+(i-(len f-'i1))
by A18,A19,A20,A26,SCMFSA_7:3
.=len f-'1+i-(len f-'i1) by XCMPLX_1:29
.=len f-1+i-(len f-'i1) by A3,SCMFSA_7:3
.=len f-1+i-(len f-i1) by A1,SCMFSA_7:3
.=len f-1+i-len f+i1 by XCMPLX_1:37
.=len f-1-len f+i+i1 by XCMPLX_1:29
.=len f+-1-len f+i+i1 by XCMPLX_0:def 8
.=-1+i+i1 by XCMPLX_1:26
.=-1+(i+i1) by XCMPLX_1:1
.=(i+i1)-1 by XCMPLX_0:def 8
.=i1+i-'1 by A17,Th2;
then S_Drop((i1+i)-'1,f) =S_Drop(i-'(len f-'i1),f) by Th35
.=i-'(len f-'i1) by A29,A30,Th34;
hence (mid(f,i1,len f-'1)^mid(f,1,i2)).i=f.S_Drop((i1+i)-'1,f) by A31;
end;
hence (mid(f,i1,len f-'1)^mid(f,1,i2)).i=f.S_Drop((i1+i)-'1,f);
end;
hence thesis by A1,A2,A5,A6,A13,A14,A16,Def2;
end;
theorem Th46:for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<i2 & i2<len f
holds mid(f,i1,1)^mid(f,len f-'1,i2) is_a_part<_of f,i1,i2
proof let f be non constant standard special_circular_sequence,
i1,i2 be Nat;assume 1<=i1 & i1<i2 & i2<len f;
then A1: mid(f,i2,len f-'1)^mid(f,1,i1) is_a_part>_of f,i2,i1 by Th45;
Rev (mid(f,i2,len f-'1)^mid(f,1,i1))
=Rev(mid(f,1,i1))^Rev(mid(f,i2,len f-'1)) by FINSEQ_5:67
.=mid(f,i1,1)^Rev(mid(f,i2,len f-'1)) by Th30
.=mid(f,i1,1)^mid(f,len f-'1,i2) by Th30;
hence thesis by A1,Th41;
end;
theorem Th47:for h being FinSequence of TOP-REAL 2,i1,i2 st
1<=i1 & i1<=len h & 1<=i2 & i2<=len h holds L~mid(h,i1,i2) c= L~h
proof let h be FinSequence of TOP-REAL 2,i1,i2;
assume A1:1<=i1 & i1<=len h & 1<=i2 & i2<=len h;
thus L~mid(h,i1,i2) c= L~h
proof let x be set;assume
A2: x in L~mid(h,i1,i2);
now per cases;
case A3:i1<=i2;
x in union { LSeg(mid(h,i1,i2),i) : 1 <= i & i+1 <= len mid(h,i1,i2) }
by A2,TOPREAL1:def 6;
then consider Y being set such that A4: x in Y
& Y in { LSeg(mid(h,i1,i2),i) : 1 <= i & i+1 <= len mid(h,i1,i2) }
by TARSKI:def 4;
consider i such that A5:Y=LSeg(mid(h,i1,i2),i)
& (1 <= i & i+1 <= len mid(h,i1,i2)) by A4;
A6:LSeg(mid(h,i1,i2),i)=LSeg(mid(h,i1,i2)/.i,mid(h,i1,i2)/.(i+1))
by A5,TOPREAL1:def 5;
i<=i+1 by NAT_1:29;
then A7:i<=len mid(h,i1,i2) by A5,AXIOMS:22;
then A8:mid(h,i1,i2).i=h.(i+i1-'1) by A1,A3,A5,JORDAN3:27;
A9:len mid(h,i1,i2)=i2-'i1+1 by A1,A3,JORDAN3:27;
A10:1<=i+1 & i+1<=len mid(h,i1,i2) by A5,NAT_1:29;
then A11:mid(h,i1,i2).(i+1)=h.(i+1+i1-'1) by A1,A3,JORDAN3:27;
A12:mid(h,i1,i2)/.i=mid(h,i1,i2).i by A5,A7,FINSEQ_4:24;
A13:mid(h,i1,i2)/.(i+1)=mid(h,i1,i2).(i+1) by A10,FINSEQ_4:24;
1+1<=i+i1 by A1,A5,REAL_1:55;
then A14: 1+1-1<=i+i1-1 by REAL_1:49;
then A15:1<=i+i1-'1 by A1,Th2;
i+1-1<=i2-'i1+1-1 by A5,A9,REAL_1:49;
then i<=i2-'i1+1-1 by XCMPLX_1:26;
then i<=i2-'i1 by XCMPLX_1:26;
then i<=i2-i1 by A3,SCMFSA_7:3;
then i+i1<=i2-i1+i1 by AXIOMS:24;
then A16: i+i1<=i2 by XCMPLX_1:27;
then i+i1<=len h by A1,AXIOMS:22;
then A17:1<=i+i1-'1 & i+i1-'1<=len h by A1,A14,Th2,JORDAN3:7;
then A18:h/.(i+i1-'1)=h.(i+i1-'1) by FINSEQ_4:24;
A19:i+1+i1-'1=i+1+i1-1 by A1,Th2 .=i+i1 by XCMPLX_1:226;
then A20:i+1+i1-'1=i+i1-1+1 by XCMPLX_1:27 .=i+i1-'1+1 by A1,Th2;
i+i1-'1<=i+i1-'1+1 by NAT_1:29;
then i+i1-'1<=i+i1-1+1 by A1,Th2;
then i+i1-'1<=i+i1 by XCMPLX_1:27;
then A21:1<=i+i1 & i+i1<=len h by A1,A16,A17,AXIOMS:22;
then LSeg(mid(h,i1,i2),i)=LSeg(h/.(i+i1-'1),h/.(i+1+i1-'1))
by A6,A8,A11,A12,A13,A18,A19,FINSEQ_4:24
.=LSeg(h,i+i1-'1) by A17,A19,A20,A21,TOPREAL1:def 5;
then LSeg(mid(h,i1,i2),i) in { LSeg(h,j) : 1 <= j & j+1 <= len h}
by A15,A19,A20,A21;
then x in union { LSeg(h,j) : 1 <= j & j+1 <= len h} by A4,A5,TARSKI:def 4
;
hence x in L~h by TOPREAL1:def 6;
case A22:i1>i2;
mid(h,i1,i2)=Rev mid(h,i2,i1) by Th30;
then x in L~mid(h,i2,i1) by A2,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 6;
then consider Y being set such that A23: 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 A24:Y=LSeg(mid(h,i2,i1),i)
& (1 <= i & i+1 <= len mid(h,i2,i1)) by A23;
A25:LSeg(mid(h,i2,i1),i)=LSeg(mid(h,i2,i1)/.i,mid(h,i2,i1)/.(i+1))
by A24,TOPREAL1:def 5;
i<=i+1 by NAT_1:29;
then A26:i<=len mid(h,i2,i1) by A24,AXIOMS:22;
then A27:mid(h,i2,i1).i=h.(i+i2-'1) by A1,A22,A24,JORDAN3:27;
A28:len mid(h,i2,i1)=i1-'i2+1 by A1,A22,JORDAN3:27;
A29:1<=i+1 & i+1<=len mid(h,i2,i1) by A24,NAT_1:29;
then A30:mid(h,i2,i1).(i+1)=h.(i+1+i2-'1) by A1,A22,JORDAN3:27;
A31:mid(h,i2,i1)/.i=mid(h,i2,i1).i by A24,A26,FINSEQ_4:24;
A32:mid(h,i2,i1)/.(i+1)=mid(h,i2,i1).(i+1) by A29,FINSEQ_4:24;
1+1<=i+i2 by A1,A24,REAL_1:55;
then A33: 1+1-1<=i+i2-1 by REAL_1:49;
then A34:1<=i+i2-'1 by A1,Th2;
i+1-1<=i1-'i2+1-1 by A24,A28,REAL_1:49;
then i<=i1-'i2+1-1 by XCMPLX_1:26;
then i<=i1-'i2 by XCMPLX_1:26;
then i<=i1-i2 by A22,SCMFSA_7:3;
then i+i2<=i1-i2+i2 by AXIOMS:24;
then A35: i+i2<=i1 by XCMPLX_1:27;
then A36:i+i2<=len h by A1,AXIOMS:22;
then A37: i+i2-'1<=len h by JORDAN3:7;
A38:1<=i+i2-'1 & i+i2-'1<=len h by A1,A33,A36,Th2,JORDAN3:7;
A39:h/.(i+i2-'1)=h.(i+i2-'1) by A34,A37,FINSEQ_4:24;
A40:i+1+i2-'1=i+1+i2-1 by A1,Th2 .=i+i2 by XCMPLX_1:226;
then A41:i+1+i2-'1=i+i2-1+1 by XCMPLX_1:27 .=i+i2-'1+1 by A1,Th2;
i+i2-'1<=i+i2-'1+1 by NAT_1:29;
then i+i2-'1<=i+i2-1+1 by A1,Th2;
then i+i2-'1<=i+i2 by XCMPLX_1:27;
then A42:1<=i+i2 & i+i2<=len h by A1,A34,A35,AXIOMS:22;
then LSeg(mid(h,i2,i1),i)=LSeg(h/.(i+i2-'1),h/.(i+1+i2-'1))
by A25,A27,A30,A31,A32,A39,A40,FINSEQ_4:24
.=LSeg(h,i+i2-'1) by A38,A40,A41,A42,TOPREAL1:def 5;
then LSeg(mid(h,i2,i1),i) in { LSeg(h,j) : 1 <= j & j+1 <= len h}
by A34,A40,A41,A42;
then x in union { LSeg(h,j) : 1 <= j & j+1 <= len h} by A23,A24,TARSKI:def
4;
hence x in L~h by TOPREAL1:def 6;
end;
hence x in L~h;
end;
end;
theorem Th48: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: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 A2: 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 A3:1<=i1 & i1<=len g & 1<=i2 & i2<=len g &
(g.i1=g.i2 or g/.i1=g/.i2);
then A4:i1 in dom g by FINSEQ_3:27;
A5:i2 in dom g by A3,FINSEQ_3:27;
A6:g/.i1=g.i1 by A3,FINSEQ_4:24;
g/.i2=g.i2 by A3,FINSEQ_4:24;
hence i1=i2 by A2,A3,A4,A5,A6,FUNCT_1:def 8;
end;
end;
(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 A7:(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 A8:x1 in dom g & x2 in dom g & g.x1=g.x2;
then reconsider n1=x1 as Nat;
reconsider n2=x2 as Nat by A8;
A9:1<=n1 & n1<=len g by A8,FINSEQ_3:27;
1<=n2 & n2<=len g by A8,FINSEQ_3:27;
hence x1=x2 by A7,A8,A9;
end;
hence g is one-to-one by FUNCT_1:def 8;
end;
hence thesis by A1;
end;
theorem Th49:for f being non constant standard special_circular_sequence,
i2 st 1<i2 & i2+1<=len f holds f|i2 is_S-Seq
proof let f be non constant standard special_circular_sequence,i2;
assume A1: 1<i2 & i2+1<=len f;
then i2<=len f by NAT_1:38;
then A2:len (f|i2)=i2 by TOPREAL1:3;
then A3:1+1<=len (f|i2) by A1,NAT_1:38;
for i,j st i+1 < j holds LSeg(f|i2,i) misses LSeg(f|i2,j)
proof let i,j;assume A4:i+1 < j;
now per cases;
case A5:1<=i & j+1<=len (f|i2);
then A6:LSeg(f|i2,j)=LSeg(f,j) by SPPOL_2:3;
j<=len (f|i2) by A5,NAT_1:38;
then i+1<=len (f|i2) by A4,AXIOMS:22;
then A7:LSeg(f|i2,i) /\ LSeg(f|i2,j) = LSeg(f,i) /\ LSeg(f,j) by A6,
SPPOL_2:3;
i2<=len f by A1,NAT_1:38;
then len (f|i2)=i2 by TOPREAL1:3;
then j+1<i2+1 by A5,NAT_1:38;
then j+1<len f by A1,AXIOMS:22;
then LSeg(f,i) misses LSeg(f,j) by A4,GOBOARD5:def 4;
then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {} by A7,XBOOLE_0:def 7;
hence LSeg(f|i2,i) misses LSeg(f|i2,j) by XBOOLE_0:def 7;
case A8:1>i or j+1>len (f|i2);
now per cases by A8;
case 1>i;
then LSeg(f|i2,i)={} by TOPREAL1:def 5;
then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {};
hence LSeg(f|i2,i) misses LSeg(f|i2,j) by XBOOLE_0:def 7;
case j+1>len (f|i2);
then LSeg(f|i2,j)={} by TOPREAL1:def 5;
then LSeg(f|i2,i) /\ LSeg(f|i2,j) = {};
hence LSeg(f|i2,i) misses LSeg(f|i2,j) by XBOOLE_0:def 7;
end;
hence LSeg(f|i2,i) misses LSeg(f|i2,j);
end;
hence LSeg(f|i2,i) misses LSeg(f|i2,j);
end;
then A9:f|i2 is s.n.c. by TOPREAL1:def 9;
f|i2 is one-to-one
proof
for n1,n2 being 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 Nat;assume A10: 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);
then A11:n1 in dom (f|i2) by FINSEQ_3:27;
A12:n2 in dom (f|i2) by A10,FINSEQ_3:27;
now per cases by REAL_1:def 5;
case A13:n1<n2;
n2+1<=i2+1 by A2,A10,AXIOMS:24;
then n2+1<=len f by A1,AXIOMS:22;
then A14:n2<len f by NAT_1:38;
len f>4 by GOBOARD7:36;
then A15:f/.n1<>f/.n2 by A10,A13,A14,GOBOARD7:37;
A16:(f|i2)/.n1=f/.n1 by A11,TOPREAL1:1;
A17:(f|i2)/.n2=f/.n2 by A12,TOPREAL1:1;
(f|i2)/.n1=(f|i2).n1 by A10,FINSEQ_4:24;
hence contradiction by A10,A15,A16,A17,FINSEQ_4:24;
case n1=n2;
hence n1=n2;
case A18:n2<n1;
n1+1<=i2+1 by A2,A10,AXIOMS:24;
then n1+1<=len f by A1,AXIOMS:22;
then A19:n1<len f by NAT_1:38;
len f>4 by GOBOARD7:36;
then A20:f/.n2<>f/.n1 by A10,A18,A19,GOBOARD7:37;
A21:(f|i2)/.n2=f/.n2 by A12,TOPREAL1:1;
A22:(f|i2)/.n1=f/.n1 by A11,TOPREAL1:1;
(f|i2)/.n2=(f|i2).n2 by A10,FINSEQ_4:24;
hence contradiction by A10,A20,A21,A22,FINSEQ_4:24;
end;
hence n1=n2;
end;
hence thesis by Th48;
end;
hence thesis by A3,A9,TOPREAL1:def 10;
end;
theorem Th50:for f being non constant standard special_circular_sequence,
i2 st 1<=i2 & i2+1<len f holds f/^i2 is_S-Seq
proof let f be non constant standard special_circular_sequence,i2;
assume A1: 1<=i2 & i2+1<len f;
then A2:i2<len f by NAT_1:38;
then A3:len (f/^i2)=len f-i2 by RFINSEQ:def 2;
i2+1-i2<len f-i2 by A1,REAL_1:54;
then 1<len (f/^i2) by A3,XCMPLX_1:26;
then A4:1+1<=len (f/^i2) by NAT_1:38;
for i,j st i+1 < j holds LSeg(f/^i2,i) misses LSeg(f/^i2,j)
proof let i,j;assume A5:i+1 < j;
then A6:i<j by NAT_1:38;
now per cases;
case A7:1<=i & j<len (f/^i2); then 1<j by A6,AXIOMS:22;
then A8:LSeg(f/^i2,j)=LSeg(f,i2+j) by A2,SPPOL_2:4;
A9:j<len f-i2 by A2,A7,RFINSEQ:def 2;
A10:LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = LSeg(f,i2+i) /\ LSeg(f,i2+j)
by A2,A7,A8,SPPOL_2:4;
i2+(i+1)<i2+j by A5,REAL_1:53;
then A11:i2+i+1<i2+j by XCMPLX_1:1;
A12: 1+1<=i2+i by A1,A7,REAL_1:55;
j+i2<len f-i2+i2 by A9,REAL_1:53;
then 1<i2+i & i2+j<len f by A12,AXIOMS:22,XCMPLX_1:27;
then LSeg(f,i2+i) misses LSeg(f,i2+j) by A11,GOBOARD5:def 4;
then LSeg(f,i2+i) /\ LSeg(f,i2+j) = {} by XBOOLE_0:def 7;
hence LSeg(f/^i2,i) misses LSeg(f/^i2,j) by A10,XBOOLE_0:def 7;
case A13:1>i or j>=len (f/^i2);
now per cases by A13;
case 1>i;
then LSeg(f/^i2,i)={} by TOPREAL1:def 5;
then LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = {};
hence LSeg(f/^i2,i) misses LSeg(f/^i2,j) by XBOOLE_0:def 7;
case j>=len (f/^i2);
then j+1>len (f/^i2) by NAT_1:38;
then LSeg(f/^i2,j)={} by TOPREAL1:def 5;
then LSeg(f/^i2,i) /\ LSeg(f/^i2,j) = {};
hence LSeg(f/^i2,i) misses LSeg(f/^i2,j) by XBOOLE_0:def 7;
end;
hence LSeg(f/^i2,i) misses LSeg(f/^i2,j);
end;
hence LSeg(f/^i2,i) misses LSeg(f/^i2,j);
end;
then A14:f/^i2 is s.n.c. by TOPREAL1:def 9;
f/^i2 is one-to-one
proof
for n1,n2 being 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 Nat;assume A15: 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);
then A16:n1 in dom (f/^i2) by FINSEQ_3:27;
A17:n2 in dom (f/^i2) by A15,FINSEQ_3:27;
now per cases by REAL_1:def 5;
case A18:n1<n2;
A19: n2+i2<=len f-i2+i2 by A3,A15,AXIOMS:24;
A20:i2+1<=i2+n1 by A15,AXIOMS:24;
1<i2+1 by A1,NAT_1:38;
then A21:1<i2+n1 by A20,AXIOMS:22;
A22:i2+n1<i2+n2 by A18,REAL_1:53;
i2+n2<=len f by A19,XCMPLX_1:27;
then A23:f/.(i2+n1)<>f/.(i2+n2) by A21,A22,GOBOARD7:39;
A24:(f/^i2)/.n1=f/.(i2+n1) by A16,FINSEQ_5:30;
A25:(f/^i2)/.n2=f/.(i2+n2) by A17,FINSEQ_5:30;
(f/^i2)/.n1=(f/^i2).(n1) by A15,FINSEQ_4:24;
hence contradiction by A15,A23,A24,A25,FINSEQ_4:24;
case n1=n2;
hence n1=n2;
case A26:n2<n1;
A27: n1+i2<=len f-i2+i2 by A3,A15,AXIOMS:24;
A28:i2+1<=i2+n2 by A15,AXIOMS:24;
1<i2+1 by A1,NAT_1:38;
then A29:1<i2+n2 by A28,AXIOMS:22;
A30:i2+n2<i2+n1 by A26,REAL_1:53;
i2+n1<=len f by A27,XCMPLX_1:27;
then A31:f/.(i2+n2)<>f/.(i2+n1) by A29,A30,GOBOARD7:39;
n2 in dom (f/^i2) by A15,FINSEQ_3:27;
then A32:(f/^i2)/.n2=f/.(i2+n2) by FINSEQ_5:30;
n1 in dom (f/^i2) by A15,FINSEQ_3:27;
then A33:(f/^i2)/.n1=f/.(i2+n1) by FINSEQ_5:30;
(f/^i2)/.n2=(f/^i2).n2 by A15,FINSEQ_4:24;
hence contradiction by A15,A31,A32,A33,FINSEQ_4:24;
end;
hence n1=n2;
end;
hence thesis by Th48;
end;
hence thesis by A4,A14,TOPREAL1:def 10;
end;
theorem Th51:for f being non constant standard special_circular_sequence,
i1,i2 st 1<=i1 & i1<i2 & i2+1<=len f holds mid(f,i1,i2) is_S-Seq
proof let f be non constant standard special_circular_sequence,
i1,i2;assume A1:1<=i1 & i1<i2 & i2+1<=len f;
then A2:1<i2 by AXIOMS:22;
A3:i2<len f by A1,NAT_1:38;
i1<i1+1 by NAT_1:38; then i1-1<i1+1-1 by REAL_1:54;
then i1-1<i1 by XCMPLX_1:26; then i1-1<i2 by A1,AXIOMS:22;
then A4: i1-'1<i2 by A1,SCMFSA_7:3;
A5:i2-'i1+1=i2-i1+1 by A1,SCMFSA_7:3 .=i2-(i1-1) by XCMPLX_1:37
.=i2-(i1-'1) by A1,SCMFSA_7:3.=i2-'(i1-'1)
by A4,SCMFSA_7:3;
mid(f,i1,i2)=(f/^(i1-'1))|(i2-'i1+1) by A1,JORDAN3:def 1;
then A6:mid(f,i1,i2)=(f|i2)/^(i1-'1) by A5,JORDAN3:21;
A7:f|i2 is_S-Seq by A1,A2,Th49;
len (f|i2)=i2 by A3,TOPREAL1:3;
then i1-1+1<len (f|i2) by A1,XCMPLX_1:27;
then i1-'1+1<len (f|i2) by A1,SCMFSA_7:3;
hence thesis by A6,A7,Th19;
end;
theorem Th52:for f being non constant standard special_circular_sequence,
i1,i2 st 1<i1 & i1<i2 & i2<=len f holds mid(f,i1,i2) is_S-Seq
proof let f be non constant standard special_circular_sequence,
i1,i2;assume A1:1<i1 & i1<i2 & i2<=len f;
then A2:i1<len f by AXIOMS:22;
i2-i1>0 by A1,SQUARE_1:11;
then i2-'i1>0 by BINARITH:def 3;
then A3: i2-'i1>=0+1 by NAT_1:38;
1+1<=i1 by A1,NAT_1:38;
then 1+1-1<=i1-1 by REAL_1:49;
then A4:1<=i1-'1 by JORDAN3:1;
A5:i1-'1+1<len f by A1,A2,AMI_5:4;
i1<i1+1 by NAT_1:38; then i1-1<i1+1-1 by REAL_1:54;
then i1-1<i1 by XCMPLX_1:26; then i1-1<i2 by A1,AXIOMS:22;
then A6:i1-'1<i2 by A1,SCMFSA_7:3;
A7: mid(f,i1,i2)=(f/^(i1-'1))|(i2-'i1+1) by A1,JORDAN3:def 1;
A8:i1-'1+1<len f by A1,A2,AMI_5:4;
A9:f/^(i1-'1) is_S-Seq by A4,A5,Th50;
i1-'1<len f by A1,A6,AXIOMS:22;
then A10:len (f/^(i1-'1))=len f-(i1-'1) by RFINSEQ:def 2;
A11: i1-'1+1-(i1-'1)<len f-(i1-'1) by A8,REAL_1:54;
i2-(i1-'1)<=len f-(i1-'1) by A1,REAL_1:49;
then i2-(i1-1)<=len (f/^(i1-'1)) by A1,A10,SCMFSA_7:3;
then i2-i1+1<=len (f/^(i1-'1)) by XCMPLX_1:37;
then A12:1<=1 & 1<=len (f/^(i1-'1)) & 1<=i2-'i1+1
& i2-'i1+1<=len (f/^(i1-'1)) & 1<>i2-'i1+1
by A3,A10,A11,JORDAN3:1,NAT_1:38,XCMPLX_1:26;
then mid(f/^(i1-'1),1,i2-'i1+1) is_S-Seq by A9,JORDAN3:39;
hence thesis by A7,A12,JORDAN3:25;
end;
theorem Th53: for p0,p,q1,q2 being Point of TOP-REAL 2 st
p0 in LSeg(p,q1) & p0 in LSeg(p,q2) & p<>p0 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 A1: p0 in LSeg(p,q1) & p0 in LSeg(p,q2) & p<>p0;
then p0 in { (1-r)*p + r*q1: 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that A2: p0=(1-r)*p + r*q1 &( 0 <= r & r <= 1);
p0 in { (1-s)*p + s*q2: 0 <= s & s <= 1 } by A1,TOPREAL1:def 4;
then consider s such that A3: p0=(1-s)*p + s*q2 &( 0 <= s & s <= 1);
A4:1-r>=0 by A2,SQUARE_1:12;
A5:1-s>=0 by A3,SQUARE_1:12;
A6:p0-(1-r)*p=r*q1 by A2,EUCLID:52;
A7:p0-r*q1=(1-r)*p by A2,EUCLID:52;
A8:p0-(1-s)*p=s*q2 by A3,EUCLID:52;
A9:p0-s*q2=(1-s)*p by A3,EUCLID:52;
A10:now assume r=s;
then r*q1+((1-r)*p-(1-r)*p) =r*q2+(1-r)*p-(1-r)*p by A2,A3,EUCLID:49;
then r*q1+0.REAL 2 =r*q2+(1-r)*p-(1-r)*p by EUCLID:46;
then r*q1+0.REAL 2 =r*q2 by EUCLID:52;
then A11:r*q1=r*q2 by EUCLID:31;
A12:q1 in LSeg(p,q1) by TOPREAL1:6;
now per cases;
case r<>0;
hence q1 in LSeg(p,q2) or q2 in LSeg(p,q1) by A11,A12,EUCLID:38;
case r=0; then p0=(1-0)*p+0.REAL 2 by A2,EUCLID:33;
then p0=(1-0)*p by EUCLID:31;
hence contradiction by A1,EUCLID:33;
end;
hence q1 in LSeg(p,q2) or q2 in LSeg(p,q1);
end;
now assume A13: r<>s;
now per cases by A13,REAL_1:def 5;
case A14:r<s;
(1-r)*p0-(1-r)*((1-s)*p)=(1-r)*(s*q2) by A8,EUCLID:53;
then (1-r)*p0-((1-r)*(1-s))*p=(1-r)*(s*q2) by EUCLID:34;
then (1-r)*p0-((1-r)*(1-s))*p=((1-r)*s)*q2 by EUCLID:34;
then (1-r)*p0-(1-s)*((1-r)*p)=((1-r)*s)*q2 by EUCLID:34;
then (1-r)*p0-((1-s)*p0-(1-s)*(r*q1))=((1-r)*s)*q2 by A7,EUCLID:53;
then (1-r)*p0-(1-s)*p0+(1-s)*(r*q1)=((1-r)*s)*q2 by EUCLID:51;
then ((1-r)-(1-s))*p0+(1-s)*(r*q1)=((1-r)*s)*q2 by EUCLID:54;
then ((1-r)-1+s)*p0+(1-s)*(r*q1)=((1-r)*s)*q2 by XCMPLX_1:37;
then (s+(1-r)-1)*p0+(1-s)*(r*q1)=((1-r)*s)*q2 by XCMPLX_1:29;
then (s+1-r-1)*p