:: A Theory of Sequential Files :: by Hirofumi Fukura and Yatsuka Nakamura :: :: Received August 12, 2005 :: Copyright (c) 2005-2021 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; begin reserve a,b,c for set; theorem :: FILEREC1:1 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); theorem :: FILEREC1:2 for f being FinSequence holds f|(len f) = f; theorem :: FILEREC1:3 for p,q being FinSequence st len p=0 holds q = p ^ q; theorem :: FILEREC1:4 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); theorem :: FILEREC1:5 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; theorem :: FILEREC1:6 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); theorem :: FILEREC1:7 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); theorem :: FILEREC1:8 for D being non empty set,f being FinSequence of D st f=<*a*> holds a in D; theorem :: FILEREC1:9 for D being non empty set,f being FinSequence of D st f=<*a,b*> holds a in D & b in D; theorem :: FILEREC1:10 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; theorem :: FILEREC1:11 for f being FinSequence st f=<*a*> holds f|1=<*a*>; theorem :: FILEREC1:12 :: FINSEQ_6:50 for D being non empty set,f being FinSequence of D st f=<*a,b*> holds f/^1=<*b*>; theorem :: FILEREC1:13 for D being non empty set,f being FinSequence of D st f=<*a,b,c*> holds f|1=<*a*>; theorem :: FILEREC1:14 for D being non empty set,f being FinSequence of D st f=<*a,b,c *> holds f|2=<*a,b*>; theorem :: FILEREC1:15 for D being non empty set,f being FinSequence of D st f=<*a,b,c*> holds f/^1=<*b,c*>; theorem :: FILEREC1:16 for D being non empty set,f being FinSequence of D st f=<*a,b,c*> holds f/^2=<*c*>; theorem :: FILEREC1:17 for f being FinSequence st len f=0 holds Rev f=f; theorem :: FILEREC1:18 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); theorem :: FILEREC1:19 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; theorem :: FILEREC1:20 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; ::========================================================================== :: 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 :: FILEREC1:def 1 (CR^r is_substring_of addcr(f,CR),1 or r is_preposition_of addcr(f,CR)) & r is_terminated_by CR; end; theorem :: FILEREC1:21 for D being non empty set,r being FinSequence of D holds ovlpart (<*>D,r)=<*>D & ovlpart(r,<*>D)=<*>D; theorem :: FILEREC1:22 for D being non empty set,CR being FinSequence of D holds CR is_a_record_of <*>D,CR; theorem :: FILEREC1:23 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; theorem :: FILEREC1:24 for D being non empty set,f,CR being File of D holds f is_preposition_of f^CR ; theorem :: FILEREC1:25 for D being non empty set,f,CR being File of D holds f is_preposition_of addcr(f,CR); theorem :: FILEREC1:26 for D being non empty set,r,CR being File of D st CR is_postposition_of r holds 0<=len r-len CR; theorem :: FILEREC1:27 for D being non empty set,CR,r being File of D st CR is_postposition_of r holds r=addcr(r,CR); theorem :: FILEREC1:28 for D being non empty set,CR,r being File of D st r is_terminated_by CR holds r=addcr(r,CR); theorem :: FILEREC1:29 for D being non empty set,f,g being File of D st f is_terminated_by g holds len g <=len f; theorem :: FILEREC1:30 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; theorem :: FILEREC1:31 for D being non empty set,f,g being FinSequence of D holds g = ovlpart(f,g)^ovlrdiff(f,g); theorem :: FILEREC1:32 for D being non empty set,f,g being FinSequence of D holds ovlcon(f,g) = ovlldiff(f,g) ^ g; theorem :: FILEREC1:33 for D being non empty set,CR,r being File of D holds addcr(r,CR)= ovlldiff(r,CR)^CR; theorem :: FILEREC1:34 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; theorem :: FILEREC1:35 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; theorem :: FILEREC1:36 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; theorem :: FILEREC1:37 for D being non empty set,f,g being File of D,n being Element of NAT st 00 holds g is_substring_of f,1 ; theorem :: FILEREC1:42 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; theorem :: FILEREC1:43 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; theorem :: FILEREC1:44 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;