:: A Theory of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005-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 NUMBERS, XBOOLE_0, FINSEQ_1, ORDINAL4, RELAT_1, CARD_1, SUBSET_1,
XXREAL_0, RFINSEQ, ARYTM_1, ARYTM_3, JORDAN3, FUNCT_1, FINSEQ_5, NAT_1,
PARTFUN1, FINSEQ_8, FILEREC1;
notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
NAT_D, RELAT_1, RFINSEQ, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4,
FINSEQ_6, FINSEQ_5, FINSEQ_8;
constructors NAT_1, RFINSEQ, NAT_D, FINSEQ_4, FINSEQ_5, CQC_LANG, FINSEQ_6,
FINSEQ_8, REAL_1, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, FINSEQ_1,
FINSEQ_5, ORDINAL1, CARD_1, NAT_1;
requirements NUMERALS, REAL, SUBSET, ARITHM;
theorems NAT_1, NAT_2, REVROT_1, FINSEQ_1, FINSEQ_2, FINSEQ_5,
FINSEQ_6, RFINSEQ, FUNCT_2, FINSEQ_8, GENEALG1, CALCUL_1, FINSEQ_3,
XREAL_1, CARD_1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D;
begin
reserve a,b,c for set;
theorem Th1:
for p,q,r,s being FinSequence holds
p^q^r^s=p^(q^r)^s & p^q^r^s=(p^q)^(r^s) & p^(q^r)^s=(p^q)^(r^s)
proof
let p,q,r,s be FinSequence;
p^q^r^s=(p^q)^(r^s) by FINSEQ_1:32;
hence thesis by FINSEQ_1:32;
end;
theorem Th2:
for f being FinSequence holds f|(len f) = f
proof
let f be FinSequence;
f|len f = f|(Seg len f) by FINSEQ_1:def 16;
hence thesis by FINSEQ_2:20;
end;
theorem Th3:
for p,q being FinSequence st len p = 0 holds q = p ^ q
proof
let p,q be FinSequence;
assume len p = 0;
then p = {};
hence thesis by FINSEQ_1:34;
end;
theorem Th4:
for D being non empty set,f being FinSequence of D, n,m being
Element of NAT st n<=m holds len (f/^m)<=len (f/^n)
proof
let D be non empty set,f be FinSequence of D,n,m be Element of NAT;
A1: len (f/^m) = len f -' m by RFINSEQ:29;
assume
A2: n<=m;
then
A3: n-n<=m-n by XREAL_1:9;
now
per cases;
suppose
A4: len f <= n;
then len f -' n - (len f -' m) = len f -' n - 0 by A2,NAT_2:8,XXREAL_0:2
.= 0 by A4,NAT_2:8;
hence len (f/^n) - len (f/^m) >= 0 by A1,RFINSEQ:29;
end;
suppose
A5: len f > n;
per cases;
suppose
len f <= m;
then len f -' n - (len f -' m) = len f -' n - 0 by NAT_2:8
.= len f -' n;
hence len (f/^n) - len (f/^m) >= 0 by A1;
end;
suppose
len f > m;
then len f-'n-(len f-'m)= len f-'n-(len f-m) by XREAL_1:233
.= len f-n-(len f-m) by A5,XREAL_1:233
.= m-n;
hence len (f/^n) - len (f/^m) >= 0 by A3,A1,RFINSEQ:29;
end;
end;
end;
then len (f/^n) - len (f/^m) + len (f/^m) >= 0 + len (f/^m) by XREAL_1:6;
hence thesis;
end;
theorem Th5:
for D being non empty set,f,g being FinSequence of D st len g>=1
holds mid(f^g,len f+1,len f+len g)=g
proof
let D be non empty set,f,g be FinSequence of D;
assume
A1: len g>=1;
A2: g|len g=g|(Seg len g) by FINSEQ_1:def 16;
per cases;
suppose
A3: len f+1<=len f+len g;
then
A4: len f < len f+len g by NAT_1:13;
then len f-len f < len f+len g-len f by XREAL_1:14;
then
A5: len f+len g-'len f=len g by XREAL_0:def 2;
mid(f^g,len f+1,len f+len g)=((f^g)/^(len f+1-'1))|(len f+len g-'(len
f+1) + 1 ) by A3,FINSEQ_6:def 3
.=((f^g)/^len f)|(len f+len g-'(len f+1)+1) by NAT_D:34
.=((f^g)/^len f)|(len f+len g-'len f) by A4,NAT_2:7
.=g|len g by A5;
hence thesis by A2,FINSEQ_2:20;
end;
suppose
len f+1>len f+len g;
then len f+1-len f>len f+len g-len f by XREAL_1:14;
hence thesis by A1;
end;
end;
theorem Th6:
for D being non empty set,f,g being FinSequence of D, i,j being
Element of NAT st 1<=i & i<=j & j<=len f holds mid(f^g,i,j)=mid(f,i,j)
proof
let D be non empty set,f,g be FinSequence of D,i,j be Element of NAT;
assume that
A1: 1<=i and
A2: i<=j and
A3: j<=len f;
A4: len (f/^(i-'1))+(i-1)-(i-1)=len (f/^(i-'1));
len f>=i by A2,A3,XXREAL_0:2;
then len f-0 >=i-1 by XREAL_1:13;
then
A5: len f >=i-'1 by A1,XREAL_1:233;
len (f/^(i-'1))+(i-'1)=len f-'(i-'1)+(i-'1) by RFINSEQ:29
.=len f by A5,XREAL_1:235;
then
A6: len (f/^(i-'1))=len f-(i-1) by A1,A4,XREAL_1:233
.=len f-i+1;
len f-i>=j-i by A3,XREAL_1:9;
then
A7: len f-i+1>=j-i+1 by XREAL_1:6;
j-i>=i-i by A2,XREAL_1:9;
then
A8: len (f/^(i-'1))>=j-'i+1 by A7,A6,XREAL_0:def 2;
A9: i-'1<=i & i<=len f by A2,A3,NAT_D:35,XXREAL_0:2;
mid(f^g,i,j) = ((f^g)/^(i-'1))|(j-'i+1) by A2,FINSEQ_6:def 3
.= ((f/^(i-'1))^g)|(j-'i+1) by A9,GENEALG1:1,XXREAL_0:2
.= (f/^(i-'1))|(j-'i+1) by A8,FINSEQ_5:22;
hence thesis by A2,FINSEQ_6:def 3;
end;
theorem
for D being non empty set,f being FinSequence of D, i,j,n being
Element of NAT st 1<=i & i<=j & i<=len (f|n) & j<=len (f|n) holds mid(f,i,j)=
mid(f|n,i,j)
proof
let D be non empty set,f be FinSequence of D,i,j,n be Element of NAT;
assume that
A1: 1<=i and
A2: i<=j and
A3: i<=len (f|n) and
A4: j<=len (f|n);
A5: j-'i+1 = j-i+1 by A2,XREAL_1:233;
A6: len (f|n) <= n by FINSEQ_5:17;
then n>=i by A3,XXREAL_0:2;
then
A7: n-0>=i-1 by XREAL_1:13;
j<=n by A4,A6,XXREAL_0:2;
then j-i <= n-i by XREAL_1:9;
then
A8: j-i+1<=n-i+1 by XREAL_1:6;
i-'1 = i-1 by A1,XREAL_1:233;
then
A9: n-'(i-'1) = n-(i-1) by A7,XREAL_1:233
.= n-i+1;
mid(f|n,i,j)= ((f|n)/^(i-'1))|(j-'i+1) by A2,FINSEQ_6:def 3
.= ((f/^(i-'1))|(n-'(i-'1)))|(j-'i+1) by FINSEQ_5:80
.= (f/^(i-'1))|(j-'i+1) by A9,A5,A8,FINSEQ_5:77;
hence thesis by A2,FINSEQ_6:def 3;
end;
theorem
for D being non empty set,f being FinSequence of D st f=<*a*> holds a in D
proof
let D be non empty set,f be FinSequence of D;
A1: f is Function of dom f,D by FINSEQ_2:26;
assume
A2: f=<*a*>;
then 1<=len f by FINSEQ_1:40;
then
A3: 1 in dom f by FINSEQ_3:25;
f.1=a by A2;
hence thesis by A3,A1,FUNCT_2:5;
end;
theorem
for D being non empty set,f being FinSequence of D st f=<*a,b*> holds
a in D & b in D
proof
let D be non empty set,f be FinSequence of D;
A1: f is Function of dom f,D by FINSEQ_2:26;
assume
A2: f=<*a,b*>;
then
A3: 1 in dom f & 2 in dom f by CALCUL_1:14;
f.1=a & f.2=b by A2;
hence thesis by A3,A1,FUNCT_2:5;
end;
theorem Th10:
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds a in D & b in D & c in D
proof
let D be non empty set,f be FinSequence of D;
A1: f is Function of dom f,D by FINSEQ_2:26;
assume
A2: f=<*a,b,c*>;
then
A3: f.3=c & 1 in dom f by FINSEQ_1:81;
A4: 2 in dom f & 3 in dom f by A2,FINSEQ_1:81;
f.1=a & f.2=b by A2;
hence thesis by A3,A4,A1,FUNCT_2:5;
end;
theorem
for f being FinSequence st f=<*a*> holds f|1=<*a*>
proof
let f be FinSequence;
assume
A1: f=<*a*>;
then len f <=1 by FINSEQ_1:40;
hence thesis by A1,FINSEQ_1:58;
end;
theorem :: FINSEQ_6:50
for D being non empty set,f being FinSequence of D st f=<*a,b*> holds
f/^1=<*b*>
proof
let D be non empty set,f be FinSequence of D;
A1: f is Function of (dom f),D by FINSEQ_2:26;
assume
A2: f = <*a,b*>;
then
A3: 1 in dom f & 2 in dom f by CALCUL_1:14;
f.1=a & f.2=b by A2;
then reconsider a2=a, b2=b as Element of D by A3,A1,FUNCT_2:5;
f/^1 = <*a2,b2*>/^1 by A2
.= <*b2*> by FINSEQ_6:46;
hence thesis;
end;
theorem
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds f|1=<*a*>
proof
let D be non empty set,f be FinSequence of D;
assume
A1: f=<*a,b,c*>;
f|1 = f|Seg 1 by FINSEQ_1:def 16
.= <*a*> by A1,FINSEQ_6:4;
hence thesis;
end;
theorem Th14:
for D being non empty set,f being FinSequence of D st f=<*a,b,c
*> holds f|2=<*a,b*>
proof
let D be non empty set,f be FinSequence of D;
assume
A1: f=<*a,b,c*>;
f|2 = f|Seg 2 by FINSEQ_1:def 16
.= <*a,b*> by A1,FINSEQ_6:5;
hence thesis;
end;
theorem
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds f/^1=<*b,c*>
proof
let D be non empty set,f be FinSequence of D;
assume
A1: f = <*a,b,c*>;
then reconsider a2=a,b2=b,c2=c as Element of D by Th10;
A2: f.3=c2 by A1;
f.1=a2 & f.2=b2 by A1;
hence thesis by A1,A2,FINSEQ_6:47;
end;
theorem
for D being non empty set,f being FinSequence of D st f=<*a,b,c*>
holds f/^2=<*c*>
proof
let D be non empty set,f be FinSequence of D;
assume
A1: f = <*a,b,c*>;
then reconsider a2=a,b2=b,c2=c as Element of D by Th10;
f/^2 = (<*a2*>^<*b2,c2*>)/^(1+1) by A1,FINSEQ_1:43
.= (<*a2*>^<*b2,c2*>)/^(len <*a2*> +1) by FINSEQ_1:40
.= <*b2,c2*>/^1 by FINSEQ_5:36
.= <*c2*> by FINSEQ_6:46;
hence thesis;
end;
theorem
for f being FinSequence st len f=0 holds Rev f=f
proof
let f be FinSequence;
assume len f=0;
then f = {};
hence thesis;
end;
theorem Th18:
for D being non empty set, r being FinSequence of D,i being
Element of NAT st i<=len r holds Rev(r/^i)=(Rev r)|(len r-'i)
proof
let D be non empty set,r be FinSequence of D,i be Element of NAT;
set s=Rev r;
len r-'i<=len r by NAT_D:50;
then len r-'i<=len s by FINSEQ_5:def 3;
then
A1: len s-'i <= len s by FINSEQ_5:def 3;
A2: len (s|((len r)-'i)) = len (s|((len s)-'i)) by FINSEQ_5:def 3
.= len s -'i by A1,FINSEQ_1:59;
assume
A3: i<=len r;
then len r -i>=0 by XREAL_1:48;
then
A4: len r-i=len r -'i by XREAL_0:def 2;
A5: for k being Nat st 1<=k & k<=len Rev(r/^i) holds (Rev(r/^i)).k= (s|((len
r)-'i)).k
proof
let k be Nat;
assume that
A6: 1<=k and
A7: k<=len Rev(r/^i);
k in dom Rev(r/^i) by A6,A7,FINSEQ_3:25;
then
A8: (Rev(r/^i)).k = (r/^i).(len (r/^i) -k+1) by FINSEQ_5:def 3
.=(r/^i).(len r -i-k+1) by A3,RFINSEQ:def 1;
len r+0<=len r +i by XREAL_1:7;
then len r-i<=len r+i-i by XREAL_1:9;
then len (r/^i)<=len r by A3,RFINSEQ:def 1;
then len (Rev(r/^i))<=len r by FINSEQ_5:def 3;
then
A9: k<=len r by A7,XXREAL_0:2;
then
A10: len r-k>=0 by XREAL_1:48;
then
A11: len r-k=len r-'k by XREAL_0:def 2;
k-1>=0 by A6,XREAL_1:48;
then len r+0<=len r+(k-1) by XREAL_1:7;
then len r-(k-1)<=len r+(k-1)-(k-1) by XREAL_1:9;
then len r-k+1<=len r;
then
A12: len r-'k+1<=len r by A10,XREAL_0:def 2;
len r-k+1>=0+1 by A11,NAT_1:13;
then
A13: len r-k+1 in dom r by A11,A12,FINSEQ_3:25;
k in dom r by A6,A9,FINSEQ_3:25;
then
A15: k in dom Rev r by FINSEQ_5:57;
k<=len (r/^i) by A7,FINSEQ_5:def 3;
then
A16: k<=len r -i by A3,RFINSEQ:def 1;
then
A17: len r-'i-k>=0 by A4,XREAL_1:48;
then
A18: len r -'i-'k=len r-'i-k by XREAL_0:def 2;
k<=len r-'i by A16,XREAL_0:def 2;
then
A19: (s|((len r)-'i)).k=(Rev r).k by FINSEQ_3:112
.=r.(len r-k+1) by A15,FINSEQ_5:def 3;
A20: i+(len r -'i-'k+1)=i+(len r-i-k+1) by A4,A17,XREAL_0:def 2
.=len r-i+i-k+1;
k-1>=0 by A6,XREAL_1:48;
then len r-i+0<=len r-i+(k-1) by XREAL_1:7;
then len r-i-(k-1)<=len r-i+(k-1)-(k-1) by XREAL_1:9;
then len r -'i-'k +1>=0+1 & len r-'i-'k+1<=len (r/^i) by A3,A4,A18,
RFINSEQ:def 1,XREAL_1:7;
then len r -i-k+1 in Seg len (r/^i) by A4,A18,FINSEQ_1:1;
then
A21: len r -i-k+1 in dom (r/^i) by FINSEQ_1:def 3;
then (r/^i).(len r -i-k+1) = (r/^i)/.(len r -'i-'k+1) by A4,A18,
PARTFUN1:def 6
.=(r/^0) /. (i+(len r -'i-'k+1)) by A4,A18,A21,FINSEQ_5:27
.=r.(len r-k+1) by A20,A13,PARTFUN1:def 6;
hence thesis by A8,A19;
end;
len Rev(r/^i)= len (r/^i) by FINSEQ_5:def 3
.=len r-'i by RFINSEQ:29
.=len (s|((len r)-'i)) by A2,FINSEQ_5:def 3;
hence thesis by A5,FINSEQ_1:14;
end;
theorem Th19:
for D being non empty set,f,CR being FinSequence of D st not CR
is_substring_of f,1 & CR separates_uniquely holds instr(1,f^CR,CR)=len f +1
proof
let D be non empty set,f,CR be FinSequence of D;
assume that
A1: not CR is_substring_of f,1 and
A2: CR separates_uniquely;
A3: len CR>0 by A1,FINSEQ_8:def 7;
then
A4: len CR>=0+1 by NAT_1:13;
A5: for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (f^
CR)/^(j-'1) holds j >= len f+1
proof
set i0=len f+1,j0=i0+len CR -'1;
let j be Element of NAT;
assume that
A6: j >= 1 and
j > 0 and
A7: CR is_preposition_of (f^CR)/^(j-'1);
A8: len CR>0 implies 1<=len ((f^CR)/^(j-'1)) & mid((f^CR)/^(j-'1),1,len CR
)=CR by A7,FINSEQ_8:def 8;
A9: 0+j<len CR +j by A3,XREAL_1:8;
then j+1<=len CR+j by NAT_1:13;
then
A10: j<=len CR+j-1 by XREAL_1:19;
1<=len CR +j by A6,A9,XXREAL_0:2;
then
A11: len CR +j -1>=0 by XREAL_1:48;
then
A12: len CR+j-'1=len CR+j-1 by XREAL_0:def 2;
len CR-1>=0 by A4,XREAL_1:48;
then ((len CR+j-'1)-'j+1)=len CR+j-1-j+1 by A12,XREAL_0:def 2
.=len CR;
then
A13: ((f^CR)/^(j-'1))|((len CR+j-'1)-'j+1)=CR by A4,A8,FINSEQ_6:116;
j+len CR-1>=0 by A6,NAT_1:12,XREAL_1:48;
then
A14: j+len CR-'1=j+len CR-1 by XREAL_0:def 2;
A15: i0+len CR-'1=len f+len CR+1-'1 .=len f+len CR by NAT_D:34;
j0= len CR+len f +1-'1 .=len CR+len f by NAT_D:34;
then mid(f^CR,i0,i0+len CR-'1)=CR by A4,Th5;
then
A16: smid(f^CR,i0,i0+len CR-'1)=CR by A4,A15,FINSEQ_8:4,XREAL_1:7;
A17: len CR>0 implies len CR>=0+1 by NAT_1:13;
then j+len CR>=j+1 by A1,FINSEQ_8:def 7,XREAL_1:7;
then
A18: j+len CR-1>=j+1-1 by XREAL_1:9;
j+len CR>=j+1 by A1,A17,FINSEQ_8:def 7,XREAL_1:7;
then
A19: j+len CR-1>=j+1-1 by XREAL_1:9;
A20: j-1>=0 by A6,XREAL_1:48;
then
A21: j-'1=j-1 by XREAL_0:def 2;
j-'1+len CR=j-1+len CR by A20,XREAL_0:def 2
.=len CR+j-'1 by A11,XREAL_0:def 2;
then
A22: mid(f^CR,j,j-'1+len CR)=CR by A10,A12,A13,FINSEQ_6:def 3;
j-'1+len CR=j-1+len CR by A20,XREAL_0:def 2
.=j+len CR -1;
then
A23: smid(f^CR,j,j+len CR-'1)=CR by A14,A19,A22,FINSEQ_8:4;
now
assume
A24: j<i0;
then i0-j>0 by XREAL_1:50;
then
A25: i0-'j =len f+1-j by XREAL_0:def 2;
i0+len CR-'1<=len (f^CR) by A15,FINSEQ_1:22;
then i0-'j>=len CR by A2,A6,A16,A23,A24,FINSEQ_8:def 6;
then len f+1-j+j>=len CR+j by A25,XREAL_1:7;
then len f+1-1>=j+len CR-1 by XREAL_1:9;
then mid(f,j,(j-'1)+len CR)=CR by A6,A21,A18,A22,Th6;
then j>len f by A1,A6,FINSEQ_8:def 7;
hence contradiction by A24,NAT_1:13;
end;
hence thesis;
end;
(f^CR)/^(len f)=CR;
then
len f+1 <> 0 implies 1 <= len f+1 & CR is_preposition_of (f^CR)/^(len f
+1-'1) & for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of (
f^CR)/^(j-'1) holds j >= len f+1 by A5,NAT_1:11,NAT_D:34;
hence thesis by FINSEQ_8:def 10;
end;
theorem
for D being non empty set,f,CR being FinSequence of D st not CR
is_substring_of f,1 & CR separates_uniquely holds f^CR is_terminated_by CR
proof
let D be non empty set,f,CR be FinSequence of D;
A1: len (f^CR) + 1 -'len CR=len f+len CR +1-'len CR by FINSEQ_1:22
.=len CR+(len f+1)-'len CR
.=len f+1 by NAT_D:34;
len CR<=len f+len CR by NAT_1:12;
then
A2: len CR <=len (f^CR) by FINSEQ_1:22;
assume ( not CR is_substring_of f,1)& CR separates_uniquely;
then instr(1,f^CR,CR)=len (f^CR) + 1 -'len CR by A1,Th19;
hence thesis by A2,FINSEQ_8:def 12;
end;
::==========================================================================
:: file and record
::==========================================================================
notation
let D be set;
synonym File of D for FinSequence of D;
end;
definition
let D be non empty set, r,f,CR be File of D;
pred r is_a_record_of f,CR means
(CR^r is_substring_of addcr(f,CR),1
or r is_preposition_of addcr(f,CR)) & r is_terminated_by CR;
end;
theorem Th21:
for D being non empty set,r being FinSequence of D holds ovlpart
(<*>D,r)=<*>D & ovlpart(r,<*>D)=<*>D
proof
let D be non empty set,r be FinSequence of D;
<*>D^r=r & r^<*>D=r by FINSEQ_1:34;
hence thesis by FINSEQ_8:14;
end;
theorem Th22:
for D being non empty set,CR being FinSequence of D holds CR
is_a_record_of <*>D,CR
proof
let D be non empty set,CR be FinSequence of D;
A1: CR is_terminated_by CR by FINSEQ_8:28;
addcr(<*>D,CR)=ovlcon(<*>D,CR) by FINSEQ_8:def 11
.=<*>D^(CR/^(len ovlpart(<*>D,CR))) by FINSEQ_8:def 3
.=<*>D^(CR/^(len <*>D)) by Th21
.=<*>D^(CR/^0)
.=(CR/^0) by FINSEQ_1:34
.=CR;
hence thesis by A1;
end;
theorem
for D being non empty set,a,b be set,f,r,CR being File of D st a <> b
& CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds CR is_a_record_of f,CR & r
is_a_record_of f,CR
proof
let D be non empty set,a,b be set,f,r,CR be File of D;
assume that
A1: a <> b and
A2: CR = <*b*> and
A3: f = <*b,a,b*> and
A4: r = <*a,b*>;
reconsider b2=b,a2=a as Element of D by A3,Th10;
A5: CR.1=b & len CR=1 by A2,FINSEQ_1:40;
f =<*b,a*>^<*b*> by A3,FINSEQ_1:43
.=(f|2)^CR by A2,A3,Th14;
then ovlpart(f,CR)=CR by FINSEQ_8:14;
then CR/^(len ovlpart(f,CR))={} by FINSEQ_6:167;
then f^(CR/^(len ovlpart(f,CR)))=f by FINSEQ_1:34;
then
A6: ovlcon(f,CR)=f by FINSEQ_8:def 3;
A7: f=CR^r by A2,A3,A4,FINSEQ_1:43;
then
A8: len f = len CR + len r by FINSEQ_1:22
.= 1 + len <*a,b*> by A2,A4,FINSEQ_1:40
.= 1 + 2 by FINSEQ_1:44
.= 3;
then CR^r is_substring_of f,1 by A7,FINSEQ_8:19;
then
A9: CR^r is_substring_of addcr(f,CR),1 by A6,FINSEQ_8:def 11;
A10: len CR = 1 by A2,FINSEQ_1:40;
then mid(f,1,len CR) = (f/^(1-'1))|(1-'1+1) by FINSEQ_6:def 3
.= (f/^(1-'1))|(1+(0)) by NAT_2:8
.= (f/^(0))|1 by NAT_D:34
.= (f)|1
.= (<*b2,a2,b2*>)|Seg 1 by A3,FINSEQ_1:def 16
.= CR by A2,FINSEQ_6:4;
then CR is_preposition_of f by A8,FINSEQ_8:def 8;
then
A11: CR is_preposition_of addcr(f,CR) by A6,FINSEQ_8:def 11;
r/^(1-'1)=r/^(0+1-'1) .=r/^0 by NAT_D:34
.=r;
then (r/^(1-'1)).1=a by A4;
then
A12: not CR is_preposition_of (r/^(1-'1)) by A1,A5,FINSEQ_8:21;
A13: for j being Element of NAT st j >= 1 & j > 0 & CR is_preposition_of r/^
(j-'1) holds j >= 2
proof
let j be Element of NAT;
assume that
A14: j >= 1 and
j > 0 and
A15: CR is_preposition_of r/^(j-'1);
j>1 by A12,A14,A15,XXREAL_0:1;
then 1+1<=j by NAT_1:13;
hence thesis;
end;
r/^(2-'1) = r/^(1+1-'1) .= <*a2,b2*>/^1 by A4,NAT_D:34
.= CR by A2,FINSEQ_6:46;
then
A16: instr(1,r,CR) = 2 by A13,FINSEQ_8:def 10;
A17: len r = 2 by A4,FINSEQ_1:44;
then len r + 1 -' len CR = 2 by A10,NAT_D:34;
then CR is_terminated_by CR & r is_terminated_by CR by A10,A17,A16,
FINSEQ_8:28,def 12;
hence thesis by A11,A9;
end;
theorem Th24:
for D being non empty set,f,CR being File of D holds f is_preposition_of f^CR
proof
let D be non empty set,f,CR be File of D;
per cases;
suppose
A1: len f>0;
0+1<= len f + len CR by A1,NAT_1:13;
then
A2: 1<= len (f^CR) by FINSEQ_1:22;
0+1<= len f by A1,NAT_1:13;
then mid(f^CR,1,len f)=f by FINSEQ_8:1;
hence thesis by A2,FINSEQ_8:def 8;
end;
suppose
len f<=0;
hence thesis by FINSEQ_8:def 8;
end;
end;
theorem
for D being non empty set,f,CR being File of D holds f
is_preposition_of addcr(f,CR)
proof
let D be non empty set,f,CR be File of D;
addcr(f,CR)=ovlcon(f,CR) by FINSEQ_8:def 11
.=f^(CR/^(len ovlpart(f,CR))) by FINSEQ_8:def 3;
hence thesis by Th24;
end;
theorem Th26:
for D being non empty set,r,CR being File of D st CR
is_postposition_of r holds 0<=len r-len CR
proof
let D be non empty set,f,g be File of D;
assume g is_postposition_of f;
then len g <= len f by FINSEQ_8:23;
then len g - len g <= len f - len g by XREAL_1:9;
hence thesis;
end;
theorem Th27:
for D being non empty set,CR,r being File of D st CR
is_postposition_of r holds r=addcr(r,CR)
proof
let D be non empty set,CR,r be File of D;
A1: len r = len Rev r by FINSEQ_5:def 3;
assume
A2: CR is_postposition_of r;
then
A3: len CR = len Rev CR & Rev CR is_preposition_of Rev r by FINSEQ_5:def 3
,FINSEQ_8:def 9;
0<=len r - len CR by A2,Th26;
then
A4: 0+len CR<=len r-len CR+len CR by XREAL_1:7;
per cases;
suppose
A5: len CR>0;
then Rev mid(Rev r,1,len CR)=Rev Rev CR by A3,FINSEQ_8:def 8;
then
A6: mid(Rev r,len CR,1)=Rev Rev CR by FINSEQ_6:196
.=CR;
A7: len Rev r = len Rev r - len CR +len CR;
A8: mid(r,(len r+1) -' len CR,len r)=CR & len CR >=0+1 by A2,A5,FINSEQ_8:24
,NAT_1:13;
now
per cases;
case
A9: len CR>1;
then len CR>=1+1 by NAT_1:13;
then len CR-1>=1+1-1 by XREAL_1:9;
then
A10: len CR-'1+1=len CR by NAT_D:43;
A11: len Rev r -'len CR=len Rev r -len CR by A1,A4,XREAL_1:233;
mid(Rev r,len CR,1)=Rev (((Rev r)/^(1-'1))|(len CR-'1+1)) by A9,
FINSEQ_6:def 3
.=Rev (((Rev r)/^0)|len CR) by A10,NAT_2:8
.=Rev (Rev r|len CR)
.=Rev (Rev r)/^(len (Rev r)-'len CR) by A7,A11,FINSEQ_6:85
.=r/^(len r-'len CR) by A1;
then
A12: ovlpart(r,CR) = ovlpart((r|(len r-'len CR))^CR,CR) by A6,RFINSEQ:8
.= CR by FINSEQ_8:14;
ovlcon(r,CR)=r^(CR/^(len ovlpart(r,CR))) by FINSEQ_8:def 3
.=r^{} by A12,FINSEQ_6:167
.=r by FINSEQ_1:34;
hence thesis by FINSEQ_8:def 11;
end;
case
len CR<=1;
then CR=mid(r,(len r+1) -'1,len r) by A8,XXREAL_0:1
.=mid(r,len r,len r) by NAT_D:34
.=r/^(len r-'1) by FINSEQ_6:117;
then
A13: r=(r|(len r-'1))^CR by RFINSEQ:8;
A14: CR/^len CR={} by FINSEQ_6:167;
ovlcon(r,CR)=r^(CR/^(len ovlpart(r,CR))) by FINSEQ_8:def 3
.=r^(CR/^len CR) by A13,FINSEQ_8:14
.=r by A14,FINSEQ_1:34;
hence thesis by FINSEQ_8:def 11;
end;
end;
hence thesis;
end;
suppose
len CR<= 0;
then
A15: CR={};
then
A16: len ovlpart(r,CR)=len <*>D by Th21
.=0;
thus addcr(r,CR)=ovlcon(r,CR) by FINSEQ_8:def 11
.=r^(CR/^(len ovlpart(r,CR))) by FINSEQ_8:def 3
.=r^CR by A16
.=r by A15,FINSEQ_1:34;
end;
end;
theorem Th28:
for D being non empty set,CR,r being File of D st
r is_terminated_by CR holds r=addcr(r,CR)
proof
let D be non empty set,CR,r be File of D;
assume
A1: r is_terminated_by CR;
per cases;
suppose
len CR<=0;
then len CR=0;
then len Rev CR=0 by FINSEQ_5:def 3;
then Rev CR is_preposition_of Rev r by FINSEQ_8:def 8;
then CR is_postposition_of r by FINSEQ_8:def 9;
hence thesis by Th27;
end;
suppose
A2: len CR>0;
then 0<len r by A1,FINSEQ_8:def 12;
then 0+1<=len r by NAT_1:13;
then
A3: 1<=len Rev r by FINSEQ_5:def 3;
A4: 0+1<=len CR by A2,NAT_1:13;
then len CR -1>=0 by XREAL_1:48;
then
A5: len CR -'1=len CR -1 by XREAL_0:def 2;
A6: len r>=len CR by A1,FINSEQ_8:def 12;
then len r +1>len CR by NAT_1:13;
then
A7: len r+1-len CR>0 by XREAL_1:50;
then
A8: len r+1-'len CR=len r+1-len CR by XREAL_0:def 2;
A9: len r-len CR>=0 by A6,XREAL_1:48;
then
A10: len r-len CR=len r-'len CR by XREAL_0:def 2;
then
A11: len (r/^(len r -'len CR))=len r-'(len r -'len CR) & len r-(len r -'
len CR)= len r-'(len r -'len CR) by RFINSEQ:29,XREAL_0:def 2;
instr(1,r,CR) = len r + 1 -'len CR by A1,A2,FINSEQ_8:def 12;
then CR is_preposition_of r/^(len r + 1 -'len CR-'1) by A7,A8,
FINSEQ_8:def 10;
then mid(r/^(len r + 1 -'len CR-'1),1,len CR)=CR by A2,FINSEQ_8:def 8;
then ((r/^(len r + 1 -'len CR-'1))/^(1-'1))|(len CR-'1+1)=CR by A4,
FINSEQ_6:def 3;
then
A12: ((r/^(len r + 1 -'len CR-'1))/^(0))|(len CR-'1+1)=CR by NAT_2:8;
len r-(len r-'len CR)>=0 by NAT_D:35,XREAL_1:48;
then
A13: len r-'(len r-'len CR)=len r-(len r-'len CR) by XREAL_0:def 2
.=len r-(len r-len CR) by A9,XREAL_0:def 2
.=len CR;
len r+1-len CR>=0+1 by A7,A8,NAT_1:13;
then len r+1-'len CR-1>=0 by A8,XREAL_1:48;
then len r+1-'len CR-'1=len r-len CR by A8,XREAL_0:def 2;
then
A14: (r/^(len r -'len CR)) |(len CR)=CR by A5,A10,A12;
mid(Rev r,1,len CR) =(Rev r/^(1-'1))|(len CR-'1+1) by A4,FINSEQ_6:def 3
.=(Rev r/^(0))|(len CR) by A5,NAT_2:8
.=(Rev r)|(len r-'(len r-'len CR)) by A13
.=Rev(r/^(len r-'len CR)) by Th18,NAT_D:35
.=Rev CR by A10,A14,A11,FINSEQ_1:58;
then mid(Rev r,1,len Rev CR)=Rev CR by FINSEQ_5:def 3;
then Rev CR is_preposition_of Rev r by A3,FINSEQ_8:def 8;
then CR is_postposition_of r by FINSEQ_8:def 9;
hence thesis by Th27;
end;
end;
theorem
for D being non empty set,f,g being File of D st f is_terminated_by g
holds len g <=len f by FINSEQ_8:def 12;
theorem Th30:
for D being non empty set,f,CR being File of D holds len addcr(f
,CR) >= len f & len addcr(f,CR) >= len CR
proof
let D be non empty set,f,CR be File of D;
A1: addcr(f,CR)=ovlcon(f,CR) by FINSEQ_8:def 11;
len ovlcon(f,CR)=len f+(len CR -'len ovlpart(f,CR)) by FINSEQ_8:15;
hence len addcr(f,CR) >= len f by A1,NAT_1:12;
ovlcon(f,CR)=(f|(len f-'len ovlpart(f,CR)))^CR by FINSEQ_8:11;
then len ovlcon(f,CR)= len (f|(len f-'len ovlpart(f,CR))) + len CR by
FINSEQ_1:22;
hence thesis by A1,NAT_1:12;
end;
theorem Th31:
for D being non empty set,f,g being FinSequence of D holds g =
ovlpart(f,g)^ovlrdiff(f,g)
proof
let D be non empty set,f,g be FinSequence of D;
ovlpart(f,g)=smid(g,1,len ovlpart(f,g)) by FINSEQ_8:def 2
.=g|len ovlpart(f,g) by FINSEQ_8:5;
then
ovlpart(f,g)^ovlrdiff(f,g)=(g|len ovlpart(f,g))^(g/^(len ovlpart(f,g)))
by FINSEQ_8:def 5
.=g by RFINSEQ:8;
hence thesis;
end;
theorem
for D being non empty set,f,g being FinSequence of D holds ovlcon(f,g)
= ovlldiff(f,g) ^ g
proof
let D be non empty set,f,g be FinSequence of D;
ovlcon(f,g) = ovlldiff(f,g)^(ovlpart(f,g)^ovlrdiff(f,g)) by FINSEQ_8:12;
hence thesis by Th31;
end;
theorem
for D being non empty set,CR,r being File of D holds addcr(r,CR)=
ovlldiff(r,CR)^CR
proof
let D be non empty set,CR,r be File of D;
thus addcr(r,CR) = ovlcon(r,CR) by FINSEQ_8:def 11
.= ovlldiff(r,CR)^(ovlpart(r,CR)^ovlrdiff(r,CR)) by FINSEQ_8:12
.= ovlldiff(r,CR)^CR by Th31;
end;
theorem Th34:
for D being non empty set,r1,r2,f being File of D st f = r1 ^ r2
holds r1 is_substring_of f,1 & r2 is_substring_of f,1
proof
let D be non empty set,r1,r2,f be File of D;
A1: len (r1^r2)=len r1+len r2 by FINSEQ_1:22;
assume
A2: f = r1 ^ r2;
A3: now
per cases;
suppose
A4: len r2>0;
then
A5: len r1 + len r2 > len r1 + 0 by XREAL_1:8;
A6: r2|len r2=r2|(Seg len r2) by FINSEQ_1:def 16;
A7: len r1+len r2-'len r1=len r1+len r2-len r1 by XREAL_0:def 2
.=len r2;
A8: len r2>=0+1 by A4,NAT_1:13;
then len r1+1<=len (r1^r2) by A1,XREAL_1:6;
then
A9: mid(r1^r2,len r1+1,len (r1^r2))= ((r1^r2)/^(len r1+1-'1))|(len (r1^
r2)-'(len r1+1)+1) by FINSEQ_6:def 3
.= ((r1^r2)/^len r1)|(len (r1^r2)-'(len r1+1)+1) by NAT_D:34
.= ((r1^r2)/^len r1)|(len r1 + len r2 -'(len r1+1)+1) by FINSEQ_1:22
.= ((r1^r2)/^len r1)|(len r1 + len r2 -'len r1) by A5,NAT_2:7
.= r2|len r2 by A7
.= r2 by A6,FINSEQ_2:20;
len r2>0 implies ex i being Element of NAT st 1<=i & i<=len (r1^r2)
& mid(r1^r2,i,(i-'1)+len r2)=r2
proof
consider i being Element of NAT such that
A10: i=len r1+1;
A11: i<=len (r1^r2) by A1,A8,A10,XREAL_1:6;
A12: (len r1+1)-'1+len r2=len r1+len r2 by NAT_D:34
.=len (r1^r2) by FINSEQ_1:22;
1<=i by A8,A10,XREAL_1:6;
hence thesis by A9,A10,A12,A11;
end;
hence r2 is_substring_of f,1 by A2,FINSEQ_8:def 7;
end;
suppose
len r2<=0;
hence r2 is_substring_of f,1 by FINSEQ_8:def 7;
end;
end;
A13: len r2 >=0 & len (r1^r2)=len r1+len r2 by FINSEQ_1:22;
now
per cases;
suppose
len r1>0;
then
A14: len r1>=0+1 by NAT_1:13;
then
A15: mid(r1^r2,1,len r1)= ((r1^r2)/^(1-'1))|(len r1-'1+1) by FINSEQ_6:def 3
.= ((r1^r2)/^0)|(len r1-'1+1) by XREAL_1:232
.= ((r1^r2)/^0)|len r1 by A14,XREAL_1:235
.= (r1^r2)|len r1
.= r1 by FINSEQ_5:23;
len r1>0 implies ex i being Element of NAT st 1<=i & i<=len (r1^r2)
& mid(r1^r2,i,(i-'1)+len r1)=r1
proof
set i = 1;
A16: (1-'1)+len r1=0+len r1 by XREAL_1:232
.=len r1;
i<=len (r1^r2) by A13,A14,XREAL_1:7;
hence thesis by A15,A16;
end;
hence r1 is_substring_of f,1 by A2,FINSEQ_8:def 7;
end;
suppose
len r1<=0;
hence r1 is_substring_of f,1 by FINSEQ_8:def 7;
end;
end;
hence thesis by A3;
end;
theorem Th35:
for D being non empty set,r1,r2,r3,f being File of D st f = r1 ^
r2 ^ r3 holds r1 is_substring_of f,1 & r2 is_substring_of f,1 & r3
is_substring_of f,1
proof
let D be non empty set,r1,r2,r3,f be File of D;
assume
A1: f = r1 ^ r2 ^ r3;
A2: len (r1^r2)=len r1+len r2 by FINSEQ_1:22;
A3: now
per cases;
suppose
A4: len r2>0;
A5: len r1+len r2-'len r1=len r1+len r2-len r1 by XREAL_0:def 2
.=len r2;
A6: len r1 + len r2 > len r1 + 0 by A4,XREAL_1:8;
len r2>=0+1 by A4,NAT_1:13;
then
A7: len r1+1<=len (r1^r2) by A2,XREAL_1:6;
then
A8: mid(r1^r2^r3,len r1+1,len (r1^r2))= ((r1^r2^r3)/^(len r1+1-'1))|(
len (r1^r2)-'(len r1+1)+1) by FINSEQ_6:def 3
.= ((r1^r2^r3)/^len r1)|(len (r1^r2)-'(len r1+1)+1) by NAT_D:34
.= ((r1^r2^r3)/^len r1)|(len r1 + len r2 -'(len r1+1)+1) by FINSEQ_1:22
.= ((r1^r2^r3)/^len r1)|(len r1 + len r2 -'len r1) by A6,NAT_2:7
.= ((r1^(r2^r3))/^len r1)|len r2 by A5,FINSEQ_1:32
.= (r2^r3)|len r2
.= r2 by FINSEQ_5:23;
A9: len r1 + 1>=0+1 by XREAL_1:6;
A10: len r1+1+0<=len r1+len r2+len r3 by A2,A7,XREAL_1:7;
len r2>0 implies ex i being Element of NAT st 1<=i & i<=len (r1^r2^
r3) & mid(r1^r2^r3,i,(i-'1)+len r2)=r2
proof
A11: (len r1+1)-'1+len r2=len r1+len r2 by NAT_D:34
.=len (r1^r2) by FINSEQ_1:22;
consider i being Element of NAT such that
A12: i=len r1+1;
i<=len (r1^r2^r3) by A2,A10,A12,FINSEQ_1:22;
hence thesis by A9,A8,A12,A11;
end;
hence r2 is_substring_of f,1 by A1,FINSEQ_8:def 7;
end;
suppose
len r2<=0;
hence r2 is_substring_of f,1 by FINSEQ_8:def 7;
end;
end;
f=r1^(r2^r3) by A1,FINSEQ_1:32;
hence thesis by A1,A3,Th34;
end;
theorem Th36:
for D being non empty set,CR,r1,r2 being File of D st r1
is_terminated_by CR & r2 is_terminated_by CR holds CR^r2 is_substring_of addcr(
r1^r2,CR),1
proof
let D be non empty set,CR,r1,r2 be File of D;
assume that
A1: r1 is_terminated_by CR and
A2: r2 is_terminated_by CR;
r2 = addcr(r2,CR) by A2,Th28;
then r2 = ovlcon(r2,CR) by FINSEQ_8:def 11;
then
A3: r2 = r2^(CR/^len ovlpart(r2,CR)) by FINSEQ_8:def 3;
r1 = addcr(r1,CR) by A1,Th28;
then r1 = ovlcon(r1,CR) by FINSEQ_8:def 11;
then
A4: r1 ^r2=((r1|(len r1-'len ovlpart(r1,CR)))^CR)^(r2^(CR/^len ovlpart(r2,CR
))) by A3,FINSEQ_8:11;
addcr(r1^r2,CR) = ovlcon(r1^r2,CR) by FINSEQ_8:def 11
.= r1^r2^(CR/^(len ovlpart(r1^r2,CR))) by FINSEQ_8:def 3
.=(r1|(len r1-'len ovlpart(r1,CR)))^(CR^r2)^(CR/^len ovlpart(r2,CR)) ^(
CR/^(len ovlpart(r1^r2,CR))) by A4,Th1
.=(r1|(len r1-'len ovlpart(r1,CR)))^(CR^r2)^ ( (CR/^len ovlpart(r2,CR))^
(CR/^(len ovlpart(r1^r2,CR))) ) by FINSEQ_1:32;
hence thesis by Th35;
end;
theorem Th37:
for D being non empty set,f,g being File of D,n being Element of
NAT st 0<n & g={} holds instr(n,f,g)=n
proof
let D be non empty set,f,g being File of D,n being Element of NAT;
assume that
A1: 0<n and
A2: g={};
A3: len g=0 by A2;
instr(n,f,g) <> 0
proof
assume instr(n,f,g)=0;
then not g is_substring_of f,n by FINSEQ_8:def 10;
hence contradiction by A3,FINSEQ_8:def 7;
end;
then
A4: n <= instr(n,f,g) by FINSEQ_8:def 10;
g is_preposition_of f/^(n-'1) by A3,FINSEQ_8:def 8;
then n >= instr(n,f,g) by A1,FINSEQ_8:def 10;
hence thesis by A4,XXREAL_0:1;
end;
theorem
for D being non empty set,f,g being File of D,n being Element of NAT
st 0<n & n<=len f holds instr(n,f,g)<=len f
proof
let D be non empty set,f,g be File of D,n be Element of NAT;
assume
A1: 0<n & n<=len f;
assume
A2: instr(n,f,g)>len f;
then instr(n,f,g) >= len f + 1 by NAT_1:13;
then instr(n,f,g)-1 >= len f +1-1 by XREAL_1:9;
then instr(n,f,g)-'1>=len f by XREAL_0:def 2;
then f/^(instr(n,f,g)-'1)={} by FINSEQ_5:32;
then
A3: len (f/^(instr(n,f,g)-'1)) < 1;
instr(n,f,g)>0 by A2;
then len g>=0 & g is_preposition_of f/^(instr(n,f,g)-'1) by FINSEQ_8:def 10;
then g={} by A3,FINSEQ_8:def 8;
hence thesis by A1,A2,Th37;
end;
theorem Th39:
for D being non empty set,f,CR being File of D holds CR
is_substring_of ovlcon(f,CR),1
proof
let D be non empty set,f,CR be File of D;
per cases;
suppose
A1: len CR >0;
set i3=len f-'len ovlpart(f,CR);
A2: len CR>= 0+1 by A1,NAT_1:13;
then
A3: i3+1 <= i3+ len CR by XREAL_1:6;
then
A4: i3+len CR-'(i3+1)+1=i3+len CR-(i3+1)+1 by XREAL_1:233
.=len CR;
1-len ovlpart(f,CR)<=len CR - len ovlpart(f,CR) by A2,XREAL_1:9;
then 1-len ovlpart(f,CR)+len f <=len CR - len ovlpart(f,CR) + len f by
XREAL_1:7;
then
A5: len f - len ovlpart(f,CR)>=0 & len f -len ovlpart(f,CR)+1<= len f + (
len CR - len ovlpart(f,CR)) by FINSEQ_8:10,XREAL_1:48;
len ovlpart(f,CR)<= len CR by FINSEQ_8:def 2;
then
A6: len CR - len ovlpart(f,CR) >=0 by XREAL_1:48;
set i4= len f-'len ovlpart(f,CR)+1;
A7: i3<=len (f|i3) by FINSEQ_1:59,NAT_D:35;
A8: (f|i3)/^i3=(f/^i3)|(i3-'i3) by FINSEQ_5:80
.=(f/^i3)|0 by XREAL_1:232
.={};
len (CR/^(len ovlpart(f,CR)))= len CR -' len ovlpart(f,CR) by RFINSEQ:29
.= len CR - len ovlpart(f,CR) by A6,XREAL_0:def 2;
then
ovlcon(f,CR)=f^(CR/^(len ovlpart(f,CR))) & len f-'len ovlpart(f,CR)+1
<= len f + len (CR/^(len ovlpart(f,CR))) by A5,FINSEQ_8:def 3,XREAL_0:def 2
;
then
A9: 1<=i4 & i4<=len ovlcon(f,CR) by FINSEQ_1:22,NAT_1:11;
mid((ovlcon(f,CR)),i4,(i4-'1)+len CR) =mid(((f|i3)^CR),i4,(i4-'1)+len
CR) by FINSEQ_8:11
.=mid(((f|i3)^CR),i3+1,i3+len CR) by NAT_D:34
.=(((f|i3)^CR)/^(i3+1-'1)) | (i3+len CR-'(i3+1)+1 ) by A3,FINSEQ_6:def 3
.=(((f|i3)^CR)/^i3) |(len CR) by A4,NAT_D:34
.=(((f|i3)/^i3)^CR) | (len CR) by A7,GENEALG1:1
.= CR|(len CR) by A8,FINSEQ_1:34
.=CR by Th2;
hence thesis by A9,FINSEQ_8:def 7;
end;
suppose len CR<=0;
hence thesis by FINSEQ_8:def 7;
end;
end;
theorem Th40:
for D being non empty set,f,CR being File of D holds
CR is_substring_of addcr(f,CR),1
proof
let D be non empty set,f,CR be File of D;
addcr(f,CR)=ovlcon(f,CR) by FINSEQ_8:def 11;
hence thesis by Th39;
end;
theorem Th41:
for D being non empty set,f,g being FinSequence of D, n being
Element of NAT st g is_substring_of f|n,1 & len g>0 holds g is_substring_of f,1
proof
let D be non empty set,f,g be FinSequence of D,n be Element of NAT;
assume that
A1: g is_substring_of f|n,1 and
A2: len g>0;
consider i2 being Nat such that
A3: 1<=i2 and
A4: i2<=len (f|n) and
A5: mid(f|n,i2,(i2-'1)+len g)=g by A1,A2,FINSEQ_8:def 7;
len g>= 0+1 by A2,NAT_1:13;
then len g -1>=0 by XREAL_1:48;
then
A6: len g-1+i2>=0+i2 by XREAL_1:7;
then
A7: i2-1+len g >=i2;
per cases;
suppose
A8: len f>=n;
(i2-'1)+len g=(i2-1)+len g by A3,XREAL_1:233;
then
A9: (i2-'1)+len g-'i2+1 = (i2-1)+len g-i2+1 by A6,XREAL_1:233
.= len g;
i2-1>=0 by A3,XREAL_1:48;
then
A10: i2<=(i2-'1)+len g by A7,XREAL_0:def 2;
then
A11: g = ((f|n)/^(i2-'1))|((i2-'1)+len g-'i2+1) by A5,FINSEQ_6:def 3
.=((f/^(i2-'1))|(n-'(i2-'1)))|len g by A9,FINSEQ_5:80;
now
A12: len (f/^(i2-'1))=len f -'(i2-'1) by RFINSEQ:29;
assume
A13: n-'(i2-'1)<len g;
then g=((f/^(i2-'1))|(n-'(i2-'1))) by A11,FINSEQ_5:77;
hence contradiction by A8,A13,A12,FINSEQ_1:59,NAT_D:42;
end;
then
A14: g=(f/^(i2-'1))|len g by A11,FINSEQ_5:77
.= mid(f,i2,(i2-'1)+len g) by A10,A9,FINSEQ_6:def 3;
len (f|n)<=len f by FINSEQ_5:16;
then i2<=len f by A4,XXREAL_0:2;
hence thesis by A3,A14,FINSEQ_8:def 7;
end;
suppose
len f<n;
hence thesis by A1,FINSEQ_1:58;
end;
end;
theorem
for D being non empty set, f,CR being File of D ex r being File of D
st r is_a_record_of f,CR
proof
let D be non empty set,f,CR be File of D;
set i0=instr(1,addcr(f,CR),CR);
A1: i0<>0
proof
assume i0=0;
then not CR is_substring_of addcr(f,CR),1 by FINSEQ_8:def 10;
hence contradiction by Th40;
end;
then i0>0;
then
A2: i0>=0+1 by NAT_1:13;
then i0-1>=0 by XREAL_1:48;
then
A3: i0-'1=i0-1 by XREAL_0:def 2;
per cases;
suppose
len f = 0;
then f= <*>D;
hence thesis by Th22;
end;
suppose
A4: len f<>0;
set r=addcr(f,CR)|(i0+len CR-'1);
A5: CR is_preposition_of (addcr(f,CR))/^(i0-'1) by A1,FINSEQ_8:def 10;
now
per cases;
suppose
A6: len CR<=0;
then
A7: CR=<*>D;
then CR/^(len ovlpart(f,CR))=CR by FINSEQ_6:80;
then f^(CR/^(len ovlpart(f,CR)))=f by A7,FINSEQ_1:34;
then
A8: ovlcon(f,CR)=f by FINSEQ_8:def 3;
len f> 0 by A4;
then
A9: len f>=0+1 by NAT_1:13;
A10: len r>0 implies 1<=len f & mid(f,1,len r)=r
proof
assume len r>0;
then
A11: len r>=0+1 by NAT_1:13;
per cases;
suppose
A12: len r < i0+len CR-'1;
r=(addcr(f,CR)|(i0+len CR-'1))|(len r) by FINSEQ_1:58
.= addcr(f,CR)|(len r) by A12,FINSEQ_5:77
.=f|(len r) by A8,FINSEQ_8:def 11
.=mid(f,1,len r) by A11,FINSEQ_6:116;
hence thesis by A9;
end;
suppose
A13: len r>= i0+len CR-'1;
A14: len r<= (i0+len CR-'1) by FINSEQ_5:17;
mid(f,1,len r)= f|(len r) by A11,FINSEQ_6:116
.=addcr(f,CR)|(len r) by A8,FINSEQ_8:def 11;
hence thesis by A9,A13,A14,XXREAL_0:1;
end;
end;
A15: r is_terminated_by CR by A6,FINSEQ_8:def 12;
addcr(f,CR)=f by A8,FINSEQ_8:def 11;
then r is_preposition_of addcr(f,CR) by A10,FINSEQ_8:def 8;
hence r is_a_record_of f,CR by A15;
end;
suppose
A16: len CR>0;
CR is_preposition_of addcr(f,CR)/^(i0-'1) by A1,FINSEQ_8:def 10;
then
A17: len CR <=len (addcr(f,CR)/^(i0-'1)) by NAT_1:43;
then i0-'1<=len addcr(f,CR) by A16,CARD_1:27,RFINSEQ:def 1;
then len (addcr(f,CR)/^(i0-'1)) =len addcr(f,CR) -(i0-'1) by
RFINSEQ:def 1;
then
A18: len CR +(i0-'1)<=len addcr(f,CR) by A17,XREAL_1:19;
A19: len CR>=0+1 by A16,NAT_1:13;
mid((addcr(f,CR))/^(i0-'1),1,len CR)=CR by A5,A16,FINSEQ_8:def 8;
then ((addcr(f,CR))/^(i0-'1))|(len CR)=CR by A19,FINSEQ_6:116;
then
A20: len CR <=len ((addcr(f,CR))/^(i0-'1)) by FINSEQ_5:16;
A21: len ((addcr(f,CR))/^(i0-'1)) <= len (addcr(f,CR)) by FINSEQ_5:25;
A22: now
per cases;
suppose
i0+len CR-'1>=len addcr(f,CR);
then addcr(f,CR)|(i0+len CR-'1)=addcr(f,CR) by FINSEQ_1:58;
hence len (addcr(f,CR)|(i0+len CR-'1))>=len CR by A20,A21,
XXREAL_0:2;
end;
suppose
A23: i0+len CR-'1<len addcr(f,CR);
i0-1>=0 by A2,XREAL_1:48;
then
A24: len CR +(i0-1)>=len CR +0 by XREAL_1:7;
then i0+ len CR -'1=len CR+i0 -1 by XREAL_0:def 2;
hence len (addcr(f,CR)|(i0+len CR-'1))>=len CR by A23,A24,
FINSEQ_1:59;
end;
end;
i0+len CR -1>=0 by A2,NAT_1:12,XREAL_1:48;
then
A25: len CR+i0 -'1<= len addcr(f,CR) by A3,A18,XREAL_0:def 2;
then
A26: len r= i0+len CR-'1 by FINSEQ_1:59;
((len r + 1 -'len CR) <> 0 implies 1 <= (len r + 1 -'len CR) & CR
is_preposition_of r/^((len r + 1 -'len CR)-'1) & for j being Element of NAT st
j >= 1 & j > 0 & CR is_preposition_of r/^(j-'1) holds j >= len r + 1 -'len CR)
& ((len r + 1 -'len CR)=0 implies not CR is_substring_of r,1 )
proof
thus (len r + 1 -'len CR) <> 0 implies 1 <= len r + 1 -'len CR & CR
is_preposition_of r/^((len r + 1 -'len CR)-'1) & for j being Element of NAT st
j >= 1 & j > 0 & CR is_preposition_of r/^(j-'1) holds j >= len r + 1 -'len CR
proof
assume len r + 1 -'len CR <> 0;
then 0+1<= len r + 1 -'len CR by NAT_1:13;
hence 1 <= len r + 1 -'len CR;
set f2= (addcr(f,CR)|(i0+len CR-'1))/^(i0-'1);
A27: i0<=i0+len CR by NAT_1:12;
i0-1>=0 by A2,XREAL_1:48;
then
A28: i0-'1=i0-1 by XREAL_0:def 2;
A29: i0+len CR -1>=0 by A19,NAT_1:12,XREAL_1:48;
then i0+len CR-'1=i0 +len CR -1 by XREAL_0:def 2;
then i0-'1<=len r by A3,A26,A27,XREAL_1:9;
then
A30: len f2= len r -(i0-'1) by RFINSEQ:def 1
.=i0+len CR-'1-(i0-'1) by A25,FINSEQ_1:59
.= i0+len CR-1-(i0-1) by A29,A28,XREAL_0:def 2
.=len CR;
A31: i0+len CR -1>=0 by A19,NAT_1:12,XREAL_1:48;
i0+len CR>=i0 by NAT_1:12;
then i0+len CR -'1-(i0-'1)>=0 by NAT_D:42,XREAL_1:48;
then i0+len CR-'1-'(i0-'1) = i0+len CR-'1-(i0-'1) by XREAL_0:def 2
.=i0+len CR-1-(i0-1) by A3,A31,XREAL_0:def 2
.=len CR;
then
A32: ((addcr(f,CR))|(i0+len CR-'1))/^(i0-'1) = ((addcr(f,CR))/^(i0
-'1))|(len CR) by FINSEQ_5:80;
mid((addcr(f,CR))/^(i0-'1),1,len CR)=CR by A5,A16,FINSEQ_8:def 8;
then f2=CR by A19,A32,FINSEQ_6:116;
then f2|(len CR)=CR by FINSEQ_1:58;
then
A33: mid(f2,1,len CR)=CR by A19,FINSEQ_6:116;
i0+len CR -1>=0 by A19,NAT_1:12,XREAL_1:48;
then
A34: i0+len CR-'1+1=i0 +len CR -1+1 by XREAL_0:def 2
.=i0+len CR;
i0+len CR -1>=0 by A2,NAT_1:12,XREAL_1:48;
then len r +1=i0+len CR-1+1 by A26,XREAL_0:def 2;
then
A35: len r+1-'len CR=i0 by NAT_D:34;
i0+len CR-len CR>=0;
then
A36: i0+len CR-'len CR=i0 by XREAL_0:def 2;
i0+len CR-'1+1=i0 +len CR -1+1 by A31,XREAL_0:def 2
.=i0+len CR;
then
r/^((len r + 1 -'len CR)-'1) =(addcr(f,CR)|(i0+len CR-'1))/^(
i0-'1) by A3,A18,A36,FINSEQ_1:59;
hence CR is_preposition_of r/^((len r + 1 -'len CR)-'1) by A16,A30
,A33,FINSEQ_8:def 8;
i0+len CR-len CR>=0;
then
A37: i0+len CR-'len CR=i0 by XREAL_0:def 2;
i0+len CR -1>=0 by A19,NAT_1:12,XREAL_1:48;
then
A38: i0+len CR-'1=i0 +len CR -1 by XREAL_0:def 2;
thus for j being Element of NAT st j >= 1 & j > 0 & CR
is_preposition_of r/^(j-'1) holds j >= len r + 1 -'len CR
proof
let j be Element of NAT;
assume that
A39: j >= 1 and
j > 0 and
A40: CR is_preposition_of r/^(j-'1);
A41: (r/^(j-'1))|(len CR)=(r/^(j-'1))|((j-'1)+len CR -'(j-'1))
by NAT_D:34
.=(r|(len CR+(j-'1)))/^(j-'1) by FINSEQ_5:80;
A42: mid(r/^(j-'1),1,len CR) =(r/^(j-'1))|(len CR) by A19,FINSEQ_6:116
;
A43: j-1>=0 by A39,XREAL_1:48;
now
assume
A44: j < len r + 1 -'len CR;
then j<i0 by A3,A18,A34,A37,FINSEQ_1:59;
then j-'1<i0-'1 by A39,NAT_D:56;
then
A45: len ((addcr(f,CR))/^(i0-'1))<=len ((addcr(f,CR))/^(j-'1)
) by Th4;
A46: j+len CR -1>=0 by A39,NAT_1:12,XREAL_1:48;
then
A47: j+len CR -'1=len CR +(j-1) by XREAL_0:def 2
.=len CR +(j-'1) by A43,XREAL_0:def 2;
j< i0+len CR-'1 +1-'len CR by A25,A44,FINSEQ_1:59;
then j+len CR<i0+len CR by A34,A37,XREAL_1:8;
then j+len CR -1 < i0+len CR -1 by XREAL_1:9;
then
A48: j+len CR-'1<i0+len CR-'1 by A38,A46,XREAL_0:def 2;
((addcr(f,CR))/^(j-'1))|(len CR) =((addcr(f,CR))/^(j-'1))
|((j-'1)+len CR -'(j-'1)) by NAT_D:34
.=((addcr(f,CR))|(len CR+(j-'1)))/^(j-'1) by FINSEQ_5:80
.=((addcr(f,CR)|(i0+len CR-'1))|(j+len CR-'1))/^(j-'1) by A47
,A48,FINSEQ_5:77
.= CR by A16,A40,A42,A41,A47,FINSEQ_8:def 8;
then
A49: mid(((addcr(f,CR))/^(j-'1)),1,len CR)=CR by A19,FINSEQ_6:116;
1<=len ((addcr(f,CR))/^(i0-'1)) by A5,A16,FINSEQ_8:def 8;
then 1<=len ((addcr(f,CR))/^(j-'1)) by A45,XXREAL_0:2;
then CR is_preposition_of ((addcr(f,CR))/^(j-'1)) by A49,
FINSEQ_8:def 8;
hence contradiction by A35,A39,A44,FINSEQ_8:def 10;
end;
hence thesis;
end;
end;
i0+len CR-len CR>=0;
then
A50: i0+len CR-'len CR=i0 by XREAL_0:def 2;
i0+len CR -1>=0 by A19,NAT_1:12,XREAL_1:48;
then
A51: i0+len CR-'1+1=i0 +len CR -1+1 by XREAL_0:def 2
.=i0+len CR;
assume len r + 1 -'len CR=0;
then instr(1,addcr(f,CR),CR)=0 by A3,A18,A51,A50,FINSEQ_1:59;
then not CR is_substring_of addcr(f,CR),1 by FINSEQ_8:def 10;
hence thesis by A16,Th41;
end;
then
A52: instr(1,r,CR) = len r + 1 -'len CR by FINSEQ_8:def 10;
per cases;
suppose
A53: 1<=len r;
addcr(f,CR)|(len r)=r & len (addcr(f,CR)|(i0+len CR-'1))<= len
addcr(f,CR) by A25,FINSEQ_1:59;
then len r>0 implies 1<=len (addcr(f,CR)) & mid(addcr(f,CR),1,len r
)=r by A53,FINSEQ_6:116,XXREAL_0:2;
then
A54: CR^r is_substring_of addcr(f,CR),1 or r is_preposition_of
addcr(f,CR) by FINSEQ_8:def 8;
r is_terminated_by CR by A22,A52,FINSEQ_8:def 12;
hence r is_a_record_of f,CR by A54;
end;
suppose
1>len r;
then
A55: 0+1>=len r +1 by NAT_1:13;
then
A56: len CR<=0 by A22,XREAL_1:6;
then
A57: r is_terminated_by CR by FINSEQ_8:def 12;
0>=len r by A55,XREAL_1:6;
then r= {};
then CR^r=CR by FINSEQ_1:34;
then CR^r is_substring_of addcr(f,CR),1 by A56,FINSEQ_8:def 7;
hence r is_a_record_of f,CR by A57;
end;
end;
end;
hence thesis;
end;
end;
theorem
for D being non empty set,f,CR,r being File of D st r is_a_record_of f
,CR holds r is_a_record_of r,CR
by Th28;
theorem
for D being non empty set,CR,r1,r2,f being File of D st r1
is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 holds r1
is_a_record_of f,CR & r2 is_a_record_of f,CR
proof
let D be non empty set,CR,r1,r2,f be File of D;
assume that
A1: r1 is_terminated_by CR and
A2: r2 is_terminated_by CR and
A3: f = r1 ^ r2;
per cases;
suppose
len r1<=0 & len r2 <=0;
then
r1 is_preposition_of addcr(f,CR) & r2 is_preposition_of addcr(f,CR) by
FINSEQ_8:def 8;
hence thesis by A1,A2;
end;
suppose
A4: len r1<=0 & len r2 >0;
then
A5: r1 is_preposition_of addcr(f,CR) by FINSEQ_8:def 8;
len r1=0 by A4;
then
A6: f = r2 by A3,Th3;
then f is_preposition_of addcr(f,CR) by A2,Th28;
hence thesis by A1,A2,A5,A6;
end;
suppose
A7: len r1>0 & len r2 <=0;
1+0<=len r1 + len r2 by A7,NAT_1:13;
then
A8: 1 <=len f by A3,FINSEQ_1:22;
0+1<=len r1 by A7,NAT_1:13;
then
A9: mid(addcr(f,CR),1,len r1)=addcr(f,CR)|len r1 by FINSEQ_6:116
.=ovlcon(f,CR)|len r1 by FINSEQ_8:def 11
.=(f^(CR/^(len ovlpart(f,CR))))|len r1 by FINSEQ_8:def 3
.=(r1^(r2^(CR/^(len ovlpart(f,CR)))))|len r1 by A3,FINSEQ_1:32
.= r1|len r1 by FINSEQ_5:22
.= r1 by FINSEQ_1:58;
len f<= len addcr(f,CR) by Th30;
then
len r1>0 implies 1<=len addcr(f,CR) & mid(addcr(f,CR),1,len r1)=r1 by A8,A9
,XXREAL_0:2;
then
A10: r1 is_preposition_of addcr(f,CR) by FINSEQ_8:def 8;
r2 is_preposition_of addcr(f,CR) by A7,FINSEQ_8:def 8;
hence thesis by A1,A2,A10;
end;
suppose
A11: len r1>0 & len r2>0;
then 1+0<=len r1 + len r2 by NAT_1:13;
then
A12: 1 <=len f by A3,FINSEQ_1:22;
0+1<=len r1 by A11,NAT_1:13;
then
A13: mid(addcr(f,CR),1,len r1)=addcr(f,CR)|len r1 by FINSEQ_6:116
.=ovlcon(f,CR)|len r1 by FINSEQ_8:def 11
.=(f^(CR/^(len ovlpart(f,CR))))|len r1 by FINSEQ_8:def 3
.=(r1^(r2^(CR/^(len ovlpart(f,CR)))))|len r1 by A3,FINSEQ_1:32
.= r1|len r1 by FINSEQ_5:22
.= r1 by FINSEQ_1:58;
len f<= len addcr(f,CR) by Th30;
then
len r1>0 implies 1<=len addcr(f,CR) & mid(addcr(f,CR),1,len r1)=r1 by A12
,A13,XXREAL_0:2;
then
A14: r1 is_preposition_of addcr(f,CR) by FINSEQ_8:def 8;
CR^r2 is_substring_of addcr(r1^r2,CR),1 by A1,A2,Th36;
hence thesis by A1,A2,A3,A14;
end;
end;