:: A Theory of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Copyright (c) 2005-2017 Association of Mizar Users

theorem Th1: :: 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) )
proof end;

theorem Th2: :: FILEREC1:2
for f being FinSequence holds f | (len f) = f
proof end;

theorem Th3: :: FILEREC1:3
for p, q being FinSequence st len p = 0 holds
q = p ^ q
proof end;

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)
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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 )
proof end;

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 )
proof end;

theorem :: FILEREC1:11
for a being set
for f being FinSequence st f = <*a*> holds
f | 1 = <*a*>
proof end;

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*>
proof end;

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*>
proof end;

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*>
proof end;

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*>
proof end;

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*>
proof end;

theorem :: FILEREC1:17
for f being FinSequence st len f = 0 holds
Rev f = f
proof end;

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)
proof end;

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
proof end;

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
proof end;

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;
pred r is_a_record_of f,CR means :: 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 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 )
proof end;

theorem Th22: :: FILEREC1:22
for D being non empty set
for CR being FinSequence of D holds CR is_a_record_of <*> D,CR
proof end;

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 )
proof end;

theorem Th24: :: FILEREC1:24
for D being non empty set
for f, CR being File of D holds f ^ CR is_preposition_of
proof end;

theorem :: FILEREC1:25
for D being non empty set
for f, CR being File of D holds addcr (f,CR) is_preposition_of
proof end;

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)
proof end;

theorem Th27: :: FILEREC1:27
for D being non empty set
for CR, r being File of D st CR is_postposition_of r holds
proof end;

theorem Th28: :: FILEREC1:28
for D being non empty set
for CR, r being File of D st r is_terminated_by CR holds
proof end;

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 by FINSEQ_8:def 12;

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 )
proof end;

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))
proof end;

theorem :: FILEREC1:32
for D being non empty set
for f, g being FinSequence of D holds ovlcon (f,g) = (ovlldiff (f,g)) ^ g
proof end;

theorem :: FILEREC1:33
for D being non empty set
for CR, r being File of D holds addcr (r,CR) = (ovlldiff (r,CR)) ^ CR
proof end;

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 )
proof end;

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 )
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 by Th28;

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 )
proof end;