:: FINSEQ_8 semantic presentation

theorem Th1: :: FINSEQ_8:1

for b₁ being set
for b₂ being FinSequence of b₁ holds b₂ | 0 = {}

proof end;

theorem Th2: :: FINSEQ_8:2

for b₁ being set
for b₂ being FinSequence of b₁ holds b₂ /^ 0 = b₂

proof end;

definition

let c₁ be set ;
let c₂, c₃ be FinSequence of c₁;
redefine func ^ as c₂ ^ c₃ -> FinSequence of a₁;
correctness

proof end;

end;

theorem Th3: :: FINSEQ_8:3

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st len b₂ >= 1 holds
mid (b₂ ^ b₃),1,(len b₂) = b₂

proof end;

theorem Th4: :: FINSEQ_8:4

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being Nat st b₃ >= len b₂ holds
b₂ /^ b₃ = <*> b₁

proof end;

theorem Th5: :: FINSEQ_8:5

for b₁ being non empty set
for b₂, b₃ being Nat holds mid (<*> b₁),b₂,b₃ = <*> b₁

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃, c₄ be Nat;
func smid c₂,c₃,c₄ -> FinSequence of a₁ equals :: FINSEQ_8:def 1
(a₂ /^ (a₃ -' 1)) | ((a₄ + 1) -' a₃);
correctness ;

end;

:: deftheorem Def1 defines smid FINSEQ_8:def 1 :

theorem Th6: :: FINSEQ_8:6

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
smid b₂,b₃,b₄ = mid b₂,b₃,b₄

proof end;

theorem Th7: :: FINSEQ_8:7

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat holds smid b₂,1,b₃ = b₂ | b₃

proof end;

theorem Th8: :: FINSEQ_8:8

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st len b₂ <= b₃ holds
smid b₂,1,b₃ = b₂

proof end;

theorem Th9: :: FINSEQ_8:9

for b₁ being set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st b₃ > b₄ holds
( smid b₂,b₃,b₄ = {} & smid b₂,b₃,b₄ = <*> b₁ )

proof end;

theorem Th10: :: FINSEQ_8:10

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being Nat holds smid b₂,0,b₃ = smid b₂,1,(b₃ + 1)

proof end;

theorem Th11: :: FINSEQ_8:11

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds smid (b₂ ^ b₃),((len b₂) + 1),((len b₂) + (len b₃)) = b₃

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
func ovlpart c₂,c₃ -> FinSequence of a₁ means :Def2: :: FINSEQ_8:def 2
( len a₄ <= len a₃ & a₄ = smid a₃,1,(len a₄) & a₄ = smid a₂,(((len a₂) -' (len a₄)) + 1),(len a₂) & ( for b₁ being Nat st b₁ <= len a₃ & smid a₃,1,b₁ = smid a₂,(((len a₂) -' b₁) + 1),(len a₂) holds
b₁ <= len a₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ovlpart FINSEQ_8:def 2 :

theorem Th12: :: FINSEQ_8:12

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds len (ovlpart b₂,b₃) <= len b₂

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
func ovlcon c₂,c₃ -> FinSequence of a₁ equals :: FINSEQ_8:def 3
a₂ ^ (a₃ /^ (len (ovlpart a₂,a₃)));
correctness ;

end;

:: deftheorem Def3 defines ovlcon FINSEQ_8:def 3 :

theorem Th13: :: FINSEQ_8:13

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds ovlcon b₂,b₃ = (b₂ | ((len b₂) -' (len (ovlpart b₂,b₃)))) ^ b₃

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
func ovlldiff c₂,c₃ -> FinSequence of a₁ equals :: FINSEQ_8:def 4
a₂ | ((len a₂) -' (len (ovlpart a₂,a₃)));
correctness ;

end;

:: deftheorem Def4 defines ovlldiff FINSEQ_8:def 4 :

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
func ovlrdiff c₂,c₃ -> FinSequence of a₁ equals :: FINSEQ_8:def 5
a₃ /^ (len (ovlpart a₂,a₃));
correctness ;

end;

:: deftheorem Def5 defines ovlrdiff FINSEQ_8:def 5 :

theorem Th14: :: FINSEQ_8:14

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds
( ovlcon b₂,b₃ = ((ovlldiff b₂,b₃) ^ (ovlpart b₂,b₃)) ^ (ovlrdiff b₂,b₃) & ovlcon b₂,b₃ = (ovlldiff b₂,b₃) ^ ((ovlpart b₂,b₃) ^ (ovlrdiff b₂,b₃)) )

proof end;

theorem Th15: :: FINSEQ_8:15

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds
( ovlcon b₂,b₂ = b₂ & ovlpart b₂,b₂ = b₂ & ovlldiff b₂,b₂ = {} & ovlrdiff b₂,b₂ = {} )

proof end;

theorem Th16: :: FINSEQ_8:16

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds
( ovlpart (b₂ ^ b₃),b₃ = b₃ & ovlpart b₂,(b₂ ^ b₃) = b₂ )

proof end;

theorem Th17: :: FINSEQ_8:17

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds
( len (ovlcon b₂,b₃) = ((len b₂) + (len b₃)) - (len (ovlpart b₂,b₃)) & len (ovlcon b₂,b₃) = ((len b₂) + (len b₃)) -' (len (ovlpart b₂,b₃)) & len (ovlcon b₂,b₃) = (len b₂) + ((len b₃) -' (len (ovlpart b₂,b₃))) )

proof end;

theorem Th18: :: FINSEQ_8:18

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds
( len (ovlpart b₂,b₃) <= len b₂ & len (ovlpart b₂,b₃) <= len b₃ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
pred c₂ separates_uniquely means :Def6: :: FINSEQ_8:def 6
for b₁ being FinSequence of a₁
for b₂, b₃ being Nat st 1 <= b₂ & b₂ < b₃ & (b₃ + (len a₂)) -' 1 <= len b₁ & smid b₁,b₂,((b₂ + (len a₂)) -' 1) = smid b₁,b₃,((b₃ + (len a₂)) -' 1) & smid b₁,b₂,((b₂ + (len a₂)) -' 1) = a₂ holds
b₃ -' b₂ >= len a₂;

end;

:: deftheorem Def6 defines separates_uniquely FINSEQ_8:def 6 :

theorem Th19: :: FINSEQ_8:19

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

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
let c₄ be Nat;
pred c₃ is_substring_of c₂,c₄ means :Def7: :: FINSEQ_8:def 7
( len a₃ > 0 implies ex b₁ being Nat st
( a₄ <= b₁ & b₁ <= len a₂ & mid a₂,b₁,((b₁ -' 1) + (len a₃)) = a₃ ) );
correctness ;

end;

:: deftheorem Def7 defines is_substring_of FINSEQ_8:def 7 :

theorem Th20: :: FINSEQ_8:20

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being Nat st len b₃ = 0 holds
b₃ is_substring_of b₂,b₄ by Def7;

theorem Th21: :: FINSEQ_8:21

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄, b₅ being Nat st b₅ >= b₄ & b₃ is_substring_of b₂,b₅ holds
b₃ is_substring_of b₂,b₄

proof end;

theorem Th22: :: FINSEQ_8:22

for b₁ being non empty set
for b₂ being FinSequence of b₁ st 1 <= len b₂ holds
b₂ is_substring_of b₂,1

proof end;

theorem Th23: :: FINSEQ_8:23

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₃ is_substring_of b₂,0 holds
b₃ is_substring_of b₂,1

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
pred c₃ is_preposition_of c₂ means :Def8: :: FINSEQ_8:def 8
( len a₃ > 0 implies ( 1 <= len a₂ & mid a₂,1,(len a₃) = a₃ ) );
correctness ;

end;

:: deftheorem Def8 defines is_preposition_of FINSEQ_8:def 8 :

theorem Th24: :: FINSEQ_8:24

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st len b₃ = 0 holds
b₃ is_preposition_of b₂ by Def8;

theorem Th25: :: FINSEQ_8:25

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds b₂ is_preposition_of b₂

proof end;

theorem Th26: :: FINSEQ_8:26

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₃ is_preposition_of b₂ holds
len b₃ <= len b₂

proof end;

theorem Th27: :: FINSEQ_8:27

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st len b₃ > 0 & b₃ is_preposition_of b₂ holds
b₃ . 1 = b₂ . 1

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
pred c₃ is_postposition_of c₂ means :Def9: :: FINSEQ_8:def 9
Rev a₃ is_preposition_of Rev a₂;
correctness ;

end;

:: deftheorem Def9 defines is_postposition_of FINSEQ_8:def 9 :

theorem Th28: :: FINSEQ_8:28

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st len b₃ = 0 holds
b₃ is_postposition_of b₂

proof end;

theorem Th29: :: FINSEQ_8:29

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₃ is_postposition_of b₂ holds
len b₃ <= len b₂

proof end;

theorem Th30: :: FINSEQ_8:30

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₃ is_postposition_of b₂ & len b₃ > 0 holds
( len b₃ <= len b₂ & mid b₂,(((len b₂) + 1) -' (len b₃)),(len b₂) = b₃ )

proof end;

theorem Th31: :: FINSEQ_8:31

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st ( len b₃ > 0 implies ( len b₃ <= len b₂ & mid b₂,(((len b₂) + 1) -' (len b₃)),(len b₂) = b₃ ) ) holds
b₃ is_postposition_of b₂

proof end;

theorem Th32: :: FINSEQ_8:32

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st len b₃ = 0 holds
b₃ is_preposition_of b₂ by Def8;

theorem Th33: :: FINSEQ_8:33

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st 1 <= len b₂ & b₃ is_preposition_of b₂ holds
b₃ is_substring_of b₂,1

proof end;

theorem Th34: :: FINSEQ_8:34

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being Nat st not b₃ is_substring_of b₂,b₄ holds
for b₅ being Nat st b₄ <= b₅ & 0 < b₅ holds
mid b₂,b₅,((b₅ -' 1) + (len b₃)) <> b₃

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
let c₄ be Nat;
func instr c₄,c₂,c₃ -> Nat means :Def10: :: FINSEQ_8:def 10
( ( a₅ <> 0 implies ( a₄ <= a₅ & a₃ is_preposition_of a₂ /^ (a₅ -' 1) & ( for b₁ being Nat st b₁ >= a₄ & b₁ > 0 & a₃ is_preposition_of a₂ /^ (b₁ -' 1) holds
b₁ >= a₅ ) ) ) & ( a₅ = 0 implies not a₃ is_substring_of a₂,a₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines instr FINSEQ_8:def 10 :

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
func addcr c₂,c₃ -> FinSequence of a₁ equals :: FINSEQ_8:def 11
ovlcon a₂,a₃;
correctness ;

end;

:: deftheorem Def11 defines addcr FINSEQ_8:def 11 :

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
pred c₂ is_terminated_by c₃ means :Def12: :: FINSEQ_8:def 12
( len a₃ > 0 implies ( len a₂ >= len a₃ & instr 1,a₂,a₃ = ((len a₂) + 1) -' (len a₃) ) );
correctness ;

end;

:: deftheorem Def12 defines is_terminated_by FINSEQ_8:def 12 :

theorem Th35: :: FINSEQ_8:35

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds b₂ is_terminated_by b₂

proof end;