Copyright (c) 1996 Association of Mizar Users
environ
vocabulary ARYTM_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_5, RFINSEQ, BOOLE,
EUCLID, TOPREAL1, TARSKI, PRE_TOPC, MCART_1, SPPOL_2, GROUP_2, SQUARE_1,
ARYTM_3, JORDAN3, FINSEQ_4, ORDINAL2, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, XREAL_0,
XCMPLX_0, REAL_1, NAT_1, RFINSEQ, BINARITH, RELAT_1, FUNCT_1, FINSEQ_1,
FINSEQ_4, FINSEQ_5, CQC_SIM1, STRUCT_0, TOPREAL1, PRE_TOPC, EUCLID,
SPPOL_2;
constructors GOBOARD9, BINARITH, RFINSEQ, REAL_1, REALSET1, FINSEQ_4,
CQC_SIM1, MEMBERED;
clusters SUBSET_1, STRUCT_0, RELSET_1, FUNCT_1, EUCLID, SPPOL_2, FINSEQ_5,
XREAL_0, ARYTM_3, MEMBERED, ORDINAL2, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
theorems TARSKI, AXIOMS, TOPREAL1, FINSEQ_1, FINSEQ_4, RFINSEQ, SPPOL_1,
FUNCT_1, NAT_1, REAL_1, REAL_2, GOBOARD9, BINARITH, SQUARE_1, TOPREAL3,
SPPOL_2, FINSEQ_5, EUCLID, FINSEQ_6, RLVECT_1, ZFMISC_1, SCMFSA_7,
FINSEQ_3, RELAT_1, CQC_SIM1, PARTFUN2, AMI_5, XBOOLE_0, XBOOLE_1,
FINSEQ_2, XCMPLX_0, XCMPLX_1;
begin
::-------------------------------------------:
:: Preliminaries :
::-------------------------------------------:
reserve i,i1,i2,n for natural number;
theorem Th1:
i-'i1>=1 or i-i1>=1 implies i-'i1=i-i1
proof
assume A1: i-'i1>=1 or i-i1>=1;
per cases by A1;
suppose A2:i-'i1>=1;
now assume not i-i1>=0; then i-'i1=0 by BINARITH:def 3;
hence contradiction by A2;
end;
hence thesis by BINARITH:def 3;
suppose i-i1>=1;
then 0<=i-i1 by AXIOMS:22;
hence thesis by BINARITH:def 3;
end;
theorem Th2:n-'0=n
proof n>=0 by NAT_1:18;
then n-'0=n-0 by BINARITH:def 3 .=n;
hence thesis;
end;
theorem i1-i2<=i1-'i2
proof
i1-i2>=0 or i1-i2<0;
hence thesis by BINARITH:def 3;
end;
theorem Th4: i1<=i2 implies n-'i2<=n-'i1
proof assume A1:i1<=i2;
per cases;
suppose A2:i2<=n; then i1<=n by A1,AXIOMS:22;
then A3:n-'i1=n-i1 by SCMFSA_7:3;
n-'i2=n-i2 by A2,SCMFSA_7:3;
hence n-'i2<=n-'i1 by A1,A3,REAL_2:106;
suppose i2>n; then n-i2<0 by REAL_2:105; then n-'i2=0 by BINARITH:def 3;
hence n-'i2<=n-'i1 by NAT_1:18;
end;
theorem Th5: i1<=i2 implies i1-'n<=i2-'n
proof assume A1:i1<=i2;
per cases;
suppose A2:i1-n>=0; then A3:i1-'n=i1-n by BINARITH:def 3;
i1-n<=i2-n by A1,REAL_1:49;
hence thesis by A2,A3,BINARITH:def 3;
suppose i1-n<0; then i1-'n=0 by BINARITH:def 3;
hence thesis by NAT_1:18;
end;
theorem Th6:i-'i1>=1 or i-i1>=1 implies i-'i1+i1=i
proof assume i-'i1>=1 or i-i1>=1;
then i-'i1+i1=i-i1+i1 by Th1 .=i by XCMPLX_1:27;
hence thesis;
end;
theorem Th7:i1<=i2 implies i1-'1<=i2
proof assume A1:i1<=i2;
per cases;
suppose i1-1>=0; then i1-'1=i1-1 by BINARITH:def 3;
then i1-'1<=i1-1+1 by NAT_1:37;
then i1-'1<=i1 by XCMPLX_1:27;
hence i1-'1<=i2 by A1,AXIOMS:22;
suppose i1-1<0; then i1-'1=0 by BINARITH:def 3;
hence i1-'1<=i2 by NAT_1:18;
end;
theorem Th8:i-'2=i-'1-'1
proof
per cases;
suppose A1:i>=2; then A2: i-2>=0 by SQUARE_1:12;
1<=i by A1,AXIOMS:22;
then i-1>=0 by SQUARE_1:12;
then A3:i-'1=i-1 by BINARITH:def 3;
i-1>=1+1-1 by A1,REAL_1:49;
then i-1-1>=1-1 by REAL_1:49;
then i-'1-'1 = i-1-1 by A3,BINARITH:def 3
.=i-(1+1) by XCMPLX_1:36 .=i-2;
hence thesis by A2,BINARITH:def 3;
suppose A4:i<2; then i-2<2-2 by REAL_1:54;
then A5:i-'2=0 by BINARITH:def 3;
i+1<=2 by A4,NAT_1:38; then i+1-1<=1+1-1 by REAL_1:49;
then A6:i<=1 by XCMPLX_1:26;
now per cases;
case 1<=i; then i=1 by A6,AXIOMS:21;
then A7:i-'1-'1=0-'1 by GOBOARD9:1;
0<=0-'1 by NAT_1:18;
hence thesis by A5,A7,GOBOARD9:2;
case i<1; then i-1<1-1 by REAL_1:54;
then A8:i-'1-'1=0-'1 by BINARITH:def 3;
0<=0-'1 by NAT_1:18;
hence thesis by A5,A8,GOBOARD9:2;
end;
hence thesis;
end;
theorem Th9:
i1+1<=i2 implies i1-'1<i2 & i1-'2<i2 & i1<=i2
proof assume
A1: i1+1<=i2;
then i1+1<i2+1 by NAT_1:38;
then i1+1-1<i2+1-1 by REAL_1:54;
then A2: i1<i2+1-1 by XCMPLX_1:26;
A3: i1<i2 by A1,NAT_1:38;
i1-'1<=i1 by GOBOARD9:2;
hence A4:i1-'1<i2 by A3,AXIOMS:22;
A5:i1-'1-'1=i1-'2 by Th8;
i1-'1-'1<=i1-'1 by GOBOARD9:2;
hence i1-'2<i2 by A4,A5,AXIOMS:22;
thus thesis by A2,XCMPLX_1:26;
end;
theorem Th10:i1+2<=i2 or i1+1+1<=i2
implies i1+1<i2 & i1+1-'1<i2 & i1+1-'2<i2 & i1+1<=i2 &
i1-'1+1<i2 & i1-'1+1-'1<i2 &
i1<i2 & i1-'1<i2 & i1-'2<i2 & i1<=i2
proof assume A1: i1+2<=i2 or i1+1+1<=i2;
i1+2<=i2 implies i1+(1+1)<=i2;
then i1+1+1<=i2 by A1,XCMPLX_1:1;
hence A2:i1+1<i2 & i1+1-'1<i2 & i1+1-'2<i2 & i1+1<=i2 by Th9,NAT_1:38;
i1-'1<=i1 by GOBOARD9:2; then i1-'1+1<=i1+1 by AXIOMS:24;
then A3:i1-'1+1<i2 by A2,AXIOMS:22;
i1-'1+1-'1<=i1-'1+1 by GOBOARD9:2;
hence i1-'1+1<i2 & i1-'1+1-'1<i2 by A3,AXIOMS:22;
thus i1<i2 & i1-'1<i2 & i1-'2<i2 & i1<=i2 by A2,Th9,NAT_1:38;
end;
theorem Th11:i1<=i2 or i1<=i2-'1
implies i1<i2+1 & i1<=i2+1 & i1<i2+1+1 & i1<=i2+1+1 & i1<i2+2 & i1<=i2+2
proof assume A1:i1<=i2 or i1<=i2-'1;
A2:now assume i1<=i2;
then A3:i1<i2+1 by NAT_1:38;
i2+1+1=i2+(1+1) by XCMPLX_1:1;
hence i1<i2+1 & i1<=i2+1 & i1<i2+1+1 & i1<=i2+1+1 & i1<i2+2 & i1<=i2+2
by A3,NAT_1:38;
end;
now assume A4:i1<=i2-'1;
i2-'1<=i2 by GOBOARD9:2;
hence i1<i2+1 & i1<=i2+1 & i1<i2+1+1 & i1<=i2+1+1 & i1<i2+2 & i1<=i2+2
by A2,A4,AXIOMS:22;
end;
hence thesis by A1,A2;
end;
theorem Th12:i1<i2 or i1+1<=i2 implies i1<=i2-'1
proof assume A1:i1<i2 or i1+1<=i2;
per cases by A1;
suppose A2:i1<i2; then i1+1<=i2 by NAT_1:38; then i1+1-1<=i2-1 by REAL_1:49;
then A3:i1<=i2-1 by XCMPLX_1:26;
0<=i1 by NAT_1:18; then 0+1<=i2 by A2,NAT_1:38;
hence i1<=i2-'1 by A3,SCMFSA_7:3;
suppose A4:i1+1<=i2; then i1+1-1<=i2-1 by REAL_1:49;
then A5:i1<=i2-1 by XCMPLX_1:26;
0<=i1 by NAT_1:18;
then 0<i2 by A4,NAT_1:38;
then 0+1<=i2 by NAT_1:38;
hence i1<=i2-'1 by A5,SCMFSA_7:3;
end;
theorem Th13:i>=i1 implies i>=i1-'i2
proof assume A1:i>=i1;
i1>=i1-'i2 by GOBOARD9:2;
hence thesis by A1,AXIOMS:22;
end;
theorem
1<=i & 1<=i1-'i implies i1-'i<i1
proof assume A1:1<=i & 1<=i1-'i;
then A2:i1-i=(i1-'i)+i-i by Th6 .=i1-'i by XCMPLX_1:26;
A3:i>0 by A1,AXIOMS:22;
i1-(i1-'i) = i by A2,XCMPLX_1:18;
hence thesis by A3,REAL_2:106;
end;
reserve r,r1,r2 for Real;
reserve n,i,i1,i2,j,j1,j2 for Nat;
reserve D for non empty set;
theorem Th15:for p,q being FinSequence st len p<i
& (i<=len p +len q or i<=len (p^q)) holds
(p^q).i=q.(i-len p)
proof let p,q be FinSequence;assume A1:len p<i &
(i<=len p +len q or i<=len (p^q));
then len p +1<=i by NAT_1:38; then len p +1-len p<=i-len p by REAL_1:49;
then A2:1<=i-len p by XCMPLX_1:26;
then A3:0<=i-len p by AXIOMS:22;
then A4:i-len p=i-'len p by BINARITH:def 3;
A5:len p+(i-'len p)=len p+(i-len p) by A3,BINARITH:def 3 .=i by XCMPLX_1:27;
i<=len p + len q by A1,FINSEQ_1:35;
then i-len p<=len p+len q -len p by REAL_1:49;
then i-len p<=len q by XCMPLX_1:26;
then i-'len p in dom q by A2,A4,FINSEQ_3:27;
then (p^q).(len p+(i-'len p))=q.(i-'len p) by FINSEQ_1:def 7;
hence thesis by A3,A5,BINARITH:def 3;
end;
theorem Th16:
for x being set,f being FinSequence holds
(f^<*x*>).(len f +1)=x & (<*x*>^f).1=x
proof let x be set,f be FinSequence;
1<=len <*x*> by FINSEQ_1:56;
then A1:1 in dom <*x*> by FINSEQ_3:27;
then A2:(f^<*x*>).(len f +1)=<*x*>.1 by FINSEQ_1:def 7 .=x by FINSEQ_1:def 8;
(<*x*>^f).1=<*x*>.1 by A1,FINSEQ_1:def 7.=x by FINSEQ_1:def 8;
hence thesis by A2;
end;
theorem Th17:for x being set,f being FinSequence of D st 1<=len f holds
(f^<*x*>).1=f.1 & (f^<*x*>).1=f/.1 &
(<*x*>^f).(len f +1)=f.len f & (<*x*>^f).(len f +1)=f/.len f
proof let x be set,f be FinSequence of D;assume A1:1<=len f;
then 1 in dom f by FINSEQ_3:27;
then A2:(f^<*x*>).1=f.1 by FINSEQ_1:def 7;
A3:len f in dom f by A1,FINSEQ_3:27;
(<*x*>^f).(len f +1)
=(<*x*>^f).(len <*x*>+len f) by FINSEQ_1:56
.=f.len f by A3,FINSEQ_1:def 7;
hence thesis by A1,A2,FINSEQ_4:24;
end;
theorem Th18:for f being FinSequence st len f=1 holds Rev f=f
proof let f be FinSequence;
assume len f=1;
then f=<*f.1*> by FINSEQ_1:57;
hence Rev f=f by FINSEQ_5:63;
end;
theorem Th19:for f being FinSequence of D,k being Nat holds
len (f/^k)=len f-'k
proof let f be FinSequence of D,k be Nat;
per cases;
suppose A1:k<=len f; then len f-'k=len f-k by SCMFSA_7:3;
hence len (f/^k)=len f-'k by A1,RFINSEQ:def 2;
suppose A2:k>len f; then (f/^k)=<*>D by RFINSEQ:def 2;
then A3:len (f/^k)=0 by FINSEQ_1:32;
len f-k<0 by A2,REAL_2:105;
hence len (f/^k)=len f-'k by A3,BINARITH:def 3;
end;
theorem Th20:
for D being set
for f being FinSequence of D,k being Nat st
k<=n holds (f|n).k=f.k
proof let D be set;
let f be FinSequence of D,k be Nat;
assume
A1: k<=n;
per cases by RLVECT_1:99;
suppose
A2: k = 0;
then A3: not k in dom f by FINSEQ_3:27;
not k in dom(f|n) by A2,FINSEQ_3:27;
hence (f|n).k = {} by FUNCT_1:def 4 .= f.k by A3,FUNCT_1:def 4;
suppose 1 <= k;
then k in Seg n by A1,FINSEQ_1:3;
then (f|Seg n).k=f.k by FUNCT_1:72;
hence (f|n).k=f.k by TOPREAL1:def 1;
end;
theorem Th21:for f being FinSequence of D,l1,l2 being Nat holds
(f/^l1)|(l2-'l1)=(f|l2)/^l1
proof let f be FinSequence of D,l1,l2 be Nat;
A1:now assume A2:l1<=l2;
now per cases;
case A3:l2<=len f;
then A4:l1<=len f by A2,AXIOMS:22;
then A5:len (f/^l1)=len f-l1 by RFINSEQ:def 2;
A6:l1<=len (f|l2) by A2,A3,TOPREAL1:3;
l2-l1<=len f-l1 by A3,REAL_1:49;
then A7:l2-'l1<=len (f/^l1) by A2,A5,SCMFSA_7:3;
then A8:len ((f/^l1)|(l2-'l1)) = l2-'l1 by TOPREAL1:3;
A9:len ((f|l2)/^l1)=len (f|l2)-l1 by A6,RFINSEQ:def 2
.=l2-l1 by A3,TOPREAL1:3
.=l2-'l1 by A2,SCMFSA_7:3;
for k being Nat st 1<=k & k<=len ((f|l2)/^l1) holds
((f/^l1)|(l2-'l1)).k=((f|l2)/^l1).k
proof let k be Nat such that
A10: 1<=k and
A11: k<=len ((f|l2)/^l1);
A12:k<=len (f/^l1) by A7,A9,A11,AXIOMS:22;
A13:k in Seg (l2-'l1) by A9,A10,A11,FINSEQ_1:3;
A14:k in dom (f/^l1) by A10,A12,FINSEQ_3:27;
k<=l2-l1 by A2,A9,A11,SCMFSA_7:3; then k+l1<=l2-l1+l1 by AXIOMS:24;
then A15:k+l1<=l2 by XCMPLX_1:27;
A16:k in dom ((f|l2)/^l1) by A10,A11,FINSEQ_3:27;
((f/^l1)|(l2-'l1)).k
=((f/^l1)|Seg (l2-'l1)).k by TOPREAL1:def 1
.=(f/^l1).k by A13,FUNCT_1:72
.=f.(k+l1) by A4,A14,RFINSEQ:def 2
.=(f|l2).(k+l1) by A15,Th20
.=((f|l2)/^l1).k by A6,A16,RFINSEQ:def 2;
hence ((f/^l1)|(l2-'l1)).k=((f|l2)/^l1).k;
end;
hence (f/^l1)|(l2-'l1)=(f|l2)/^l1 by A8,A9,FINSEQ_1:18;
case A17:l2>len f;
then A18:f|l2=f by TOPREAL1:2;
len (f/^l1)=len f-'l1 by Th19;
then len (f/^l1)<=l2-'l1 by A17,Th5;
hence (f/^l1)|(l2-'l1)=(f|l2)/^l1 by A18,TOPREAL1:2;
end;
hence (f/^l1)|(l2-'l1)=(f|l2)/^l1;
end;
now assume A19:l1>l2; then l1-l1>l2-l1 by REAL_1:54;
then 0>l2-l1 by XCMPLX_1:14; then l2-'l1=0 by BINARITH:def 3;
then (f/^l1)|(l2-'l1) =(f/^l1)|({} NAT) by FINSEQ_1:4,TOPREAL1:def 1;
then dom ((f/^l1)|(l2-'l1)) =dom (f/^l1) /\ ({} NAT) by FUNCT_1:68
.=({} NAT);
then A20:(f/^l1)|(l2-'l1)=<*>(D) by FINSEQ_1:26;
now per cases;
case l1<=len f; then l2<len f by A19,AXIOMS:22;
then l1>len (f|l2) by A19,TOPREAL1:3;
hence (f/^l1)|(l2-'l1)=(f|l2)/^l1 by A20,FINSEQ_5:35;
case A21:l1>len f;
len (f|l2)<=len f by FINSEQ_5:18;
then l1>len (f|l2) by A21,AXIOMS:22;
hence (f/^l1)|(l2-'l1)=(f|l2)/^l1 by A20,FINSEQ_5:35;
end;
hence (f/^l1)|(l2-'l1)=(f|l2)/^l1;
end;
hence (f/^l1)|(l2-'l1)=(f|l2)/^l1 by A1;
end;
begin
::-------------------------------------------:
:: Middle Function for Finite Sequences :
::-------------------------------------------:
definition let D; let f be FinSequence of D,k1,k2 be Nat;
func mid(f,k1,k2) -> FinSequence of D equals
:Def1:(f/^(k1-'1))|(k2-'k1+1) if k1<=k2
otherwise Rev ((f/^(k2-'1))|(k1-'k2+1));
correctness;
end;
theorem Th22:for f being FinSequence of D,k1,k2 being Nat
st 1<=k1 & k1<=len f & 1<=k2 & k2<=len f
holds Rev mid(f,k1,k2)=mid(Rev f,len f-'k2+1,len f-'k1+1)
proof let f be FinSequence of D,k1,k2 be Nat;
assume A1: 1<=k1 & k1<=len f & 1<=k2 & k2<=len f;
per cases;
suppose A2:k1<=k2;
A3:len f-'k1=len f-k1 by A1,SCMFSA_7:3;
A4:len f-'k2=len f-k2 by A1,SCMFSA_7:3;
A5:k1-'1<=len f by A1,Th13;
then A6:(len f-'(k1-'1))+(k1-'1)
=(len f-(k1-'1))+(k1-'1)by SCMFSA_7:3
.=len f by XCMPLX_1:27;
A7:len f-'(k1-'1)=len f-(k1-'1) by A5,SCMFSA_7:3
.=len f-(k1-1) by A1,SCMFSA_7:3
.=len f-k1+1 by XCMPLX_1:37 .=len f-'k1+1 by A1,SCMFSA_7:3;
len f-'k1>=len f-'k2 by A2,Th4;
then A8:len f-'k1+1>=len f-'k2+1 by AXIOMS:24;
k2-k1<=len f-k1 by A1,REAL_1:49;
then k2-'k1<=len f-k1 by A2,SCMFSA_7:3;
then k2-'k1<=len f-'k1 by A1,SCMFSA_7:3;
then k2-'k1+1<=len f-'k1+1 by AXIOMS:24;
then A9:(len f-'(k1-'1)-'(k2-'k1+1))
=(len f-'k1+1)-(k2-'k1+1) by A7,SCMFSA_7:3
.=(len f-k1+1)-(k2-k1+1) by A2,A3,SCMFSA_7:3
.=(len f-k1+1)-(k2-k1)-1 by XCMPLX_1:36
.=len f-k1+1-k2+k1-1 by XCMPLX_1:37
.=len f-k1+1+k1-k2-1 by XCMPLX_1:29
.=len f-k1+k1+1-k2-1 by XCMPLX_1:1
.=len f+1-k2-1 by XCMPLX_1:27
.=len f+1-1-k2 by XCMPLX_1:21
.=len f-k2 by XCMPLX_1:26
.=len f-'k2 by A1,SCMFSA_7:3;
A10:len f-'k1>=len f-'k2 by A2,Th4;
len f-'k1<=len f-'k1+1 by NAT_1:29;
then len f-'k2<=len f-'k1+1 by A10,AXIOMS:22;
then A11:len f-'(k1-'1)-'(len f-'k2)
=len f-'k1+1-(len f-'k2) by A7,SCMFSA_7:3
.=len f-k1+1-(len f-k2) by A1,A3,SCMFSA_7:3
.=len f-k1+1-len f+k2 by XCMPLX_1:37
.=len f-(k1-1)-len f+k2 by XCMPLX_1:37
.=len f+-(k1-1)-len f+k2 by XCMPLX_0:def 8
.=k2+-(k1-1) by XCMPLX_1:26
.=k2-(k1-1) by XCMPLX_0:def 8
.=k2-k1+1 by XCMPLX_1:37
.=k2-'k1+1 by A2,SCMFSA_7:3;
A12:k1-'1<=len f by A1,Th13;
A13:(len (f/^(k1-'1))-'(k2-'k1+1))+(k2-'k1+1)
=len f-'k2+(k2-'k1+1) by A9,Th19
.=len f-k2+(k2-k1+1) by A2,A4,SCMFSA_7:3
.=len f-k2+(k2-k1)+1 by XCMPLX_1:1
.=len f-k2+k2-k1+1 by XCMPLX_1:29
.=len f-k1+1 by XCMPLX_1:27
.=len f-(k1-1) by XCMPLX_1:37
.=len f-(k1-'1) by A1,SCMFSA_7:3
.=len f-'(k1-'1) by A12,SCMFSA_7:3
.=len (f/^(k1-'1)) by Th19;
A14:(len f-'k1+1)-'(len f-'k2+1)+1
=(len f-'k1+1)-(len f-'k2+1)+1 by A8,SCMFSA_7:3
.=(len f-k1+1)-(len f-k2+1)+1 by A1,A3,SCMFSA_7:3
.=(len f-k1+1)-(len f+1-k2)+1 by XCMPLX_1:29
.=(len f+1-k1)-(len f+1-k2)+1 by XCMPLX_1:29
.=-k1+(len f+1)-(len f+1-k2)+1 by XCMPLX_0:def 8
.=-k1+(len f+1)-(len f+1)+k2+1 by XCMPLX_1:37
.=k2+-k1+1 by XCMPLX_1:26
.=k2-k1+1 by XCMPLX_0:def 8
.=k2-'k1+1 by A2,SCMFSA_7:3;
len f-'k1>=len f-'k2 by A2,Th4;
then len f-'k1+1>=len f-'k2+1 by AXIOMS:24;
then mid(Rev f,len f-'k2+1,len f-'k1+1)
=(((Rev f)/^((len f-'k2+1)-'1))|(k2-'k1+1)) by A14,Def1
.=(Rev f/^(len f-'k2))|(len f-'(k1-'1)-'(len f-'k2)) by A11,BINARITH:39
.=(Rev f|(len f-'(k1-'1)))/^(len f-'k2) by Th21
.=(Rev f|(len f-'(k1-'1)))/^(len (f/^(k1-'1))-'(k2-'k1+1)) by A9,Th19
.=(Rev (f/^(k1-'1)))/^(len (f/^(k1-'1))-'(k2-'k1+1)) by A6,FINSEQ_6:90
.=Rev (((f/^(k1-'1))|(k2-'k1+1))) by A13,FINSEQ_6:91
.=Rev mid(f,k1,k2) by A2,Def1;
hence Rev mid(f,k1,k2)=mid(Rev f,len f-'k2+1,len f-'k1+1);
suppose A15:k1>k2;
A16:len f-'k2=len f-k2 by A1,SCMFSA_7:3;
A17:len f-'k1=len f-k1 by A1,SCMFSA_7:3;
A18:k2-'1<=len f by A1,Th13;
then A19:(len f-'(k2-'1))+(k2-'1)
=(len f-(k2-'1))+(k2-'1)by SCMFSA_7:3
.=len f by XCMPLX_1:27;
A20:len f-'(k2-'1)=len f-(k2-'1) by A18,SCMFSA_7:3
.=len f-(k2-1) by A1,SCMFSA_7:3
.=len f-k2+1 by XCMPLX_1:37 .=len f-'k2+1 by A1,SCMFSA_7:3;
len f-'k2>=len f-'k1 by A15,Th4;
then A21:len f-'k2+1>=len f-'k1+1 by AXIOMS:24;
k1-k2<=len f-k2 by A1,REAL_1:49;
then k1-'k2<=len f-k2 by A15,SCMFSA_7:3;
then k1-'k2<=len f-'k2 by A1,SCMFSA_7:3;
then k1-'k2+1<=len f-'k2+1 by AXIOMS:24;
then A22:(len f-'(k2-'1)-'(k1-'k2+1))
=(len f-'k2+1)-(k1-'k2+1) by A20,SCMFSA_7:3
.=(len f-k2+1)-(k1-k2+1) by A15,A16,SCMFSA_7:3
.=(len f-k2+1)-(k1-k2)-1 by XCMPLX_1:36
.=len f-k2+1-k1+k2-1 by XCMPLX_1:37
.=len f-k2+1+k2-k1-1 by XCMPLX_1:29
.=len f-k2+k2+1-k1-1 by XCMPLX_1:1
.=len f+1-k1-1 by XCMPLX_1:27
.=len f+1-1-k1 by XCMPLX_1:21
.=len f-k1 by XCMPLX_1:26
.=len f-'k1 by A1,SCMFSA_7:3;
A23:len f-'k2>=len f-'k1 by A15,Th4;
len f-'k2<=len f-'k2+1 by NAT_1:29;
then len f-'k1<=len f-'k2+1 by A23,AXIOMS:22;
then A24:len f-'(k2-'1)-'(len f-'k1)
=len f-'k2+1-(len f-'k1) by A20,SCMFSA_7:3
.=len f-k2+1-(len f-k1) by A1,A16,SCMFSA_7:3
.=len f-k2+1-len f+k1 by XCMPLX_1:37
.=len f-(k2-1)-len f+k1 by XCMPLX_1:37
.=len f+-(k2-1)-len f+k1 by XCMPLX_0:def 8
.=-(k2-1)+k1 by XCMPLX_1:26
.=k1-(k2-1) by XCMPLX_0:def 8
.=k1-k2+1 by XCMPLX_1:37
.=k1-'k2+1 by A15,SCMFSA_7:3;
A25:k2-'1<=len f by A1,Th13;
A26:(len (f/^(k2-'1))-'(k1-'k2+1))+(k1-'k2+1)
=len f-'k1+(k1-'k2+1) by A22,Th19
.=len f-k1+(k1-k2+1) by A15,A17,SCMFSA_7:3
.=len f-k1+(k1-k2)+1 by XCMPLX_1:1
.=len f-k1+k1-k2+1 by XCMPLX_1:29
.=len f-k2+1 by XCMPLX_1:27
.=len f-(k2-1) by XCMPLX_1:37
.=len f-(k2-'1) by A1,SCMFSA_7:3
.=len f-'(k2-'1) by A25,SCMFSA_7:3
.=len (f/^(k2-'1)) by Th19;
A27:(len f-'k2+1)-'(len f-'k1+1)+1
=(len f-'k2+1)-(len f-'k1+1)+1 by A21,SCMFSA_7:3
.=(len f-k2+1)-(len f-k1+1)+1 by A1,A16,SCMFSA_7:3
.=(len f-k2+1)-(len f+1-k1)+1 by XCMPLX_1:29
.=(len f+1-k2)-(len f+1-k1)+1 by XCMPLX_1:29
.=-k2+(1+len f)-(len f+1-k1)+1 by XCMPLX_0:def 8
.=-k2+(len f+1)-(len f+1)+k1+1 by XCMPLX_1:37
.=-k2+k1+1 by XCMPLX_1:26
.=k1-k2+1 by XCMPLX_0:def 8
.=k1-'k2+1 by A15,SCMFSA_7:3;
len f-k2>len f-k1 by A15,REAL_2:105;
then len f-'k2+1>len f-'k1+1 by A16,A17,REAL_1:53;
then mid(Rev f,len f-'k2+1,len f-'k1+1)
=Rev((((Rev f)/^((len f-'k1+1)-'1))|(k1-'k2+1))) by A27,Def1
.=Rev((Rev f/^(len f-'k1))|(len f-'(k2-'1)-'(len f-'k1))) by A24,BINARITH:39
.=Rev((Rev f|(len f-'(k2-'1)))/^(len f-'k1)) by Th21
.=Rev((Rev f|(len f-'(k2-'1)))/^(len (f/^(k2-'1))-'(k1-'k2+1))) by A22,Th19
.=Rev((Rev (f/^(k2-'1)))/^(len (f/^(k2-'1))-'(k1-'k2+1))) by A19,FINSEQ_6:90
.=Rev(Rev (((f/^(k2-'1))|(k1-'k2+1)))) by A26,FINSEQ_6:91
.= Rev mid(f,k1,k2) by A15,Def1;
hence Rev mid(f,k1,k2)=mid(Rev f,len f-'k2+1,len f-'k1+1);
end;
theorem Th23:
for n,m being Nat,f being FinSequence of D st
1<= m &m+n<=len f holds (f/^n).m=f.(m+n)
proof let n,m be Nat,f be FinSequence of D;
assume A1: 1<= m & m+n<=len f;
n<=n+m by NAT_1:29;
then A2:n<=len f by A1,AXIOMS:22;
then A3:len (f/^n) = len f -n by RFINSEQ:def 2;
m+n-n<=len f -n by A1,REAL_1:49;
then m<=len (f/^n) by A3,XCMPLX_1:26;
then m in dom (f/^n) by A1,FINSEQ_3:27;
hence (f/^n).m=f.(m+n) by A2,RFINSEQ:def 2;
end;
theorem Th24: for i being Nat,f being FinSequence of D st
1<=i & i<=len f holds (Rev f).i=f.(len f -i+1)
proof let i be Nat,f be FinSequence of D;
assume 1<=i & i<=len f;
then i in dom (f) by FINSEQ_3:27;
hence (Rev f).i=f.(len f -i+1) by FINSEQ_5:61;
end;
theorem for f being FinSequence of D,k being Nat st
1<=k holds mid(f,1,k)=f|k
proof let f be FinSequence of D,k be Nat;
assume A1:1<=k;
then A2:mid(f,1,k)=(f/^(1-'1))|(k-'1+1) by Def1;
1-'1=0 by GOBOARD9:1;
then f/^(1-'1)=f by FINSEQ_5:31;
hence mid(f,1,k)=f|k by A1,A2,AMI_5:4;
end;
theorem Th26:for f being FinSequence of D,k being Nat st
k<=len f holds mid(f,k,len f)=f/^(k-'1)
proof let f be FinSequence of D,k be Nat;
assume A1:k<=len f;
then A2:mid(f,k,len f)=(f/^(k-'1))|(len f-'k+1) by Def1;
k-'1<=len f by A1,Th7;
then A3:len (f/^(k-'1))=len f-(k-'1) by RFINSEQ:def 2;
A4:len f-'k+1=len f-k+1 by A1,SCMFSA_7:3 .=len f -(k-1) by XCMPLX_1:37;
now per cases;
case A5:k=0; then len f-'k+1=len f +1 by Th2;
then len f <= len f-'k+1 by NAT_1:29;
then A6:Seg len f c= Seg (len f -'k+1) by FINSEQ_1:7;
0-1<0;
then k-'1=0 by A5,BINARITH:def 3;
then f/^(k-'1)=f by FINSEQ_5:31;
then dom (f/^(k-'1)) c= Seg (len f -'k+1) by A6,FINSEQ_1:def 3;
then (f/^(k-'1))|Seg (len f -'k+1)=
f/^(k-'1) by RELAT_1:97;
hence mid(f,k,len f)=f/^(k-'1) by A2,TOPREAL1:def 1;
case k<>0; then k>0 by NAT_1:19; then 0+1<=k by NAT_1:38;
then len (f/^(k-'1))=len f-'k+1 by A3,A4,SCMFSA_7:3;
hence
mid(f,k,len f)=(f/^(k-'1))|Seg len (f/^(k-'1)) by A2,TOPREAL1:def 1
.=(f/^(k-'1))|dom (f/^(k-'1)) by FINSEQ_1:def 3
.=(f/^(k-'1)) by RELAT_1:97;
end;
hence mid(f,k,len f)=f/^(k-'1);
end;
theorem Th27:for f being FinSequence of D,k1,k2 being Nat st
1<=k1 & k1<=len f & 1<=k2 & k2<=len f holds
mid(f,k1,k2).1=f.k1 &
(k1<=k2 implies len mid(f,k1,k2) = k2 -' k1 +1 &
for i being Nat st 1<=i & i<=len mid(f,k1,k2)
holds mid(f,k1,k2).i=f.(i+k1-'1))
& (k1>k2 implies len mid(f,k1,k2) = k1 -' k2 +1 &
for i being Nat st 1<=i & i<=len mid(f,k1,k2)
holds mid(f,k1,k2).i=f.(k1-'i+1))
proof let f be FinSequence of D,k11,k21 be Nat;
assume A1: 1<=k11 & k11<=len f & 1<=k21 & k21<=len f;
A2:now let k1,k2 be Nat;
now assume A3:k1<=k2 & 1<=k1 & k1<=len f;
then A4:mid(f,k1,k2).1=((f/^(k1-'1))|(k2-'k1+1)).1 by Def1
.=((f/^(k1-'1))|(Seg (k2-'k1+1))).1 by TOPREAL1:def 1;
k1-1>=0 by A3,SQUARE_1:12;
then A5:1+(k1-'1)=1+(k1-1) by BINARITH:def 3 .=k1 by XCMPLX_1:27;
then 1+(k1-'1)<=len f -(k1-'1)+(k1-'1) by A3,XCMPLX_1:27;
then A6:1<=len f - (k1-'1) by REAL_1:53;
A7:k1-'1<=len f by A3,Th7;
then A8:len (f/^(k1-'1))=len f -(k1-'1) by RFINSEQ:def 2;
k1-k1<=k2-k1 by A3,REAL_1:49;
then A9:0<=k2-k1 by XCMPLX_1:14;
then k2-'k1=k2-k1 by BINARITH:def 3;
then 0+1<=k2-'k1+1 by A9,AXIOMS:24;
then 1 in Seg (k2-'k1+1) & 1 in Seg(len (f/^(k1-'1))) by A6,A8,FINSEQ_1:3
;
then A10:1 in dom (f/^(k1-'1)) & 1 in Seg(k2-'k1+1) by FINSEQ_1:def 3;
then 1 in dom (f/^(k1-'1)) /\ Seg(k2-'k1+1) by XBOOLE_0:def 3;
then 1 in dom ((f/^(k1-'1))|(Seg (k2-'k1+1))) by RELAT_1:90;
then mid(f,k1,k2).1=(f/^(k1-'1)).1 by A4,FUNCT_1:70;
hence mid(f,k1,k2).1=f.k1 by A5,A7,A10,RFINSEQ:def 2;
end;
hence k1<=k2 & 1<=k1 & k1<=len f implies mid(f,k1,k2).1=f.k1;
end;
thus mid(f,k11,k21).1=f.k11
proof per cases;
suppose k11<=k21;
hence mid(f,k11,k21).1=f.k11 by A1,A2;
suppose A11:k11>k21;
A12:1<=(k11-'k21+1) by NAT_1:29;
k21-'1<=len f by A1,Th7;
then A13:len (f/^(k21-'1))=len f -(k21-'1) by RFINSEQ:def 2;
A14: k21-1>=0 by A1,SQUARE_1:12;
A15: k11-k21>=0 by A11,SQUARE_1:12;
then A16:k11-'k21=k11-k21 by BINARITH:def 3;
k11-'k21+1=k11-k21+1 by A15,BINARITH:def 3 .=k11-(k21-1) by XCMPLX_1:37
.=k11-(k21-'1) by A14,BINARITH:def 3;
then A17:k11-'k21+1 <=len (f/^(k21-'1)) by A1,A13,REAL_1:49;
then A18:len ((f/^(k21-'1))|(k11-'k21+1))=(k11-'k21+1) by TOPREAL1:3;
then A19:k11-'k21+1 in dom ((f/^(k21-'1))|(k11-'k21+1)) by A12,FINSEQ_3:27;
A20:k11-'k21+1 in dom (f/^(k21-'1)) by A12,A17,FINSEQ_3:27;
A21:k21-'1 +(k11-'k21+1)=k21-1+(k11-k21+1) by A14,A16,BINARITH:def 3
.= k21-1+(k11-(k21-1)) by XCMPLX_1:37
.=k11 by XCMPLX_1:27;
A22:((f/^(k21-'1))|(k11-'k21+1)).len ((f/^(k21-'1))|(k11-'k21+1))
=((f/^(k21-'1))|(k11-'k21+1))/.(k11-'k21+1) by A12,A18,FINSEQ_4:24
.=(f/^(k21-'1))/.(k11-'k21+1) by A19,TOPREAL1:1
.=f/.((k21-'1 +(k11-'k21+1))) by A20,FINSEQ_5:30
.=f.k11 by A1,A21,FINSEQ_4:24;
1 in dom ((f/^(k21-'1))|(k11-'k21+1)) by A12,A18,FINSEQ_3:27;
then (Rev ((f/^(k21-'1))|(k11-'k21+1))).1
= ((f/^(k21-'1))|(k11-'k21+1))
.(len ((f/^(k21-'1))|(k11-'k21+1))
- 1 + 1) by FINSEQ_5:61
.= f.k11 by A22,XCMPLX_1:27;
hence mid(f,k11,k21).1=f.k11 by A11,Def1;
end;
thus k11<=k21 implies len mid(f,k11,k21) = k21 -' k11 +1 &
for i being Nat st 1<=i & i<=len mid(f,k11,k21)
holds mid(f,k11,k21).i=f.(i+k11-'1)
proof assume A23:k11<=k21;
then A24:mid(f,k11,k21)=(f/^(k11-'1))|(k21-'k11+1) by Def1;
k11-'1<=len f by A1,Th7;
then A25:len (f/^(k11-'1))=len f -(k11-'1) by RFINSEQ:def 2;
A26: k11-1>=0 by A1,SQUARE_1:12;
then A27:k11-'1=k11-1 by BINARITH:def 3;
A28: k21-k11>=0 by A23,SQUARE_1:12;
then A29:k21-'k11=k21-k11 by BINARITH:def 3;
k21-'k11+1=k21-k11+1 by A28,BINARITH:def 3 .=k21-(k11-1) by XCMPLX_1:37
.=k21-(k11-'1) by A26,BINARITH:def 3;
then A30:k21-'k11+1 <=len (f/^(k11-'1)) by A1,A25,REAL_1:49;
then A31: len ((f/^(k11-'1))|(k21-'k11+1))=(k21-'k11+1) by TOPREAL1:3;
for i being Nat st 1<=i & i<=len mid(f,k11,k21)
holds mid(f,k11,k21).i=f.(i+k11-'1)
proof let i be Nat;assume A32:1<=i & i<=len mid(f,k11,k21);
then i<=k21-(k11-1) by A24,A29,A31,XCMPLX_1:37;
then i+(k11-1)<=k21-(k11-1)+(k11-1) by AXIOMS:24;
then A33:i+(k11-'1)<=k21 by A27,XCMPLX_1:27;
A34:i<= (k21-'k11+1) & (k21-'k11+1)<=len (f/^(k11-'1))
by A24,A30,A32,TOPREAL1:3;
A35:1<=i & i+(k11-'1)<=len f by A1,A32,A33,AXIOMS:22;
k11<=k11+i by NAT_1:29;
then A36:i+k11>=1 by A1,AXIOMS:22;
A37:i+(k11-'1)=i+(k11-1) by A26,BINARITH:def 3 .=i+k11-1 by XCMPLX_1:29
.=i+k11-'1 by A36,SCMFSA_7:3;
mid(f,k11,k21).i=(f/^(k11-'1))|(k21-'k11+1).i by A23,Def1
.=(f/^(k11-'1)).i by A34,Th20
.=f.(i+(k11-'1)) by A35,Th23;
hence mid(f,k11,k21).i=f.(i+k11-'1) by A37;
end;
hence len mid(f,k11,k21) = k21 -' k11 +1 &
for i being Nat st 1<=i & i<=len mid(f,k11,k21)
holds mid(f,k11,k21).i=f.(i+k11-'1) by A24,A30,TOPREAL1:3;
end;
assume A38:k11>k21;
then A39:mid(f,k11,k21)=Rev ((f/^(k21-'1))|(k11-'k21+1)) by Def1;
then A40:len mid(f,k11,k21)=len ((f/^(k21-'1))|(k11-'k21+1)) by FINSEQ_5:
def 3;
k21-'1<=len f by A1,Th7;
then A41:len (f/^(k21-'1))=len f -(k21-'1) by RFINSEQ:def 2;
A42: k21-1>=0 by A1,SQUARE_1:12;
then A43:k21-'1=k21-1 by BINARITH:def 3;
A44: k11-k21>=0 by A38,SQUARE_1:12;
then A45:k11-'k21=k11-k21 by BINARITH:def 3;
k11-'k21+1=k11-k21+1 by A44,BINARITH:def 3 .=k11-(k21-1) by XCMPLX_1:37
.=k11-(k21-'1) by A42,BINARITH:def 3;
then A46:k11-'k21+1 <=len (f/^(k21-'1)) by A1,A41,REAL_1:49;
then A47:len ((f/^(k21-'1))|(k11-'k21+1))=(k11-'k21+1) by TOPREAL1:3;
thus A48:len mid(f,k11,k21) = k11 -' k21 +1 by A40,A46,TOPREAL1:3;
thus for i being Nat st 1<=i & i<=len mid(f,k11,k21)
holds mid(f,k11,k21).i=f.(k11-'i+1)
proof let i be Nat;assume A49:1<=i & i<=len mid(f,k11,k21);
then A50:i<=k11-'k21+1 by A40,A46,TOPREAL1:3;
i<=k11-(k21-1) by A45,A48,A49,XCMPLX_1:37;
then i+(k21-1)<=k11-(k21-1)+(k21-1) by AXIOMS:24;
then A51:i+(k21-'1)<=k11 by A43,XCMPLX_1:27;
i<=i+(k21-'1) by NAT_1:29;
then A52:i<=k11 by A51,AXIOMS:22;
A53:k11-'k21+1-'i+1+(k21-'1)
=k11-'k21+1-i+1+(k21-'1) by A48,A49,SCMFSA_7:3
.= k11-k21+1-i+1+(k21-1) by A42,A45,BINARITH:def 3
.= k11-(k21-1)-i+1+(k21-1) by XCMPLX_1:37
.= k11-(k21-1)-(i-1)+(k21-1) by XCMPLX_1:37
.= k11-(k21-1)+(k21-1)-(i-1) by XCMPLX_1:29
.=k11-(i-1) by XCMPLX_1:27
.=k11-i+1 by XCMPLX_1:37
.=k11-'i+1 by A52,SCMFSA_7:3;
k11-'k21+1<= k11-'k21+1+(i-'1) by NAT_1:29;
then k11-'k21+1<= k11-'k21+1+(i-1) by A49,SCMFSA_7:3;
then k11-'k21+1-(i-1)<= k11-'k21+1+(i-1)-(i-1) by REAL_1:49;
then k11-'k21+1-(i-1)<= k11-'k21+1 by XCMPLX_1:26;
then k11-'k21+1-i+1<= k11-'k21+1 by XCMPLX_1:37;
then A54: (k11-'k21+1-'i+1)<=(k11-'k21+1) by A50,SCMFSA_7:3;
A55:1+k11<=i+k11 by A49,AXIOMS:24;
i+k11<=i+len f by A1,AXIOMS:24;
then 1+k11<=i+len f by A55,AXIOMS:22;
then 1+k11-i<=i+len f -i by REAL_1:49;
then 1+k11-i<=len f by XCMPLX_1:26;
then k11-i+1<=len f by XCMPLX_1:29;
then A56:1<=k11-'k21+1-'i+1 & k11-'k21+1-'i+1+(k21-'1)<= len f
by A52,A53,NAT_1:29,SCMFSA_7:3;
mid(f,k11,k21).i=((f/^(k21-'1))|(k11-'k21+1))
.(len ((f/^(k21-'1))|(k11-'k21+1)) -i+1)
by A39,A40,A49,Th24
.=((f/^(k21-'1))|(k11-'k21+1))
.(len ((f/^(k21-'1))|(k11-'k21+1)) -'i+1)
by A40,A49,SCMFSA_7:3
.=(f/^(k21-'1)).(k11-'k21+1-'i+1) by A47,A54,Th20
.=f.(k11-'i+1) by A53,A56,Th23;
hence mid(f,k11,k21).i=f.(k11-'i+1);
end;
end;
theorem Th28: for f being FinSequence of D,k1,k2 being Nat holds
rng mid(f,k1,k2) c= rng f
proof let f be FinSequence of D,k1,k2 be Nat;
per cases;
suppose k1<=k2;
then mid(f,k1,k2) = (f/^(k1-'1))|(k2-'k1+1) by Def1;
then A1:rng mid(f,k1,k2) c= rng (f/^(k1-'1)) by FINSEQ_5:21;
rng (f/^(k1-'1)) c= rng f by FINSEQ_5:36;
hence rng mid(f,k1,k2) c= rng f by A1,XBOOLE_1:1;
suppose k1>k2;
then mid(f,k1,k2) = Rev ((f/^(k2-'1))|(k1-'k2+1)) by Def1;
then rng mid(f,k1,k2) = rng ((f/^(k2-'1))|(k1-'k2+1)) by FINSEQ_5:60;
then A2:rng mid(f,k1,k2) c= rng (f/^(k2-'1)) by FINSEQ_5:21;
rng (f/^(k2-'1)) c= rng f by FINSEQ_5:36;
hence rng mid(f,k1,k2) c= rng f by A2,XBOOLE_1:1;
end;
theorem for f being FinSequence of D st 1<=len f holds
mid(f,1,len f)=f
proof let f be FinSequence of D;
assume A1:1<=len f;
then mid(f,1,len f)=(f/^(1-'1))|(len f-'1+1) by Def1
.=(f/^0)|(len f-'1+1) by GOBOARD9:1
.=f|(len f-'1+1) by FINSEQ_5:31
.=f|len f by A1,AMI_5:4
.=f by TOPREAL1:2;
hence mid(f,1,len f)=f;
end;
theorem for f being FinSequence of D st 1<=len f holds
mid(f,len f,1)=Rev f
proof let f be FinSequence of D;
assume A1:1<=len f;
A2:1-'1=0 by GOBOARD9:1;
per cases;
suppose len f<>1; then 1<len f by A1,REAL_1:def 5;
then mid(f,len f,1)=Rev ((f/^(1-'1))|(len f-'1+1)) by Def1
.=Rev ((f/^0)|len f) by A1,A2,AMI_5:4
.=Rev (f|len f) by FINSEQ_5:31
.=Rev f by TOPREAL1:2;
hence mid(f,len f,1)=Rev f;
suppose A3:len f=1;
then A4:mid(f,len f,1)=(f/^(1-'1))|(1-'1+1) by Def1
.=f|1 by A2,FINSEQ_5:31;
A5:f|1=f by A3,TOPREAL1:2;
len (f|1)=1 by A1,TOPREAL1:3;
hence mid(f,len f,1)=Rev f by A4,A5,Th18;
end;
theorem Th31:for f being FinSequence of D, k1,k2,i being Nat
st 1<=k1 & k1<=k2 & k2<=len f & 1<=i &
(i<=k2-'k1+1 or i<=k2-k1+1 or i<=k2+1-k1) holds
mid(f,k1,k2).i=f.(i+k1-'1) & mid(f,k1,k2).i=f.(i-'1+k1) &
mid(f,k1,k2).i=f.(i+k1-1) & mid(f,k1,k2).i=f.(i-1+k1)
proof let f be FinSequence of D, k1,k2,i be Nat;
assume A1:1<=k1 & k1<=k2 & k2<=len f & 1<=i &
(i<=k2-'k1+1 or i<=k2-k1+1 or i<=k2+1-k1);
then A2:1<=k2 by AXIOMS:22;
A3:k1<=len f by A1,AXIOMS:22;
A4: i-1>=1-1 by A1,REAL_1:49;
i+k1>=1+k1 by A1,AXIOMS:24;
then i+k1-1>=1+k1-1 by REAL_1:49;
then A5:i+k1-1>=k1 by XCMPLX_1:26;
A6: 0<=k1 by NAT_1:18;
A7:len mid(f,k1,k2)=k2-'k1+1 by A1,A2,A3,Th27;
A8:i<=k2-k1+1 implies i<=k2-'k1+1 by A1,SCMFSA_7:3;
i-'1+k1=i-1+k1 by A4,BINARITH:def 3 .=i+k1-1 by XCMPLX_1:29
.=i+k1-'1 by A5,A6,BINARITH:def 3;
hence A9:mid(f,k1,k2).i=f.(i+k1-'1) & mid(f,k1,k2).i=f.(i-'1+k1)
by A1,A2,A3,A7,A8,Th27,XCMPLX_1:29;
hence mid(f,k1,k2).i=f.(i+k1-1) by A5,A6,BINARITH:def 3;
thus mid(f,k1,k2).i=f.(i-1+k1) by A1,A9,SCMFSA_7:3;
end;
theorem Th32:for f being FinSequence of D,k,i being Nat
st 1<=i & i<=k & k<=len f holds
mid(f,1,k).i=f.i
proof let f be FinSequence of D,k,i be Nat;
assume A1: 1<=i & i<=k & k<=len f;
then A2:1<=k & k<=len f & 1<=i & i<=k by AXIOMS:22;
i<=k-1+1 by A1,XCMPLX_1:27;
then mid(f,1,k).i=f.(i+1-'1) by A2,Th31;
hence thesis by BINARITH:39;
end;
theorem
for f being FinSequence of D, k1,k2 being Nat
st 1<=k1 & k1<=k2 & k2<=len f holds len mid(f,k1,k2)<=len f
proof let f be FinSequence of D, k1,k2 be Nat;
assume A1:1<=k1 & k1<=k2 & k2<=len f;
then A2:1<=k2 by AXIOMS:22;
k1<=len f by A1,AXIOMS:22;
then A3:len mid(f,k1,k2)=k2-'k1+1 by A1,A2,Th27;
k2-k1>=0 by A1,SQUARE_1:12;
then A4:k2-'k1+1=k2-k1+1 by BINARITH:def 3 .=k2-(k1-1) by XCMPLX_1:37;
k1-1>=0 by A1,SQUARE_1:12;
then A5:k1-1=k1-'1 by BINARITH:def 3;
k2<=k2+(k1-'1) by NAT_1:29;
then k2-(k1-'1)<=k2+(k1-'1)-(k1-'1) by REAL_1:49;
then k2-(k1-'1)<=k2 by XCMPLX_1:26;
hence len mid(f,k1,k2)<=len f by A1,A3,A4,A5,AXIOMS:22;
end;
theorem
for f being FinSequence of TOP-REAL n st 2<=len f
holds f.1 in L~f & f/.1 in L~f & f.len f in L~f & f/.len f in L~f
proof let f be FinSequence of TOP-REAL n;
assume A1:2<=len f;
then A2: 1+1<=len f;
f/.1 in LSeg(f/.1,f/.(1+1)) by TOPREAL1:6;
then A3:f/.1 in LSeg(f,1) by A1,TOPREAL1:def 5;
LSeg(f,1) in {LSeg(f,i):1<=i & i+1<=len f} by A2;
then f/.1 in union{LSeg(f,i):1<=i & i+1<=len f} by A3,TARSKI:def 4;
then A4:f/.1 in L~f by TOPREAL1:def 6;
A5:1<=len f by A2,Th9;
A6:1<=len f-'1 by A2,Th12;
A7:len f-'1+1=len f by A5,AMI_5:4;
then f/.len f in LSeg(f/.(len f-'1),f/.(len f-'1+1)) by TOPREAL1:6;
then A8:f/.len f in LSeg(f,len f-'1) by A6,A7,TOPREAL1:def 5;
LSeg(f,len f-'1) in {LSeg(f,i):1<=i & i+1<=len f} by A6,A7;
then f/.len f in union{LSeg(f,i):1<=i & i+1<=len f} by A8,TARSKI:def 4;
then f/.len f in L~f by TOPREAL1:def 6;
hence f.1 in L~f & f/.1 in L~f & f.len f in L~f & f/.len f in L~f
by A4,A5,FINSEQ_4:24;
end;
theorem Th35:for p1,p2,q1,q2 being Point of TOP-REAL 2 st
(p1`1 = p2`1 or p1`2 = p2`2)& q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2)
holds q1`1 = q2`1 or q1`2 = q2`2
proof let p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1:(p1`1 = p2`1 or p1`2 = p2`2)& q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2);
then q1 in { (1-r)*p1 + r*p2 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r1 such that A2:q1= (1-r1)*p1 + r1*p2 & 0 <= r1 & r1 <= 1;
q2 in { (1-r)*p1 + r*p2 : 0 <= r & r <= 1 } by A1,TOPREAL1:def 4;
then consider r2 such that A3:q2= (1-r2)*p1 + r2*p2 & 0 <= r2 & r2 <= 1;
q1`1=((1-r1)*p1)`1+(r1*p2)`1 by A2,TOPREAL3:7;
then q1`1=(1-r1)*(p1`1)+(r1*p2)`1 by TOPREAL3:9;
then A4:q1`1=(1-r1)*(p1`1)+r1*(p2`1) by TOPREAL3:9;
q1`2=((1-r1)*p1)`2+(r1*p2)`2 by A2,TOPREAL3:7;
then q1`2=(1-r1)*(p1`2)+(r1*p2)`2 by TOPREAL3:9;
then A5:q1`2=(1-r1)*(p1`2)+r1*(p2`2) by TOPREAL3:9;
q2`1=((1-r2)*p1)`1+(r2*p2)`1 by A3,TOPREAL3:7;
then q2`1=(1-r2)*(p1`1)+(r2*p2)`1 by TOPREAL3:9;
then A6:q2`1=(1-r2)*(p1`1)+r2*(p2`1) by TOPREAL3:9;
q2`2=((1-r2)*p1)`2+(r2*p2)`2 by A3,TOPREAL3:7;
then q2`2=(1-r2)*(p1`2)+(r2*p2)`2 by TOPREAL3:9;
then A7:q2`2=(1-r2)*(p1`2)+r2*(p2`2) by TOPREAL3:9;
per cases by A1;
suppose A8:p1`1 = p2`1;
then A9:q1`1=((1-r1)+r1)*(p1`1) by A4,XCMPLX_1:8 .=1*(p1`1) by XCMPLX_1:27
.=p1`1;
q2`1=((1-r2)+r2)*(p1`1) by A6,A8,XCMPLX_1:8 .=1*(p1`1) by XCMPLX_1:27
.=p1`1;
hence thesis by A9;
suppose A10:p1`2 = p2`2;
then A11:q1`2=((1-r1)+r1)*(p1`2) by A5,XCMPLX_1:8 .=1*(p1`2) by XCMPLX_1:27
.=p1`2;
q2`2=((1-r2)+r2)*(p1`2) by A7,A10,XCMPLX_1:8 .=1*(p1`2) by XCMPLX_1:27
.=p1`2;
hence thesis by A11;
end;
theorem Th36:for p1,p2,q1,q2 being Point of TOP-REAL 2 st
(p1`1 = p2`1 or p1`2 = p2`2)& LSeg(q1,q2) c= LSeg(p1,p2)
holds q1`1 = q2`1 or q1`2 = q2`2
proof let p1,p2,q1,q2 be Point of TOP-REAL 2;
q1 in LSeg(q1,q2) & q2 in LSeg(q1,q2) by TOPREAL1:6;
hence thesis by Th35;
end;
theorem Th37: for f being FinSequence of TOP-REAL 2,n being Nat
st 2<=n & f is_S-Seq holds f|n is_S-Seq
proof let f be FinSequence of TOP-REAL 2,n be Nat;
assume A1:2<=n & f is_S-Seq;
then A2:f is one-to-one & len f >= 2
& f is unfolded s.n.c. special by TOPREAL1:def 10;
reconsider f'=f as s.n.c. special unfolded one-to-one
FinSequence of TOP-REAL 2 by A1,TOPREAL1:def 10;
now per cases;
case n<=len f;
hence len (f|n) >= 2 by A1,TOPREAL1:3;
case n>len f;
hence len (f|n) >= 2 by A2,TOPREAL1:2;
end;
then f'|n is one-to-one & len (f|n) >= 2
& f'|n is unfolded s.n.c. special;
hence f|n is_S-Seq by TOPREAL1:def 10;
end;
theorem Th38: for f being FinSequence of TOP-REAL 2,n being Nat
st n<=len f & 2<=len f-'n & f is_S-Seq holds f/^n is_S-Seq
proof let f be FinSequence of TOP-REAL 2,n be Nat;
assume A1:n<=len f & 2<=len f-'n & f is_S-Seq;
then reconsider f' = f as
one-to-one special s.n.c. unfolded FinSequence of TOP-REAL 2
by TOPREAL1:def 10;
len (f/^n)=len f-n by A1,RFINSEQ:def 2;
then f'/^n is one-to-one & len (f'/^n) >= 2
& f'/^n is unfolded s.n.c. special by A1,SCMFSA_7:3;
hence f/^n is_S-Seq by TOPREAL1:def 10;
end;
theorem for f being FinSequence of TOP-REAL 2,k1,k2 being Nat
st f is_S-Seq & 1<=k1 & k1<=len f & 1<=k2 & k2<=len f & k1<>k2 holds
mid(f,k1,k2) is_S-Seq
proof let f be FinSequence of TOP-REAL 2,k1,k2 be Nat;
assume A1: f is_S-Seq & 1<=k1 & k1<=len f & 1<=k2 & k2<=len f & k1<>k2;
per cases;
suppose A2:k1<=k2;
then A3:mid(f,k1,k2)=(f/^(k1-'1))|(k2-'k1+1) by Def1;
k1<k2 by A1,A2,REAL_1:def 5;
then A4:k1+1<=k2 by NAT_1:38;
then A5:k1+1<=len f by A1,AXIOMS:22;
A6:k1-'1<=len f by A1,Th13;
then A7:len f-'(k1-'1)= len f-(k1-'1) by SCMFSA_7:3
.=len f-(k1-1) by A1,SCMFSA_7:3
.=len f-k1+1 by XCMPLX_1:37;
k1+1-k1<=len f-k1 by A5,REAL_1:49; then 1<=len f-k1 by XCMPLX_1:26
;
then 1+1<=len f-k1+1 by AXIOMS:24;
then A8:f/^(k1-'1) is_S-Seq by A1,A6,A7,Th38;
k1+1-k1<=k2-k1 by A4,REAL_1:49; then 1<=k2-k1 by XCMPLX_1:26;
then 1<=k2-'k1 by Th1;
then 1+1<=k2-'k1+1 by AXIOMS:24;
hence mid(f,k1,k2) is_S-Seq by A3,A8,Th37;
suppose A9:k1>k2;
then A10:mid(f,k1,k2)= Rev ((f/^(k2-'1))|(k1-'k2+1)) by Def1;
A11:k2+1<=k1 by A9,NAT_1:38;
then A12:k2+1<=len f by A1,AXIOMS:22;
A13:k2-'1<=len f by A1,Th13;
then A14:len f-'(k2-'1)= len f-(k2-'1) by SCMFSA_7:3
.=len f-(k2-1) by A1,SCMFSA_7:3
.=len f-k2+1 by XCMPLX_1:37;
k2+1-k2<=len f-k2 by A12,REAL_1:49; then 1<=len f-k2 by XCMPLX_1:26
;
then 1+1<=len f-k2+1 by AXIOMS:24;
then A15:f/^(k2-'1) is_S-Seq by A1,A13,A14,Th38;
k2+1-k2<=k1-k2 by A11,REAL_1:49; then 1<=k1-k2 by XCMPLX_1:26;
then 1<=k1-'k2 by Th1;
then 1+1<=k1-'k2+1 by AXIOMS:24;
then (f/^(k2-'1))|(k1-'k2+1) is S-Sequence_in_R2 by A15,Th37;
hence mid(f,k1,k2) is_S-Seq by A10,SPPOL_2:47;
end;
begin
::---------------------------------------------------------:
:: A Concept of Index for Finite Sequences in TOP-REAL 2 :
::---------------------------------------------------------:
definition let f be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2;
assume A1: p in L~f;
func Index(p,f) -> Nat means
:Def2: ex S being non empty Subset of NAT st
it = min S & S = { i: p in LSeg(f,i) };
existence
proof set S = { i: p in LSeg(f,i) };
consider i2 being Nat such that 1<=i2 & i2+1<=len f and
A2: p in LSeg(f,i2) by A1,SPPOL_2:13;
A3: i2 in S by A2;
S c= NAT
proof let x be set;
assume x in S;
then ex i st x = i & p in LSeg(f,i);
hence thesis;
end;
then reconsider S as non empty Subset of NAT by A3;
take min S, S;
thus thesis;
end;
uniqueness;
end;
theorem Th40:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2, i being Nat st p in LSeg(f,i)
holds Index(p,f) <= i
proof let f being FinSequence of TOP-REAL 2;
let p being Point of TOP-REAL 2, i0 be Nat;
A1: LSeg(f,i0) c= L~f by TOPREAL3:26;
assume
A2: p in LSeg(f,i0);
then consider S being non empty Subset of NAT such that
A3: Index(p,f) = min S and
A4: S = { i: p in LSeg(f,i) } by A1,Def2;
i0 in S by A2,A4;
hence Index(p,f) <= i0 by A3,CQC_SIM1:def 8;
end;
theorem Th41:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st p in L~f
holds 1<=Index(p,f) & Index(p,f) < len f
proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume p in L~f;
then consider S being non empty Subset of NAT such that
A1: Index(p,f) = min S and
A2: S = { i: p in LSeg(f,i) } by Def2;
Index(p,f) in S by A1,CQC_SIM1:def 8;
then A3: ex i st i = Index(p,f) & p in LSeg(f,i) by A2;
hence 1 <= Index(p,f) by TOPREAL1:def 5;
Index(p,f) + 1 <= len f by A3,TOPREAL1:def 5;
hence thesis by NAT_1:38;
end;
theorem Th42:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st p in L~f
holds p in LSeg(f,Index(p,f))
proof let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume p in L~f;
then consider S being non empty Subset of NAT such that
A1: Index(p,f) = min S and
A2: S = { i: p in LSeg(f,i) } by Def2;
Index(p,f) in S by A1,CQC_SIM1:def 8;
then ex i st i = Index(p,f) & p in LSeg(f,i) by A2;
hence p in LSeg(f,Index(p,f));
end;
theorem Th43:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st p in LSeg(f,1)
holds Index(p,f) = 1
proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume
A1: p in LSeg(f,1);
then A2: Index(p,f) <= 1 by Th40;
LSeg(f,1) c= L~f by TOPREAL3:26;
then Index(p,f) >= 1 by A1,Th41;
hence Index(p,f) = 1 by A2,AXIOMS:21;
end;
theorem Th44:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st len f >= 2
holds Index(f/.1,f) = 1
proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume len f >= 2;
then 1+1 <= len f;
then f/.1 in LSeg(f,1) by TOPREAL1:27;
hence thesis by Th43;
end;
theorem Th45:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2,i1 st f is_S-Seq
& 1<i1 & i1<=len f & p=f.i1 holds Index(p,f) + 1 = i1
proof let f be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2,i1;
assume
A1: f is_S-Seq;
assume
A2: 1<i1 & i1<=len f;
then A3: i1 in dom f by FINSEQ_3:27;
0 < i1 by A2,AXIOMS:22;
then consider j being Nat such that
A4: i1 = j+1 by NAT_1:22;
A5: 1 + 0 <= j by A2,A4,NAT_1:38;
assume p=f.i1;
then A6: p = f/.i1 by A3,FINSEQ_4:def 4;
then A7: p in LSeg(f,j) by A2,A4,A5,TOPREAL1:27;
then A8: Index(p,f) <= j by Th40;
assume Index(p,f) + 1 <> i1;
then Index(p,f) < j by A4,A8,AXIOMS:21;
then A9: Index(p,f) + 1 <= j by NAT_1:38;
A10: LSeg(f,j) c= L~f by TOPREAL3:26;
then A11: p in LSeg(f,Index(p,f)) by A7,Th42;
per cases by A9,AXIOMS:21;
suppose
A12: Index(p,f) + 1 = j;
A13: f is unfolded by A1,TOPREAL1:def 10;
1 <= Index(p,f) & Index(p,f) + (1+1) <= len f by A2,A4,A7,A10,A12,Th41,
XCMPLX_1:1;
then LSeg(f,Index(p,f)) /\ LSeg(f,j) = {f/.j} by A12,A13,TOPREAL1:def 8;
then p in {f/.j} by A7,A11,XBOOLE_0:def 3;
then A14: p = f/.j by TARSKI:def 1;
A15: j < i1 by A4,NAT_1:38;
j < len f by A2,A4,NAT_1:38;
then A16: j in dom f by A5,FINSEQ_3:27;
f is one-to-one by A1,TOPREAL1:def 10;
hence contradiction by A3,A6,A14,A15,A16,PARTFUN2:17;
suppose
A17: Index(p,f) + 1 < j;
p in LSeg(f,Index(p,f)) /\ LSeg(f,j) by A7,A11,XBOOLE_0:def 3;
then A18: LSeg(f,Index(p,f)) meets LSeg(f,j) by XBOOLE_0:4;
f is s.n.c. by A1,TOPREAL1:def 10;
hence contradiction by A17,A18,TOPREAL1:def 9;
end;
theorem Th46: for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2,i1
st f is_S-Seq & p in LSeg(f,i1)
holds i1=Index(p,f) or i1=Index(p,f)+1
proof let f be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2,i1;
assume that
A1:f is_S-Seq and
A2: p in LSeg(f,i1);
A3: p in L~f by A2,SPPOL_2:17;
A4: Index(p,f) <= i1 by A2,Th40;
assume
A5: not thesis;
then Index(p,f) < i1 by A4,AXIOMS:21;
then Index(p,f)+1 <= i1 by NAT_1:38;
then A6: Index(p,f)+1 < i1 by A5,AXIOMS:21;
p in LSeg(f,Index(p,f)) by A3,Th42;
then p in LSeg(f,Index(p,f)) /\ LSeg(f,i1) by A2,XBOOLE_0:def 3;
then A7: LSeg(f,Index(p,f)) meets LSeg(f,i1) by XBOOLE_0:4;
f is s.n.c. by A1,TOPREAL1:def 10;
hence contradiction by A6,A7,TOPREAL1:def 9;
end;
theorem Th47:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2,i1
st f is_S-Seq & i1+1<=len f & p in LSeg(f,i1) & p <> f.i1
holds i1=Index(p,f)
proof let f be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2,i1;
assume that
A1:f is_S-Seq and
A2: i1+1<=len f and
A3: p in LSeg(f,i1);
assume
A4: p <> f.i1;
A5: p in L~f by A3,SPPOL_2:17;
A6: Index(p,f) <= i1 by A3,Th40;
p in LSeg(f,Index(p,f)) by A5,Th42;
then A7: p in LSeg(f,Index(p,f)) /\ LSeg(f,i1) by A3,XBOOLE_0:def 3;
A8: f is unfolded by A1,TOPREAL1:def 10;
A9: 1 <= Index(p,f) by A5,Th41;
A10: 1 <= Index(p,f)+1 by NAT_1:29;
i1 < len f by A2,NAT_1:38;
then Index(p,f) < len f by A6,AXIOMS:22;
then Index(p,f)+1 <= len f by NAT_1:38;
then A11: Index(p,f) + 1 in dom f by A10,FINSEQ_3:27;
now assume
A12: i1 = Index(p,f)+1;
then Index(p,f) + (1+1) <= len f by A2,XCMPLX_1:1;
then p in {f/.(Index(p,f)+1)} by A7,A8,A9,A12,TOPREAL1:def 8;
then p = f/.(Index(p,f)+1) by TARSKI:def 1;
hence contradiction by A4,A11,A12,FINSEQ_4:def 4;
end;
hence thesis by A1,A3,Th46;
end;
definition let g be FinSequence of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
pred g is_S-Seq_joining p1,p2 means
:Def3: g is_S-Seq & g.1 = p1 & g.len g = p2;
end;
theorem Th48: for g being FinSequence of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st
g is_S-Seq_joining p1,p2
holds Rev g is_S-Seq_joining p2,p1
proof let g be FinSequence of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume that
A1: g is_S-Seq and
A2: g.1=p1 and
A3: g.len g=p2;
thus Rev g is_S-Seq by A1,SPPOL_2:47;
thus (Rev g).1 = p2 by A3,FINSEQ_5:65;
dom g = dom Rev g by FINSEQ_5:60;
hence (Rev g).len Rev g = (Rev g).len g by FINSEQ_3:31
.= p1 by A2,FINSEQ_5:65;
end;
theorem Th49: for f,g being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2,j
st p in L~f
& g=<*p*>^mid(f,Index(p,f)+1,len f) & 1<=j & j+1<=len g
holds LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1)
proof let f,g be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2,j;
assume that
A1: p in L~f and
A2: g=<*p*>^mid(f,Index(p,f)+1,len f) and
A3: 1<=j and
A4: j+1<=len g;
consider i such that A5:1<=i & i+1<=len f & p in LSeg(f,i)
by A1,SPPOL_2:13;
1<=i+1 by NAT_1:37;
then A6:1<=len f by A5,AXIOMS:22;
A7:len g=(len <*p*>)+ len(mid(f,Index(p,f)+1,len f))
by A2,FINSEQ_1:35
.=1+ len(mid(f,Index(p,f)+1,len f)) by FINSEQ_1:56;
then A8: 1<=len g by NAT_1:29;
A9: Index(p,f)<len f by A1,Th41;
then Index(p,f)+1<=len f by NAT_1:38;
then Index(p,f)+1-Index(p,f)<=len f - Index(p,f) by REAL_1:49;
then 1<=len f - Index(p,f) by XCMPLX_1:26;
then 1-1<=len f - Index(p,f)-1 by REAL_1:49;
then A10:0<=len f - (Index(p,f)+1) by XCMPLX_1:36;
A11:Index(p,f)+1<=len f by A9,NAT_1:38;
0<=Index(p,f) by NAT_1:18;
then 0< Index(p,f)+1 by NAT_1:38;
then A12: 0+1<=Index(p,f)+1 by NAT_1:38;
then A13:len(mid(f,Index(p,f)+1,len f))=len f -' (Index(p,f)+1)+1
by A6,A11,Th27;
A14:1<=Index(p,f)+1 & Index(p,f)+1<=len f & 1<=len f & len f<=len f
by A11,A12,AXIOMS:22;
A15:len g=1+(len f -(Index(p,f)+1)+1) by A7,A10,A13,BINARITH:def 3
.=1+((len f - Index(p,f))-1+1) by XCMPLX_1:36
.=1+(len f - Index(p,f)) by XCMPLX_1:27;
A16: len f -'(Index(p,f)+1)=len f -(Index(p,f)+1) by A10,BINARITH:def 3
.=len f - Index(p,f) -1 by XCMPLX_1:36;
len g=len <*p*> + len mid(f,Index(p,f)+1,len f)
by A2,FINSEQ_1:35;
then A17:len g=1+len mid(f,Index(p,f)+1,len f) by FINSEQ_1:56;
A18:len mid(f,Index(p,f)+1,len f)=len f -Index(p,f)
by A13,A16,XCMPLX_1:27;
A19:j<=len g by A4,NAT_1:38;
A20:1<=j+1 by A3,NAT_1:38;
A21:j-'1=j-1 by A3,SCMFSA_7:3;
A22:j+1-'1=j+1-1 by A20,SCMFSA_7:3;
A23:j=1+j-1 by XCMPLX_1:26 .=1+(j-1) by XCMPLX_1:29
.=len <*p*> +(j-'1) by A21,FINSEQ_1:56;
A24:j+1=1+(j+1-1) by XCMPLX_1:26
.=len <*p*> +(j+1-1) by FINSEQ_1:56
.=len <*p*> +(j+1-'1) by A20,SCMFSA_7:3;
A25:1<=Index(p,f)+j by A3,NAT_1:37;
then A26: 1-1<=Index(p,f)+j-1 by REAL_1:49;
j+1-1<=1+len mid(f,Index(p,f)+1,len f)-1
by A4,A17,REAL_1:49;
then j+1-1<= len f -Index(p,f) by A18,XCMPLX_1:26;
then j<=len f -Index(p,f) by XCMPLX_1:26;
then j+Index(p,f)<= len f -Index(p,f)+Index(p,f) by AXIOMS:24;
then Index(p,f)+j <= len f by XCMPLX_1:27;
then Index(p,f)+(j-1+1) <= len f by XCMPLX_1:27;
then Index(p,f)+(j-1)+1 <= len f by XCMPLX_1:1;
then Index(p,f)+j-1+1 <= len f by XCMPLX_1:29;
then A27:Index(p,f)+j-'1+1 <= len f by A26,BINARITH:def 3;
A28: j+1-1<=1+len mid(f,Index(p,f)+1,len f)-1
by A4,A17,REAL_1:49;
then A29: j+1-1<=len mid(f,Index(p,f)+1,len f) by XCMPLX_1:26;
A30:1<=j+1-'1 & j+1-'1<=len mid(f,Index(p,f)+1,len f)
by A3,A22,A28,XCMPLX_1:26;
then A31:j+1-'1 in dom mid(f,Index(p,f)+1,len f) by FINSEQ_3:27;
A32:j<=len mid(f,Index(p,f)+1,len f) by A29,XCMPLX_1:26;
j-'1<=j by GOBOARD9:2;
then A33:j-'1<=len mid(f,Index(p,f)+1,len f) by A32,AXIOMS:22;
A34:g.(j+1) =mid(f,Index(p,f)+1,len f).(j+1-'1)
by A2,A24,A31,FINSEQ_1:def 7
.=f.(j+1-'1+(Index(p,f)+1)-'1) by A14,A30,Th27
.=f.(j+1-'1+1+Index(p,f)-'1) by XCMPLX_1:1
.=f.(j+1+Index(p,f)-'1) by A20,AMI_5:4
.=f.(Index(p,f)+j+1-'1) by XCMPLX_1:1
.=f.(Index(p,f)+j) by BINARITH:39
.=f.(Index(p,f)+j-'1+1) by A25,AMI_5:4;
j<=len f - Index(p,f) by A4,A15,REAL_1:53;
then j+Index(p,f)<=len f - Index(p,f)+Index(p,f) by AXIOMS:24;
then A35:Index(p,f)+j<=len f by XCMPLX_1:27;
then A36:Index(p,f)+j-'1+1<=len f by A25,AMI_5:4;
A37:Index(p,f)+j-'1<=len f by A35,Th13;
A38:1<=Index(p,f)+j-'1+1 by NAT_1:29;
g/.(j+1)=g.(j+1) by A4,A20,FINSEQ_4:24;
then A39:f/.(Index(p,f)+j-'1+1)=g/.(j+1) by A34,A36,A38,FINSEQ_4:24;
1 <= Index(p,f) by A1,Th41;
then 1+1 <= Index(p,f)+j by A3,REAL_1:55;
then 1<=Index(p,f)+j-1 by REAL_1:84;
then A40:1<=Index(p,f)+j-'1 by Th1;
then A41:LSeg(f,Index(p,f)+j-'1)
=LSeg(f/.(Index(p,f)+j-'1),f/.(Index(p,f)+j-'1+1))
by A27,TOPREAL1:def 5;
now per cases by A3,REAL_1:def 5;
case A42:1<j;
then A43:j-'1=j-1 by SCMFSA_7:3;
then A44:1<=j-'1 by A42,SPPOL_1:6;
j-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A17,A19,REAL_1:49;
then j-'1<=len mid(f,Index(p,f)+1,len f) by A43,XCMPLX_1:26;
then j-'1 in dom mid(f,Index(p,f)+1,len f) by A44,FINSEQ_3:27;
then A45:g.j =mid(f,Index(p,f)+1,len f).(j-'1)
by A2,A23,FINSEQ_1:def 7
.=f.(j-'1+(Index(p,f)+1)-'1) by A14,A33,A44,Th27
.=f.(j-'1+1+Index(p,f)-'1) by XCMPLX_1:1
.=f.(Index(p,f)+j-'1) by A3,AMI_5:4;
g/.j=g.j by A3,A19,FINSEQ_4:24;
then LSeg(f,Index(p,f)+j-'1)
=LSeg(g/.j,g/.(j+1)) by A37,A39,A40,A41,A45,FINSEQ_4:24
.=LSeg(g,j) by A3,A4,TOPREAL1:def 5;
hence thesis;
case A46:1=j;
then 1<=j & j<=len <*p*> by FINSEQ_1:56;
then j in dom <*p*> by FINSEQ_3:27;
then A47:g.j =<*p*>.j by A2,FINSEQ_1:def 7
.=p by A46,FINSEQ_1:57;
A48:g/.j=g.j by A8,A46,FINSEQ_4:24;
A49:f/.(Index(p,f)+j-'1+1)
in LSeg(f/.(Index(p,f)+j-'1),f/.(Index(p,f)+j-'1+1))
by TOPREAL1:6;
A50: Index(p,f)+j-'1 = Index(p,f) by A46,BINARITH:39;
p in LSeg(f,Index(p,f)) by A1,Th42;
then LSeg(p,g/.(j+1))
c= LSeg(f,Index(p,f)+j-'1) by A39,A41,A49,A50,TOPREAL1:12;
hence thesis by A3,A4,A47,A48,TOPREAL1:def 5;
end;
hence LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1);
end;
theorem
for f,g being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2
st f is_S-Seq & p in L~f & p<>f.(Index(p,f)+1) &
g=<*p*>^mid(f,Index(p,f)+1,len f)
holds g is_S-Seq_joining p,f/.len f
proof let f,g be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq and
A2: p in L~f and
A3: p<>f.(Index(p,f)+1) and
A4: g=<*p*>^mid(f,Index(p,f)+1,len f);
consider i such that A5:1<=i & i+1<=len f & p in LSeg(f,i)
by A2,SPPOL_2:13;
1<=1+i by NAT_1:37;
then A6:1<=len f by A5,AXIOMS:22;
A7:len g=(len <*p*>)+ len(mid(f,Index(p,f)+1,len f))
by A4,FINSEQ_1:35
.=1+ len(mid(f,Index(p,f)+1,len f)) by FINSEQ_1:56;
A8: f is unfolded by A1,TOPREAL1:def 10;
A9: Index(p,f)<len f by A2,Th41;
then Index(p,f)+1<=len f by NAT_1:38;
then Index(p,f)+1-Index(p,f)<=len f - Index(p,f) by REAL_1:49;
then A10:1<=len f - Index(p,f) by XCMPLX_1:26;
then 1-1<=len f - Index(p,f)-1 by REAL_1:49;
then A11:0<=len f - (Index(p,f)+1) by XCMPLX_1:36;
A12:Index(p,f)<len f by A2,Th41;
A13:Index(p,f)+1<=len f by A9,NAT_1:38;
A14: len f - Index(p,f)>=0 by A12,SQUARE_1:11;
A15: 0+1<=Index(p,f)+1 by NAT_1:29;
then A16:len(mid(f,Index(p,f)+1,len f))=len f -' (Index(p,f)+1)+1
by A6,A13,Th27;
then len g=1+(len f -(Index(p,f)+1)+1) by A7,A11,BINARITH:def 3
.=1+((len f - Index(p,f))-1+1) by XCMPLX_1:36
.=1+(len f - Index(p,f)) by XCMPLX_1:27;
then A17:len g -1 =len f -Index(p,f) by XCMPLX_1:26;
then 0<len g -1 by A10,AXIOMS:22;
then A18:len g -'1=len g -1 by BINARITH:def 3;
len f -'(Index(p,f)+1)=len f -(Index(p,f)+1) by A11,BINARITH:def 3
.=len f - Index(p,f) -1 by XCMPLX_1:36;
then A19:len f -'(Index(p,f)+1)+1=len f -Index(p,f) by XCMPLX_1:27;
then A20:len g -'1 in dom (mid(f,Index(p,f)+1,len f))
by A10,A16,A17,A18,FINSEQ_3:27;
1<=1+ len(mid(f,Index(p,f)+1,len f)) by NAT_1:29;
then len g -1>=0 by A7,SQUARE_1:12;
then 1+(len g -'1)=1+(len g -1) by BINARITH:def 3
.=len g by XCMPLX_1:27;
then A21:g.len g =g.(len <*p*> + (len g -'1)) by FINSEQ_1:56
.=mid(f,Index(p,f)+1,len f).(len g -'1)
by A4,A20,FINSEQ_1:def 7;
A22:len f -Index(p,f)=len f -' Index(p,f) by A14,BINARITH:def 3;
A23:len g -'1= len f -' Index(p,f) by A14,A17,A18,BINARITH:def 3;
A24:mid(f,Index(p,f)+1,len f).(len f -' Index(p,f))
=f.(len f -' Index(p,f)+(Index(p,f)+1)-'1)
by A6,A10,A13,A15,A16,A19,A22,Th27;
len f -' Index(p,f)+(Index(p,f)+1)
=len f - Index(p,f)+(Index(p,f)+1) by A14,BINARITH:def 3
.=len f - Index(p,f)+Index(p,f)+1 by XCMPLX_1:1
.= len f +1 by XCMPLX_1:27;
then A25: g.len g=f.len f by A21,A23,A24,BINARITH:39;
len g=len <*p*> + len mid(f,Index(p,f)+1,len f)
by A4,FINSEQ_1:35;
then A26:len g=1+len mid(f,Index(p,f)+1,len f) by FINSEQ_1:56;
A27:f is one-to-one by A1,TOPREAL1:def 10;
A28: 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 A29:x1 in dom g & x2 in dom g & g.x1=g.x2;
then reconsider n1=x1,n2=x2 as Nat;
A30:1<=n1 & n1<=len g & 1<=n2 & n2<=len g by A29,FINSEQ_3:27;
now per cases by A30,REAL_1:def 5;
case n1=1 & n2=1;
hence x1=x2;
case that
A31: n1=1 and
A32: n2>1;
1 <= Index(p,f) by A2,Th41;
then 1 + 1 < n2+Index(p,f) by A32,REAL_1:67;
then A33: 1< n2+Index(p,f)-1 by REAL_1:86;
then 0<=n2+Index(p,f)-1 by AXIOMS:22;
then A34: n2+Index(p,f)-'1 = n2+Index(p,f)-1 by BINARITH:def 3;
1<=n1 & n1<=len <*p*> by A31,FINSEQ_1:56;
then n1 in dom <*p*> by FINSEQ_3:27;
then A35: g.n1=<*p*>.n1 by A4,FINSEQ_1:def 7;
n2-1>0 by A32,SQUARE_1:11;
then A36:n2-'1=n2-1 by BINARITH:def 3;
then A37: 0+1<=n2-'1 by A32,SPPOL_1:6;
n2-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A26,A30,REAL_1:49;
then A38:1<=n2-'1 & n2-'1<=len mid(f,Index(p,f)+1,len f)
by A32,A36,SPPOL_1:6,XCMPLX_1:26;
then A39:n2-'1 in dom mid(f,Index(p,f)+1,len f) by FINSEQ_3:27;
len <*p*>+(n2-'1)=1+(n2-1) by A36,FINSEQ_1:56 .=n2 by XCMPLX_1:27;
then g.n2 =mid(f,Index(p,f)+1,len f).(n2-'1)
by A4,A39,FINSEQ_1:def 7
.=f.(n2-'1+(Index(p,f)+1)-'1) by A6,A13,A15,A38,Th27
.=f.(n2-'1+1+Index(p,f)-'1) by XCMPLX_1:1
.=f.(n2+Index(p,f)-'1) by A37,Th6;
then A40:f.(n2+Index(p,f)-'1)=p by A29,A31,A35,FINSEQ_1:57;
n2 -' 1 <= len f - Index(p,f) by A17,A18,A30,Th5;
then n2-1 <= len f - Index(p,f) by A32,SCMFSA_7:3;
then n2-1+Index(p,f) <= len f - Index(p,f)+ Index(p,f) by AXIOMS:24
;
then n2-1+Index(p,f) <= len f by XCMPLX_1:27;
then n2+Index(p,f)-'1 <= len f by A34,XCMPLX_1:29;
hence contradiction by A1,A3,A33,A34,A40,Th45;
case that
A41: n1>1 and
A42: n2=1;
1 <= Index(p,f) by A2,Th41;
then 1 + 1 < n1+Index(p,f) by A41,REAL_1:67;
then A43: 1< n1+Index(p,f)-1 by REAL_1:86;
then 0<=n1+Index(p,f)-1 by AXIOMS:22;
then A44: n1+Index(p,f)-'1 = n1+Index(p,f)-1 by BINARITH:def 3;
1<=n2 & n2<=len <*p*> by A42,FINSEQ_1:56;
then n2 in dom <*p*> by FINSEQ_3:27;
then A45: g.n2=<*p*>.n2 by A4,FINSEQ_1:def 7;
n1-1>0 by A41,SQUARE_1:11;
then A46:n1-'1=n1-1 by BINARITH:def 3;
then A47: 0+1<=n1-'1 by A41,SPPOL_1:6;
n1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A26,A30,REAL_1:49;
then A48:1<=n1-'1 & n1-'1<=len mid(f,Index(p,f)+1,len f)
by A41,A46,SPPOL_1:6,XCMPLX_1:26;
then A49:n1-'1 in dom mid(f,Index(p,f)+1,len f) by FINSEQ_3:27;
len <*p*>+(n1-'1)=1+(n1-1) by A46,FINSEQ_1:56 .=n1 by XCMPLX_1:27;
then g.n1 =mid(f,Index(p,f)+1,len f).(n1-'1)
by A4,A49,FINSEQ_1:def 7
.=f.(n1-'1+(Index(p,f)+1)-'1) by A6,A13,A15,A48,Th27
.=f.(n1-'1+1+Index(p,f)-'1) by XCMPLX_1:1
.=f.(n1+Index(p,f)-'1) by A47,Th6;
then A50:f.(n1+Index(p,f)-'1)=p by A29,A42,A45,FINSEQ_1:57;
n1 -' 1 <= len f - Index(p,f) by A17,A18,A30,Th5;
then n1-1 <= len f - Index(p,f) by A41,SCMFSA_7:3;
then n1-1+Index(p,f) <= len f - Index(p,f)+ Index(p,f) by AXIOMS:24
;
then n1-1+Index(p,f) <= len f by XCMPLX_1:27;
then n1+Index(p,f)-'1 <= len f by A44,XCMPLX_1:29;
hence contradiction by A1,A3,A43,A44,A50,Th45;
case that
A51: n1>1 and
A52: n2>1;
A53:n2-1>0 by A52,SQUARE_1:11;
then A54:n2-'1=n2-1 by BINARITH:def 3;
then A55: 0+1<=n2-'1 by A53,NAT_1:38;
n2-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A26,A30,REAL_1:49;
then A56:1<=n2-'1 & n2-'1<=len mid(f,Index(p,f)+1,len f)
by A54,A55,XCMPLX_1:26;
then A57:n2-'1 in dom mid(f,Index(p,f)+1,len f) by FINSEQ_3:27;
len <*p*>+(n2-'1)=1+(n2-1) by A54,FINSEQ_1:56 .=n2 by XCMPLX_1:27;
then A58:g.n2 =mid(f,Index(p,f)+1,len f).(n2-'1)
by A4,A57,FINSEQ_1:def 7
.=f.(n2-'1+(Index(p,f)+1)-'1) by A6,A13,A15,A56,Th27
.=f.(n2-'1+1+Index(p,f)-'1) by XCMPLX_1:1
.=f.(n2+Index(p,f)-'1) by A55,Th6;
A59: 1<=n2-'1 + Index(p,f) by A55,NAT_1:37;
then 1<=n2+Index(p,f)-1 by A54,XCMPLX_1:29;
then 0<=n2+Index(p,f)-1 by AXIOMS:22;
then A60:n2+Index(p,f)-'1 = n2+Index(p,f)-1 by BINARITH:def 3;
n2-'1 <= len f -' Index(p,f) by A23,A30,Th5;
then n2-'1+Index(p,f)<=len f - Index(p,f)+ Index(p,f)
by A22,AXIOMS:24;
then n2-1+Index(p,f)<=len f by A54,XCMPLX_1:27;
then 1<=n2+Index(p,f)-'1 & n2+Index(p,f)-'1<=len f
by A54,A59,A60,XCMPLX_1:29;
then A61:n2+Index(p,f)-'1 in dom f by FINSEQ_3:27;
A62:n1-1>0 by A51,SQUARE_1:11;
then A63:n1-'1=n1-1 by BINARITH:def 3;
then A64: 0+1<=n1-'1 by A62,NAT_1:38;
n1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A26,A30,REAL_1:49;
then A65:1<=n1-'1 & n1-'1<=len mid(f,Index(p,f)+1,len f)
by A63,A64,XCMPLX_1:26;
then A66:n1-'1 in dom mid(f,Index(p,f)+1,len f) by FINSEQ_3:27;
len <*p*>+(n1-'1)=1+(n1-1) by A63,FINSEQ_1:56 .=n1 by XCMPLX_1:27;
then A67:g.n1 =mid(f,Index(p,f)+1,len f).(n1-'1)
by A4,A66,FINSEQ_1:def 7
.=f.(n1-'1+(Index(p,f)+1)-'1) by A6,A13,A15,A65,Th27
.=f.(n1-'1+1+Index(p,f)-'1) by XCMPLX_1:1
.=f.(n1+Index(p,f)-'1) by A64,Th6;
1<=n1-1+Index(p,f) by A63,A64,NAT_1:37;
then A68:1<=n1+Index(p,f)-1 by XCMPLX_1:29;
then 0<=n1+Index(p,f)-1 by AXIOMS:22;
then A69:n1+Index(p,f)-'1 = n1+Index(p,f)-1 by BINARITH:def 3;
n1-'1 <= len f -' Index(p,f) by A23,A30,Th5;
then n1-'1+Index(p,f)<=len f - Index(p,f)+ Index(p,f)
by A22,AXIOMS:24;
then n1-'1+Index(p,f)<=len f by XCMPLX_1:27;
then n1+Index(p,f)-'1<=len f by A63,A69,XCMPLX_1:29;
then n1+Index(p,f)-'1 in dom f by A68,A69,FINSEQ_3:27;
then n1+Index(p,f)-'1=n2+Index(p,f)-'1
by A27,A29,A58,A61,A67,FUNCT_1:def 8;
then n1+Index(p,f)=n2+Index(p,f)-1+1 by A60,A69,XCMPLX_1:27;
then n1+Index(p,f)=n2+Index(p,f) by XCMPLX_1:27;
hence x1=x2 by XCMPLX_1:2;
end;
hence x1=x2;
end;
A70: len g -1+1>=1+1 by A10,A17,AXIOMS:24;
A71: for j st 1 <= j & j + 2 <= len g
holds LSeg(g,j) /\ LSeg(g,j+1) = {g/.(j+1)}
proof let j;assume A72:1 <= j & j + 2 <= len g;
A73:j+2=j+(1+1) .=j+1+1 by XCMPLX_1:1;
then A74:j+1<=len g by A72,NAT_1:38;
A75:1<j+1 by A72,NAT_1:38;
A76:1<=(j+1) by A72,NAT_1:38;
A77: 1+1-1<=(j+1)-1 by A75,SPPOL_1:6;
A78:LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1)
by A2,A4,A72,A74,Th49;
LSeg(g,(j+1)) c= LSeg(f,Index(p,f)+(j+1)-'1)
by A2,A4,A72,A73,A76,Th49;
then A79:LSeg(g,j)/\ LSeg(g,(j+1))
c= LSeg(f,Index(p,f)+j-'1)/\ LSeg(f,Index(p,f)+(j+1)-'1)
by A78,XBOOLE_1:27;
1<=Index(p,f) by A2,Th41;
then A80:1<=Index(p,f)+j by NAT_1:37;
then A81: 1-1<=Index(p,f)+j-1 by REAL_1:49;
A82:1<=Index(p,f)+j-'1+1 by NAT_1:29;
A83:j+1=j+1-1+1 by XCMPLX_1:26 .=j+1-'1+1 by A75,SCMFSA_7:3;
then A84:j+1=len <*p*>+(j+1-'1) by FINSEQ_1:56;
A85:1<=j+1-'1 & j+1-'1<=len mid(f,Index(p,f)+1,len f)
by A26,A74,A77,A83,Th1,REAL_1:53;
then j+1-'1 in dom mid(f,Index(p,f)+1,len f) by FINSEQ_3:27;
then A86:g.(j+1) = mid(f,Index(p,f)+1,len f).(j+1-'1)
by A4,A84,FINSEQ_1:def 7
.=f.(j+1-'1+(Index(p,f)+1)-'1) by A6,A13,A15,A85,Th27
.=f.(j+1-'1+1+Index(p,f)-'1) by XCMPLX_1:1
.=f.(j+1+Index(p,f)-'1) by A75,AMI_5:4
.=f.(Index(p,f)+j+1-'1) by XCMPLX_1:1
.=f.(Index(p,f)+j) by BINARITH:39
.=f.(Index(p,f)+j-'1+1) by A80,AMI_5:4;
1 <= Index(p,f) by A2,Th41;
then 1+1 <= Index(p,f)+j by A72,REAL_1:55;
then 1<=Index(p,f)+j-1 by REAL_1:84;
then A87:1<=Index(p,f)+j-'1 by Th1;
A88:1<=Index(p,f)+j+1 by NAT_1:29;
A89:Index(p,f)+(j+1)-'1
=Index(p,f)+j+1-'1 by XCMPLX_1:1
.=Index(p,f)+j+1-1 by A88,SCMFSA_7:3
.=Index(p,f)+j-1+1 by XCMPLX_1:29
.=Index(p,f)+j-'1+1 by A80,SCMFSA_7:3;
A90:g/.(j+1)=g.(j+1) by A74,A75,FINSEQ_4:24;
A91:LSeg(g/.(j+1),g/.(j+1+1))=LSeg(g,j+1)
by A72,A73,A75,TOPREAL1:def 5;
j+1+1-1<=1+len mid(f,Index(p,f)+1,len f)-1
by A26,A72,A73,REAL_1:49;
then j+1+1-1<=len mid(f,Index(p,f)+1,len f) by XCMPLX_1:26;
then j+1<=len f -Index(p,f) by A16,A19,XCMPLX_1:26;
then j+1+Index(p,f)<= len f -Index(p,f)+Index(p,f) by AXIOMS:24;
then j+1+Index(p,f)<= len f by XCMPLX_1:27;
then A92:Index(p,f)+j+1 <= len f by XCMPLX_1:1;
then Index(p,f)+(j-1+1)+1 <= len f by XCMPLX_1:27;
then Index(p,f)+(j-1)+1+1 <= len f by XCMPLX_1:1;
then Index(p,f)+j-1+1+1 <= len f by XCMPLX_1:29;
then Index(p,f)+j-1+(1+1) <= len f by XCMPLX_1:1;
then Index(p,f)+j-'1+2 <= len f by A81,BINARITH:def 3;
then A93:{f/.(Index(p,f)+j-'1+1)}
= LSeg(f,Index(p,f)+j-'1)/\ LSeg(f,Index(p,f)+j-'1+1)
by A8,A87,TOPREAL1:def 8;
Index(p,f)+j<=len f by A92,Th9;
then Index(p,f)+(j-1+1) <= len f by XCMPLX_1:27;
then Index(p,f)+(j-1)+1 <= len f by XCMPLX_1:1;
then Index(p,f)+j-1+1 <= len f by XCMPLX_1:29;
then Index(p,f)+j-'1+1 <= len f by A81,BINARITH:def 3;
then A94:f/.(Index(p,f)+j-'1+1)=g/.(j+1) by A82,A86,A90,FINSEQ_4:24;
A95:LSeg(g,j)=LSeg(g/.j,g/.(j+1)) by A72,A74,TOPREAL1:def 5;
A96:g/.(j+1) in LSeg(g/.j,g/.(j+1)) by TOPREAL1:6;
g/.(j+1) in LSeg(g/.(j+1),g/.(j+1+1)) by TOPREAL1:6;
then g/.(j+1) in LSeg(g/.j,g/.(j+1)) /\ LSeg(g/.(j+1),g/.(j+1+1))
by A96,XBOOLE_0:def 3;
then {g/.(j+1)} c= LSeg(g,j) /\ LSeg(g,j+1) by A91,A95,ZFMISC_1:37;
hence {g/.(j+1)} = LSeg(g,j)/\ LSeg(g,j+1)
by A79,A89,A93,A94,XBOOLE_0:def 10;
end;
A97: f is s.n.c. by A1,TOPREAL1:def 10;
A98: for j1,j2 st j1+1 < j2 holds LSeg(g,j1) misses LSeg(g,j2)
proof let j1,j2;assume A99:j1+1 < j2;
j1>=0 by NAT_1:18;
then A100: j1=0 or j1>=0+1 by NAT_1:38;
now per cases by A100,REAL_1:def 5;
case j1=0;
then LSeg(g,j1)={} by TOPREAL1:def 5;
then LSeg(g,j1) /\ LSeg(g,j2) = {};
hence LSeg(g,j1) misses LSeg(g,j2) by XBOOLE_0:def 7;
case that A101:j1=1 or j1>1 and
A102: j2+1<=len g;
j2<len g by A102,NAT_1:38;
then A103:j1+1<=len g by A99,AXIOMS:22;
1<j1+1 by A101,NAT_1:38;
then A104:1<=j2 by A99,AXIOMS:22;
A105:LSeg(g,j1) c= LSeg(f,Index(p,f)+j1-'1)
by A2,A4,A101,A103,Th49;
LSeg(g,j2) c= LSeg(f,Index(p,f)+j2-'1) by A2,A4,A102,A104,Th49;
then A106:LSeg(g,j1)/\ LSeg(g,j2)
c= LSeg(f,Index(p,f)+j1-'1)/\ LSeg(f,Index(p,f)+j2-'1)
by A105,XBOOLE_1:27;
Index(p,f)+(j1+1)<Index(p,f)+j2 by A99,REAL_1:53;
then Index(p,f)+j1+1<Index(p,f)+j2 by XCMPLX_1:1;
then Index(p,f)+j1+1-1<Index(p,f)+j2-1 by REAL_1:54;
then A107:Index(p,f)+j1-1+1<Index(p,f)+j2-1 by XCMPLX_1:29;
1<=Index(p,f) by A2,Th41;
then 1<=Index(p,f)+j1 by NAT_1:37;
then 1-1<=Index(p,f)+j1-1 by REAL_1:49;
then A108:Index(p,f)+j1-1=Index(p,f)+j1-'1 by BINARITH:def 3;
1<=Index(p,f) by A2,Th41;
then 1<=Index(p,f)+j2 by NAT_1:37;
then 1-1<=Index(p,f)+j2-1 by REAL_1:49;
then Index(p,f)+j1-'1+1<Index(p,f)+j2-'1
by A107,A108,BINARITH:def 3;
then LSeg(f,Index(p,f)+j1-'1) misses LSeg(f,Index(p,f)+j2-'1) by A97,
TOPREAL1:def 9;
then LSeg(f,Index(p,f)+j1-'1) /\ LSeg(f,Index(p,f)+j2-'1) = {}
by XBOOLE_0:def 7;
then LSeg(g,j1) /\ LSeg(g,j2) = {} by A106,XBOOLE_1:3;
hence LSeg(g,j1) misses LSeg(g,j2) by XBOOLE_0:def 7;
case j2+1>len g; then LSeg(g,j2)={} by TOPREAL1:def 5;
then LSeg(g,j1) /\ LSeg(g,j2) = {};
hence thesis by XBOOLE_0:def 7;
end;
hence LSeg(g,j1) misses LSeg(g,j2);
end;
A109: f is special by A1,TOPREAL1:def 10;
for j st 1 <= j & j+1 <= len g holds
(g/.j)`1 = (g/.(j+1))`1 or (g/.j)`2 = (g/.(j+1))`2
proof let j;assume A110: 1 <= j & j+1 <= len g;
then A111:LSeg(g,j) c= LSeg(f,Index(p,f)+j-'1) by A2,A4,Th49;
A112:LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A110,TOPREAL1:def 5;
1<=Index(p,f) by A2,Th41;
then A113:1<Index(p,f)+1 by NAT_1:38;
Index(p,f)+1<=Index(p,f)+j by A110,AXIOMS:24;
then 1<Index(p,f)+j by A113,AXIOMS:22;
then A114:1<=Index(p,f)+j-1 by SPPOL_1:6;
then 0<=Index(p,f)+j-1 by AXIOMS:22;
then A115:Index(p,f)+j-1=Index(p,f)+j-'1 by BINARITH:def 3;
j+1-1<=1+len mid(f,Index(p,f)+1,len f)-1 by A26,A110,REAL_1:49;
then j+1-1<= len f -Index(p,f) by A16,A19,XCMPLX_1:26;
then j<=len f -Index(p,f) by XCMPLX_1:26;
then j+Index(p,f)<= len f -Index(p,f)+Index(p,f) by AXIOMS:24;
then j+Index(p,f)<= len f by XCMPLX_1:27;
then Index(p,f)+(j-1+1) <= len f by XCMPLX_1:27;
then Index(p,f)+(j-1)+1 <= len f by XCMPLX_1:1;
then A116:Index(p,f)+j-'1+1 <= len f by A115,XCMPLX_1:29;
then A117:LSeg(f,Index(p,f)+j-'1)
= LSeg(f/.(Index(p,f)+j-'1),f/.(Index(p,f)+j-'1+1))
by A114,A115,TOPREAL1:def 5;
(f/.(Index(p,f)+j-'1))`1 = (f/.(Index(p,f)+j-'1+1))`1
or (f/.(Index(p,f)+j-'1))`2 = (f/.(Index(p,f)+j-'1+1))`2
by A109,A114,A115,A116,TOPREAL1:def 7;
hence (g/.j)`1 = (g/.(j+1))`1 or (g/.j)`2 = (g/.(j+1))`2
by A111,A112,A117,Th36;
end;
then g is one-to-one & len g >= 2
& g is unfolded s.n.c. special by A28,A70,A71,A98,FUNCT_1:def 8,TOPREAL1:
def 7,def 8,def 9,XCMPLX_1:27;
then g is_S-Seq & g.1 = p & g.len g = f/.len f by A4,A6,A25,FINSEQ_1:58,
FINSEQ_4:24,TOPREAL1:def 10;
hence g is_S-Seq_joining p,f/.len f by Def3;
end;
theorem Th51: for f,g being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2,j
st p in L~f & 1<=j & j+1<=len g
& g=mid(f,1,Index(p,f))^<*p*>
holds LSeg(g,j) c= LSeg(f,j)
proof let f,g be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2,j;
assume that
A1: p in L~f and
A2: 1<=j and
A3: j+1<=len g and
A4: g=mid(f,1,Index(p,f))^<*p*>;
A5:1<=Index(p,f) by A1,Th41;
A6:Index(p,f) < len f by A1,Th41;
then A7:1<=1 & 1<=len f & 1<=Index(p,f) & Index(p,f)<=len f by A5,AXIOMS:22;
j<=j+1 by NAT_1:29;
then A8:j<=len g by A3,AXIOMS:22;
A9:1<=j+1 by NAT_1:29;
now
len g=len mid(f,1,Index(p,f)) + len <*p*> by A4,FINSEQ_1:35
.=len mid(f,1,Index(p,f))+1 by FINSEQ_1:56;
then len g=Index(p,f)-'1+1+1 by A7,Th27;
then A10:len g=Index(p,f)+1 by A5,AMI_5:4;
Index(p,f)+1<=len f +1 by A6,AXIOMS:24;
then j+1<=len f +1 by A3,A10,AXIOMS:22;
then j+1-1<=len f +1-1 by REAL_1:49;
then j<=len f +1-1 by XCMPLX_1:26;
then A11:j<=len f by XCMPLX_1:26;
A12:j<=Index(p,f) by A3,A10,REAL_1:53;
A13: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A7,Th27
.=Index(p,f) by A5,AMI_5:4;
then A14:j in dom mid(f,1,Index(p,f)) by A2,A12,FINSEQ_3:27;
A15:g/.j=g.j by A2,A8,FINSEQ_4:24
.=mid(f,1,Index(p,f)).j by A4,A14,FINSEQ_1:def 7
.=f.(j+1-'1) by A2,A7,A12,A13,Th27
.=f.j by BINARITH:39
.=f/.j by A2,A11,FINSEQ_4:24;
now per cases;
case A16:j+1<=Index(p,f);
then A17:j+1<=len f by A6,AXIOMS:22;
A18: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A7,Th27
.=Index(p,f) by A5,AMI_5:4;
then A19:j+1 in dom mid(f,1,Index(p,f)) by A9,A16,FINSEQ_3:27;
A20:g/.(j+1)=g.(j+1) by A3,A9,FINSEQ_4:24
.= mid(f,1,Index(p,f)).(j+1) by A4,A19,FINSEQ_1:def 7
.=f.(j+1+1-'1) by A7,A9,A16,A18,Th27
.=f.(j+1) by BINARITH:39
.=f/.(j+1) by A9,A17,FINSEQ_4:24;
LSeg(g,j)=LSeg(g/.j,g/.(j+1)) by A2,A3,TOPREAL1:def 5;
hence LSeg(g,j) c= LSeg(f,j) by A2,A15,A17,A20,TOPREAL1:def 5;
case j+1>Index(p,f);
then j>=Index(p,f) by NAT_1:38;
then A21:j=Index(p,f) by A12,AXIOMS:21;
1<=1 & 1<=len <*p*> by FINSEQ_1:57;
then A22:1 in dom <*p*> by FINSEQ_3:27;
A23:len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A7,Th27
.=Index(p,f) by A5,AMI_5:4;
A24:g/.(j+1)=g.(j+1) by A3,A9,FINSEQ_4:24
.=<*p*>.1 by A4,A21,A22,A23,FINSEQ_1:def 7
.=p by FINSEQ_1:def 8;
A25:f/.j in LSeg(f/.j,f/.(j+1)) by TOPREAL1:6;
A26:p in LSeg(f,j) by A1,A21,Th42;
now assume j+1>len f;
then j>=len f by NAT_1:38;
hence contradiction by A1,A21,Th41;
end;
then A27:LSeg(f,j)=LSeg(f/.j,f/.(j+1)) by A2,TOPREAL1:def 5;
then LSeg(g/.j,g/.(j+1)) c= LSeg(f/.j,f/.(j+1))
by A15,A24,A25,A26,TOPREAL1:12;
hence LSeg(g,j) c= LSeg(f,j) by A2,A3,A27,TOPREAL1:def 5;
end;
hence LSeg(g,j) c= LSeg(f,j);
end;
hence LSeg(g,j) c= LSeg(f,j);
end;
theorem Th52: for f,g being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2
st f is_S-Seq & p in L~f & p<>f.1
& g=mid(f,1,Index(p,f))^<*p*>
holds g is_S-Seq_joining f/.1,p
proof let f,g be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2;
assume that
A1:f is_S-Seq and
A2: p in L~f and
A3: p<>f.1 and
A4: g=mid(f,1,Index(p,f))^<*p*>;
consider i such that A5:1<=i & i+1<=len f & p in LSeg(f,i)
by A2,SPPOL_2:13;
A6:1<=Index(p,f) by A2,Th41;
A7:Index(p,f)<=len f by A2,Th41;
1<=1+i by NAT_1:37;
then A8:1<=len f by A5,AXIOMS:22;
then A9: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A6,A7,Th27;
then A10:len mid(f,1,Index(p,f))=Index(p,f) by A6,AMI_5:4;
1<=len <*p*> by FINSEQ_1:56;
then A11: 1 in dom <*p*> by FINSEQ_3:27;
g.1=mid(f,1,Index(p,f)).1 by A4,A6,A10,Th17;
then g.1=f.1 by A6,A7,A8,Th27;
then A12: g.1=f/.1 by A8,FINSEQ_4:24;
A13: len g = len mid(f,1,Index(p,f))+ len<*p*> by A4,FINSEQ_1:35
.= len mid(f,1,Index(p,f))+ 1 by FINSEQ_1:56;
then A14: g.len g = p by A4,Th16;
A15: 1+1<=len g by A6,A10,A13,AXIOMS:24;
A16: f is one-to-one by A1,TOPREAL1:def 10;
A17:for n1,n2 being Nat st 1<=n1 & n1<=len f
& 1<=n2 & n2<=len f & f.n1=f.n2
holds n1=n2
proof let n1,n2 be Nat;assume A18:1<=n1 & n1<=len f
& 1<=n2 & n2<=len f & f.n1=f.n2;
then n1 in dom f & n2 in dom f by FINSEQ_3:27;
hence n1=n2 by A16,A18,FUNCT_1:def 8;
end;
A19: 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 A20:x1 in dom g & x2 in dom g & g.x1=g.x2;
then reconsider n1=x1,n2=x2 as Nat;
A21:1<=n1 & n1<=len g & 1<=n2 & n2<=len g by A20,FINSEQ_3:27;
now
A22:g.len g =<*p*>.1 by A4,A11,A13,FINSEQ_1:def 7
.=p by FINSEQ_1:def 8;
now per cases;
case A23:n1=len g;
now assume A24: n2<>len g; then n2<len g by A21,REAL_1:def 5;
then A25:n2<=len mid(f,1,Index(p,f)) by A13,NAT_1:38;
then g.n2=mid(f,1,Index(p,f)).n2 by A4,A21,SCMFSA_7:9;
then g.n2=f.(n2+1-'1) by A6,A7,A8,A21,A25,Th27;
then A26:p=f.n2 by A20,A22,A23,BINARITH:39;
A27: n2 <= len f by A7,A10,A25,AXIOMS:22;
1 < n2 by A3,A21,A26,AXIOMS:21;
then Index(p,f)+1 = n2 by A1,A26,A27,Th45;
hence contradiction by A6,A9,A13,A24,AMI_5:4;
end;
hence x1=x2 by A23;
case A28:n2=len g;
now assume A29: n1<>len g; then n1<len g by A21,REAL_1:def 5;
then A30:n1<=len mid(f,1,Index(p,f)) by A13,NAT_1:38;
then g.n1=mid(f,1,Index(p,f)).n1 by A4,A21,SCMFSA_7:9;
then g.n1=f.(n1+1-'1) by A6,A7,A8,A21,A30,Th27;
then A31:p=f.n1 by A20,A22,A28,BINARITH:39;
A32: n1 <= len f by A7,A10,A30,AXIOMS:22;
1 < n1 by A3,A21,A31,AXIOMS:21;
then Index(p,f)+1 = n1 by A1,A31,A32,Th45;
hence contradiction by A6,A9,A13,A29,AMI_5:4;
end;
hence x1=x2 by A28;
case that
A33: n1<>len g and
A34: n2 <> len g;
n1<len g by A21,A33,REAL_1:def 5;
then A35:n1<=len mid(f,1,Index(p,f)) by A13,NAT_1:38;
then A36:n1<=len f by A7,A10,AXIOMS:22;
A37:g.n1=mid(f,1,Index(p,f)).n1 by A4,A21,A35,SCMFSA_7:9
.=f.n1 by A7,A10,A21,A35,Th32;
n2 < len g by A21,A34,AXIOMS:21;
then A38:n2<=len mid(f,1,Index(p,f)) by A13,NAT_1:38;
then A39:n2<=len f by A7,A10,AXIOMS:22;
g.n2=mid(f,1,Index(p,f)).n2 by A4,A21,A38,SCMFSA_7:9
.=f.n2 by A7,A10,A21,A38,Th32;
hence x1=x2 by A17,A20,A21,A36,A37,A39;
end;
hence x1=x2;
end;
hence x1=x2;
end;
A40: f is unfolded by A1,TOPREAL1:def 10;
A41: for j st 1 <= j & j + 2 <= len g
holds LSeg(g,j) /\ LSeg(g,j+1) = {g/.(j+1)}
proof let j;assume A42: 1 <= j & j + 2 <= len g;
then j+1<=len g by Th10;
then A43:LSeg(g,j) c= LSeg(f,j) by A2,A4,A42,Th51;
j+(1+1)<=len g by A42;
then A44:j+1+1<=len g by XCMPLX_1:1;
A45:1<=j+1 by A42,Th11;
then LSeg(g,j+1) c= LSeg(f,j+1) by A2,A4,A44,Th51;
then A46:LSeg(g,j)/\ LSeg(g,j+1) c= LSeg(f,j)/\ LSeg(f,j+1) by A43,XBOOLE_1:
27;
A47:j+1<=len g by A42,Th10;
then LSeg(g,j)=LSeg(g/.j,g/.(j+1)) by A42,TOPREAL1:def 5;
then A48:g/.(j+1) in LSeg(g,j) by TOPREAL1:6;
A49:g/.(j+1)=g.(j+1) by A45,A47,FINSEQ_4:24;
A50:Index(p,f)<=len f by A2,Th41;
j+(1+1)<=len g by A42;
then j+1+1<=len g by XCMPLX_1:1;
then LSeg(g,j+1)=LSeg(g/.(j+1),g/.(j+1+1)) by A45,TOPREAL1:def 5;
then g/.(j+1) in LSeg(g,j+1) by TOPREAL1:6;
then g/.(j+1) in LSeg(g,j) /\ LSeg(g,j+1) by A48,XBOOLE_0:def 3;
then A51:{g/.(j+1)} c= LSeg(g,j) /\ LSeg(g,j+1) by ZFMISC_1:37;
now
A52:len g=len mid(f,1,Index(p,f))+1 by A4,FINSEQ_2:19;
Index(p,f)<=len f by A2,Th41;
then A53: len g<=len f +1 by A10,A52,AXIOMS:24;
now per cases by A53,REAL_1:def 5;
case len g=len f +1;
then len f =Index(p,f) by A10,A52,XCMPLX_1:2;
hence contradiction by A2,Th41;
case len g<len f+1;
then len g<=len f by NAT_1:38;
then A54:j+2<=len f by A42,AXIOMS:22;
A55:j+1<=Index(p,f) by A10,A44,A52,REAL_1:53;
then A56:j+1<=len f by A50,AXIOMS:22;
A57:LSeg(g,j)/\ LSeg(g,j+1) c= {f/.(j+1)}
by A40,A42,A46,A54,TOPREAL1:def 8;
A58:f.(j+1)=f/.(j+1) by A45,A56,FINSEQ_4:24;
g.(j+1)=mid(f,1,Index(p,f)).(j+1) by A4,A10,A45,A55,SCMFSA_7:9
.=f.(j+1) by A7,A45,A55,Th32;
hence LSeg(g,j)/\ LSeg(g,j+1) = {g/.(j+1)}
by A49,A51,A57,A58,XBOOLE_0:def 10;
end;
hence LSeg(g,j) /\ LSeg(g,j+1) = {g/.(j+1)};
end;
hence LSeg(g,j) /\ LSeg(g,j+1) = {g/.(j+1)};
end;
A59: f is s.n.c. by A1,TOPREAL1:def 10;
A60: for j1,j2 st j1+1 < j2 holds LSeg(g,j1) misses LSeg(g,j2)
proof let j1,j2;assume A61:j1+1 < j2;
j1>=0 by NAT_1:18;
then A62: j1=0 or j1>=0+1 by NAT_1:38;
now per cases by A62,REAL_1:def 5;
case j1=0;
then LSeg(g,j1)={} by TOPREAL1:def 5;
then LSeg(g,j1) /\ LSeg(g,j2) = {};
hence LSeg(g,j1) misses LSeg(g,j2) by XBOOLE_0:def 7;
case that
A63: j1=1 or j1>1 and
A64: j2+1<=len g;
j2<len g by A64,NAT_1:38;
then j1+1<len g by A61,AXIOMS:22;
then A65:LSeg(g,j1) c= LSeg(f,j1) by A2,A4,A63,Th51;
1+1<=j1+1 by A63,AXIOMS:24;
then 2<=j2 by A61,AXIOMS:22;
then 1<=j2 by AXIOMS:22;
then LSeg(g,j2) c= LSeg(f,j2) by A2,A4,A64,Th51;
then A66:LSeg(g,j1)/\ LSeg(g,j2) c= LSeg(f,j1)/\ LSeg(f,j2)
by A65,XBOOLE_1:27;
LSeg(f,j1) misses LSeg(f,j2) by A59,A61,TOPREAL1:def 9;
then LSeg(f,j1) /\ LSeg(f,j2) = {} by XBOOLE_0:def 7;
then LSeg(g,j1) /\ LSeg(g,j2) = {} by A66,XBOOLE_1:3;
hence LSeg(g,j1) misses LSeg(g,j2) by XBOOLE_0:def 7;
case j2+1>len g; then LSeg(g,j2)={} by TOPREAL1:def 5;
then LSeg(g,j1)/\ LSeg(g,j2)={};
hence thesis by XBOOLE_0:def 7;
end;
hence LSeg(g,j1) misses LSeg(g,j2);
end;
A67: f is special by A1,TOPREAL1:def 10;
for j st 1 <= j & j+1 <= len g holds
(g/.j)`1 = (g/.(j+1))`1 or (g/.j)`2 = (g/.(j+1))`2
proof let j;assume A68: 1 <= j & j+1 <= len g;
A69: now
j+1<=Index(p,f)+1 by A4,A10,A68,FINSEQ_2:19;
then A70:j<=Index(p,f) by REAL_1:53;
Index(p,f)<len f by A2,Th41;
then j<len f by A70,AXIOMS:22;
hence j+1<=len f by NAT_1:38;
end;
A71:LSeg(g,j) c= LSeg(f,j) by A2,A4,A68,Th51;
A72:LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A68,TOPREAL1:def 5;
A73:LSeg(f,j)
= LSeg(f/.j,f/.(j+1)) by A68,A69,TOPREAL1:def 5;
(f/.j)`1 = (f/.(j+1))`1
or (f/.j)`2 = (f/.(j+1))`2 by A67,A68,A69,TOPREAL1:def 7;
hence (g/.j)`1 = (g/.(j+1))`1 or (g/.j)`2 = (g/.(j+1))`2
by A71,A72,A73,Th36;
end;
then g is one-to-one & len g >= 2 & g is unfolded s.n.c. special
by A15,A19,A41,A60,FUNCT_1:def 8,TOPREAL1:def 7,def 8,def 9;
then g is_S-Seq by TOPREAL1:def 10;
hence g is_S-Seq_joining f/.1,p by A12,A14,Def3;
end;
begin
::----------------------------------------------------------------------:
:: Left and Right Cutting Functions for Finite Sequences in TOP-REAL 2 :
::----------------------------------------------------------------------:
definition let f be FinSequence of TOP-REAL 2,p be Point of TOP-REAL 2;
func L_Cut(f,p) -> FinSequence of TOP-REAL 2 equals
:Def4:
<*p*>^mid(f,Index(p,f)+1,len f) if p<>f.(Index(p,f)+1)
otherwise mid(f,Index(p,f)+1,len f);
correctness;
func R_Cut(f,p) -> FinSequence of TOP-REAL 2 equals
:Def5:
mid(f,1,Index(p,f))^<*p*> if p<>f.1
otherwise <*p*>;
correctness;
end;
theorem Th53:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st f is_S-Seq & p in L~f & p = f.(Index(p,f)+1) & p <> f.len f
holds Index(p,Rev f) + Index(p,f) + 1 = len f
proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: f is_S-Seq and
A2: p in L~f and
A3: p = f.(Index(p,f)+1) and
A4: p <> f.len f;
A5: Rev f is_S-Seq by A1,SPPOL_2:47;
A6: len f = len Rev f by FINSEQ_5:def 3;
len f <= len f + Index(p,f) by NAT_1:29;
then A7: len f - Index(p,f) <= len Rev f by A6,REAL_1:86;
Index(p,f) < len f by A2,Th41;
then A8: Index(p,f)+1 <= len f by NAT_1:38;
1 <= Index(p,f)+1 by NAT_1:29;
then Index(p,f)+1 in dom f by A8,FINSEQ_3:27;
then A9: Index(p,f)+1 in dom Rev f by FINSEQ_5:60;
Index(p,f)+1 < len f by A3,A4,A8,AXIOMS:21;
then A10: 1 < len f - Index(p,f) by REAL_1:86;
Index(p,f) <= len f by A2,Th41;
then A11: len f - Index(p,f) = len f -' Index(p,f) by SCMFSA_7:3;
p = (Rev Rev f).(Index(p,f)+1) by A3,FINSEQ_6:29
.= (Rev f).(len Rev f - (Index(p,f)+1) + 1) by A9,FINSEQ_5:61
.= (Rev f).(len Rev f - Index(p,f) - 1 + 1) by XCMPLX_1:36
.= (Rev f).(len Rev f - Index(p,f)) by XCMPLX_1:27
.= (Rev f).(len f - Index(p,f)) by FINSEQ_5:def 3;
then A12: Index(p,Rev f) + 1 = len f -' Index(p,f) by A5,A7,A10,A11,Th45;
thus Index(p,Rev f) + Index(p,f) + 1
= Index(p,Rev f) + 1 + Index(p,f) by XCMPLX_1:1
.= len f by A11,A12,XCMPLX_1:27;
end;
theorem Th54:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st f is_S-Seq & p in L~f & p <> f.(Index(p,f)+1) holds
Index(p,Rev f) + Index(p,f) = len f
proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: f is_S-Seq and
A2: p in L~f and
A3: p <> f.(Index(p,f)+1);
A4: Rev f is_S-Seq by A1,SPPOL_2:47;
A5: Index(p,f) < len f by A2,Th41;
then A6: len f -' Index(p,f) + Index(p,f) = len f by AMI_5:4;
A7: len f = len Rev f by FINSEQ_5:def 3;
p in LSeg(f,Index(p,f)) by A2,Th42;
then A8: p in LSeg(Rev f,len f -' Index(p,f)) by A6,SPPOL_2:2;
A9: Index(p,f) < len f by A2,Th41;
then Index(p,f) + 1 <= len f by NAT_1:38;
then 1<=len f - Index(p,f) by REAL_1:84;
then A10: 1<=len f -' Index(p,f) by Th1;
0+1 <= Index(p,f) by A2,Th41;
then 0 < Index(p,f) by NAT_1:38;
then len f + 0 < len f + Index(p,f) by REAL_1:53;
then len f - Index(p,f) < len f by REAL_1:84;
then A11: len f -' Index(p,f) < len f by A5,SCMFSA_7:3;
then A12: len f -' Index(p,f)+1<=len Rev f by A7,NAT_1:38;
len f -' Index(p,f) in dom f by A10,A11,FINSEQ_3:27;
then (Rev f).(len f -' Index(p,f))
= f.(len f - (len f -' Index(p,f)) + 1) by FINSEQ_5:61
.= f.(len f - (len f - Index(p,f)) + 1) by A9,SCMFSA_7:3
.= f.(len f - len f + Index(p,f) + 1) by XCMPLX_1:37
.= f.(0 + Index(p,f) + 1) by XCMPLX_1:14;
then len f -' Index(p,f)=Index(p,Rev f) by A3,A4,A8,A12,Th47;
hence Index(p,Rev f) + Index(p,f) = len f by A9,AMI_5:4;
end;
theorem Th55:
for D for f being FinSequence of D, k being Nat, p being Element of D
holds (<*p*>^f)|(k+1) = <*p*>^(f|k)
proof let D; let f be FinSequence of D, k be Nat, p be Element of D;
A1: f|Seg k = f|k by TOPREAL1:def 1;
thus (<*p*>^f)|(k+1) = (<*p*>^f)|Seg(k+1) by TOPREAL1:def 1
.= (<*p*>^f)|Seg(k+len<*p*>) by FINSEQ_1:56
.= <*p*>^(f|k) by A1,FINSEQ_6:16;
end;
theorem Th56:
for D for f being non empty FinSequence of D, k1,k2 being Nat
st k1 < k2 & k1 in dom f
holds mid(f,k1,k2) = <*f.k1*>^ mid(f,k1+1,k2)
proof let D; let f be non empty FinSequence of D, k1,k2 being Nat;
assume
A1: k1 < k2;
then A2: k1+1 <= k2 by NAT_1:38;
A3: 1 <= k2 -' k1
proof
per cases by A2,AXIOMS:21;
suppose k1 + 1 = k2;
hence 1 <= k2 -' k1 by BINARITH:39;
suppose
A4: k1 + 1 < k2;
k2-'k1 <= 1 implies k2 <= 1 + k1
proof assume
k2-'k1 <= 1;
then k2-'k1 +k1 <= 1 + k1 by AXIOMS:24;
hence k2 <= 1 + k1 by A1,AMI_5:4;
end;
hence 1 <= k2 -' k1 by A4;
end;
assume
A5: k1 in dom f;
then A6: f.k1 = f/.k1 by FINSEQ_4:def 4;
k2-'k1 = k2-k1 by A3,Th1;
then A7: k2-'k1-'1 = k2-k1-1 by A3,SCMFSA_7:3
.= k2-(k1+1) by XCMPLX_1:36
.= k2-'(k1+1) by A2,SCMFSA_7:3;
1 <= k1 by A5,FINSEQ_3:27;
then k1 -' 1 + 1 = k1 by AMI_5:4;
then (f/^(k1-'1)) = <*f/.k1*>^(f/^k1) by A5,FINSEQ_5:34;
hence mid(f,k1,k2) = (<*f/.k1*>^ (f/^k1))|(k2-'k1+1) by A1,Def1
.= <*f.k1*>^ ((f/^k1)|(k2-'k1)) by A6,Th55
.= <*f.k1*>^ ((f/^k1)|(k2-'(k1+1)+1)) by A3,A7,AMI_5:4
.= <*f.k1*>^ ((f/^(k1+1-'1))|(k2-'(k1+1)+1)) by BINARITH:39
.= <*f.k1*>^ mid(f,k1+1,k2) by A2,Def1;
end;
definition let f be non empty FinSequence;
cluster Rev f -> non empty;
coherence
proof
dom Rev f = dom f by FINSEQ_5:60;
hence thesis by RELAT_1:60,64;
end;
end;
theorem Th57:
for f being non empty FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st f is_S-Seq & p in L~f holds
L_Cut(Rev f,p) = Rev R_Cut(f,p)
proof
let f be non empty FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2
such that
A1: f is_S-Seq and
A2: p in L~f;
A3: Rev f is_S-Seq by A1,SPPOL_2:47;
A4: p in L~Rev f by A2,SPPOL_2:22;
A5: Rev Rev f = f by FINSEQ_6:29;
A6: len f = len Rev f by FINSEQ_5:def 3;
A7: L~f = L~Rev f by SPPOL_2:22;
A8: dom Rev f = dom f by FINSEQ_5:60;
A9: 1 <= Index(p, Rev f)+1 by NAT_1:29;
Index(p, Rev f) < len Rev f by A2,A7,Th41;
then A10: Index(p, Rev f) + 1 <= len f by A6,NAT_1:38;
then A11: Index(p, Rev f)+1 in dom f by A9,FINSEQ_3:27;
A12: 1+1 <= len f by A1,TOPREAL1:def 10;
then A13: 1 < len f by NAT_1:38;
A14: 1 <= Index(p,f) by A2,Th41;
A15: Index(p,f) < len f by A2,Th41;
A16: 1 in dom f by A13,FINSEQ_3:27;
A17: 2 in dom f by A12,FINSEQ_3:27;
A18: len f in dom f by A13,FINSEQ_3:27;
per cases;
suppose
A19: p = f.len f;
then A20: p = (Rev f).1 by FINSEQ_5:65;
then p = (Rev f)/.1 by A8,A16,FINSEQ_4:def 4;
then A21: Index(p,Rev f) = 1 by A6,A12,Th44;
f is one-to-one by A1,TOPREAL1:def 10;
then A22: p<>f.1 by A13,A16,A18,A19,FUNCT_1:def 8;
Rev f is one-to-one by A3,TOPREAL1:def 10;
then A23: p <> (Rev f).(1+1) by A8,A16,A17,A20,FUNCT_1:def 8;
then Index(p,Rev f) + Index(p,f) = len f by A3,A4,A5,A6,A21,Th54;
then A24: Index(p,Rev f) = len f - Index(p,f) by XCMPLX_1:26;
thus L_Cut(Rev f,p)
= <*p*>^mid(Rev f,Index(p,Rev f)+1,len f) by A6,A21,A23,Def4
.= <*p*>^mid(Rev f,len f -'Index(p,f)+1,len f) by A15,A24,SCMFSA_7:3
.= <*p*>^mid(Rev f,len f -'Index(p,f)+1,len f -' 1 + 1) by A13,AMI_5:
4
.= <*p*>^Rev mid(f,1,Index(p,f)) by A13,A14,A15,Th22
.= Rev(mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:66
.= Rev R_Cut(f,p) by A22,Def5;
suppose
A25: p = f.1;
then A26: p = (Rev f).len f by FINSEQ_5:65;
A27:len (Rev f/^(len Rev f-'1))=len Rev f-'(len Rev f-'1) by Th19;
A28: len Rev f-'1+1=len Rev f by A6,A13,AMI_5:4;
then A29:(Rev f/^(len Rev f-'1)).1=Rev f.len Rev f by Th23;
1<=len Rev f-(len Rev f-'1) by A28,XCMPLX_1:26;
then A30: 1<=len (Rev f/^(len Rev f-'1)) by A27,Th1;
then 0<len (Rev f/^(len Rev f-'1)) by AXIOMS:22;
then A31:Rev f/^(len Rev f-'1) is non empty by FINSEQ_1:25;
len Rev f-'len Rev f+1=len Rev f-len Rev f+1 by SCMFSA_7:3
.=1 by XCMPLX_1:25;
then A32: mid(Rev f,len Rev f,len Rev f)=(Rev f/^(len Rev f-'1))|1 by Def1
.=<*(Rev f/^(len Rev f-'1))/.1 *> by A31,FINSEQ_5:23
.=<*Rev f.len Rev f*> by A29,A30,FINSEQ_4:24;
Index(p,Rev f) + 1 = len f by A3,A6,A13,A26,Th45;
hence L_Cut(Rev f,p) = <*p*> by A6,A26,A32,Def4
.= Rev <*p*> by FINSEQ_5:63
.= Rev R_Cut(f,p) by A25,Def5;
suppose that
A33: p <> f.1 and
A34: p <> f.len f and
A35: p = f.(Index(p,f)+1);
A36: p <> (Rev f).len f by A33,FINSEQ_5:65;
len f = Index(p,Rev f) + Index(p,f) + 1 by A1,A2,A34,A35,Th53
.= Index(p,Rev f) + (Index(p,f) + 1) by XCMPLX_1:1;
then Index(p,f) + 1 = len f - Index(p,Rev f) by XCMPLX_1:26;
then A37: p = f.(len f - Index(p, Rev f) - 1 + 1) by A35,XCMPLX_1:27
.= f.(len f - (Index(p, Rev f)+1) + 1) by XCMPLX_1:36
.= (Rev f).(Index(p, Rev f)+1) by A11,FINSEQ_5:61;
A38: len f = Index(p,Rev f) + Index(p,f) + 1 by A1,A2,A34,A35,Th53
.= Index(p,f) + (Index(p,Rev f) + 1) by XCMPLX_1:1;
A39: len f -' Index(p,f) = len f - Index(p,f) by A15,SCMFSA_7:3
.= Index(p,Rev f)+1 by A38,XCMPLX_1:26;
A40: Index(p, Rev f)+1 < len f by A10,A36,A37,AXIOMS:21;
thus L_Cut(Rev f,p)
= mid(Rev f,Index(p,Rev f)+1,len f) by A6,A37,Def4
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f)
by A8,A11,A37,A39,A40,Th56
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f-'1+1) by A13,AMI_5:4
.= <*p*>^Rev mid(f,1,Index(p,f)) by A13,A14,A15,Th22
.= Rev (mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:66
.= Rev R_Cut(f,p) by A33,Def5;
suppose that
A41: p <> f.1 and
A42: p <> f.(Index(p,f)+1);
A43: p <> (Rev f).len f by A41,FINSEQ_5:65;
A44: now assume
A45: p = (Rev f).(Index(p, Rev f)+1);
then len Rev f = Index(p,Rev Rev f) + Index(p,Rev f) + 1
by A3,A4,A6,A43,Th53
.= Index(p,f) + 1 + Index(p,Rev f) by A5,XCMPLX_1:1;
then A46: Index(p,f) + 1 = len f - Index(p,Rev f) by A6,XCMPLX_1:26;
p = f.(len f - (Index(p, Rev f)+1) + 1) by A11,A45,FINSEQ_5:61
.= f.(len f - Index(p, Rev f) - 1 + 1) by XCMPLX_1:36
.= f.(Index(p,f)+1) by A46,XCMPLX_1:27;
hence contradiction by A42;
end;
A47: len f = Index(p,Rev f) + Index(p,f) by A1,A2,A42,Th54;
A48: Index(p, f) < len f by A2,Th41;
Index(p,Rev f) = len f - Index(p,f) by A47,XCMPLX_1:26
.= len f -' Index(p,f) by A48,SCMFSA_7:3;
hence L_Cut(Rev f,p)
= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f) by A6,A44,Def4
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f-'1+1) by A13,AMI_5:4
.= <*p*>^Rev mid(f,1,Index(p,f)) by A13,A14,A15,Th22
.= Rev (mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:66
.= Rev R_Cut(f,p) by A41,Def5;
end;
theorem Th58:
for f being non empty FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st p in L~f holds
(L_Cut(f,p)).1=p &
for i st 1<i & i<=len L_Cut(f,p)
holds
(p = f.(Index(p,f)+1) implies (L_Cut(f,p)).i=f.(Index(p,f)+i)) &
(p <> f.(Index(p,f)+1) implies (L_Cut(f,p)).i=f.(Index(p,f)+i-1))
proof let f be non empty FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2 such that
A1: p in L~f;
now per cases;
suppose
A2: p = f.(Index(p,f)+1);
then A3: L_Cut(f,p)=mid(f,Index(p,f)+1,len f) by Def4;
A4: 1 <= Index(p,f)+1 by NAT_1:29;
Index(p,f) < len f by A1,Th41;
then A5: Index(p,f)+1 <= len f by NAT_1:38;
1 in dom f by FINSEQ_5:6;
then 1 <= len f by FINSEQ_3:27;
hence (L_Cut(f,p)).1 = p by A2,A3,A4,A5,Th27;
suppose p<> f.(Index(p,f)+1);
then L_Cut(f,p)=<*p*>^mid(f,Index(p,f)+1,len f) by Def4;
hence (L_Cut(f,p)).1=p by Th16;
end;
hence (L_Cut(f,p)).1=p;
let i;assume A6: 1<i & i<=len L_Cut(f,p);
Index(p,f) < len f by A1,Th41;
then A7:1<=Index(p,f)+1 & Index(p,f)+1<=len f by NAT_1:29,38;
then A8:1<=len f by AXIOMS:22;
A9:len <*p*><=i by A6,FINSEQ_1:57;
A10:len <*p*><i by A6,FINSEQ_1:56;
A11: 1<=i-1 by A6,SPPOL_1:6;
A12:(i-'1)+1=i-1+1 by A6,SCMFSA_7:3 .=i by XCMPLX_1:27;
hereby assume p = f.(Index(p,f)+1);
then L_Cut(f,p)=mid(f,Index(p,f)+1,len f) by Def4;
hence (L_Cut(f,p)).i = f.(i+(Index(p,f)+1)-'1) by A6,A7,A8,Th27
.= f.(i+Index(p,f)+1-'1) by XCMPLX_1:1
.= f.(Index(p,f)+i) by BINARITH:39;
end;
assume p <> f.(Index(p,f)+1);
then A13: L_Cut(f,p)=<*p*>^mid(f,Index(p,f)+1,len f) by Def4;
then A14: i<=len <*p*>+len mid(f,Index(p,f)+1,len f) by A6,FINSEQ_1:35;
len mid(f,Index(p,f)+1,len f)=len f -'(Index(p,f)+1)+1
by A7,A8,Th27;
then len <*p*>+len mid(f,Index(p,f)+1,len f)
=1+(len f -'(Index(p,f)+1)+1) by FINSEQ_1:57
.=1+(len f -(Index(p,f)+1)+1) by A7,SCMFSA_7:3
.=1+(len f -Index(p,f)-1+1) by XCMPLX_1:36
.=(len f -Index(p,f))+1 by XCMPLX_1:27;
then i-1<=len f -Index(p,f)+1-1 by A14,REAL_1:49;
then i-1<=len f -Index(p,f)-1+1 by XCMPLX_1:29;
then i-1<=len f -(Index(p,f)+1)+1 by XCMPLX_1:36;
then A15:1<=i-'1 & i-'1<=len f -(Index(p,f)+1)+1 by A11,Th1;
A16: (L_Cut(f,p)).i =mid(f,Index(p,f)+1,len f).(i-len <*p*>) by A6,A10,A13,Th15
.=mid(f,Index(p,f)+1,len f).(i-'len <*p*>) by A9,SCMFSA_7:3
.=mid(f,Index(p,f)+1,len f).(i-'1) by FINSEQ_1:56
.=f.((i-'1)+(Index(p,f)+1)-'1) by A7,A15,Th31
.=f.(Index(p,f)+i-'1) by A12,XCMPLX_1:1;
i <=i+Index(p,f) by NAT_1:29; then 1<=i+Index(p,f) by A6,AXIOMS:22;
hence (L_Cut(f,p)).i=f.(Index(p,f)+i-1) by A16,SCMFSA_7:3;
end;
theorem Th59:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st f is_S-Seq & p in L~f holds
(R_Cut(f,p)).(len R_Cut(f,p))=p &
for i st 1<=i & i<=Index(p,f) holds R_Cut(f,p).i=f.i
proof let f be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq and
A2: p in L~f;
f is one-to-one & len f >= 2
& f is unfolded s.n.c. special by A1,TOPREAL1:def 10;
then A3:1<=len f by AXIOMS:22;
A4:1<=Index(p,f) & Index(p,f)<=len f by A2,Th41;
then A5:len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A3,Th27
.=Index(p,f) by A4,AMI_5:4;
now per cases;
case p<>f.1;
then A6:R_Cut(f,p)= mid(f,1,Index(p,f))^<*p*> by Def5;
len (mid(f,1,Index(p,f))^<*p*>)= len mid(f,1,Index(p,f))+len <*p*>
by FINSEQ_1:35
.= len mid(f,1,Index(p,f))+1 by FINSEQ_1:56;
hence (R_Cut(f,p)).(len R_Cut(f,p))=p by A6,FINSEQ_1:59;
case p=f.1;
then A7:R_Cut(f,p)=<*p*> by Def5;
then len R_Cut(f,p) = 1 by FINSEQ_1:57;
hence (R_Cut(f,p)).(len R_Cut(f,p))=p by A7,FINSEQ_1:57;
end;
hence (R_Cut(f,p)).(len R_Cut(f,p))=p;
thus for i st 1<=i & i<=Index(p,f) holds R_Cut(f,p).i=f.i
proof let i;assume A8: 1<=i & i<=Index(p,f);
now per cases;
case p<>f.1;
then (R_Cut(f,p)).i=(mid(f,1,Index(p,f))^<*p*>).i by Def5
.=mid(f,1,Index(p,f)).i by A5,A8,SCMFSA_7:9
.=f.i by A4,A8,Th32;
hence R_Cut(f,p).i=f.i;
case
A9: p=f.1;
then A10: (R_Cut(f,p)) = <*p*> by Def5;
A11: 1+1 <= len f by A1,TOPREAL1:def 10;
then 1 < len f by NAT_1:38;
then 1 in dom f by FINSEQ_3:27;
then p = f/.1 by A9,FINSEQ_4:def 4;
then Index(p,f) = 1 by A11,Th44;
then i = 1 by A8,AXIOMS:21;
hence R_Cut(f,p).i = f.i by A9,A10,FINSEQ_1:57;
end;
hence (R_Cut(f,p)).i=f.i;
end;
end;
theorem Th60:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st f is_S-Seq & p in L~f holds
(p<>f.1 implies len R_Cut(f,p)=Index(p,f)+1)&
(p=f.1 implies len R_Cut(f,p)=Index(p,f))
proof let f be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq and
A2: p in L~f;
consider i such that A3: 1 <= i & i+1 <= len f & p in LSeg(f,i)
by A2,SPPOL_2:13;
i<=len f by A3,Th9;
then A4:1<=len f by A3,AXIOMS:22;
A5:1<=Index(p,f) & Index(p,f)<=len f by A2,Th41;
now per cases;
case p<>f.1;
then R_Cut(f,p)=mid(f,1,Index(p,f))^<*p*> by Def5;
hence len R_Cut(f,p) = len mid(f,1,Index(p,f))+len <*p*> by FINSEQ_1:35
.= len mid(f,1,Index(p,f))+1 by FINSEQ_1:56
.= Index(p,f)-'1+1+1 by A4,A5,Th27
.=Index(p,f)+1 by A5,AMI_5:4;
case A6:p=f.1;
then A7:R_Cut(f,p)=<*p*> by Def5;
A8: len f >= 1+1 by A1,TOPREAL1:def 10;
len f <> 0 by A1,TOPREAL1:def 10;
then f <> {} by FINSEQ_1:25;
then 1 in dom f by FINSEQ_5:6;
then A9: p = f/.1 by A6,FINSEQ_4:def 4;
thus len R_Cut(f,p)= 1 by A7,FINSEQ_1:56
.= Index(p,f) by A8,A9,Th44;
end;
hence
(p<>f.1 implies len R_Cut(f,p)=Index(p,f)+1)&
(p=f.1 implies len R_Cut(f,p)=Index(p,f));
end;
theorem Th61:for f being non empty FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st f is_S-Seq & p in L~f & p<>f.len f holds
( p = f.(Index(p,f)+1) implies len L_Cut(f,p)=len f -Index(p,f)) &
( p <> f.(Index(p,f)+1) implies len L_Cut(f,p)=len f -Index(p,f)+1)
proof let f be non empty FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq and
A2: p in L~f and
A3: p<>f.len f;
A4: Rev f is_S-Seq & p in L~Rev f by A1,A2,SPPOL_2:22,47;
A5: p <> (Rev f).1 by A3,FINSEQ_5:65;
L_Cut(f,p) = L_Cut(Rev Rev f,p) by FINSEQ_6:29
.= Rev R_Cut(Rev f,p) by A4,Th57;
then A6: len L_Cut(f,p) = len R_Cut(Rev f,p) by FINSEQ_5:def 3
.= Index(p,Rev f)+1 by A4,A5,Th60;
now per cases;
case
A7: p = f.(Index(p,f)+1);
Index(p,Rev f) + (Index(p,f) + 1)
= Index(p,Rev f) + Index(p,f) + 1 by XCMPLX_1:1
.= len f by A1,A2,A3,A7,Th53;
then Index(p,Rev f) = len f - (Index(p,f) + 1) by XCMPLX_1:26
.= len f - Index(p,f) - 1 by XCMPLX_1:36;
hence len L_Cut(f,p) = len f - Index(p,f) by A6,XCMPLX_1:27;
case p <> f.(Index(p,f)+1);
then Index(p,Rev f) + Index(p,f) = len f by A1,A2,Th54;
hence len L_Cut(f,p) = len f - Index(p,f) + 1 by A6,XCMPLX_1:26;
end;
hence thesis;
end;
definition let p1,p2,q1,q2 be Point of TOP-REAL 2;
pred LE q1,q2,p1,p2 means
:Def6:q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) & for r1,r2 being Real st
0<=r1 & r1<=1 & q1=(1-r1)*p1+r1*p2 &
0<=r2 & r2<=1 & q2=(1-r2)*p1+r2*p2 holds
r1<=r2;
end;
definition let p1,p2,q1,q2 be Point of TOP-REAL 2;
pred LT q1,q2,p1,p2 means
:Def7:LE q1,q2,p1,p2 & q1<>q2;
end;
theorem
for p1,p2,q1,q2 being Point of TOP-REAL 2 st
LE q1,q2,p1,p2 & LE q2,q1,p1,p2 holds q1=q2
proof let p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1:LE q1,q2,p1,p2 & LE q2,q1,p1,p2;
then A2:q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) & for r1,r2 being Real st
0<=r1 & r1<=1 & q1=(1-r1)*p1+r1*p2 &
0<=r2 & r2<=1 & q2=(1-r2)*p1+r2*p2 holds
r1<=r2 by Def6;
then consider r1 such that A3: 0<=r1 & r1<=1 & q1 = (1-r1)*p1+r1*p2 by SPPOL_1
:21;
consider r2 such that A4: 0<=r2 & r2<=1 & q2 = (1-r2)*p1+r2*p2 by A2,SPPOL_1:
21;
A5:r1<=r2 by A1,A3,A4,Def6;
r2<=r1 by A1,A3,A4,Def6;
then r1=r2 by A5,AXIOMS:21;
hence q1=q2 by A3,A4;
end;
theorem Th63:for p1,p2,q1,q2 being Point of TOP-REAL 2 st
q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2) & p1<>p2
holds (LE q1,q2,p1,p2 or LT q2,q1,p1,p2)
& not(LE q1,q2,p1,p2 & LT q2,q1,p1,p2)
proof let p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1: q1 in LSeg(p1,p2) & q2 in LSeg(p1,p2)& p1<>p2;
then consider r1 such that
A2: 0 <= r1 & r1 <= 1 & q1= (1-r1)*p1 + r1*p2 by SPPOL_1:21;
consider r2 such that
A3: 0 <= r2 & r2 <= 1& q2= (1-r2)*p1 + r2*p2 by A1,SPPOL_1:21;
A4:now per cases;
case A5:r1<=r2;
for s1,s2 being Real st
0<=s1 & s1<=1 & q1=(1-s1)*p1+s1*p2 &
0<=s2 & s2<=1 & q2=(1-s2)*p1+s2*p2 holds s1<=s2
proof let s1,s2 be Real;
assume A6: 0<=s1 & s1<=1 & q1=(1-s1)*p1+s1*p2 &
0<=s2 & s2<=1 & q2=(1-s2)*p1+s2*p2;
then (1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+r1*p2-s1*p2 by A2,EUCLID:49;
then (1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+(r1*p2-s1*p2) by EUCLID:49;
then (1-s1)*p1+(0.REAL 2)=(1-r1)*p1+(r1*p2-s1*p2) by EUCLID:46;
then (1-s1)*p1=(1-r1)*p1+(r1*p2-s1*p2) by EUCLID:31;
then (1-s1)*p1=(1-r1)*p1+(r1-s1)*p2 by EUCLID:54;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+((1-r1)*p1-(1-r1)*p1) by EUCLID:49;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+(0.REAL 2) by EUCLID:46;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2 by EUCLID:31;
then ((1-s1)-(1-r1))*p1=(r1-s1)*p2 by EUCLID:54;
then ((1-s1)-1+r1)*p1=(r1-s1)*p2 by XCMPLX_1:37;
then ((1+-s1)-1+r1)*p1=(r1-s1)*p2 by XCMPLX_0:def 8;
then (-s1+r1)*p1=(r1-s1)*p2 by XCMPLX_1:26;
then (r1-s1)*p1=(r1-s1)*p2 by XCMPLX_0:def 8;
then (r1-s1)=0 or p1=p2 by EUCLID:38;
then A7:r1=s1 by A1,XCMPLX_1:15;
(1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+r2*p2-s2*p2 by A3,A6,EUCLID:49;
then (1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+(r2*p2-s2*p2) by EUCLID:49;
then (1-s2)*p1+(0.REAL 2)=(1-r2)*p1+(r2*p2-s2*p2) by EUCLID:46;
then (1-s2)*p1=(1-r2)*p1+(r2*p2-s2*p2) by EUCLID:31;
then (1-s2)*p1=(1-r2)*p1+(r2-s2)*p2 by EUCLID:54;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+((1-r2)*p1-(1-r2)*p1) by EUCLID:49;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+(0.REAL 2) by EUCLID:46;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2 by EUCLID:31;
then ((1-s2)-(1-r2))*p1=(r2-s2)*p2 by EUCLID:54;
then ((1-s2)-1+r2)*p1=(r2-s2)*p2 by XCMPLX_1:37;
then ((1+-s2)-1+r2)*p1=(r2-s2)*p2 by XCMPLX_0:def 8;
then (-s2+r2)*p1=(r2-s2)*p2 by XCMPLX_1:26;
then (r2-s2)*p1=(r2-s2)*p2 by XCMPLX_0:def 8;
then (r2-s2)=0 or p1=p2 by EUCLID:38;
hence s1<=s2 by A1,A5,A7,XCMPLX_1:15;
end;
hence (LE q1,q2,p1,p2 or LT q2,q1,p1,p2) by A1,Def6;
case A8:r1>r2;
for s2,s1 being Real st
0<=s2 & s2<=1 & q2=(1-s2)*p1+s2*p2 &
0<=s1 & s1<=1 & q1=(1-s1)*p1+s1*p2 holds s1>=s2
proof let s2,s1 be Real;
assume A9:0<=s2 & s2<=1 & q2=(1-s2)*p1+s2*p2 &
0<=s1 & s1<=1 & q1=(1-s1)*p1+s1*p2;
then (1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+r1*p2-s1*p2 by A2,EUCLID:49;
then (1-s1)*p1+(s1*p2-s1*p2)=(1-r1)*p1+(r1*p2-s1*p2) by EUCLID:49;
then (1-s1)*p1+(0.REAL 2)=(1-r1)*p1+(r1*p2-s1*p2) by EUCLID:46;
then (1-s1)*p1=(1-r1)*p1+(r1*p2-s1*p2) by EUCLID:31;
then (1-s1)*p1=(1-r1)*p1+(r1-s1)*p2 by EUCLID:54;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+((1-r1)*p1-(1-r1)*p1) by EUCLID:49;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2+(0.REAL 2) by EUCLID:46;
then (1-s1)*p1-(1-r1)*p1=(r1-s1)*p2 by EUCLID:31;
then ((1-s1)-(1-r1))*p1=(r1-s1)*p2 by EUCLID:54;
then ((1-s1)-1+r1)*p1=(r1-s1)*p2 by XCMPLX_1:37;
then ((1+-s1)-1+r1)*p1=(r1-s1)*p2 by XCMPLX_0:def 8;
then (-s1+r1)*p1=(r1-s1)*p2 by XCMPLX_1:26;
then (r1-s1)*p1=(r1-s1)*p2 by XCMPLX_0:def 8;
then (r1-s1)=0 or p1=p2 by EUCLID:38;
then A10:r1=s1 by A1,XCMPLX_1:15;
(1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+r2*p2-s2*p2 by A3,A9,EUCLID:49;
then (1-s2)*p1+(s2*p2-s2*p2)=(1-r2)*p1+(r2*p2-s2*p2) by EUCLID:49;
then (1-s2)*p1+(0.REAL 2)=(1-r2)*p1+(r2*p2-s2*p2) by EUCLID:46;
then (1-s2)*p1=(1-r2)*p1+(r2*p2-s2*p2) by EUCLID:31
.=(r2-s2)*p2+(1-r2)*p1 by EUCLID:54;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+((1-r2)*p1-(1-r2)*p1) by EUCLID:49;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2+(0.REAL 2) by EUCLID:46;
then (1-s2)*p1-(1-r2)*p1=(r2-s2)*p2 by EUCLID:31;
then ((1-s2)-(1-r2))*p1=(r2-s2)*p2 by EUCLID:54;
then ((1-s2)-1+r2)*p1=(r2-s2)*p2 by XCMPLX_1:37;
then ((1+-s2)-1+r2)*p1=(r2-s2)*p2 by XCMPLX_0:def 8;
then (-s2+r2)*p1=(r2-s2)*p2 by XCMPLX_1:26;
then (r2-s2)*p1=(r2-s2)*p2 by XCMPLX_0:def 8;
then (r2-s2)=0 or p1=p2 by EUCLID:38;
hence s1>=s2 by A1,A8,A10,XCMPLX_1:15;
end;
then LE q2,q1,p1,p2 & q1<>q2 by A1,A2,A3,A8,Def6;
hence (LE q1,q2,p1,p2 or LT q2,q1,p1,p2) by Def7;
end;
now assume A11: LE q1,q2,p1,p2 & LT q2,q1,p1,p2;
then A12:r1<=r2 by A2,A3,Def6;
LE q2,q1,p1,p2 & q1<>q2 by A11,Def7;
then r2<=r1 by A2,A3,Def6;
then r1=r2 by A12,AXIOMS:21;
hence contradiction by A2,A3,A11,Def7;
end;
hence (LE q1,q2,p1,p2 or LT q2,q1,p1,p2)
& not(LE q1,q2,p1,p2 & LT q2,q1,p1,p2) by A4;
end;
theorem Th64:
for f being non empty FinSequence of TOP-REAL 2,
p,q,p1,p2 being Point of TOP-REAL 2 st
f is_S-Seq & p in L~f & q in L~f & Index(p,f)<Index(q,f)
holds q in L~L_Cut(f,p)
proof
let f be non empty FinSequence of TOP-REAL 2,p,q,p1,p2 be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq and
A2: p in L~f and
A3: q in L~f and
A4: Index(p,f)<Index(q,f);
set i1=Index(q,f)-'Index(p,f)+1;
A5:1<=Index(q,f) & Index(q,f)<len f by A3,Th41;
A6:Index(p,f)+1<=Index(q,f) by A4,NAT_1:38;
then Index(p,f)+1-Index(p,f)<=Index(q,f)-Index(p,f) by REAL_1:49;
then A7:1<=Index(q,f)-Index(p,f) by XCMPLX_1:26;
then A8:0<=Index(q,f)-Index(p,f) by AXIOMS:22;
then A9:1<=Index(q,f)-'Index(p,f) by A7,BINARITH:def 3;
then A10:1<=Index(q,f)-'Index(p,f)+1 by Th11;
1+1<=Index(q,f)-'Index(p,f)+1 by A9,AXIOMS:24;
then A11: 1<Index(q,f)-'Index(p,f)+1 by AXIOMS:22;
then A12:len <*p*><Index(q,f)-'Index(p,f)+1 by FINSEQ_1:57;
then A13:len <*p*><Index(q,f)-'Index(p,f)+1+1 by NAT_1:38;
A14:1<=Index(q,f)-'Index(p,f)+1 by NAT_1:29;
A15:1<=Index(p,f)+1 & Index(p,f)+1<=len f by A5,A6,AXIOMS:22,NAT_1:29;
A16: 1<len f by A5,AXIOMS:22;
then len mid(f,Index(p,f)+1,len f)=len f -'(Index(p,f)+1)+1 by A15,Th27;
then A17:len <*p*>+len mid(f,Index(p,f)+1,len f)=1+(len f -'(Index(p,f)+1)+1)
by FINSEQ_1:57
.=1+(len f -(Index(p,f)+1)+1) by A15,SCMFSA_7:3
.=1+(len f -Index(p,f)-1+1) by XCMPLX_1:36
.=(len f -Index(p,f))+1 by XCMPLX_1:27;
A18:Index(q,f)-Index(p,f)<=len f -Index(p,f) by A5,REAL_1:49;
then A19: Index(q,f)-Index(p,f)+1<=len f -Index(p,f)+1 by AXIOMS:24;
then A20:Index(q,f)-'Index(p,f)+1<=len <*p*>+len mid(f,Index(p,f)+1,len f)
by A4,A17,SCMFSA_7:3;
Index(q,f)-Index(p,f)<=len f -Index(p,f)-1+1 by A18,XCMPLX_1:27;
then Index(q,f)-Index(p,f)<=len f -(Index(p,f)+1)+1 by XCMPLX_1:36;
then A21:Index(q,f)-'Index(p,f)<=len f - (Index(p,f)+1)+1 by A4,SCMFSA_7:3;
A22:1<=Index(q,f)-'Index(p,f)+1+1 by NAT_1:29;
A23: now assume p=f.len f;
then len f <= Index(q,f) by A1,A6,A16,Th45;
hence contradiction by A3,Th41;
end;
per cases;
suppose
A24: p = f.(Index(p,f)+1);
then A25:len L_Cut(f,p)=len f -Index(p,f) by A1,A2,A23,Th61;
then len L_Cut(f,p)>=Index(q,f)-'Index(p,f) by A4,A18,SCMFSA_7:3;
then (L_Cut(f,p))/.(Index(q,f)-'Index(p,f))
=L_Cut(f,p).(Index(q,f)-'Index(p,f)) by A9,FINSEQ_4:24
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)) by A24,Def4
.=f.(Index(p,f)+1+(Index(q,f)-'Index(p,f))-1) by A9,A15,A21,Th31
.=f.(Index(p,f)+1+(Index(q,f)-Index(p,f))-1) by A4,SCMFSA_7:3
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f)))-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+Index(q,f)-Index(p,f))-1) by XCMPLX_1:29
.=f.(1+(Index(q,f))-1) by XCMPLX_1:26
.=f.Index(q,f) by XCMPLX_1:26;
then A26:(L_Cut(f,p))/.(Index(q,f)-'Index(p,f))=f/.Index(q,f)
by A5,FINSEQ_4:24;
A27:Index(q,f)<len f by A3,Th41;
then A28:Index(q,f)+1<=len f by NAT_1:38;
then Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by REAL_1:49;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by XCMPLX_1:29;
then A29:i1<=len L_Cut(f,p) by A8,A25,BINARITH:def 3;
A30:1<=Index(q,f) & Index(q,f)+1<=len f & q in LSeg(f,Index(q,f))
by A3,A27,Th41,Th42,NAT_1:38;
A31:Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by A28,REAL_1:49;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by XCMPLX_1:29;
then A32:len L_Cut(f,p)>=Index(q,f)-'Index(p,f)+1 by A4,A25,SCMFSA_7:3;
Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by A31,XCMPLX_1:29;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f)-1+1 by XCMPLX_1:27;
then Index(q,f)-Index(p,f)+1<=len f -(Index(p,f)+1)+1 by XCMPLX_1:36;
then A33:Index(q,f)-'Index(p,f)+1<=len f - (Index(p,f)+1)+1 by A4,SCMFSA_7:
3;
A34:1<=Index(q,f)+1 & Index(q,f)+1<=len f by A30,Th11;
A35:(L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1)
=L_Cut(f,p).(Index(q,f)-'Index(p,f)+1) by A11,A32,FINSEQ_4:24
.=(mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1) by A24,Def4
.=f.(Index(p,f)+1+(Index(q,f)-'Index(p,f)+1)-1)
by A10,A15,A33,Th31
.=f.(Index(p,f)+1+(Index(q,f)-Index(p,f)+1)-1) by A4,SCMFSA_7:3
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f)+1))-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f))+1)-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+Index(q,f)-Index(p,f)+1)-1) by XCMPLX_1:29
.=f.((Index(q,f)+1)+1-1) by XCMPLX_1:26
.=f.(Index(q,f)+1) by XCMPLX_1:26
.=f/.(Index(q,f)+1) by A34,FINSEQ_4:24;
q in LSeg(f,Index(q,f)) by A3,Th42;
then q in LSeg((L_Cut(f,p))/.((Index(q,f)-'Index(p,f))),
(L_Cut(f,p))/.((Index(q,f)-'Index(p,f)+1)))
by A5,A26,A28,A35,TOPREAL1:def 5;
hence q in L~(L_Cut(f,p)) by A9,A29,SPPOL_2:15;
suppose that
A36: p <> f.(Index(p,f)+1);
A37:len L_Cut(f,p)=len f -Index(p,f)+1 by A1,A2,A23,A36,Th61;
then len L_Cut(f,p)>=Index(q,f)-'Index(p,f)+1 by A4,A19,SCMFSA_7:3;
then (L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1)
=L_Cut(f,p).(Index(q,f)-'Index(p,f)+1) by A14,FINSEQ_4:24
.=(<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1) by A36,Def4
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1-len <*p*>)
by A12,A20,Th15
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1-1)
by FINSEQ_1:57
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f))
by XCMPLX_1:26
.=f.(Index(p,f)+1+(Index(q,f)-'Index(p,f))-1) by A9,A15,A21,Th31
.=f.(Index(p,f)+1+(Index(q,f)-Index(p,f))-1) by A4,SCMFSA_7:3
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f)))-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+Index(q,f)-Index(p,f))-1) by XCMPLX_1:29
.=f.(1+(Index(q,f))-1) by XCMPLX_1:26
.=f.Index(q,f) by XCMPLX_1:26;
then A38:(L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1)=f/.Index(q,f) by A5,FINSEQ_4:
24;
A39:Index(q,f)<len f by A3,Th41;
then A40:Index(q,f)+1<=len f by NAT_1:38;
then Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by REAL_1:49;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by XCMPLX_1:29;
then i1<=len f -Index(p,f) by A8,BINARITH:def 3;
then A41:i1+1<=len L_Cut(f,p) by A37,AXIOMS:24;
A42:1<=Index(q,f) & Index(q,f)+1<=len f & q in LSeg(f,Index(q,f))
by A3,A39,Th41,Th42,NAT_1:38;
A43:Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by A40,REAL_1:49;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by XCMPLX_1:29;
then A44: Index(q,f)-Index(p,f)+1+1<=len f -Index(p,f)+1 by AXIOMS:24;
then A45:len L_Cut(f,p)>=Index(q,f)-'Index(p,f)+1+1 by A4,A37,SCMFSA_7:3;
A46:Index(q,f)-'Index(p,f)+1+1<=len <*p*>+len mid(f,Index(p,f)+1,len f)
by A4,A17,A44,SCMFSA_7:3;
Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by A43,XCMPLX_1:29;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f)-1+1 by XCMPLX_1:27;
then Index(q,f)-Index(p,f)+1<=len f -(Index(p,f)+1)+1 by XCMPLX_1:36;
then A47:Index(q,f)-'Index(p,f)+1<=len f - (Index(p,f)+1)+1 by A4,SCMFSA_7:
3;
A48:1<=Index(q,f)+1 & Index(q,f)+1<=len f by A42,Th11;
A49:(L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1+1)
=L_Cut(f,p).(Index(q,f)-'Index(p,f)+1+1) by A22,A45,FINSEQ_4:24
.=(<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1+1)
by A36,Def4
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-len <*p*>)
by A13,A46,Th15
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-1)
by FINSEQ_1:57
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1)
by XCMPLX_1:26
.=f.(Index(p,f)+1+(Index(q,f)-'Index(p,f)+1)-1)
by A10,A15,A47,Th31
.=f.(Index(p,f)+1+(Index(q,f)-Index(p,f)+1)-1) by A4,SCMFSA_7:3
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f)+1))-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f))+1)-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+Index(q,f)-Index(p,f)+1)-1) by XCMPLX_1:29
.=f.((Index(q,f)+1)+1-1) by XCMPLX_1:26
.=f.(Index(q,f)+1) by XCMPLX_1:26
.=f/.(Index(q,f)+1) by A48,FINSEQ_4:24;
q in LSeg(f,Index(q,f)) by A3,Th42;
then q in LSeg((L_Cut(f,p))/.((Index(q,f)-'Index(p,f)+1)),
(L_Cut(f,p))/.((Index(q,f)-'Index(p,f)+1+1)))
by A5,A38,A40,A49,TOPREAL1:def 5;
hence q in L~(L_Cut(f,p)) by A14,A41,SPPOL_2:15;
end;
theorem Th65:
for p,q,p1,p2 being Point of TOP-REAL 2 st
LE p,q,p1,p2 holds q in LSeg(p,p2) & p in LSeg(p1,q)
proof let p,q,p1,p2 be Point of TOP-REAL 2;
assume A1: LE p,q,p1,p2;
then A2:p in LSeg(p1,p2) & q in LSeg(p1,p2) & for r1,r2 being Real st
0<=r1 & r1<=1 & p=(1-r1)*p1+r1*p2 &
0<=r2 & r2<=1 & q=(1-r2)*p1+r2*p2 holds
r1<=r2 by Def6;
then consider s1 being Real such that
A3:0<=s1 & s1<=1 & p=(1-s1)*p1+s1*p2 by SPPOL_1:21;
consider s2 being Real such that
A4:0<=s2 & s2<=1 & q=(1-s2)*p1+s2*p2 by A2,SPPOL_1:21;
A5:s1<=s2 by A1,A3,A4,Def6;
A6: 1-s1>=0 by A3,SQUARE_1:12;
A7:now per cases;
case A8:1-s1<>0;
A9:s2-s1>=0 by A5,SQUARE_1:12;
set s=(s2-s1)/(1-s1);
A10:s>=0 by A6,A9,REAL_2:125;
A11:(1-s1)+s1-s2=1-s2 by XCMPLX_1:27;
A12:(s2-s1)+s1-s2*s1=s2-s2*s1 by XCMPLX_1:27;
A13:(1-s1)*(((1-s2)/(1-s1)))=1-s2 by A8,XCMPLX_1:88;
A14:(1-s1)*(((s2-s1)/(1-s1)))=s2-s1 by A8,XCMPLX_1:88;
A15:(1-(s2-s1)/(1-s1))=(1*(1-s1)-(s2-s1))/(1-s1) by A8,XCMPLX_1:128
.=((1-s1)-s2+s1)/(1-s1) by XCMPLX_1:37
.=((1-s1)+s1-s2)/(1-s1) by XCMPLX_1:29;
1-s1>=s2-s1 by A4,REAL_1:49;
then (1-s1)/(1-s1)>=(s2-s1)/(1-s1) by A6,A8,REAL_1:73;
then A16:1>=s by A8,XCMPLX_1:60;
(1-s1)*((1-s)*p+s*p2)
=(1-s1)*(((1-s2)/(1-s1))*((1-s1)*p1+s1*p2))
+(1-s1)*(((s2-s1)/(1-s1))*p2) by A3,A11,A15,EUCLID:36
.=(1-s1)*(((1-s2)/(1-s1)))*((1-s1)*p1+s1*p2)
+(1-s1)*(((s2-s1)/(1-s1))*p2) by EUCLID:34
.=(1-s2)*((1-s1)*p1+s1*p2)
+(1-s1)*(((s2-s1)/(1-s1)))*p2 by A13,EUCLID:34
.=(1-s2)*((1-s1)*p1)+(1-s2)*(s1*p2)
+(s2-s1)*p2 by A14,EUCLID:36
.=(1-s2)*(1-s1)*p1+(1-s2)*(s1*p2)
+(s2-s1)*p2 by EUCLID:34
.=(1-s2)*(1-s1)*p1+(1-s2)*s1*p2
+(s2-s1)*p2 by EUCLID:34
.=(1-s2)*(1-s1)*p1+((1-s2)*s1*p2
+(s2-s1)*p2) by EUCLID:30
.=(1-s2)*(1-s1)*p1+((1-s2)*s1+(s2-s1))*p2 by EUCLID:37
.=(1-s2)*(1-s1)*p1+(1*s1-s2*s1+(s2-s1))*p2 by XCMPLX_1:40
.=(1-s2)*(1-s1)*p1+(1*s2-s1*s2)*p2 by A12,XCMPLX_1:29
.=(1-s2)*(1-s1)*p1+(1-s1)*s2*p2 by XCMPLX_1:40
.=(1-s1)*((1-s2)*p1)+(1-s1)*s2*p2 by EUCLID:34
.=(1-s1)*((1-s2)*p1)+(1-s1)*(s2*p2) by EUCLID:34
.=(1-s1)*q by A4,EUCLID:36;
then q=(1-s)*p+s*p2 by A8,EUCLID:38;
hence q in LSeg(p,p2) by A10,A16,SPPOL_1:22;
case 1-s1=0;
then 1=0+s1 by XCMPLX_1:27 .=s1;
then s2=1 by A4,A5,AXIOMS:21;
then q =0.REAL 2 + 1*p2 by A4,EUCLID:33
.=0.REAL 2 + p2 by EUCLID:33
.=p2 by EUCLID:31;
hence q in LSeg(p,p2) by TOPREAL1:6;
end;
now per cases;
case A17:s2<>0;
set s=s1/s2;
A18:s>=0 by A3,A4,REAL_2:125;
A19:s2*(((s2-s1)/s2))=s2-s1 by A17,XCMPLX_1:88;
A20: s2*((s1)/s2)=s1 by A17,XCMPLX_1:88;
A21:(s2-s1)+s1*(1-s2)=(s2-s1)+(s1*1-s1*s2) by XCMPLX_1:40
.=(s2-s1)+s1-s1*s2 by XCMPLX_1:29
.=1*s2-s1*s2 by XCMPLX_1:27 .=s2*(1-s1) by XCMPLX_1:40;
s2/s2>=s1/s2 by A4,A5,A17,REAL_1:73;
then A22:1>=s by A17,XCMPLX_1:60;
s2*((1-s)*p1+s*q)
=s2*(((1*s2-s1)/s2)*p1
+(s1/s2)*((1-s2)*p1+s2*p2)) by A4,A17,XCMPLX_1:128
.=s2*(((s2-s1)/s2)*p1)
+s2*((s1/s2)*((1-s2)*p1+s2*p2)) by EUCLID:36
.=s2*(((s2-s1)/s2))*p1
+s2*((s1/s2)*((1-s2)*p1+s2*p2)) by EUCLID:34
.=(s2-s1)*p1 +s2*(s1/s2)*((1-s2)*p1+s2*p2) by A19,EUCLID:34
.=(s2-s1)*p1 +(s1*((1-s2)*p1)+s1*(s2*p2)) by A20,EUCLID:36
.=(s2-s1)*p1 +(s1*(1-s2)*p1+s1*(s2*p2)) by EUCLID:34
.=(s2-s1)*p1 +(s1*(1-s2)*p1+s1*s2*p2) by EUCLID:34
.=(s2-s1)*p1 +s1*(1-s2)*p1+s1*s2*p2 by EUCLID:30
.=((s2-s1)+s1*(1-s2))*p1+s1*s2*p2 by EUCLID:37
.=s2*((1-s1)*p1)+s2*s1*p2 by A21,EUCLID:34
.=s2*((1-s1)*p1)+s2*(s1*p2) by EUCLID:34
.=s2*p by A3,EUCLID:36;
then p=(1-s)*p1+s*q by A17,EUCLID:38;
hence p in LSeg(p1,q) by A18,A22,SPPOL_1:22;
case s2=0;
then s1=0 by A1,A3,A4,Def6;
then p =1*p1+(0.REAL 2) by A3,EUCLID:33
.=p1+(0.REAL 2) by EUCLID:33
.=p1 by EUCLID:31;
hence p in LSeg(p1,q) by TOPREAL1:6;
end;
hence q in LSeg(p,p2) & p in LSeg(p1,q) by A7;
end;
theorem Th66:
for f being non empty FinSequence of TOP-REAL 2,p,q,p1,p2 being
Point of TOP-REAL 2 st f is_S-Seq & p in L~f & q in L~f & p<>q
& Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1)
holds q in L~(L_Cut(f,p))
proof let f be non empty FinSequence of TOP-REAL 2,p,q,p1,p2 be
Point of TOP-REAL 2;
assume that
A1:f is_S-Seq and
A2: p in L~f and
A3: q in L~f and
A4: p<>q and
A5: Index(p,f)=Index(q,f) and
A6: LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1);
set i1=Index(q,f)-'Index(p,f)+1;
A7:1<=Index(q,f) & Index(q,f)<len f by A3,Th41;
Index(q,f)<len f by A3,Th41;
then A8:Index(q,f)+1<=len f by NAT_1:38;
A9:Index(q,f)-'Index(p,f)=Index(q,f)-Index(p,f) by A5,SCMFSA_7:3
.=0 by A5,XCMPLX_1:14;
A10:0<=Index(q,f)-Index(p,f) by A5,XCMPLX_1:14;
1<0+1+1;
then A11:len <*p*><Index(q,f)-'Index(p,f)+1+1 by A9,FINSEQ_1:57;
A12:1<=Index(p,f)+1 by NAT_1:29;
A13: 1<len f by A7,AXIOMS:22;
then len mid(f,Index(p,f)+1,len f)=len f -'(Index(p,f)+1)+1
by A5,A8,A12,Th27;
then A14:len <*p*>+len mid(f,Index(p,f)+1,len f)=1+(len f -'(Index(p,f)+1)+1)
by FINSEQ_1:57
.=1+(len f -(Index(p,f)+1)+1) by A5,A8,SCMFSA_7:3
.=1+(len f -Index(p,f)-1+1) by XCMPLX_1:36
.=(len f -Index(p,f))+1 by XCMPLX_1:27;
Index(q,f)-Index(p,f)<=len f -Index(p,f) by A7,REAL_1:49;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f)+1 by AXIOMS:24;
then A15:Index(q,f)-'Index(p,f)+1<=len f -Index(p,f)+1 by A5,SCMFSA_7:3;
A16: now assume A17: p = f.(Index(p,f)+1);
then A18: p = f/.(Index(p,f)+1) by A5,A8,A12,FINSEQ_4:24;
q in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A6,Def6;
then consider r being Real such that
A19: 0 <= r & r <= 1 and
A20: q = (1-r)*f/.(Index(p,f))+r*f/.(Index(p,f)+1) by SPPOL_1:21;
A21: p = 1*p by EUCLID:33
.= 0.REAL 2 + 1*p by EUCLID:31
.= (1-1)*f/.(Index(p,f))+1*p by EUCLID:33;
then 1<=r by A6,A18,A19,A20,Def6;
then r = 1 by A19,AXIOMS:21;
hence contradiction by A4,A5,A8,A12,A17,A20,A21,FINSEQ_4:24;
end;
then p <> f.len f by A1,A13,Th45;
then A22:len L_Cut(f,p)=len f -Index(p,f)+1 by A1,A2,A16,Th61;
then A23: (L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1)
=L_Cut(f,p).(Index(q,f)-'Index(p,f)+1) by A9,A15,FINSEQ_4:24
.=(<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1) by A16,Def4
.=p by A9,Th16;
A24:Index(q,f)<len f by A3,Th41;
then A25:Index(q,f)+1<=len f by NAT_1:38;
then Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by REAL_1:49;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by XCMPLX_1:29;
then i1<=len f -Index(p,f) by A10,BINARITH:def 3;
then A26:i1+1<=len L_Cut(f,p) by A22,AXIOMS:24;
A27:1<=Index(q,f) & Index(q,f)+1<=len f & q in LSeg(f,Index(q,f))
by A3,A24,Th41,Th42,NAT_1:38;
A28:Index(q,f)+1-Index(p,f)<=len f -Index(p,f) by A25,REAL_1:49;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by XCMPLX_1:29;
then A29: Index(q,f)-Index(p,f)+1+1<=len f -Index(p,f)+1 by AXIOMS:24;
then A30:len L_Cut(f,p)>=Index(q,f)-'Index(p,f)+1+1
by A5,A22,SCMFSA_7:3;
A31:Index(q,f)-'Index(p,f)+1+1<=len <*p*>+len mid(f,Index(p,f)+1,len f)
by A5,A14,A29,SCMFSA_7:3;
Index(q,f)-Index(p,f)+1<=len f -Index(p,f) by A28,XCMPLX_1:29;
then Index(q,f)-Index(p,f)+1<=len f -Index(p,f)-1+1 by XCMPLX_1:27;
then Index(q,f)-Index(p,f)+1<=len f -(Index(p,f)+1)+1 by XCMPLX_1:36;
then A32:Index(q,f)-'Index(p,f)+1<=len f - (Index(p,f)+1)+1
by A5,SCMFSA_7:3;
A33:1<=Index(q,f)+1 & Index(q,f)+1<=len f by A27,Th11;
(L_Cut(f,p))/.(Index(q,f)-'Index(p,f)+1+1)
=L_Cut(f,p).(Index(q,f)-'Index(p,f)+1+1) by A9,A30,FINSEQ_4:24
.=(<*p*>^mid(f,Index(p,f)+1,len f)).(Index(q,f)-'Index(p,f)+1+1)
by A16,Def4
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-len <*p*>)
by A11,A31,Th15
.=mid(f,Index(p,f)+1,len f).(Index(q,f)-'Index(p,f)+1+1-1)
by FINSEQ_1:57
.=f.(Index(p,f)+1+(Index(q,f)-'Index(p,f)+1)-1)
by A5,A8,A9,A12,A32,Th31
.=f.(Index(p,f)+1+(Index(q,f)-Index(p,f)+1)-1) by A5,SCMFSA_7:3
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f)+1))-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+(Index(q,f)-Index(p,f))+1)-1) by XCMPLX_1:1
.=f.(1+(Index(p,f)+Index(q,f)-Index(p,f)+1)-1) by XCMPLX_1:29
.=f.(1+(Index(q,f)+1)-1) by XCMPLX_1:26
.=f.(Index(q,f)+1) by XCMPLX_1:26
.=f/.(Index(q,f)+1) by A33,FINSEQ_4:24;
then q in LSeg((L_Cut(f,p))/.((Index(q,f)-'Index(p,f)+1)),
(L_Cut(f,p))/.((Index(q,f)-'Index(p,f)+1+1)))
by A5,A6,A23,Th65;
hence q in L~(L_Cut(f,p)) by A9,A26,SPPOL_2:15;
end;
begin
::--------------------------------------------------------:
:: Cutting Both Sides of a Finite Sequence and :
:: a Discussion of Speciality of Sequences in TOP-REAL 2 :
::--------------------------------------------------------:
definition let f be FinSequence of TOP-REAL 2,p,q be Point of TOP-REAL 2;
func B_Cut(f,p,q) -> FinSequence of TOP-REAL 2 equals
:Def8:
R_Cut(L_Cut(f,p),q) if p in L~f & q in L~f & Index(p,f)<Index(q,f)
or Index(p,f)=Index(q,f)
& LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1)
otherwise Rev (R_Cut(L_Cut(f,q),p));
correctness;
end;
theorem Th67:for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2
st f is_S-Seq & p in L~f & p<>f.1
holds R_Cut(f,p) is_S-Seq_joining f/.1,p
proof let f be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq and
A2: p in L~f and
A3: p<>f.1;
R_Cut(f,p)=mid(f,1,Index(p,f))^<*p*> by A3,Def5;
hence thesis by A1,A2,A3,Th52;
end;
theorem Th68:
for f being non empty FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st f is_S-Seq & p in L~f &
p<>f.len f holds L_Cut(f,p) is_S-Seq_joining p,f/.len f
proof let f be non empty FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is_S-Seq & p in L~f and
A2: p<>f.len f;
A3: Rev f is_S-Seq & p in L~Rev f by A1,SPPOL_2:22,47;
A4: L_Cut(f,p) = L_Cut(Rev Rev f,p) by FINSEQ_6:29
.= Rev R_Cut(Rev f,p) by A3,Th57;
p <> (Rev f).1 by A2,FINSEQ_5:65;
then R_Cut(Rev f,p) is_S-Seq_joining (Rev f)/.1,p by A3,Th67;
then L_Cut(f,p) is_S-Seq_joining p,(Rev f)/.1 by A4,Th48;
hence thesis by FINSEQ_5:68;
end;