:: FILEREC1 semantic presentation

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) )

proof end;

theorem Th2: :: FILEREC1:2

for D being set
for f being FinSequence of D holds f | (len f) = f

proof end;

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

proof end;

theorem Th4: :: FILEREC1:4

for D being non empty set
for f being FinSequence of D
for n, m being 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 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 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 D being non empty set
for f being FinSequence of D 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 D being non empty set
for f being FinSequence of D 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 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, g being FinSequence of D holds g is_preposition_of (f ^ g) /^ (len f)

proof end;

theorem :: FILEREC1:21

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 :Def1: :: 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 Def1 defines is_a_record_of FILEREC1:def 1 :

theorem Th22: :: FILEREC1:22

for D being non empty set
for r being FinSequence of D holds
( ovlpart (<*> D),r = <*> D & ovlpart r,(<*> D) = <*> D )

proof end;

theorem Th23: :: FILEREC1:23

for D being non empty set
for CR being FinSequence of D holds CR is_a_record_of <*> D,CR

proof end;

theorem :: FILEREC1:24

for D being non empty set
for a, b being set
for f, r, CR being File of D st a <> b & D = {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 Th25: :: FILEREC1:25

for D being non empty set
for f, CR being File of D holds f is_preposition_of f ^ CR

proof end;

theorem :: FILEREC1:26

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

proof end;

theorem Th27: :: FILEREC1:27

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 Th28: :: FILEREC1:28

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 Th29: :: FILEREC1:29

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:30

for D being non empty set
for f, g being File of D st f is_terminated_by g holds
len g <= len f

proof end;

theorem Th31: :: FILEREC1:31

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 Th32: :: FILEREC1:32

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:33

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:34

for D being non empty set
for CR, r being File of D holds addcr r,CR = (ovlldiff r,CR) ^ CR

proof end;

theorem Th35: :: FILEREC1:35

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 Th36: :: FILEREC1:36

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 Th37: :: FILEREC1:37

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 Th38: :: FILEREC1:38

for D being non empty set
for f, g being File of D
for n being Nat st 0 < n & g = {} holds
instr n,f,g = n

proof end;

theorem :: FILEREC1:39

for D being non empty set
for f, g being File of D
for n being Nat st 0 < n & n <= len f holds
instr n,f,g <= len f

proof end;

theorem Th40: :: FILEREC1:40

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 Th41: :: FILEREC1:41

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 Th42: :: FILEREC1:42

for D being non empty set
for f, g being FinSequence of D
for n being Nat st g is_substring_of f | n,1 & len g > 0 & len g <= n holds
g is_substring_of f,1

proof end;

theorem :: FILEREC1:43

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:44

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

proof end;

theorem :: FILEREC1:45

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;