:: Concatenation of Finite Sequences Reducing Overlapping Part and anArgument of Separators of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: FINSEQ_8:1
theorem Th2: :: FINSEQ_8:2
theorem :: FINSEQ_8:3
:: deftheorem defines smid FINSEQ_8:def 1 :
theorem Th4: :: FINSEQ_8:4
theorem Th5: :: FINSEQ_8:5
theorem Th6: :: FINSEQ_8:6
theorem Th7: :: FINSEQ_8:7
theorem :: FINSEQ_8:8
theorem Th9: :: FINSEQ_8:9
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 &
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: :: FINSEQ_8:10
:: deftheorem defines ovlcon FINSEQ_8:def 3 :
theorem Th11: :: FINSEQ_8:11
:: deftheorem defines ovlldiff FINSEQ_8:def 4 :
:: deftheorem defines ovlrdiff FINSEQ_8:def 5 :
theorem :: FINSEQ_8:12
theorem :: FINSEQ_8:13
theorem :: FINSEQ_8:14
theorem Th15: :: FINSEQ_8:15
theorem Th16: :: FINSEQ_8:16
:: deftheorem Def6 defines separates_uniquely FINSEQ_8:def 6 :
theorem :: FINSEQ_8:17
:: deftheorem Def7 defines is_substring_of FINSEQ_8:def 7 :
theorem :: FINSEQ_8:18
theorem Th19: :: FINSEQ_8:19
theorem Th20: :: FINSEQ_8:20
:: deftheorem Def8 defines c= FINSEQ_8:def 8 :
theorem :: FINSEQ_8:21
:: deftheorem Def9 defines is_postposition_of FINSEQ_8:def 9 :
theorem Th22: :: FINSEQ_8:22
theorem Th23: :: FINSEQ_8:23
theorem :: FINSEQ_8:24
theorem :: FINSEQ_8:25
theorem :: FINSEQ_8:26
theorem Th27: :: FINSEQ_8:27
:: 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 :: FINSEQ_8:28