:: by Hirofumi Fukura and Yatsuka Nakamura

::

:: Received March 18, 2004

:: Copyright (c) 2004-2018 Association of Mizar Users

definition

let f be FinSequence;

let k1, k2 be Nat;

correctness

coherence

(f /^ (k1 -' 1)) | ((k2 + 1) -' k1) is FinSequence;

;

end;
let k1, k2 be Nat;

correctness

coherence

(f /^ (k1 -' 1)) | ((k2 + 1) -' k1) is FinSequence;

;

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

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;

end;
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;

proof end;

:: Overlapping Part

definition

let D be non empty set ;

let f, g be FinSequence of D;

ex b_{1} being FinSequence of D st

( len b_{1} <= len g & b_{1} = smid (g,1,(len b_{1})) & b_{1} = smid (f,(((len f) -' (len b_{1})) + 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 b_{1} ) )

for b_{1}, b_{2} being FinSequence of D st len b_{1} <= len g & b_{1} = smid (g,1,(len b_{1})) & b_{1} = smid (f,(((len f) -' (len b_{1})) + 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 b_{1} ) & len b_{2} <= len g & b_{2} = smid (g,1,(len b_{2})) & b_{2} = smid (f,(((len f) -' (len b_{2})) + 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 b_{2} ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( len b

j <= len b

proof end;

uniqueness for b

j <= len b

j <= len b

b

proof end;

:: deftheorem Def2 defines ovlpart FINSEQ_8:def 2 :

for D being non empty set

for f, g, b_{4} being FinSequence of D holds

( b_{4} = ovlpart (f,g) iff ( len b_{4} <= len g & b_{4} = smid (g,1,(len b_{4})) & b_{4} = smid (f,(((len f) -' (len b_{4})) + 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 b_{4} ) ) );

for D being non empty set

for f, g, b

( b

j <= len b

:: Concatenation Reducing Overlapping Part

definition

let D be non empty set ;

let f, g be FinSequence of D;

coherence

f ^ (g /^ (len (ovlpart (f,g)))) is FinSequence of D ;

end;
let f, g be FinSequence of D;

coherence

f ^ (g /^ (len (ovlpart (f,g)))) is FinSequence of D ;

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

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

for f, g being FinSequence of D holds ovlcon (f,g) = (f | ((len f) -' (len (ovlpart (f,g))))) ^ g

proof end;

::Overlapping Left Difference

definition

let D be non empty set ;

let f, g be FinSequence of D;

f | ((len f) -' (len (ovlpart (f,g)))) is FinSequence of D ;

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

f | ((len f) -' (len (ovlpart (f,g)))) is FinSequence of D ;

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

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;

coherence

g /^ (len (ovlpart (f,g))) is FinSequence of D ;

end;
let f, g be FinSequence of D;

coherence

g /^ (len (ovlpart (f,g))) is FinSequence of D ;

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

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

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:13

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) = {} )

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:14

for D being non empty set

for f, g being FinSequence of D holds

( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f )

for f, g being FinSequence of D holds

( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f )

proof end;

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

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 Th16: :: FINSEQ_8:16

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 )

for f, g being FinSequence of D holds

( len (ovlpart (f,g)) <= len f & len (ovlpart (f,g)) <= len g )

proof end;

:: deftheorem 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 );

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 :: 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 )

for CR being FinSequence of D holds

( CR separates_uniquely iff len (ovlpart ((CR /^ 1),CR)) = 0 )

proof end;

:: deftheorem defines is_substring_of FINSEQ_8:def 7 :

for f, g being FinSequence

for n being Nat holds

( g is_substring_of f,n iff ( len g > 0 implies ex i being Nat st

( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );

for f, g being FinSequence

for n being Nat holds

( g is_substring_of f,n iff ( len g > 0 implies ex i being Nat st

( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );

theorem :: FINSEQ_8:18

for f, g being FinSequence

for n, m being Nat st m >= n & g is_substring_of f,m holds

g is_substring_of f,n

for n, m being Nat st m >= n & g is_substring_of f,m holds

g is_substring_of f,n

proof end;

definition

let g, f be FinSequence;

( g is_preposition_of f iff ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) )

end;
redefine pred g c= f means :: FINSEQ_8:def 8

( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) );

compatibility ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) );

( g is_preposition_of f iff ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) )

proof end;

:: deftheorem defines is_preposition_of FINSEQ_8:def 8 :

for g, f being FinSequence holds

( g is_preposition_of f iff ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) );

for g, f being FinSequence holds

( g is_preposition_of f iff ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) );

:: deftheorem defines is_postposition_of FINSEQ_8:def 9 :

for f, g being FinSequence holds

( g is_postposition_of f iff Rev g is_preposition_of Rev f );

for f, g being FinSequence holds

( g is_postposition_of f iff Rev g is_preposition_of Rev f );

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

for f, g being FinSequence of D st g is_postposition_of f holds

len g <= len f

proof end;

theorem :: FINSEQ_8:24

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 )

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:25

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

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 Th27: :: FINSEQ_8:27

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 Element of NAT st n <= i & 0 < i holds

mid (f,i,((i -' 1) + (len g))) <> g

for f, g being FinSequence of D

for n being Nat st not g is_substring_of f,n holds

for i being Element of 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;

ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )

for b_{1}, b_{2} being Element of NAT st ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) & ( b_{2} <> 0 implies ( n <= b_{2} & g is_preposition_of f /^ (b_{2} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{2} ) ) ) & ( b_{2} = 0 implies not g is_substring_of f,n ) holds

b_{1} = b_{2}

end;
let f, g be FinSequence of D;

let n be Nat;

func instr (n,f,g) -> Element of NAT means :Def10: :: FINSEQ_8:def 10

( ( it <> 0 implies ( n <= it & g is_preposition_of f /^ (it -' 1) & ( for j being Element of 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 ( ( it <> 0 implies ( n <= it & g is_preposition_of f /^ (it -' 1) & ( for j being Element of 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 ) );

ex b

( ( b

j >= b

proof end;

uniqueness for b

j >= b

j >= b

b

proof end;

:: deftheorem Def10 defines instr FINSEQ_8:def 10 :

for D being non empty set

for f, g being FinSequence of D

for n being Nat

for b_{5} being Element of NAT holds

( b_{5} = instr (n,f,g) iff ( ( b_{5} <> 0 implies ( n <= b_{5} & g is_preposition_of f /^ (b_{5} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{5} ) ) ) & ( b_{5} = 0 implies not g is_substring_of f,n ) ) );

for D being non empty set

for f, g being FinSequence of D

for n being Nat

for b

( b

j >= b

definition

let D be non empty set ;

let f, CR be FinSequence of D;

correctness

coherence

ovlcon (f,CR) is FinSequence of D;

;

end;
let f, CR be FinSequence of D;

correctness

coherence

ovlcon (f,CR) is FinSequence of D;

;

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

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;

;

end;
let r, CR be FinSequence of D;

pred r is_terminated_by CR means :: FINSEQ_8:def 12

( len CR > 0 implies ( len r >= len CR & instr (1,r,CR) = ((len r) + 1) -' (len CR) ) );

correctness ( len CR > 0 implies ( len r >= len CR & instr (1,r,CR) = ((len r) + 1) -' (len CR) ) );

;

:: deftheorem 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) ) ) );

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 :: FINSEQ_8:29

for f being FinSequence

for k1, k2 being Nat st k1 in dom f & k2 in dom f holds

smid (f,k1,k2) = (k1,k2) -cut f

for k1, k2 being Nat st k1 in dom f & k2 in dom f holds

smid (f,k1,k2) = (k1,k2) -cut f

proof end;