begin
theorem
theorem Th2:
theorem
:: 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);
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
definition
let D be non
empty set ;
let f,
g be
FinSequence of
D;
func ovlpart f,
g -> FinSequence of
D means :
Def2:
(
len it <= len g &
it = smid g,1,
(len it) &
it = smid f,
(((len f) -' (len it)) + 1),
(len f) & ( for
j being
Nat st
j <= len g &
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 & b1 = smid g,1,(len b1) & b1 = smid f,(((len f) -' (len b1)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len b1 ) )
uniqueness
for b1, b2 being FinSequence of D st len b1 <= len g & b1 = smid g,1,(len b1) & b1 = smid f,(((len f) -' (len b1)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len b1 ) & len b2 <= len g & b2 = smid g,1,(len b2) & b2 = smid f,(((len f) -' (len b2)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len b2 ) holds
b1 = b2
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 & b4 = smid g,1,(len b4) & b4 = smid f,(((len f) -' (len b4)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len b4 ) ) );
theorem Th10:
:: 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:
:: 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)));
:: 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
theorem
theorem
theorem Th15:
theorem Th16:
:: 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 & i < j & (j + (len CR)) -' 1 <= len f & smid f,i,((i + (len CR)) -' 1) = smid f,j,((j + (len CR)) -' 1) & smid f,i,((i + (len CR)) -' 1) = CR holds
j -' i >= len CR );
theorem
:: 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 & i <= len f & mid f,i,((i -' 1) + (len g)) = g ) ) );
theorem
theorem Th19:
theorem Th20:
:: 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 & mid f,1,(len g) = g ) ) );
theorem
:: 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:
theorem Th23:
theorem
theorem
theorem
theorem Th27:
:: 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 & f /^ (b5 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= b5 ) ) ) & ( b5 = 0 implies not g is_substring_of f,n ) ) );
:: 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;
:: 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 & instr 1,r,CR = ((len r) + 1) -' (len CR) ) ) );
theorem