:: A Theory of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005-2021 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 r is_preposition_of addcr (f,CR) ) & 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 r is_preposition_of addcr (f,CR) ) & 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 is_preposition_of f ^ CR

proof end;

theorem :: FILEREC1:25

for D being non empty set
for f, CR being File of D holds f is_preposition_of addcr (f,CR)

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
r = addcr (r,CR)

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
r = addcr (r,CR)

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;