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

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

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

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)

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)

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

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 )

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

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

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

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

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

for D being non empty set

for f being FinSequence of D st f = <*a,b,c*> holds

f /^ 2 = <*c*>

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)

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

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

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;

definition

let D be non empty set ;

let r, f, CR be File of D;

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

( ( CR ^ r is_substring_of addcr (f,CR),1 or r is_preposition_of addcr (f,CR) ) & r is_terminated_by CR );

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

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 )

for r being FinSequence of D holds

( ovlpart ((<*> D),r) = <*> D & ovlpart (r,(<*> D)) = <*> D )

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 )

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

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)

for CR, r being File of D st CR is_postposition_of r 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;

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 )

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

for f, g being FinSequence of D holds g = (ovlpart (f,g)) ^ (ovlrdiff (f,g))

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 )

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 )

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

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

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

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

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

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 )

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;