:: FINSEQ_8 semantic presentation

theorem Th1: :: FINSEQ_8:1

for D being set
for f being FinSequence of D holds f | 0 = {}

proof end;

theorem Th2: :: FINSEQ_8:2

for D being set
for f being FinSequence of D holds f /^ 0 = f

proof end;

definition

let D be set ;
let f, g be FinSequence of D;
:: original: ^
redefine func f ^ g -> FinSequence of D;
correctness

proof end;

end;

theorem :: FINSEQ_8:3

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

proof end;

theorem Th4: :: FINSEQ_8:4

for D being set
for f being FinSequence of D
for i being Nat st i >= len f holds
f /^ i = <*> D

proof end;

theorem :: FINSEQ_8:5

for D being non empty set
for k1, k2 being Nat holds mid (<*> D),k1,k2 = <*> D

proof end;

definition

let D be set ;
let f be FinSequence of D;
let k1, k2 be Nat;
func smid f,k1,k2 -> FinSequence of D equals :: FINSEQ_8:def 1
(f /^ (k1 -' 1)) | ((k2 + 1) -' k1);
correctness ;

end;

:: deftheorem defines smid FINSEQ_8:def 1 :

theorem Th6: :: FINSEQ_8:6

for D being non empty set
for f being FinSequence of D
for k1, k2 being Nat st k1 <= k2 holds
smid f,k1,k2 = mid f,k1,k2

proof end;

theorem Th7: :: FINSEQ_8:7

for D being non empty set
for f being FinSequence of D
for k2 being Nat holds smid f,1,k2 = f | k2

proof end;

theorem Th8: :: FINSEQ_8:8

for D being non empty set
for f being FinSequence of D
for k2 being Nat st len f <= k2 holds
smid f,1,k2 = f

proof end;

theorem Th9: :: FINSEQ_8:9

for D being set
for f being FinSequence of D
for k1, k2 being Nat st k1 > k2 holds
( smid f,k1,k2 = {} & smid f,k1,k2 = <*> D )

proof end;

theorem :: FINSEQ_8:10

for D being set
for f being FinSequence of D
for k2 being Nat holds smid f,0,k2 = smid f,1,(k2 + 1)

proof end;

theorem Th11: :: FINSEQ_8:11

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

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ovlpart FINSEQ_8:def 2 :

theorem Th12: :: FINSEQ_8:12

for D being non empty set
for f, g being FinSequence of D holds len (ovlpart f,g) <= len f

proof end;

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 ;

end;

:: deftheorem defines ovlcon FINSEQ_8:def 3 :

theorem Th13: :: FINSEQ_8:13

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

proof end;

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

end;

:: deftheorem defines ovlldiff FINSEQ_8:def 4 :

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

end;

:: deftheorem defines ovlrdiff FINSEQ_8:def 5 :

theorem :: FINSEQ_8:14

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) & ovlcon f,g = (ovlldiff f,g) ^ ((ovlpart f,g) ^ (ovlrdiff f,g)) )

proof end;

theorem :: FINSEQ_8:15

for D being non empty set
for f being FinSequence of D holds
( ovlcon f,f = f & ovlpart f,f = f & ovlldiff f,f = {} & ovlrdiff f,f = {} )

proof end;

theorem :: FINSEQ_8:16

for D being non empty set
for f, g being FinSequence of D holds
( ovlpart (f ^ g),g = g & ovlpart f,(f ^ g) = f )

proof end;

theorem Th17: :: FINSEQ_8:17

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)) & len (ovlcon f,g) = ((len f) + (len g)) -' (len (ovlpart f,g)) & len (ovlcon f,g) = (len f) + ((len g) -' (len (ovlpart f,g))) )

proof end;

theorem Th18: :: FINSEQ_8:18

for D being non empty set
for f, g being FinSequence of D holds
( len (ovlpart f,g) <= len f & len (ovlpart f,g) <= len g )

proof end;

definition

let D be non empty set ;
let CR be FinSequence of D;
pred CR separates_uniquely means :Def6: :: FINSEQ_8:def 6
for f being FinSequence of D
for i, j being 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;

end;

:: deftheorem Def6 defines separates_uniquely FINSEQ_8:def 6 :

theorem :: FINSEQ_8:19

for D being non empty set
for CR being FinSequence of D holds
( CR separates_uniquely iff len (ovlpart (CR /^ 1),CR) = 0 )

proof end;

definition

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

end;

:: deftheorem Def7 defines is_substring_of FINSEQ_8:def 7 :

theorem :: FINSEQ_8:20

for D being non empty set
for f, g being FinSequence of D
for n being Nat st len g = 0 holds
g is_substring_of f,n by Def7;

theorem :: FINSEQ_8:21

for D being non empty set
for f, g being FinSequence of D
for n, m being Nat st m >= n & g is_substring_of f,m holds
g is_substring_of f,n

proof end;

theorem Th22: :: FINSEQ_8:22

for D being non empty set
for f being FinSequence of D st 1 <= len f holds
f is_substring_of f,1

proof end;

theorem Th23: :: FINSEQ_8:23

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

proof end;

definition

let D be non empty set ;
let f, g be FinSequence of D;
pred g is_preposition_of f means :Def8: :: FINSEQ_8:def 8
( len g > 0 implies ( 1 <= len f & mid f,1,(len g) = g ) );
correctness ;

end;

:: deftheorem Def8 defines is_preposition_of FINSEQ_8:def 8 :

theorem :: FINSEQ_8:24

for D being non empty set
for f, g being FinSequence of D st len g = 0 holds
g is_preposition_of f by Def8;

theorem Th25: :: FINSEQ_8:25

for D being non empty set
for f being FinSequence of D holds f is_preposition_of f

proof end;

theorem Th26: :: FINSEQ_8:26

for D being non empty set
for f, g being FinSequence of D st g is_preposition_of f holds
len g <= len f

proof end;

theorem :: FINSEQ_8:27

for D being non empty set
for f, g being FinSequence of D st len g > 0 & g is_preposition_of f holds
g . 1 = f . 1

proof end;

definition

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

end;

:: deftheorem Def9 defines is_postposition_of FINSEQ_8:def 9 :

theorem Th28: :: FINSEQ_8:28

for D being non empty set
for f, g being FinSequence of D st len g = 0 holds
g is_postposition_of f

proof end;

theorem Th29: :: FINSEQ_8:29

for D being non empty set
for f, g being FinSequence of D st g is_postposition_of f holds
len g <= len f

proof end;

theorem :: FINSEQ_8:30

for D being non empty set
for f, g being FinSequence of D st g is_postposition_of f & len g > 0 holds
( len g <= len f & mid f,(((len f) + 1) -' (len g)),(len f) = g )

proof end;

theorem :: FINSEQ_8:31

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

proof end;

theorem :: FINSEQ_8:32

for D being non empty set
for f, g being FinSequence of D st len g = 0 holds
g is_preposition_of f by Def8;

theorem :: FINSEQ_8:33

for D being non empty set
for f, g being FinSequence of D st 1 <= len f & g is_preposition_of f holds
g is_substring_of f,1

proof end;

theorem Th34: :: FINSEQ_8:34

for D being non empty set
for f, g being FinSequence of D
for n being Nat st not g is_substring_of f,n holds
for i being Nat st n <= i & 0 < i holds
mid f,i,((i -' 1) + (len g)) <> g

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines instr FINSEQ_8:def 10 :

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 ;

end;

:: deftheorem defines addcr FINSEQ_8:def 11 :

definition

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

end;

:: deftheorem Def12 defines is_terminated_by FINSEQ_8:def 12 :

theorem :: FINSEQ_8:35

for D being non empty set
for f being FinSequence of D holds f is_terminated_by f

proof end;