:: Concatenation of Finite Sequences Reducing Overlapping Part and an Argument of Separators of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Received March 18, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

definition
let D be set ;
let f, g be FinSequence of D;
:: original:^
redefine funcf ^ g ->  FinSequence of D;
correctness
coherence
f ^ g is FinSequence of D;
proofend;
end;

theorem :: FINSEQ_8:1
for D being non empty set
for f, g being FinSequence of D st len f >= 1 holds
mid ((f ^ g),1,(len f)) = f
proofend;

theorem Th2: :: FINSEQ_8:2
for D being set
for f being FinSequence of D
for i being Element of NAT st i >= len f holds
f /^ i = <*> D
proofend;

theorem :: FINSEQ_8:3
for D being non empty set
for k1, k2 being Element of NAT holds mid ((<*> D),k1,k2) = <*> D
proofend;

definition
let f be FinSequence;
let k1, k2 be Nat;
func smid (f,k1,k2) ->  FinSequence equals :: FINSEQ_8:def 1
(f /^ (k1 -' 1)) | ((k2 + 1) -' k1);
correctness
coherence
(f /^ (k1 -' 1)) | ((k2 + 1) -' k1) is FinSequence;
;
end;

:: deftheorem  defines smid FINSEQ_8:def_1_:_
 for f being FinSequence
for k1, k2 being Nat holds smid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1);

definition
let D be set ;
let f be FinSequence of D;
let k1, k2 be Nat;
:: original:smid
redefine func smid (f,k1,k2) ->  FinSequence of D;
correctness
coherence
smid (f,k1,k2) is FinSequence of D;
proofend;
end;

theorem Th4: :: FINSEQ_8:4
for f being FinSequence
for k1, k2 being Element of NAT st k1 <= k2 holds
smid (f,k1,k2) = mid (f,k1,k2)
proofend;

theorem Th5: :: FINSEQ_8:5
for D being non empty set
for f being FinSequence of D
for k2 being Element of NAT holds smid (f,1,k2) = f | k2
proofend;

theorem Th6: :: FINSEQ_8:6
for D being non empty set
for f being FinSequence of D
for k2 being Element of NAT st len f <= k2 holds
smid (f,1,k2) = f
proofend;

theorem Th7: :: FINSEQ_8:7
for D being set
for f being FinSequence of D
for k1, k2 being Element of NAT st k1 > k2 holds
smid (f,k1,k2) = {}
proofend;

theorem :: FINSEQ_8:8
for D being set
for f being FinSequence of D
for k2 being Element of NAT holds smid (f,0,k2) = smid (f,1,(k2 + 1))
proofend;

theorem Th9: :: FINSEQ_8:9
for D being non empty set
for f, g being FinSequence of D holds smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g
proofend;

:: Overlapping Part
definition
let D be non empty set ;
let f, g be FinSequence of D;
func ovlpart (f,g) ->  FinSequence of D means :Def2: :: FINSEQ_8:def 2
( len it <= len g &amp; it = smid (g,1,(len it)) &amp; it = smid (f,(((len f) -' (len it)) + 1),(len f)) &amp; ( for j being Nat st j <= len g &amp; smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len it ) );
existence
 ex b1 being FinSequence of D st
( len b1 <= len g &amp; b1 = smid (g,1,(len b1)) &amp; b1 = smid (f,(((len f) -' (len b1)) + 1),(len f)) &amp; ( for j being Nat st j <= len g &amp; smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b1 ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of D st len b1 <= len g &amp; b1 = smid (g,1,(len b1)) &amp; b1 = smid (f,(((len f) -' (len b1)) + 1),(len f)) &amp; ( for j being Nat st j <= len g &amp; smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b1 ) &amp; len b2 <= len g &amp; b2 = smid (g,1,(len b2)) &amp; b2 = smid (f,(((len f) -' (len b2)) + 1),(len f)) &amp; ( for j being Nat st j <= len g &amp; smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ovlpart FINSEQ_8:def_2_:_
 for D being non empty set
for f, g, b4 being FinSequence of D holds
( b4 = ovlpart (f,g) iff ( len b4 <= len g &amp; b4 = smid (g,1,(len b4)) &amp; b4 = smid (f,(((len f) -' (len b4)) + 1),(len f)) &amp; ( for j being Nat st j <= len g &amp; smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds
j <= len b4 ) ) );

theorem Th10: :: FINSEQ_8:10
for D being non empty set
for f, g being FinSequence of D holds len (ovlpart (f,g)) <= len f
proofend;

::Concatination Reducing Overlapping Part
definition
let D be non empty set ;
let f, g be FinSequence of D;
func ovlcon (f,g) ->  FinSequence of D equals :: FINSEQ_8:def 3
f ^ (g /^ (len (ovlpart (f,g))));
correctness
coherence
f ^ (g /^ (len (ovlpart (f,g)))) is FinSequence of D;
;
end;

:: deftheorem  defines ovlcon FINSEQ_8:def_3_:_
 for D being non empty set
for f, g being FinSequence of D holds ovlcon (f,g) = f ^ (g /^ (len (ovlpart (f,g))));

theorem Th11: :: FINSEQ_8:11
for D being non empty set
for f, g being FinSequence of D holds ovlcon (f,g) = (f | ((len f) -' (len (ovlpart (f,g))))) ^ g
proofend;

::Overlapping Left Difference
definition
let D be non empty set ;
let f, g be FinSequence of D;
func ovlldiff (f,g) ->  FinSequence of D equals :: FINSEQ_8:def 4
f | ((len f) -' (len (ovlpart (f,g))));
coherence
 f | ((len f) -' (len (ovlpart (f,g)))) is FinSequence of D ;
end;

:: deftheorem  defines ovlldiff FINSEQ_8:def_4_:_
 for D being non empty set
for f, g being FinSequence of D holds ovlldiff (f,g) = f | ((len f) -' (len (ovlpart (f,g))));

::Overlapping Right Difference
definition
let D be non empty set ;
let f, g be FinSequence of D;
func ovlrdiff (f,g) ->  FinSequence of D equals :: FINSEQ_8:def 5
g /^ (len (ovlpart (f,g)));
coherence
 g /^ (len (ovlpart (f,g))) is FinSequence of D ;
end;

:: deftheorem  defines ovlrdiff FINSEQ_8:def_5_:_
 for D being non empty set
for f, g being FinSequence of D holds ovlrdiff (f,g) = g /^ (len (ovlpart (f,g)));

theorem :: FINSEQ_8:12
for D being non empty set
for f, g being FinSequence of D holds
( ovlcon (f,g) = ((ovlldiff (f,g)) ^ (ovlpart (f,g))) ^ (ovlrdiff (f,g)) &amp; ovlcon (f,g) = (ovlldiff (f,g)) ^ ((ovlpart (f,g)) ^ (ovlrdiff (f,g))) )
proofend;

theorem :: FINSEQ_8:13
for D being non empty set
for f being FinSequence of D holds
( ovlcon (f,f) = f &amp; ovlpart (f,f) = f &amp; ovlldiff (f,f) = {} &amp; ovlrdiff (f,f) = {} )
proofend;

theorem :: FINSEQ_8:14
for D being non empty set
for f, g being FinSequence of D holds
( ovlpart ((f ^ g),g) = g &amp; ovlpart (f,(f ^ g)) = f )
proofend;

theorem Th15: :: FINSEQ_8:15
for D being non empty set
for f, g being FinSequence of D holds
( len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) &amp; len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) &amp; len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) )
proofend;

theorem Th16: :: FINSEQ_8:16
for D being non empty set
for f, g being FinSequence of D holds
( len (ovlpart (f,g)) <= len f &amp; len (ovlpart (f,g)) <= len g )
proofend;

definition
let D be non empty set ;
let CR be FinSequence of D;
predCR separates_uniquely  means :Def6: :: FINSEQ_8:def 6
 for f being FinSequence of D
for i, j being Element of NAT st 1 <= i &amp; i < j &amp; (j + (len CR)) -' 1 <= len f &amp; smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) &amp; smid (f,i,((i + (len CR)) -' 1)) = CR holds
j -' i >= len CR;
end;

:: deftheorem Def6 defines separates_uniquely FINSEQ_8:def_6_:_
 for D being non empty set
for CR being FinSequence of D holds
( CR separates_uniquely iff for f being FinSequence of D
for i, j being Element of NAT st 1 <= i &amp; i < j &amp; (j + (len CR)) -' 1 <= len f &amp; smid (f,i,((i + (len CR)) -' 1)) = smid (f,j,((j + (len CR)) -' 1)) &amp; smid (f,i,((i + (len CR)) -' 1)) = CR holds
j -' i >= len CR );

theorem :: FINSEQ_8:17
for D being non empty set
for CR being FinSequence of D holds
( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 )
proofend;

definition
let D be non empty set ;
let f, g be FinSequence of D;
let n be Element of NAT ;
predg is_substring_of f,n means :Def7: :: FINSEQ_8:def 7
( len g > 0 implies ex i being Element of NAT st
( n <= i &amp; i <= len f &amp; mid (f,i,((i -' 1) + (len g))) = g ) );
correctness
;
end;

:: deftheorem Def7 defines is_substring_of FINSEQ_8:def_7_:_
 for D being non empty set
for f, g being FinSequence of D
for n being Element of NAT holds
( g is_substring_of f,n iff ( len g > 0 implies ex i being Element of NAT st
( n <= i &amp; i <= len f &amp; mid (f,i,((i -' 1) + (len g))) = g ) ) );

theorem :: FINSEQ_8:18
for D being non empty set
for f, g being FinSequence of D
for n, m being Element of NAT st m >= n &amp; g is_substring_of f,m holds
g is_substring_of f,n
proofend;

theorem Th19: :: FINSEQ_8:19
for D being non empty set
for f being FinSequence of D st 1 <= len f holds
f is_substring_of f,1
proofend;

theorem Th20: :: FINSEQ_8:20
for D being non empty set
for f, g being FinSequence of D st g is_substring_of f, 0 holds
g is_substring_of f,1
proofend;

notation
let D be non empty set ;
let g, f be FinSequence of D;
synonym g is_preposition_of f for D c= g;
end;

definition
let D be non empty set ;
let g, f be FinSequence of D;
:: original:is_preposition_of
redefine predg c= f means :Def8: :: FINSEQ_8:def 8
( len g > 0 implies ( 1 <= len f &amp; mid (f,1,(len g)) = g ) );
compatibility
 ( f is_preposition_of iff ( len g > 0 implies ( 1 <= len f &amp; mid (f,1,(len g)) = g ) ) )
proofend;
end;

:: deftheorem Def8 defines c= FINSEQ_8:def_8_:_
 for D being non empty set
for g, f being FinSequence of D holds
( g c= f iff ( len g > 0 implies ( 1 <= len f &amp; mid (f,1,(len g)) = g ) ) );

theorem :: FINSEQ_8:21
for D being non empty set
for f, g being FinSequence of D st len g > 0 &amp; f is_preposition_of holds
g . 1 = f . 1
proofend;

definition
let D be non empty set ;
let f, g be FinSequence of D;
predg is_postposition_of f means :Def9: :: FINSEQ_8:def 9
 Rev f is_preposition_of ;
correctness
;
end;

:: deftheorem Def9 defines is_postposition_of FINSEQ_8:def_9_:_
 for D being non empty set
for f, g being FinSequence of D holds
( g is_postposition_of f iff Rev f is_preposition_of );

theorem Th22: :: FINSEQ_8:22
for D being non empty set
for f, g being FinSequence of D st len g = 0 holds
g is_postposition_of f
proofend;

theorem Th23: :: FINSEQ_8:23
for D being non empty set
for f, g being FinSequence of D st g is_postposition_of f holds
len g <= len f
proofend;

theorem :: FINSEQ_8:24
for D being non empty set
for f, g being FinSequence of D st g is_postposition_of f &amp; len g > 0 holds
( len g <= len f &amp; mid (f,(((len f) + 1) -' (len g)),(len f)) = g )
proofend;

theorem :: FINSEQ_8:25
for D being non empty set
for f, g being FinSequence of D st ( len g > 0 implies ( len g <= len f &amp; mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) holds
g is_postposition_of f
proofend;

theorem :: FINSEQ_8:26
for D being non empty set
for f, g being FinSequence of D st 1 <= len f &amp; f is_preposition_of holds
g is_substring_of f,1
proofend;

theorem Th27: :: FINSEQ_8:27
for D being non empty set
for f, g being FinSequence of D
for n being Element of NAT st not g is_substring_of f,n holds
for i being Element of NAT st n <= i &amp; 0 < i holds
mid (f,i,((i -' 1) + (len g))) <> g
proofend;

definition
let D be non empty set ;
let f, g be FinSequence of D;
let n be Element of NAT ;
func instr (n,f,g) ->  Element of NAT  means :Def10: :: FINSEQ_8:def 10
( ( it <> 0 implies ( n <= it &amp; f /^ (it -' 1) is_preposition_of &amp; ( for j being Element of NAT st j >= n &amp; j > 0 &amp; f /^ (j -' 1) is_preposition_of holds
j >= it ) ) ) &amp; ( it = 0 implies not g is_substring_of f,n ) );
existence
 ex b1 being Element of NAT st
( ( b1 <> 0 implies ( n <= b1 &amp; f /^ (b1 -' 1) is_preposition_of &amp; ( for j being Element of NAT st j >= n &amp; j > 0 &amp; f /^ (j -' 1) is_preposition_of holds
j >= b1 ) ) ) &amp; ( b1 = 0 implies not g is_substring_of f,n ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ( b1 <> 0 implies ( n <= b1 &amp; f /^ (b1 -' 1) is_preposition_of &amp; ( for j being Element of NAT st j >= n &amp; j > 0 &amp; f /^ (j -' 1) is_preposition_of holds
j >= b1 ) ) ) &amp; ( b1 = 0 implies not g is_substring_of f,n ) &amp; ( b2 <> 0 implies ( n <= b2 &amp; f /^ (b2 -' 1) is_preposition_of &amp; ( for j being Element of NAT st j >= n &amp; j > 0 &amp; f /^ (j -' 1) is_preposition_of holds
j >= b2 ) ) ) &amp; ( b2 = 0 implies not g is_substring_of f,n ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines instr FINSEQ_8:def_10_:_
 for D being non empty set
for f, g being FinSequence of D
for n, b5 being Element of NAT holds
( b5 = instr (n,f,g) iff ( ( b5 <> 0 implies ( n <= b5 &amp; f /^ (b5 -' 1) is_preposition_of &amp; ( for j being Element of NAT st j >= n &amp; j > 0 &amp; f /^ (j -' 1) is_preposition_of holds
j >= b5 ) ) ) &amp; ( b5 = 0 implies not g is_substring_of f,n ) ) );

definition
let D be non empty set ;
let f, CR be FinSequence of D;
func addcr (f,CR) ->  FinSequence of D equals :: FINSEQ_8:def 11
 ovlcon (f,CR);
correctness
coherence
ovlcon (f,CR) is FinSequence of D;
;
end;

:: deftheorem  defines addcr FINSEQ_8:def_11_:_
 for D being non empty set
for f, CR being FinSequence of D holds addcr (f,CR) = ovlcon (f,CR);

definition
let D be non empty set ;
let r, CR be FinSequence of D;
predr is_terminated_by CR means :Def12: :: FINSEQ_8:def 12
( len CR > 0 implies ( len r >= len CR &amp; instr (1,r,CR) = ((len r) + 1) -' (len CR) ) );
correctness
;
end;

:: deftheorem Def12 defines is_terminated_by FINSEQ_8:def_12_:_
 for D being non empty set
for r, CR being FinSequence of D holds
( r is_terminated_by CR iff ( len CR > 0 implies ( len r >= len CR &amp; instr (1,r,CR) = ((len r) + 1) -' (len CR) ) ) );

theorem :: FINSEQ_8:28
for D being non empty set
for f being FinSequence of D holds f is_terminated_by f
proofend;