:: A Theory of Sequential Files :: by Hirofumi Fukura and Yatsuka Nakamura :: :: Received August 12, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin theorem Th1: :: FILEREC1:1 for D being non empty set for p, q, r, s being FinSequence of D 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) ) proofend; theorem Th2: :: FILEREC1:2 for D being set for f being FinSequence of D holds f | (len f) = f proofend; theorem Th3: :: FILEREC1:3 for D being non empty set for p, q being FinSequence of D st len p = 0 holds q = p ^ q proofend; theorem Th4: :: FILEREC1:4 for D being non empty set for f being FinSequence of D for n, m being Element of NAT st n <= m holds len (f /^ m) <= len (f /^ n) proofend; theorem Th5: :: FILEREC1:5 for D being non empty set for f, g being FinSequence of D st len g >= 1 holds mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g proofend; theorem Th6: :: FILEREC1:6 for D being non empty set for f, g being FinSequence of D for i, j being Element of NAT st 1 <= i & i <= j & j <= len f holds mid ((f ^ g),i,j) = mid (f,i,j) proofend; theorem :: FILEREC1:7 for D being non empty set for f being FinSequence of D for 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) proofend; theorem :: FILEREC1:8 for a being set for D being non empty set for f being FinSequence of D st f = <*a*> holds a in D proofend; theorem :: FILEREC1:9 for a, b being set for D being non empty set for f being FinSequence of D st f = <*a,b*> holds ( a in D & b in D ) proofend; theorem Th10: :: FILEREC1:10 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds ( a in D & b in D & c in D ) proofend; theorem :: FILEREC1:11 for a being set for D being non empty set for f being FinSequence of D st f = <*a*> holds f | 1 = <*a*> proofend; theorem :: FILEREC1:12 for a, b being set for D being non empty set for f being FinSequence of D st f = <*a,b*> holds f /^ 1 = <*b*> proofend; theorem :: FILEREC1:13 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f | 1 = <*a*> proofend; theorem Th14: :: FILEREC1:14 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f | 2 = <*a,b*> proofend; theorem :: FILEREC1:15 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f /^ 1 = <*b,c*> proofend; theorem :: FILEREC1:16 for a, b, c being set for D being non empty set for f being FinSequence of D st f = <*a,b,c*> holds f /^ 2 = <*c*> proofend; theorem :: FILEREC1:17 for D being non empty set for f being FinSequence of D st len f = 0 holds Rev f = f proofend; theorem Th18: :: FILEREC1:18 for D being non empty set for r being FinSequence of D for i being Element of NAT st i <= len r holds Rev (r /^ i) = (Rev r) | ((len r) -' i) proofend; theorem Th19: :: FILEREC1:19 for D being non empty set for 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 proofend; theorem :: FILEREC1:20 for D being non empty set for f, CR being FinSequence of D st not CR is_substring_of f,1 & CR separates_uniquely holds f ^ CR is_terminated_by CR proofend; notation let D be set ; synonym File of D for FinSequence of D; end; definition let D be non empty set ; let r, f, CR be File of D; predr is_a_record_of f,CR means :Def1: :: FILEREC1:def 1 ( ( CR ^ r is_substring_of addcr (f,CR),1 or addcr (f,CR) is_preposition_of ) & r is_terminated_by CR ); end; :: deftheorem Def1 defines is_a_record_of FILEREC1:def_1_:_ for D being non empty set for r, f, CR being File of D holds ( r is_a_record_of f,CR iff ( ( CR ^ r is_substring_of addcr (f,CR),1 or addcr (f,CR) is_preposition_of ) & r is_terminated_by CR ) ); theorem Th21: :: FILEREC1:21 for D being non empty set for r being FinSequence of D holds ( ovlpart ((<*> D),r) = <*> D & ovlpart (r,(<*> D)) = <*> D ) proofend; theorem Th22: :: FILEREC1:22 for D being non empty set for CR being FinSequence of D holds CR is_a_record_of <*> D,CR proofend; theorem :: FILEREC1:23 for D being non empty set for a, b being set for 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 ) proofend; theorem Th24: :: FILEREC1:24 for D being non empty set for f, CR being File of D holds f ^ CR is_preposition_of proofend; theorem :: FILEREC1:25 for D being non empty set for f, CR being File of D holds addcr (f,CR) is_preposition_of proofend; theorem Th26: :: FILEREC1:26 for D being non empty set for r, CR being File of D st CR is_postposition_of r holds 0 <= (len r) - (len CR) proofend; theorem Th27: :: FILEREC1:27 for D being non empty set for CR, r being File of D st CR is_postposition_of r holds r = addcr (r,CR) proofend; theorem Th28: :: FILEREC1:28 for D being non empty set for CR, r being File of D st r is_terminated_by CR holds r = addcr (r,CR) proofend; theorem :: FILEREC1:29 for D being non empty set for f, g being File of D st f is_terminated_by g holds len g <= len f proofend; theorem Th30: :: FILEREC1:30 for D being non empty set for f, CR being File of D holds ( len (addcr (f,CR)) >= len f & len (addcr (f,CR)) >= len CR ) proofend; theorem Th31: :: FILEREC1:31 for D being non empty set for f, g being FinSequence of D holds g = (ovlpart (f,g)) ^ (ovlrdiff (f,g)) proofend; theorem :: FILEREC1:32 for D being non empty set for f, g being FinSequence of D holds ovlcon (f,g) = (ovlldiff (f,g)) ^ g proofend; theorem :: FILEREC1:33 for D being non empty set for CR, r being File of D holds addcr (r,CR) = (ovlldiff (r,CR)) ^ CR proofend; theorem Th34: :: FILEREC1:34 for D being non empty set for r1, r2, f being File of D st f = r1 ^ r2 holds ( r1 is_substring_of f,1 & r2 is_substring_of f,1 ) proofend; theorem Th35: :: FILEREC1:35 for D being non empty set for 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 ) proofend; theorem Th36: :: FILEREC1:36 for D being non empty set for 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 proofend; theorem Th37: :: FILEREC1:37 for D being non empty set for f, g being File of D for n being Element of NAT st 0 < n & g = {} holds instr (n,f,g) = n proofend; theorem :: FILEREC1:38 for D being non empty set for f, g being File of D for n being Element of NAT st 0 < n & n <= len f holds instr (n,f,g) <= len f proofend; theorem Th39: :: FILEREC1:39 for D being non empty set for f, CR being File of D holds CR is_substring_of ovlcon (f,CR),1 proofend; theorem Th40: :: FILEREC1:40 for D being non empty set for f, CR being File of D holds CR is_substring_of addcr (f,CR),1 proofend; theorem Th41: :: FILEREC1:41 for D being non empty set for f, g being FinSequence of D for n being Element of NAT st g is_substring_of f | n,1 & len g > 0 holds g is_substring_of f,1 proofend; theorem :: FILEREC1:42 for D being non empty set for f, CR being File of D ex r being File of D st r is_a_record_of f,CR proofend; theorem :: FILEREC1:43 for D being non empty set for f, CR, r being File of D st r is_a_record_of f,CR holds r is_a_record_of r,CR proofend; theorem :: FILEREC1:44 for D being non empty set for 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 ) proofend;