begin
theorem
theorem Th2:
theorem
:: deftheorem defines smid FINSEQ_8:def 1 :
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 :
theorem Th11:
:: deftheorem defines ovlldiff FINSEQ_8:def 4 :
:: deftheorem defines ovlrdiff FINSEQ_8:def 5 :
theorem
theorem
theorem
theorem Th15:
theorem Th16:
:: deftheorem Def6 defines separates_uniquely FINSEQ_8:def 6 :
theorem
:: deftheorem Def7 defines is_substring_of FINSEQ_8:def 7 :
theorem
theorem Th19:
theorem Th20:
:: deftheorem Def8 defines c= FINSEQ_8:def 8 :
theorem
:: deftheorem Def9 defines is_postposition_of FINSEQ_8:def 9 :
theorem Th22:
theorem Th23:
theorem
theorem
theorem
theorem Th27:
:: deftheorem Def10 defines instr FINSEQ_8:def 10 :
:: deftheorem defines addcr FINSEQ_8:def 11 :
:: deftheorem Def12 defines is_terminated_by FINSEQ_8:def 12 :
theorem