:: Concatenation of Finite Sequences Reducing Overlapping Part and an
:: Argument of Separators of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Received March 18, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_8, ARYTM_1, RELAT_1, FINSEQ_1, FUNCT_1, FINSEQ_5, RFINSEQ,
JORDAN3, ARYTM_3, NUMBERS, ORDINAL4, TARSKI, XBOOLE_0, XXREAL_0, CARD_1,
SUBSET_1, NAT_1, GRAPH_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
NAT_1, NAT_D, RELAT_1, RFINSEQ, FINSEQ_1, FUNCT_1, FINSEQ_6, FINSEQ_5;
constructors SQUARE_1, NAT_1, RFINSEQ, NAT_D, FINSEQ_5, FINSEQ_6, REAL_1,
RELSET_1;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, ORDINAL1,
XBOOLE_0, CARD_1;
requirements NUMERALS, REAL, SUBSET, ARITHM;
equalities FINSEQ_1;
expansions FINSEQ_1;
theorems NAT_1, NAT_2, FINSEQ_1, FINSEQ_3, FINSEQ_5, FINSEQ_6, RFINSEQ,
RELAT_1, XREAL_1, XBOOLE_1, XXREAL_0, ORDINAL1, XREAL_0, NAT_D;
schemes NAT_1;
begin
theorem
for f,g being FinSequence st len f>=1 holds mid(f^g,1,len f)=f
proof
let f,g be FinSequence;
assume
A1: len f>=1;
then len f-1>=0 by XREAL_1:48;
then len f -1=len f-'1 by XREAL_0:def 2;
then
A2: len f-'1+1=len f;
1-1=0;
then
A3: 1-'1=0 by XREAL_0:def 2;
(f^g)|len f=f by FINSEQ_5:23;
then ((f^g)/^0)|len f=f by FINSEQ_5:28;
hence thesis by A1,A2,A3,FINSEQ_6:def 3;
end;
theorem Th2:
for f being FinSequence,i being Nat st i>=len f holds f/^i={}
proof
let f be FinSequence,i be Nat;
assume
A1: i>=len f;
per cases by A1,XXREAL_0:1;
suppose i>len f;
hence thesis by RFINSEQ:def 1;
end;
suppose
A2: i=len f;
then len (f/^i)=len f -i by RFINSEQ:def 1
.=0 by A2;
hence thesis;
end;
end;
theorem
for D being non empty set,k1,k2 being Nat holds
mid(<*>D,k1,k2)=<*>D
proof
let D be non empty set,k1,k2 be Nat;
per cases;
suppose k1<=k2;
hence mid(<*>D,k1,k2)=((<*>D)/^(k1-'1))|(k2-'k1+1) by FINSEQ_6:def 3
.= (<*>D)|(k2-'k1+1) by FINSEQ_6:80
.=<*>D by FINSEQ_5:78;
end;
suppose k1>k2;
hence mid(<*>D,k1,k2)=Rev (((<*>D)/^(k2-'1))|(k1-'k2+1)) by FINSEQ_6:def 3
.= Rev((<*>D)|(k1-'k2+1)) by FINSEQ_6:80
.= Rev(<*>D) by FINSEQ_5:78
.=<*>D by FINSEQ_5:79;
end;
end;
definition
let f be FinSequence, k1,k2 be Nat;
func smid(f,k1,k2) -> FinSequence equals
(f/^(k1-'1))|(k2+1-'k1);
correctness;
end;
definition
let D be set,f be FinSequence of D,k1,k2 be Nat;
redefine func smid(f,k1,k2) -> FinSequence of D; :: redefines smid (FINSEQ_8, definition)
correctness
proof
smid(f,k1,k2) = (f/^(k1-'1))|(k2+1-'k1);
hence thesis;
end;
end;
theorem Th4:
for f being FinSequence,k1,k2 being Nat st k1<=k2 holds
smid(f,k1,k2) = mid(f,k1,k2)
proof
let f be FinSequence,k1,k2 be Nat;
assume
A1: k1<=k2;
then k2-'k1+1=k2-k1+1 by XREAL_1:233
.=k2+1-k1
.=k2+1-'k1 by A1,NAT_1:12,XREAL_1:233;
hence thesis by A1,FINSEQ_6:def 3;
end;
theorem Th5:
for f being FinSequence, k2 being Nat holds smid(f,1,k2)=f|k2
proof
let f be FinSequence, k2 be Nat;
thus smid(f,1,k2) = (f/^0)|(k2+1-'1) by NAT_2:8
.= f|(k2+1-'1) by FINSEQ_5:28
.=f|k2 by NAT_D:34;
end;
theorem Th6:
for f being FinSequence, k2 being Nat st len f<=k2 holds
smid(f,1,k2)=f
proof
let f be FinSequence,k2 be Nat;
assume
A1: len f<=k2;
thus smid(f,1,k2)=f|k2 by Th5
.=f by A1,FINSEQ_1:58;
end;
theorem Th7:
for f being FinSequence, k1,k2 being Nat st k1>k2 holds
smid(f,k1,k2)={}
proof
let f be FinSequence,k1,k2 be Nat;
assume
A1: k1>k2;
set g=(f/^(k1-'1));
k2+1<=k1 by A1,NAT_1:13;
then smid(f,k1,k2)=g|0 by NAT_2:8;
hence thesis;
end;
theorem
for f being FinSequence, k2 being Nat holds smid(f,0,k2)=smid(f,1,k2+1)
proof
let f be FinSequence, k2 be Nat;
thus smid(f,0,k2)=(f/^0)|(k2+1-'0) by NAT_2:8
.= f|(k2+1-'0) by FINSEQ_5:28
.= f|(k2+1) by NAT_D:40
.= f|(k2+1+1-'1) by NAT_D:34
.= (f/^0)|(k2+1+1-'1) by FINSEQ_5:28
.= smid(f,1,k2+1) by NAT_2:8;
end;
theorem Th9:
for f,g being FinSequence holds smid(f^g,len f+1,len f+len g)=g
proof
let f,g be FinSequence;
len g+len f+1-'(len f+1) =len g+(len f+1)-'(len f+1) .= len g by NAT_D:34;
then g|(len g+len f+1-'(len f+1))=g by FINSEQ_1:58;
then ((f^g)/^(len f))|(len f+len g+1-'(len f+1))=g by FINSEQ_5:37;
hence thesis by NAT_D:34;
end;
:: Overlapping Part
definition
let D be non empty set,f,g be FinSequence of D;
func ovlpart(f,g) -> FinSequence of D means :Def2:
len it <=len g & it=smid(g,1,len it) & it=smid(f,len f-'len it+1,len f)
& for j being Nat st j<=len g & smid(g,1,j)=smid(f,len f-'j+1,len f)
holds j<=len it;
existence
proof
defpred P[Nat] means $1 <=len g & smid(g,1,$1)=smid(f,len f-'$1+1,len f);
A1: smid(g,1,0)={} by Th7;
len f-'0+1=len f-0+1 by XREAL_1:233
.=len f+1;
then smid(f,len f-'0+1,len f)={} by Th7,XREAL_1:29;
then
A2: ex m being Nat st P[m] by A1;
A3: for n being Nat st P[n] holds n<=len g;
consider k being Nat such that
A4: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A3,A2);
reconsider k as Element of NAT by ORDINAL1:def 12;
set b = smid(g,1,k);
now per cases;
case
A5: k>0;
then
A6: 0+1<=k by NAT_1:13;
then
A7: b=mid(g,1,k) by Th4;
now per cases;
case len g>0;
then 0+1<=len g by NAT_1:13;
hence len b=k-'1+1 by A4,A6,A7,FINSEQ_6:118
.=k-1+1 by A6,XREAL_1:233
.=k;
end;
case len g<=0;
hence contradiction by A4,A5;
end;
end;
hence len b=k;
end;
case
A8: k<=0; then
b={} by Th7;
hence len b=k by A8;
end;
end;
hence thesis by A4;
end;
uniqueness
proof
let a,b be FinSequence of D;
assume that
A10: len a<=len g and
A11: a=smid(g,1,len a) and
A12: a=smid(f,len f-'len a+1,len f) and
A13: for j being Nat st j<=len g & smid(g,1,j)=smid(f,len f-'j+1,len f)
holds j<=len a and
A14: len b<=len g and
A15: b=smid(g,1,len b) and
A16: b=smid(f,len f-'len b+1,len f) and
A17: for j being Nat st j<=len g & smid(g,1,j)=smid(f,len f-'j+1,len f)
holds j<= len b;
A18: len a<=len b by A10,A11,A12,A17;
len b<=len a by A13,A14,A15,A16;
hence thesis by A11,A15,A18,XXREAL_0:1;
end;
end;
theorem Th10:
for D being non empty set,f,g being FinSequence of D
holds len ovlpart(f,g)<=len f
proof
let D be non empty set,f,g be FinSequence of D;
now
assume
A1: len ovlpart(f,g)>len f;
then len f - len ovlpart(f,g)<0 by XREAL_1:49;
then len f -' len ovlpart(f,g)=0 by XREAL_0:def 2;
then smid(f,len f-'len ovlpart(f,g)+1,len f) =f by Th6;
hence contradiction by A1,Def2;
end;
hence thesis;
end;
:: Concatenation Reducing Overlapping Part
definition
let D be non empty set,f,g be FinSequence of D;
func ovlcon(f,g) -> FinSequence of D equals
f^(g/^(len ovlpart(f,g)));
coherence;
end;
theorem Th11:
for D being non empty set,f,g being FinSequence of D
holds ovlcon(f,g)=(f|(len f-'len ovlpart(f,g)))^g
proof
let D be non empty set,f,g be FinSequence of D;
A1: len f-'len ovlpart(f,g)=len f-len ovlpart(f,g) by Th10,XREAL_1:233;
len f+1<=len f+1+len ovlpart(f,g) by NAT_1:12;
then len f+1-len ovlpart(f,g)<= len f+1+len ovlpart(f,g)-len ovlpart(f,g)
by XREAL_1:9;
then
A2: len f+1-'(len f-'len ovlpart(f,g)+1) =len f +1-(len f-'len ovlpart(f
,g)+1) by A1,XREAL_1:233
.= len ovlpart(f,g) by A1;
len f-'len ovlpart(f,g)<=len f by NAT_D:35;
then
A3: len (f/^(len f-'len ovlpart(f,g)))
=len f-(len f-'len ovlpart(f,g)) by RFINSEQ:def 1
.=0+len ovlpart(f,g) by A1;
A4: ovlpart(f,g)=smid(f,len f-'len ovlpart(f,g)+1,len f) by Def2
.=(f/^(len f-'len ovlpart(f,g)))|(len ovlpart(f,g)) by A2,NAT_D:34
.=(f/^(len f-'len ovlpart(f,g))) by A3,FINSEQ_1:58;
ovlpart(f,g)=smid(g,1,len ovlpart(f,g)) by Def2
.=(g/^(0+1-'1))|(len ovlpart(f,g)) by NAT_D:34
.=(g/^(0))|(len ovlpart(f,g)) by NAT_D:34
.= g|(len ovlpart(f,g)) by FINSEQ_5:28;
hence ovlcon(f,g)= (f|(len f-'len ovlpart(f,g)))^
(g|(len ovlpart(f,g)))^(g/^(len ovlpart(f,g))) by A4,RFINSEQ:8
.= (f|(len f-'len ovlpart(f,g)))^
((g|(len ovlpart(f,g)))^(g/^(len ovlpart(f,g)))) by FINSEQ_1:32
.=(f|(len f-'len ovlpart(f,g)))^g by RFINSEQ:8;
end;
::Overlapping Left Difference
definition
let D be non empty set,f,g be FinSequence of D;
func ovlldiff(f,g) -> FinSequence of D equals
(f|(len f-'len ovlpart(f,g)));
coherence;
end;
::Overlapping Right Difference
definition
let D be non empty set,f,g be FinSequence of D;
func ovlrdiff(f,g) -> FinSequence of D equals
(g/^(len ovlpart(f,g)));
coherence;
end;
theorem
for D being non empty set,f,g being FinSequence of D holds ovlcon(f,g)
=ovlldiff(f,g)^ovlpart(f,g)^ovlrdiff(f,g) & ovlcon(f,g)
=ovlldiff(f,g)^(ovlpart(f,g)^ovlrdiff(f,g))
proof
let D be non empty set,f,g be FinSequence of D;
ovlpart(f,g)^(g/^(len ovlpart(f,g)))
= smid(g,1,len ovlpart(f,g))^(g/^(len ovlpart(f,g))) by Def2
.= g|(len ovlpart(f,g))^(g/^(len ovlpart(f,g))) by Th5
.= g by RFINSEQ:8;
hence ovlcon(f,g)
=(f|(len f-'len ovlpart(f,g)))^(ovlpart(f,g)^(g/^(len ovlpart(f,g))))
by Th11
.=ovlldiff(f,g)^ovlpart(f,g)^ovlrdiff(f,g) by FINSEQ_1:32;
hence thesis by FINSEQ_1:32;
end;
theorem
for D being non empty set,f being FinSequence of D
holds ovlcon(f,f)=f & ovlpart(f,f)=f & ovlldiff(f,f)={} & ovlrdiff(f,f)={}
proof
let D be non empty set,f be FinSequence of D;
A1: ovlpart(f,f)=smid(f,1,len ovlpart(f,f)) by Def2;
len f-'len f+1=len f-len f+1 by XREAL_1:233
.=0+1;
then smid(f,1,len f)=smid(f,len f-'len f+1,len f);
then
A2: len f<=len ovlpart(f,f) by Def2;
then
A3: ovlcon(f,f)=f^(<*>D) by Th2
.=f by FINSEQ_1:34;
A4: ovlldiff(f,f)= f|(len f-'len f) by A1,A2,Th6
.= f|(0) by XREAL_1:232
.= {};
ovlrdiff(f,f)= {} by A2,Th2;
hence thesis by A1,A2,A3,A4,Th6;
end;
theorem
for D being non empty set,f,g being FinSequence of D
holds ovlpart(f^g,g)=g & ovlpart(f,f^g)=f
proof
let D be non empty set,f,g be FinSequence of D;
A1: len ovlpart(f^g,g)<=len g by Def2;
A2: smid(g,1,len g)=g|(len g) by Th5
.=g by FINSEQ_1:58;
len (f^g)-'len g+1 =len f + len g -'len g+1 by FINSEQ_1:22
.=len f +1 by NAT_D:34;
then smid(f^g,len (f^g)-'len g+1,len (f^g))
= smid(f^g,len f+1,len f + len g) by FINSEQ_1:22
.= g by Th9;
then len g<=len ovlpart(f^g,g) by A2,Def2;
then
A3: len g= len ovlpart(f^g,g) by A1,XXREAL_0:1;
A4: ovlpart(f^g,g)=smid(g,1,len ovlpart(f^g,g)) by Def2
.=g|(len g) by A3,Th5
.=g by FINSEQ_1:58;
A5: len ovlpart(f,f^g)<=len f by Th10;
len f-'len f+1=0+1 by XREAL_1:232
.=1;
then
A6: smid(f,len f-'len f+1,len f) = (f/^(0+1-'1))|(len (f)) by NAT_D:34
.= (f/^(0))|(len (f)) by NAT_D:34
.= f|(len (f)) by FINSEQ_5:28
.= f by FINSEQ_1:58;
len f<=len f+len g by NAT_1:12;
then
A7: len f<=len (f^g) by FINSEQ_1:22;
smid(f^g,1,len f) = (f^g)|len f by Th5
.= f by FINSEQ_5:23;
then len f<=len ovlpart(f,f^g) by A6,A7,Def2;
then
A8: len f= len ovlpart(f,f^g) by A5,XXREAL_0:1;
ovlpart(f,f^g)=smid(f^g,1,len ovlpart(f,f^g)) by Def2
.=(f^g)|(len f) by A8,Th5
.=f by FINSEQ_5:23;
hence thesis by A4;
end;
theorem Th15:
for D being non empty set,f,g being FinSequence of D
holds len ovlcon(f,g)=len f+len g -len ovlpart(f,g) &
len ovlcon(f,g)=len f+len g -'len ovlpart(f,g) &
len ovlcon(f,g)=len f+(len g -'len ovlpart(f,g))
proof
let D be non empty set,f,g be FinSequence of D;
A1: len ovlpart(f,g) <= len g by Def2;
A2: len ovlcon(f,g)=len f +len (g/^(len ovlpart(f,g))) by FINSEQ_1:22
.=len f+(len g-'len ovlpart(f,g)) by RFINSEQ:29
.=len f+(len g -len ovlpart(f,g)) by A1,XREAL_1:233;
hence
A3: len ovlcon(f,g)=len f+len g -len ovlpart(f,g);
A4: len ovlpart(f,g)<=len g by Def2;
hence len ovlcon(f,g)
=len f+len g -'len ovlpart(f,g) by A3,NAT_1:12,XREAL_1:233;
thus thesis by A2,A4,XREAL_1:233;
end;
theorem Th16:
for D being non empty set,f,g being FinSequence of D holds
len ovlpart(f,g)<=len f & len ovlpart(f,g)<=len g
proof
let D be non empty set,f,g be FinSequence of D;
now
assume
A1: len ovlpart(f,g)>len f;
ovlpart(f,g)=smid(f,len f-'len ovlpart(f,g) +1,len f) by Def2
.=smid(f,0+1,len f) by A1,NAT_2:8
.=f by Th6;
hence contradiction by A1;
end;
hence thesis by Def2;
end;
definition
let D be non empty set,CR be FinSequence of D;
pred CR separates_uniquely means
for f being FinSequence of D,i,j being Element of NAT
st 1<=i & i<j & j+len CR-'1<=len f &
smid(f,i,i+len CR-'1)=smid(f,j,j+len CR-'1) & smid(f,i,i+len CR-'1)=CR
holds j-'i>=len CR;
end;
theorem
for D being non empty set,CR being FinSequence of D holds
CR separates_uniquely iff len ovlpart(CR/^1,CR) =0
proof
let D be non empty set,CR be FinSequence of D;
set p= ovlpart(CR/^1,CR);
A1: now
assume
A2: CR separates_uniquely;
set f=(CR|1) ^ ovlcon(CR/^1,CR);
A3: f=(CR|1) ^ (CR/^1) ^ (CR/^(len ovlpart(CR/^1,CR))) by FINSEQ_1:32
.= CR ^ (CR/^(len ovlpart(CR/^1,CR))) by RFINSEQ:8;
A4: f=(CR|1)^(((CR/^1)|(len (CR/^1)-'len ovlpart(CR/^1,CR)))^CR) by Th11
.=(CR|1)^((CR/^1)|(len (CR/^1)-'len ovlpart(CR/^1,CR)))^CR
by FINSEQ_1:32;
A5: len ((CR|1)^((CR/^1)|(len (CR/^1)-'len ovlpart(CR/^1,CR))))
=len (CR|1)+len ((CR/^1)|(len (CR/^1)-'len ovlpart(CR/^1,CR)))
by FINSEQ_1:22
.=len (CR|1) +(len (CR/^1)-'len ovlpart(CR/^1,CR)) by FINSEQ_1:59,NAT_D:35
.=len (CR|1) +(len (CR/^1)-len ovlpart(CR/^1,CR)) by Th16,XREAL_1:233
.=len (CR|1)+len (CR/^1)- len ovlpart(CR/^1,CR)
.=len ((CR|1)^(CR/^1))- len ovlpart(CR/^1,CR) by FINSEQ_1:22
.=len CR - len ovlpart(CR/^1,CR) by RFINSEQ:8;
A6: len CR - len ovlpart(CR/^1,CR)=len CR -' len ovlpart(CR/^1,CR)
by Th16,XREAL_1:233;
A7: len CR +1-'1=len CR by NAT_D:34;
A8: len ovlpart(CR/^1,CR)<=len CR by Def2;
A9: len f= len (CR|1) +len ovlcon(CR/^1,CR) by FINSEQ_1:22
.= len (CR|1) +(len (CR/^1)+len CR - len ovlpart(CR/^1,CR)) by Th15
.= len (CR|1) +len (CR/^1)+(len CR - len ovlpart(CR/^1,CR))
.= len ((CR|1)^(CR/^1))+(len CR - len ovlpart(CR/^1,CR)) by FINSEQ_1:22
.= len CR + (len CR - len ovlpart(CR/^1,CR)) by RFINSEQ:8;
set j=len CR +1-'len ovlpart(CR/^1,CR);
A10: len CR<len CR +1 by XREAL_1:29;
A11: len ovlpart(CR/^1,CR)<=len CR by Def2;
then
A12: j=1+len CR -len ovlpart(CR/^1,CR) by A10,XREAL_1:233,XXREAL_0:2
.=1+(len CR -len ovlpart(CR/^1,CR))
.=1+(len CR -'len ovlpart(CR/^1,CR)) by A11,XREAL_1:233;
then
A13: 1<=j by NAT_1:12;
A14: smid(f,1,1+len CR-'1)=(f/^(0+1-'1))|(len CR+1-'1) by NAT_D:34
.=(f/^0)|len CR by A7,NAT_D:34
.=f|len CR by FINSEQ_5:28
.=CR by A3,FINSEQ_5:23;
j+len CR-'1+1 =j+len CR-1+1 by A13,NAT_1:12,XREAL_1:233
.=j+len CR;
then
A15: j+len CR-'1+1-'j =j+len CR -j by NAT_1:12,XREAL_1:233
.=len CR;
1<= 1+(len CR -'len ovlpart(CR/^1,CR)) by NAT_1:12;
then 1<= 1+(len CR -len ovlpart(CR/^1,CR)) by A8,XREAL_1:233;
then 1<= 1+len CR -len ovlpart(CR/^1,CR);
then 1<=len CR +1-'len ovlpart(CR/^1,CR) by A8,NAT_1:12,XREAL_1:233;
then len CR +1-'len ovlpart(CR/^1,CR)-'1
=len CR +1-'len ovlpart(CR/^1,CR)-1 by XREAL_1:233;
then len CR +1-'len ovlpart(CR/^1,CR)-'1
=len CR+1-len ovlpart(CR/^1,CR) -1 by A8,NAT_1:12,XREAL_1:233
.=len CR +1 -1-len ovlpart(CR/^1,CR)
.=len CR -'len ovlpart(CR/^1,CR) by A11,XREAL_1:233;
then
A16: smid(f,j,j+len CR-'1) =CR|len CR by A4,A5,A6,A15,FINSEQ_5:37
.=smid(f,1,1+len CR-'1) by A14,FINSEQ_1:58;
len ovlpart(CR/^1,CR) <= len (CR/^1) by Th10;
then len ovlpart(CR/^1,CR) <= len CR -'1 by RFINSEQ:29;
then
A17: len CR+1-len ovlpart(CR/^1,CR) >= 1+len CR -(len CR -'1) by XREAL_1:10;
now per cases;
case len CR >=1;
then 1+len CR -(len CR -'1)=1+len CR -(len CR -1) by XREAL_1:233
.=1+1;
then 1< len CR +1-len ovlpart(CR/^1,CR) by A17,XXREAL_0:2;
then
A18: 1<j by A10,A11,XREAL_1:233,XXREAL_0:2;
(len CR -'len ovlpart(CR/^1,CR))+len CR+1 -'1
<= len CR + (len CR -' len ovlpart(CR/^1,CR)) by NAT_D:34;
then 1+(len CR -'len ovlpart(CR/^1,CR))+len CR -'1
<= len CR + (len CR - len ovlpart(CR/^1,CR)) by A11,XREAL_1:233;
then
A19: j-'1 >=len CR by A2,A9,A12,A14,A16,A18;
A20: j-'1=1+(len CR -'len ovlpart(CR/^1,CR))-1 by A12,NAT_1:12,XREAL_1:233
.= (len CR -'len ovlpart(CR/^1,CR));
A21: len CR -'len ovlpart(CR/^1,CR)<=len CR by NAT_D:35;
len CR -'len ovlpart(CR/^1,CR)=len CR -len ovlpart(CR/^1,CR)
by A11,XREAL_1:233;
then len CR -len ovlpart(CR/^1,CR)=len CR by A19,A20,A21,XXREAL_0:1;
hence len ovlpart(CR/^1,CR) =0;
end;
case len CR<1;
then len CR<0+1;
then len CR<=0 by NAT_1:13;
hence len ovlpart(CR/^1,CR) =0 by Def2;
end;
end;
hence len ovlpart(CR/^1,CR) =0;
end;
now
assume
A22: len ovlpart(CR/^1,CR) =0;
for f being FinSequence of D,i,j being Element of NAT
st 1<=i & i<j & j+len CR-'1<=len f &
smid(f,i,i+len CR-'1)=smid(f,j,j+len CR-'1) & smid(f,i,i+len CR-'1)=CR
holds j-'i>=len CR
proof
let f be FinSequence of D,i,j be Element of NAT;
assume that
A23: 1<=i and
A24: i<j and
A25: j+len CR-'1<=len f and
A26: smid(f,i,i+len CR-'1)=smid(f,j,j+len CR-'1) and
A27: smid(f,i,i+len CR-'1)=CR;
A28: j-i>0 by A24,XREAL_1:50;
then
A29: j-'i=j-i by XREAL_0:def 2;
A30: i+(j-'i)=j-i+i by A28,XREAL_0:def 2
.=j;
now per cases;
case len CR<=0;
hence thesis;
end;
case
A31: len CR>0;
then
A32: 0+1<=len CR by NAT_1:13;
then
A33: len CR -'1=len CR-1 by XREAL_1:233;
A34: i+len CR-'1=i+len CR-1 by A32,NAT_1:12,XREAL_1:233;
A35: i<=i+(len CR -'1) by NAT_1:12;
then
A36: 1<=i+len CR -'1 by A23,A33,A34,XXREAL_0:2;
set k=j-'i;
A37: 0+1<=k by A24,XREAL_1:50,A29,NAT_1:13;
then
A38: k-1=k-'1 by XREAL_1:233;
A39: i+(k-'1)=i+(k-1) by A37,XREAL_1:233
.=i+(j-i-1) by A28,XREAL_0:def 2
.=j-1;
i+1<=j by A24,NAT_1:13;
then
A40: i+1-1<=j-1 by XREAL_1:9;
then
A41: j-'1=j-1 by XREAL_0:def 2;
j-i>0 by A24,XREAL_1:50;
then j-'i>0 by XREAL_0:def 2;
then
A42: j-'i>=0+1 by NAT_1:13;
A43: j-'1<=j-'1+len CR by NAT_1:12;
j<=j+len CR by NAT_1:12;
then
A44: i<j+len CR by A24,XXREAL_0:2;
j-'1+len CR=j-1+len CR by A40,XREAL_0:def 2
.=j+len CR-1
.=j+len CR-'1 by A23,A44,XREAL_1:233,XXREAL_0:2;
then
A45: i+(k-'1)<=len f by A25,A39,A41,A43,XXREAL_0:2;
now
assume
A46: j-'i<len CR;
then k-1<len CR-1 by XREAL_1:9;
then k-'1<len CR-1 by A42,XREAL_1:233;
then k-'1<len CR -'1 by A32,XREAL_1:233;
then
A47: k-'1+1<=len CR -'1 by NAT_1:13;
A48: k-k<len CR -k by A46,XREAL_1:9;
then 0<len CR -'k by XREAL_0:def 2;
then
A49: 0+1<=len CR -'k by NAT_1:13;
A50: len CR -'k=len CR -k by A48,XREAL_0:def 2;
1<len CR by A37,A46,XXREAL_0:2;
then 1+1<=len CR by NAT_1:13;
then
A51: 1+1-1<=len CR -1 by XREAL_1:9;
A52: len CR-'1=len CR-1 by A37,A46,XREAL_1:233,XXREAL_0:2;
then
A53: len CR -'k<= len CR -'1 by A37,A50,XREAL_1:10;
i<=i+(k-'1) by NAT_1:12;
then
A54: i<=len f by A45,XXREAL_0:2;
j+len CR-'1=j+len CR-1 by A23,A44,XREAL_1:233,XXREAL_0:2
.=j+(len CR-1)
.=j+(len CR-'1) by A32,XREAL_1:233;
then j<=j+len CR -'1 by NAT_1:12;
then
A55: j<=len f by A25,XXREAL_0:2;
i+1<=j by A24,NAT_1:13;
then i+1+len CR<=j+len CR by XREAL_1:7;
then
A56: i+1+len CR-1<=j+len CR-1 by XREAL_1:9;
A57: 1<j by A23,A24,XXREAL_0:2;
A58: j<j+len CR by A31,XREAL_1:29;
then
A59: 1<j+len CR by A57,XXREAL_0:2;
A60: j+len CR-'1=j+len CR-1 by A57,A58,XREAL_1:233,XXREAL_0:2;
then
A61: i+1-1+len CR <=len f by A25,A56,XXREAL_0:2;
i+len CR<=i+len CR+1 by NAT_1:12;
then i+len CR -'1<=i+len CR by A34,XREAL_1:20;
then
A62: i+len CR-'1<=len f by A61,XXREAL_0:2;
A63: 0+1<= j+len CR-'1 by A60,NAT_1:13,A59,XREAL_1:50;
j+1<=j+len CR by A58,NAT_1:13;
then
A64: j+1-1<=j+len CR-1 by XREAL_1:9;
A65: len CR <=len CR +k by NAT_1:12;
then
A66: len CR -k<=len CR by XREAL_1:20;
A67: len CR -'k<=len CR by A50,A65,XREAL_1:20;
A68: len smid(CR,1,(len CR) -'k)
= len mid(CR,1,(len CR) -'k) by A49,Th4;
A69: len mid(CR,1,(len CR) -'k)
= (len CR) -'k -'1+1 by A32,A49,A50,A66,FINSEQ_6:118
.= (len CR) -'k -1+1 by A49,XREAL_1:233
.= (len CR) -'k;
A70: len (CR/^1) -'(len CR-'k)+1
=len CR-'1-'(len CR -'k)+1 by RFINSEQ:29
.=len CR-'1-(len CR-'k)+1 by A53,XREAL_1:233
.=len CR-1-(len CR-k)+1 by A37,A46,A50,XREAL_1:233,XXREAL_0:2
.=k;
A71: len (CR/^1)=len CR -'1 by RFINSEQ:29;
then
A72: smid(CR/^1,len (CR/^1) -'(len CR-'k)+1,len (CR/^1) )
= mid(CR/^1,k,len CR -'1) by A38,A47,A70,Th4;
A73: len mid(CR/^1,k,len CR -'1)=len CR-'1-'k+1
by A37,A38,A47,A51,A52,A71,FINSEQ_6:118
.=len CR-'1-k+1 by A38,A47,XREAL_1:233
.=len CR -1-k+1 by A37,A46,XREAL_1:233,XXREAL_0:2
.=len CR -'k by A48,XREAL_0:def 2;
for jj being Nat st 1<=jj & jj<=len CR -'k holds
smid(CR,1,(len CR) -'k).jj
=smid(CR/^1,len (CR/^1) -'(len CR-'k)+1,len (CR/^1)).jj
proof
let jj be Nat;
assume that
A74: 1<=jj and
A75: jj<=len CR-'k;
A76: jj+k<=len CR -'k+k by A75,XREAL_1:7;
then
A77: jj+k-1<=len CR -1 by A50,XREAL_1:9;
reconsider j1=jj as Element of NAT by ORDINAL1:def 12;
A78: len mid(f,i,i+len CR-'1)=i+len CR-'1-'i+1
by A23,A33,A34,A35,A36,A54,A62,FINSEQ_6:118
.=i+len CR -1-i+1 by A33,A34,A35,XREAL_1:233
.=len CR;
len CR-'k<=len CR by NAT_D:35;
then
A79: jj <= len CR by A75,XXREAL_0:2;
A80: 1<=jj+(k-'1) by A74,NAT_1:12;
A81: jj+(k-'1)=jj+(k-1) by A37,XREAL_1:233
.=jj+k-1
.=jj+k-'1 by A74,NAT_1:12,XREAL_1:233;
A82: 1<=jj+k by A74,NAT_1:12;
jj+k-'1<=len CR -1 by A74,A77,NAT_1:12,XREAL_1:233;
then jj+k-'1<=len CR -'1 by A32,XREAL_1:233;
then jj+k-'1 in Seg len (CR/^1) by A71,A80,A81;
then
A83: jj+k-'1 in dom (CR/^1) by FINSEQ_1:def 3;
A84: smid(f,j,j+len CR-'1) =mid(f,j,j+len CR-'1) by A60,A64,Th4;
thus
smid(CR/^1,len (CR/^1) -'(len CR-'k)+1,len (CR/^1)).jj
=(CR/^1).(j1+k-'1) by A37,A38,A47,A51,A52,A71,A72,A73,A74,A75,FINSEQ_6:118
.= smid(f,i,i+len CR-'1).(jj+k-'1+1) by A27,A32,A83,RFINSEQ:def 1
.= mid(f,i,i+len CR-'1).(jj+k-'1+1) by A33,A34,A35,Th4
.= mid(f,i,i+len CR-'1).(jj+k-1+1) by A74,NAT_1:12,XREAL_1:233
.=f.(i+(j1+k)-'1)
by A23,A33,A34,A35,A36,A50,A54,A62,A76,A78,A82,FINSEQ_6:118
.=f.(i+k+j1-'1)
.=CR.jj by A25,A26,A27,A30,A55,A57,A60,A63,A64,A74,A79,A84,
FINSEQ_6:118
.=CR.(j1+1-'1) by NAT_D:34
.= mid(CR,1,(len CR) -'k).j1
by A32,A49,A50,A66,A69,A74,A75,FINSEQ_6:118
.= smid(CR,1,(len CR) -'k).jj by A49,Th4;
end;
then smid(CR,1,(len CR)-'k)
=smid(CR/^1,len (CR/^1) -'(len CR-'k)+1,len (CR/^1))
by A68,A69,A72,A73;
then (len CR)-'k<=len p by A67,Def2;
hence contradiction by A22,A48,XREAL_0:def 2;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence CR separates_uniquely;
end;
hence thesis by A1;
end;
definition
let f,g be FinSequence, n be Nat;
pred g is_substring_of f,n means
len g>0 implies
ex i being Nat st n<=i & i<=len f & mid(f,i,(i-'1)+len g)=g;
end;
theorem
for f,g being FinSequence, n,m being Nat
st m>=n & g is_substring_of f,m holds g is_substring_of f,n
proof
let f,g be FinSequence,n,m be Nat;
assume that
A1: m>=n and
A2: g is_substring_of f,m;
now per cases;
case len g>0;
then consider i being Nat such that
A3: m<=i and
A4: i<=len f and
A5: mid(f,i,(i-'1)+len g)=g by A2;
n<=i by A1,A3,XXREAL_0:2;
hence thesis by A4,A5;
end;
case len g<=0;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th19:
for f being FinSequence st 1<= len f holds f is_substring_of f,1
proof
let f be FinSequence;
assume
A1: 1<= len f;
1-'1+len f =0+len f by NAT_2:8
.=len f;
then mid(f,1,(1-'1)+len f)=f by A1,FINSEQ_6:120;
hence thesis by A1;
end;
theorem Th20:
for f,g being FinSequence
st g is_substring_of f,0 holds g is_substring_of f,1
proof
let f,g be FinSequence;
assume
A1: g is_substring_of f,0;
now per cases;
case
A2: len g>0;
then consider i being Nat such that
0<=i and
A3: i<=len f and
A4: mid(f,i,(i-'1)+len g)=g by A1;
A5: len g>=0+1 by A2,NAT_1:13;
now per cases;
case
A6: i=0;
0-1<0;
then
A7: i-'1=0 by A6,XREAL_0:def 2;
then
A8: (f/^(0-'1))|(len g-'0+1)=g by A4,A6,FINSEQ_6:def 3;
len g -'0=len g -0 by XREAL_0:def 2
.=len g;
then
A9: f|(len g+1)=g by A6,A7,A8,FINSEQ_5:28;
now per cases;
case len g+1>=len f;
then f=g by A9,FINSEQ_1:58;
hence thesis by A5,Th19;
end;
case
A10: len g+1<len f;
dom ( f|Seg(len g +1))=dom f /\ Seg(len g+1) by RELAT_1:61
.= Seg(len f) /\ Seg(len g+1) by FINSEQ_1:def 3
.=Seg (len g+1) by A10,FINSEQ_1:7;
then len g=len g+1 by A9,FINSEQ_1:def 3;
hence contradiction;
end;
end;
hence thesis;
end;
case i<>0;
then i>=0+1 by NAT_1:13;
hence thesis by A3,A4;
end;
end;
hence thesis;
end;
case len g<=0;
hence thesis;
end;
end;
hence thesis;
end;
notation
let g,f be FinSequence;
synonym g is_preposition_of↑ f for g c= f;
end;
definition
let g,f be FinSequence;
redefine pred g c= f means :: redefines c= (RELAT_1, redefinition) → c= (TARSKI, definition)
len g>0 implies 1<=len f & mid(f,1,len g)=g;
compatibility
proof
thus g c= f implies (len g>0 implies 1<=len f & mid(f,1,len g)=g)
proof
assume that
A1: g c= f and
A2: len g>0;
A3: 0+1 <= len g by A2,NAT_1:13;
len g <= len f by A1,FINSEQ_1:63;
hence 1<=len f by A3,XXREAL_0:2;
thus mid(f,1,len g) = (f/^(1-'1))|(len g-'1+1) by A3,FINSEQ_6:def 3
.= (f/^(1-'1))|len g by A3,XREAL_1:235
.= (f/^0)|len g by XREAL_1:232
.= f|len g by FINSEQ_5:28
.= g by A1,FINSEQ_3:113;
end;
assume
A4: len g>0 implies 1<=len f & mid(f,1,len g)=g;
per cases by A4;
suppose len g <= 0;
then g = {};
hence thesis by XBOOLE_1:2;
end;
suppose that
A5: len g > 0 and
A6: mid(f,1,len g)=g;
0+1 <= len g by A5,NAT_1:13;
then g = f|len g by A6,FINSEQ_6:116;
hence thesis by RELAT_1:59;
end;
end;
end;
theorem
for f,g being FinSequence st len g>0 & g is_preposition_of f holds g.1=f.1
proof
let f,g be FinSequence;
assume that
A1: len g>0 and
A2: g is_preposition_of f;
A4: len g <=len f by A2,FINSEQ_1:63;
0+1<=len g by A1,NAT_1:13;
hence thesis by A2,A4,FINSEQ_6:123;
end;
definition
let f,g be FinSequence;
pred g is_postposition_of f means
Rev g is_preposition_of Rev f;
correctness;
end;
theorem Th22:
for f,g being FinSequence
st len g=0 holds g is_postposition_of f
proof
let f,g be FinSequence;
assume len g=0;
then Rev g is_preposition_of Rev f by FINSEQ_5:def 3;
hence thesis;
end;
theorem Th23:
for D being non empty set,f,g being FinSequence of D
st g is_postposition_of f holds len g <=len f
proof
let D be non empty set,f,g be FinSequence of D;
assume a1: g is_postposition_of f;
A2: len (Rev g)=len g by FINSEQ_5:def 3;
len (Rev f)=len f by FINSEQ_5:def 3;
hence thesis by a1,A2,FINSEQ_1:63;
end;
theorem
for D being non empty set,f,g being FinSequence of D
st g is_postposition_of f holds
len g>0 implies len g<=len f & mid(f,(len f+1) -' len g,len f)=g
proof
let D be non empty set,f,g be FinSequence of D;
assume
A1: g is_postposition_of f;
then
A2: Rev g is_preposition_of Rev f;
then
A3: len (Rev g)>0 implies 1<=len (Rev f) & mid(Rev f,1,len (Rev g))=Rev g;
A5: len (Rev f)=len f by FINSEQ_5:def 3;
now
assume
A6: len g>0;
then
A7: 1<=len f by A2,FINSEQ_5:def 3;
A8: mid(Rev f,1,len g)=Rev g by A2,FINSEQ_5:def 3,A6;
A9: len f -1>=0 by A3,A5,A6,FINSEQ_5:def 3,XREAL_1:48;
A10: len g<=len f by A1,Th23;
A11: len f - len g>=0 by A1,Th23,XREAL_1:48;
len f<len f+1 by XREAL_1:29;
then len g<len f+1 by A10,XXREAL_0:2;
then
A12: len f+1-len g>0 by XREAL_1:50;
A13: 0+1<=len g by A6,NAT_1:13;
A14: g=Rev Rev g
.=mid(Rev (Rev f),len f-'len g+1,len f-'1+1)
by A5,A7,A8,A10,A13,FINSEQ_6:113
.=mid(f,len f -'len g +1,len f-'1+1);
A15: len f -'len g+1=len f-len g+1 by A11,XREAL_0:def 2
.=(len f+1)-'len g by A12,XREAL_0:def 2;
len f-'1+1=len f-1+1 by A9,XREAL_0:def 2
.=len f;
hence len g<=len f & mid(f,(len f+1) -' len g,len f)=g by A1,A14,A15,Th23;
end;
hence thesis;
end;
theorem
for D being non empty set,f,g being FinSequence of D
st (len g>0 implies len g<=len f & mid(f,(len f+1) -' len g,len f)=g)
holds g is_postposition_of f
proof
let D be non empty set,f,g be FinSequence of D;
assume
A1: len g>0 implies len g<=len f & mid(f,(len f+1) -' len g,len f)=g;
A2: len (Rev f)=len f by FINSEQ_5:def 3;
now per cases;
case
A3: len g>0;
then
A4: 0+1<=len g by NAT_1:13;
then
A5: len g-1>=0 by XREAL_1:48;
len f<len f+1 by XREAL_1:29;
then a6: len g<len f+1 by A1,XXREAL_0:2;
then
A6: len f+1-len g>0 by XREAL_1:50;
then (len f+1)-'len g =len f+1-len g by XREAL_0:def 2;
then
A7: 0+1<= (len f+1)-'len g by a6,NAT_1:13,XREAL_1:50;
A8: (len f+1)-' len g=len f-(len g-1) by A6,XREAL_0:def 2;
len f+0<=len f+(len g-1) by A5,XREAL_1:7;
then
A9: len f-(len g -1)<=len f by XREAL_1:20;
A10: 1<=len f by A1,A4,XXREAL_0:2;
A11: len f-'len f+1=len f-len f+1 by XREAL_0:def 2
.=1;
len f<len f+1 by XREAL_1:29;
then len g<=len f+1 by A1,XXREAL_0:2;
then
A12: len f -((len f+1)-'len g)=len f-(len f+1-len g)
by XREAL_0:def 2,XREAL_1:48
.=len g -1;
then
A13: len f-'((len f+1)-'len g)+1
=len f -((len f+1)-'len g)+1 by A5,XREAL_0:def 2;
Rev g =mid((Rev f),len f-'len f+1,len f-'((len f+1)-'len g)+1)
by A1,A3,A7,A8,A9,A10,FINSEQ_6:113
.=mid(Rev f,1,len (Rev g)) by A11,A12,A13,FINSEQ_5:def 3;
then Rev g is_preposition_of Rev f by A1,A2,A4,XXREAL_0:2;
hence thesis;
end;
case len g<=0;
then len g=0;
hence thesis by Th22;
end;
end;
hence thesis;
end;
theorem
for f,g being FinSequence
st 1<=len f & g is_preposition_of f holds g is_substring_of f,1
proof
let f,g be FinSequence;
assume that
A1: 1<=len f and
A2: g is_preposition_of f;
now per cases;
case
A3: len g>0;
mid(f,1,(1-'1)+len g)=mid(f,1,0+len g) by NAT_2:8
.= g by A2,A3;
hence thesis by A1;
end;
case len g<=0;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th27:
for D being non empty set,f,g being FinSequence of D, n being Nat
st not g is_substring_of f,n holds for i being Element of NAT st n <= i & 0 < i
holds mid(f,i,(i-'1)+len g) <> g
proof
let D be non empty set,f,g be FinSequence of D,n be Nat;
assume
A1: not g is_substring_of f,n;
now
let i be Element of NAT;
assume that
A2: n <= i and
A3: 0 < i;
now per cases;
case i<=len f;
hence mid(f,i,(i-'1)+len g) <> g by A1,A2;
end;
case
A4: i>len f;
now per cases;
case
A5: i<=(i-'1)+len g;
then
A6: mid(f,i,(i-'1)+len g)=(f/^(i-'1))|((i-'1)+len g-'i +1)
by FINSEQ_6:def 3;
now per cases;
case
A7: i-'1<= len f;
i>=len f +1 by A4,NAT_1:13;
then
A8: i-1>= len f +1-1 by XREAL_1:9;
0+1<=i by A3,NAT_1:13;
then i-'1=i-1 by XREAL_0:def 2,XREAL_1:48;
then
A9: i-'1=len f by A7,A8,XXREAL_0:1;
len (f/^(i-'1))=len f -(i-'1) by A7,RFINSEQ:def 1;
hence len (f/^(i-'1)) =0 by A9;
end;
case i-'1>len f;
then f/^(i-'1)=<*>D by RFINSEQ:def 1;
hence len (f/^(i-'1)) =0;
end;
end;
then
A10: (f/^(i-'1))|((i-'1)+len g-'i+1)=<*>D by FINSEQ_1:58;
now
assume
A11: mid(f,i,(i-'1)+len g)=g;
a12: 0+1<=i by A3,NAT_1:13;
i-1<i+1-1 by XREAL_1:9,XREAL_1:29;
hence contradiction by A5,A6,A10,A11,a12,XREAL_0:def 2;
end;
hence mid(f,i,(i-'1)+len g)<>g;
end;
case
A13: i>(i-'1)+len g;
now
assume len g>0;
then len g >=0+1 by NAT_1:13;
then
A14: (i-'1)+len g>=(i-'1)+1 by XREAL_1:7;
0+1<=i by A3,NAT_1:13;
then i-'1=i-1 by XREAL_0:def 2,XREAL_1:48;
hence contradiction by A13,A14;
end;
hence contradiction by A1;
end;
end;
hence mid(f,i,(i-'1)+len g)<>g;
end;
end;
hence mid(f,i,(i-'1)+len g) <> g;
end;
hence thesis;
end;
definition
let D be non empty set,f,g be FinSequence of D,n be Nat;
func instr(n,f,g) -> Element of NAT means
:Def10:
(it <> 0 implies n <= it & g is_preposition_of f/^(it-'1) &
for j being Element of NAT st j >= n & j > 0
& g is_preposition_of f/^(j-'1) holds j >= it)
& (it=0 implies not g is_substring_of f,n );
existence
proof
A1: 1-'1=1-1 by XREAL_0:def 2;
now per cases;
case
A2: g is_substring_of f,n;
now per cases;
case
A3: len g>0;
A5: 0+1<=len g by A3,NAT_1:13;
now per cases;
case
A6: n>0;
defpred P[Nat] means n <= $1 &
$1 <=len f & mid(f,$1,($1-'1)+len g)=g;
A7: ex i being Nat st P[i] by A2,A3;
ex k being Nat st P[k] & for m being Nat st P[m]
holds m >= k from NAT_1:sch 5(A7);
then consider k0 being Nat such that
A8: n <= k0 and
A9: k0<=len f and
A10: mid(f,k0,(k0-'1)+len g)=g and
A11: for m being Nat st n <= m & m<=len f & mid(f,m,(m-'1)+len g)=g
holds m >= k0;
reconsider k0 as Element of NAT by ORDINAL1:def 12;
0+1<=k0 by A6,A8,NAT_1:13;
then
A12: k0-'1=k0-1 by XREAL_0:def 2,XREAL_1:48;
k0-1<k0+1-1 by XREAL_1:9,XREAL_1:29;
then k0-'1<len f by A9,A12,XXREAL_0:2;
then
A13: len (f/^(k0-'1))=len f -(k0-'1) by RFINSEQ:def 1;
len f -k0>=0 by A9,XREAL_1:48;
then
A14: len f -k0 +1 >=0+1 by XREAL_1:7;
A15: 1-'1=1-1 by XREAL_0:def 2;
A16: 0+1<=len g by A3,NAT_1:13;
then
A17: k0-'1+1<=k0-'1 + len g by XREAL_1:7;
A18: len g-1>=0 by A16,XREAL_1:48;
then -1+len g +k0-k0>=0;
then
A19: ((k0-'1)+len g)-'k0+1 =len g-1+1 by A12,XREAL_0:def 2
.=len g-'1+ 1 by A18,XREAL_0:def 2;
mid(f/^(k0-'1),1,len g)=((f/^(k0-'1))/^(1-'1))|(len g-'1+1)
by A5,FINSEQ_6:def 3
.=(f/^(k0-'1))|(((k0-'1)+len g)-'k0+1) by A15,A19,FINSEQ_5:28
.=mid(f,k0,(k0-'1)+len g) by A12,A17,FINSEQ_6:def 3;
then
A20: g is_preposition_of f/^(k0-'1) by A10,A12,A13,A14;
for j being Element of NAT st j >= n & j > 0 &
g is_preposition_of f/^(j-'1) holds j >= k0
proof
let j be Element of NAT;
assume that
A21: j >= n and
A22: j > 0 and
A23: g is_preposition_of f/^(j-'1);
A24: mid(f/^(j-'1),1, len g)=g by A3,A23;
now per cases;
case
A25: j<=len f;
0+1<=j by A22,NAT_1:13;
then
A26: j-'1=j-1 by XREAL_0:def 2,XREAL_1:48;
-1+len g +j-j>=0 by A18;
then
A27: ((j-'1)+len g)-'j+1 =len g-1+1 by A26,XREAL_0:def 2
.=len g-'1+1 by A18,XREAL_0:def 2;
A28: j-'1+1<=j-'1 + len g by A16,XREAL_1:7;
mid(f/^(j-'1),1,len g)=((f/^(j-'1))/^(1-'1))|(len g-'1+1
) by A5,FINSEQ_6:def 3
.=(f/^(j-'1))|(((j-'1)+len g)-'j+1) by A15,A27,FINSEQ_5:28
.=mid(f,j,(j-'1)+len g) by A26,A28,FINSEQ_6:def 3;
hence thesis by A11,A21,A24,A25;
end;
case j>len f;
hence thesis by A9,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis by A6,A8,A20;
end;
case
A29: n=0;
then
A30: g is_substring_of f,1 by A2,Th20;
reconsider n2=1 as Element of NAT;
defpred P[Nat] means n2 <= $1 &
$1 <=len f & mid(f,$1,($1-'1)+len g)=g;
A32: ex i being Nat st P[i] by A3,A30;
ex k being Nat st P[k] & for m being Nat st P[m]
holds m >= k from NAT_1:sch 5(A32);
then consider k0 being Nat such that
A33: n2 <= k0 and
A34: k0<=len f and
A35: mid(f,k0,(k0-'1)+len g)=g and
A36: for m being Nat st n2 <= m & m<=len f & mid(f,m,(m-'1)+len g)=g
holds m >= k0;
reconsider k0 as Element of NAT by ORDINAL1:def 12;
A37: k0-'1=k0-1 by XREAL_0:def 2,A33,XREAL_1:48;
k0-1<k0+1-1 by XREAL_1:9,XREAL_1:29;
then k0-'1<len f by A34,A37,XXREAL_0:2;
then
A38: len (f/^(k0-'1))=len f -(k0-'1) by RFINSEQ:def 1;
len f -k0>=0 by A34,XREAL_1:48;
then
A39: len f -k0 +1 >=0+1 by XREAL_1:7;
A40: 0+1<=len g by A3,NAT_1:13;
then
A41: k0-'1+1<=k0-'1 + len g by XREAL_1:7;
A42: len g-1>=0 by A40,XREAL_1:48;
then -1+len g +k0-k0>=0;
then
A43: ((k0-'1)+len g)-'k0+1 =len g-1+1 by A37,XREAL_0:def 2
.=len g-'1 +1 by A42,XREAL_0:def 2;
mid(f/^(k0-'1),1,len g)=((f/^(k0-'1))/^(1-'1))|(len g-'1+1)
by A5,FINSEQ_6:def 3
.=(f/^(k0-'1))|(((k0-'1)+len g)-'k0+1) by A1,A43,FINSEQ_5:28
.=mid(f,k0,(k0-'1)+len g) by A37,A41,FINSEQ_6:def 3;
then
A44: g is_preposition_of f/^(k0-'1) by A35,A37,A38,A39;
A45: for j being Element of NAT st j >= n2 & j > 0 &
g is_preposition_of f/^(j-'1) holds j >= k0
proof
let j be Element of NAT;
assume that
A46: j >= n2 and j > 0 and
A47: g is_preposition_of f/^(j-'1);
A48: mid(f/^(j-'1),1, len g)=g by A3,A47;
now per cases;
case
A49: j<=len f;
A50: j-'1=j-1 by XREAL_0:def 2,A46,XREAL_1:48;
-1+len g +j-j>=0 by A42;
then
A51: ((j-'1)+len g)-'j+1 =len g-1+1 by A50,XREAL_0:def 2
.=len g-'1+1 by A42,XREAL_0:def 2;
A52: j-'1+1<=j-'1 + len g by A40,XREAL_1:7;
mid(f/^(j-'1),1,len g)=((f/^(j-'1))/^(1-'1))|(len g-'1+1
) by A5,FINSEQ_6:def 3
.=(f/^(j-'1))|(((j-'1)+len g)-'j+1) by A1,A51,FINSEQ_5:28
.=mid(f,j,(j-'1)+len g) by A50,A52,FINSEQ_6:def 3;
hence thesis by A36,A46,A48,A49;
end;
case j>len f;
hence thesis by A34,XXREAL_0:2;
end;
end;
hence thesis;
end;
for j being Element of NAT st j >= n & j > 0 &
g is_preposition_of f/^(j-'1) holds j >= k0
proof
let j be Element of NAT;
assume that
j >= n and
A53: j > 0 and
A54: g is_preposition_of f/^(j-'1);
j>=0+n2 by A53,NAT_1:13;
hence thesis by A45,A54;
end;
hence thesis by A29,A33,A44;
end;
end;
hence thesis;
end;
case
A55: len g<=0;
reconsider nn=max(n,1) as Element of NAT by ORDINAL1:def 12;
A56: nn>=n by XXREAL_0:25;
A57: nn>=0+1 by XXREAL_0:25;
A58: g is_preposition_of f/^(nn-'1) by A55;
for j being Element of NAT st j >= n & j > 0 &
g is_preposition_of f/^(j-'1) holds j >= nn
proof
let j be Element of NAT;
assume that
A59: j >= n and
A60: j > 0 and g is_preposition_of f/^(j-'1);
j>=0+1 by A60,NAT_1:13;
hence thesis by A59,XXREAL_0:28;
end;
hence thesis by A56,A57,A58;
end;
end;
hence thesis;
end;
case not g is_substring_of f,n;
hence thesis;
end;
end;
hence thesis;
end;
uniqueness
proof
A61: 1-'1=1-1 by XREAL_0:def 2;
thus for k1,k2 being Element of NAT st
(k1 <> 0 implies n <= k1 & g is_preposition_of f/^(k1-'1) &
for j being Element of NAT
st j >= n & j > 0 & g is_preposition_of f/^(j-'1) holds j>=k1)
& (k1 = 0 implies not g is_substring_of f,n )
& (k2 <> 0 implies n <= k2 & g is_preposition_of f/^(k2-'1) &
for j being Element of NAT
st j >= n & j > 0 & g is_preposition_of f/^(j-'1) holds j >= k2)
& (k2 = 0 implies not g is_substring_of f,n ) holds k1 = k2
proof
let k1,k2 be Element of NAT;
assume that
A62: k1 <> 0 implies n <= k1 & g is_preposition_of f/^(k1-'1) & for j being
Element of NAT st j >= n & j > 0 & g is_preposition_of f/^(j-'1) holds j >=
k1 and
A63: k1 = 0 implies not g is_substring_of f,n and
A64: k2 <> 0 implies n <= k2 & g is_preposition_of f/^(k2-'1) & for j
being Element of NAT st j >= n & j > 0 & g is_preposition_of f/^(j-'1) holds
j >= k2 and
A65: k2 = 0 implies not g is_substring_of f,n;
now per cases;
case len g>0;
then
A66: 0+1<=len g by NAT_1:13;
then
A67: len g-1>=0 by XREAL_1:48;
now per cases;
case
A68: k1 <> 0 & k2 <> 0;
then
A69: k2 >= k1 by A62,A64;
k1 >= k2 by A62,A64,A68;
hence thesis by A69,XXREAL_0:1;
end;
case
A70: k1 <> 0 & k2 = 0;
for i being Element of NAT st n <= i & 0 < i holds
not g is_preposition_of f/^(i-'1)
proof
let i be Element of NAT;
assume that
A72: n <= i and
A73: 0 < i;
0+1<=i by A73,NAT_1:13;
then
A74: i-'1=i-1 by XREAL_0:def 2,XREAL_1:48;
-1+len g +i-i>=0 by A67;
then
A75: ((i-'1)+len g)-'i+1 =len g-1+1 by A74,XREAL_0:def 2
.=len g-'1+1 by A67,XREAL_0:def 2;
A76: i-'1+1<=i-'1 + len g by A66,XREAL_1:7;
mid(f/^(i-'1),1,len g)=((f/^(i-'1))/^(1-'1))|(len g-'1+1)
by A66,FINSEQ_6:def 3
.=(f/^(i-'1))|(((i-'1)+len g)-'i+1) by A61,A75,FINSEQ_5:28
.=mid(f,i,(i-'1)+len g) by A74,A76,FINSEQ_6:def 3;
hence thesis by A65,A70,A72,A73,Th27;
end;
hence contradiction by A62,A70;
end;
case
A77: k1 = 0 & k2 <> 0;
for i being Element of NAT st n <= i & 0 < i holds
not g is_preposition_of f/^(i-'1)
proof
let i be Element of NAT;
assume that
A79: n <= i and
A80: 0 < i;
0+1<=i by A80,NAT_1:13;
then
A81: i-'1=i-1 by XREAL_0:def 2,XREAL_1:48;
-1+len g +i-i>=0 by A67;
then
A82: ((i-'1)+len g)-'i+1 =len g-1+1 by A81,XREAL_0:def 2
.=len g-'1+1 by A67,XREAL_0:def 2;
A83: i-'1+1<=i-'1 + len g by A66,XREAL_1:7;
mid(f/^(i-'1),1,len g)=((f/^(i-'1))/^(1-'1))|(len g-'1+1)
by A66,FINSEQ_6:def 3
.=(f/^(i-'1))|(((i-'1)+len g)-'i+1) by A61,A82,FINSEQ_5:28
.=mid(f,i,(i-'1)+len g) by A81,A83,FINSEQ_6:def 3;
hence thesis by A63,A77,A79,A80,Th27;
end;
hence contradiction by A64,A77;
end;
case k1 = 0 & k2 = 0;
hence thesis;
end;
end;
hence thesis;
end;
case
A84: len g<=0;
now per cases;
case
A85: k1 <> 0 & k2 <> 0;
then
A86: k2 >= k1 by A62,A64;
k1 >= k2 by A62,A64,A85;
hence thesis by A86,XXREAL_0:1;
end;
case k1 <> 0 & k2 = 0;
hence contradiction by A65,A84;
end;
case k1=0 & k2 <>0;
hence contradiction by A63,A84;
end;
case k1=0 & k2=0;
hence contradiction by A63,A84;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
end;
definition
let D be non empty set,f,CR be FinSequence of D;
func addcr(f,CR) -> FinSequence of D equals
ovlcon(f,CR);
correctness;
end;
definition
let D be non empty set, r,CR be FinSequence of D;
pred r is_terminated_by CR means
len CR >0 implies len r>=len CR & instr(1,r,CR) = len r + 1 -'len CR;
correctness;
end;
theorem
for D being non empty set,f being FinSequence of D holds f is_terminated_by f
proof
let D be non empty set,f be FinSequence of D;
A1: len f + 1 -'len f=len f+1-len f by XREAL_0:def 2;
1-'1=0+1-'1 .=0 by NAT_D:34;
then
A2: f/^(1-'1)=f by FINSEQ_5:28;
for j being Element of NAT st j >= 1 & j > 0
& f is_preposition_of f/^(j-'1) holds j >= 1;
hence thesis by A1,A2,Def10;
end;
theorem
for f being FinSequence, k1,k2 being Nat st
k1 in dom f & k2 in dom f holds smid(f,k1,k2) = (k1,k2)-cut f
proof
let f be FinSequence, k1,k2 be Nat;
set ff = (k1,k2)-cut f;
set g = smid(f,k1,k2);
reconsider af = f as FinSequence of rng f by FINSEQ_1:def 4;
assume k1 in dom f & k2 in dom f; then
S0: 1 <= k1 <= len f & 1 <= k2 <= len f by FINSEQ_3:25;
per cases;
suppose A0: k1 <= k2; then
WW: smid(f,k1,k2) = mid(f,k1,k2) by Th4;
len ff + k1 = k2 + 1 by A0,S0,FINSEQ_6:def 4; then
S2: len ff = k2 + 1 - k1 .= k2 + 1 -' k1 by A0,NAT_D:37;
k2 <= k2+1 by NAT_1:13; then
W4: k2+1-k1 = k2+1-'k1 by XREAL_1:233,A0,XXREAL_0:2;
k1-'1 <= k1 by NAT_D:35; then
k1-'1 <= len f by XXREAL_0:2,S0; then
S3: len (f/^(k1-'1)) = len f - (k1-'1) by RFINSEQ:def 1;
W3: len f - (k1-'1) = len f - (k1-1) by S0,XREAL_1:233
.= len f + 1 - k1;
k2+1 <= len f + 1 by S0,XREAL_1:6; then
k2+1-'k1 <= len (f/^(k1-'1)) by S3,W3,W4,XREAL_1:9; then
A1: len ff = len g by S2,FINSEQ_1:59;
for k being Nat st 1 <= k <= len ff holds ff.k = g.k
proof
let k be Nat;
assume Z0: 1 <= k <= len ff; then
ZZ: k-'1 + 1 = k by XREAL_1:235;
k-'1 < len ff
proof
per cases by Z0,XXREAL_0:1;
suppose k > 1; then
1 <= k-'1 by NAT_D:49; then
k-'1 < k by NAT_D:51;
hence thesis by Z0,XXREAL_0:2;
end;
suppose k = 1; then
k-'1 < k by NAT_D:51;
hence thesis by Z0,XXREAL_0:2;
end;
end; then
Z2: ff.k = f.(k1+(k-'1)) by ZZ,FINSEQ_6:def 4,A0,S0;
P1: k <= len mid (af,k1,k2) by WW,A1,Z0;
k1+k >= k by NAT_1:11; then
P2: 1 <= k1+k by XXREAL_0:2,Z0;
g.k = mid(f,k1,k2).k by Th4,A0
.= af.(k+k1-'1) by Z0,FINSEQ_6:118,A0,P1,S0
.= af.(k1+k-1) by P2,XREAL_1:233
.= af.(k1+(k-1))
.= af.(k1+(k-'1)) by Z0,XREAL_1:233;
hence thesis by Z2;
end;
hence thesis by A1;
end;
suppose A1: k1 > k2; then
(k1,k2)-cut f = {} by FINSEQ_6:def 4;
hence thesis by A1,Th7;
end;
end;