:: FILEREC1 semantic presentation

theorem Th1: :: FILEREC1:1

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

proof end;

theorem Th2: :: FILEREC1:2

for b₁ being set
for b₂ being FinSequence of b₁ holds b₂ | (len b₂) = b₂

proof end;

theorem Th3: :: FILEREC1:3

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

proof end;

theorem Th4: :: FILEREC1:4

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
len (b₂ /^ b₄) <= len (b₂ /^ b₃)

proof end;

theorem Th5: :: FILEREC1:5

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

proof end;

theorem Th6: :: FILEREC1:6

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄, b₅ being Nat st 1 <= b₄ & b₄ <= b₅ & b₅ <= len b₂ holds
mid (b₂ ^ b₃),b₄,b₅ = mid b₂,b₄,b₅

proof end;

theorem Th7: :: FILEREC1:7

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄, b₅ being Nat st 1 <= b₃ & b₃ <= b₄ & b₃ <= len (b₂ | b₅) & b₄ <= len (b₂ | b₅) holds
mid b₂,b₃,b₄ = mid (b₂ | b₅),b₃,b₄

proof end;

theorem Th8: :: FILEREC1:8

for b₁ being set
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₃ = <*b₁*> holds
b₁ in b₂

proof end;

theorem Th9: :: FILEREC1:9

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₄ = <*b₁,b₂*> holds
( b₁ in b₃ & b₂ in b₃ )

proof end;

theorem Th10: :: FILEREC1:10

for b₁, b₂, b₃ being set
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₅ = <*b₁,b₂,b₃*> holds
( b₁ in b₄ & b₂ in b₄ & b₃ in b₄ )

proof end;

theorem Th11: :: FILEREC1:11

for b₁ being set
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₃ = <*b₁*> holds
b₃ | 1 = <*b₁*>

proof end;

theorem Th12: :: FILEREC1:12

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₄ = <*b₁,b₂*> holds
b₄ /^ 1 = <*b₂*>

proof end;

theorem Th13: :: FILEREC1:13

for b₁, b₂, b₃ being set
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₅ = <*b₁,b₂,b₃*> holds
b₅ | 1 = <*b₁*>

proof end;

theorem Th14: :: FILEREC1:14

for b₁, b₂, b₃ being set
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₅ = <*b₁,b₂,b₃*> holds
b₅ | 2 = <*b₁,b₂*>

proof end;

theorem Th15: :: FILEREC1:15

for b₁, b₂, b₃ being set
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₅ = <*b₁,b₂,b₃*> holds
b₅ /^ 1 = <*b₂,b₃*>

proof end;

theorem Th16: :: FILEREC1:16

for b₁, b₂, b₃ being set
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₅ = <*b₁,b₂,b₃*> holds
b₅ /^ 2 = <*b₃*>

proof end;

theorem Th17: :: FILEREC1:17

for b₁ being non empty set
for b₂ being FinSequence of b₁ st len b₂ = 0 holds
Rev b₂ = b₂

proof end;

theorem Th18: :: FILEREC1:18

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st b₃ <= len b₂ holds
Rev (b₂ /^ b₃) = (Rev b₂) | ((len b₂) -' b₃)

proof end;

theorem Th19: :: FILEREC1:19

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st not b₃ is_substring_of b₂,1 & b₃ separates_uniquely holds
instr 1,(b₂ ^ b₃),b₃ = (len b₂) + 1

proof end;

theorem Th20: :: FILEREC1:20

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ holds b₃ is_preposition_of (b₂ ^ b₃) /^ (len b₂)

proof end;

theorem Th21: :: FILEREC1:21

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st not b₃ is_substring_of b₂,1 & b₃ separates_uniquely holds
b₂ ^ b₃ is_terminated_by b₃

proof end;

notation

let c₁ be set ;
synonym File of c₁ for FinSequence of c₁;

end;

definition

let c₁ be non empty set ;
let c₂, c₃, c₄ be File of c₁;
pred c₂ is_a_record_of c₃,c₄ means :Def1: :: FILEREC1:def 1
( ( a₄ ^ a₂ is_substring_of addcr a₃,a₄,1 or a₂ is_preposition_of addcr a₃,a₄ ) & a₂ is_terminated_by a₄ );

end;

:: deftheorem Def1 defines is_a_record_of FILEREC1:def 1 :

theorem Th22: :: FILEREC1:22

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

proof end;

theorem Th23: :: FILEREC1:23

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds b₂ is_a_record_of <*> b₁,b₂

proof end;

theorem Th24: :: FILEREC1:24

for b₁ being non empty set
for b₂, b₃ being set
for b₄, b₅, b₆ being File of b₁ st b₂ <> b₃ & b₁ = {b₂,b₃} & b₆ = <*b₃*> & b₄ = <*b₃,b₂,b₃*> & b₅ = <*b₂,b₃*> holds
( b₆ is_a_record_of b₄,b₆ & b₅ is_a_record_of b₄,b₆ )

proof end;

theorem Th25: :: FILEREC1:25

for b₁ being non empty set
for b₂, b₃ being File of b₁ holds b₂ is_preposition_of b₂ ^ b₃

proof end;

theorem Th26: :: FILEREC1:26

for b₁ being non empty set
for b₂, b₃ being File of b₁ holds b₂ is_preposition_of addcr b₂,b₃

proof end;

theorem Th27: :: FILEREC1:27

for b₁ being non empty set
for b₂, b₃ being File of b₁ st b₃ is_postposition_of b₂ holds
0 <= (len b₂) - (len b₃)

proof end;

theorem Th28: :: FILEREC1:28

for b₁ being non empty set
for b₂, b₃ being File of b₁ st b₂ is_postposition_of b₃ holds
b₃ = addcr b₃,b₂

proof end;

theorem Th29: :: FILEREC1:29

for b₁ being non empty set
for b₂, b₃ being File of b₁ st b₃ is_terminated_by b₂ holds
b₃ = addcr b₃,b₂

proof end;

theorem Th30: :: FILEREC1:30

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

proof end;

theorem Th31: :: FILEREC1:31

for b₁ being non empty set
for b₂, b₃ being File of b₁ holds
( len (addcr b₂,b₃) >= len b₂ & len (addcr b₂,b₃) >= len b₃ )

proof end;

theorem Th32: :: FILEREC1:32

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

proof end;

theorem Th33: :: FILEREC1:33

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

proof end;

theorem Th34: :: FILEREC1:34

for b₁ being non empty set
for b₂, b₃ being File of b₁ holds addcr b₃,b₂ = (ovlldiff b₃,b₂) ^ b₂

proof end;

theorem Th35: :: FILEREC1:35

for b₁ being non empty set
for b₂, b₃, b₄ being File of b₁ st b₄ = b₂ ^ b₃ holds
( b₂ is_substring_of b₄,1 & b₃ is_substring_of b₄,1 )

proof end;

theorem Th36: :: FILEREC1:36

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being File of b₁ st b₅ = (b₂ ^ b₃) ^ b₄ holds
( b₂ is_substring_of b₅,1 & b₃ is_substring_of b₅,1 & b₄ is_substring_of b₅,1 )

proof end;

theorem Th37: :: FILEREC1:37

for b₁ being non empty set
for b₂, b₃, b₄ being File of b₁ st b₃ is_terminated_by b₂ & b₄ is_terminated_by b₂ holds
b₂ ^ b₄ is_substring_of addcr (b₃ ^ b₄),b₂,1

proof end;

theorem Th38: :: FILEREC1:38

for b₁ being non empty set
for b₂, b₃ being File of b₁
for b₄ being Nat st 0 < b₄ & b₃ = {} holds
instr b₄,b₂,b₃ = b₄

proof end;

theorem Th39: :: FILEREC1:39

for b₁ being non empty set
for b₂, b₃ being File of b₁
for b₄ being Nat st 0 < b₄ & b₄ <= len b₂ holds
instr b₄,b₂,b₃ <= len b₂

proof end;

theorem Th40: :: FILEREC1:40

for b₁ being non empty set
for b₂, b₃ being File of b₁ holds b₃ is_substring_of ovlcon b₂,b₃,1

proof end;

theorem Th41: :: FILEREC1:41

for b₁ being non empty set
for b₂, b₃ being File of b₁ holds b₃ is_substring_of addcr b₂,b₃,1

proof end;

theorem Th42: :: FILEREC1:42

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being Nat st b₃ is_substring_of b₂ | b₄,1 & len b₃ > 0 & len b₃ <= b₄ holds
b₃ is_substring_of b₂,1

proof end;

theorem Th43: :: FILEREC1:43

for b₁ being non empty set
for b₂, b₃ being File of b₁ ex b₄ being File of b₁ st b₄ is_a_record_of b₂,b₃

proof end;

theorem Th44: :: FILEREC1:44

for b₁ being non empty set
for b₂, b₃, b₄ being File of b₁ st b₄ is_a_record_of b₂,b₃ holds
b₄ is_a_record_of b₄,b₃

proof end;

theorem Th45: :: FILEREC1:45

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being File of b₁ st b₃ is_terminated_by b₂ & b₄ is_terminated_by b₂ & b₅ = b₃ ^ b₄ holds
( b₃ is_a_record_of b₅,b₂ & b₄ is_a_record_of b₅,b₂ )

proof end;