:: FINSEQ_5 semantic presentation

theorem Th1: :: FINSEQ_5:1

for b₁, b₂ being Nat st b₁ <= b₂ holds
(b₂ - b₁) + 1 is Nat

proof end;

theorem Th2: :: FINSEQ_5:2

for b₁, b₂ being Nat st b₁ in Seg b₂ holds
(b₂ - b₁) + 1 in Seg b₂

proof end;

theorem Th3: :: FINSEQ_5:3

for b₁ being Function
for b₂, b₃ being set st b₁ " {b₃} = {b₂} holds
( b₂ in dom b₁ & b₃ in rng b₁ & b₁ . b₂ = b₃ )

proof end;

theorem Th4: :: FINSEQ_5:4

for b₁ being Function holds
( b₁ is one-to-one iff for b₂ being set st b₂ in dom b₁ holds
b₁ " {(b₁ . b₂)} = {b₂} )

proof end;

theorem Th5: :: FINSEQ_5:5

for b₁ being Function
for b₂, b₃ being set st b₁ is one-to-one & b₂ in rng b₁ & b₃ in rng b₁ & b₁ " {b₂} = b₁ " {b₃} holds
b₂ = b₃

proof end;

registration

cluster empty -> trivial set ;
coherence by REALSET1:def 4;

end;

registration

let c₁ be set ;
cluster <*a₁*> -> trivial ;
coherence

proof end;

let c₂ be set ;
cluster <*a₁,a₂*> -> non trivial ;
coherence

proof end;

end;

registration

cluster non empty one-to-one set ;
existence

proof end;

end;

theorem Th6: :: FINSEQ_5:6

for b₁ being non empty FinSequence holds
( 1 in dom b₁ & len b₁ in dom b₁ )

proof end;

theorem Th7: :: FINSEQ_5:7

for b₁ being non empty FinSequence ex b₂ being Nat st b₂ + 1 = len b₁

proof end;

theorem Th8: :: FINSEQ_5:8

for b₁ being set
for b₂ being FinSequence holds len (<*b₁*> ^ b₂) = 1 + (len b₂)

proof end;

scheme :: FINSEQ_5:sch 1
s1{ F₁() -> Nat, F₂( set ) -> set } :

ex b₁ being FinSequence st
( len b₁ = F₁() & ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ = F₂(b₂) ) )

proof end;

theorem Th9: :: FINSEQ_5:9

canceled;

theorem Th10: :: FINSEQ_5:10

for b₁ being FinSequence
for b₂, b₃ being set st b₂ in rng b₁ & b₃ in rng b₁ & b₂ .. b₁ = b₃ .. b₁ holds
b₂ = b₃

proof end;

theorem Th11: :: FINSEQ_5:11

for b₁ being Nat
for b₂, b₃ being FinSequence st b₁ + 1 in dom b₂ & b₃ = b₂ | (Seg b₁) holds
b₂ | (Seg (b₁ + 1)) = b₃ ^ <*(b₂ . (b₁ + 1))*>

proof end;

theorem Th12: :: FINSEQ_5:12

for b₁ being Nat
for b₂ being one-to-one FinSequence st b₁ in dom b₂ holds
(b₂ . b₁) .. b₂ = b₁

proof end;

registration

let c₁ be non empty set ;
cluster non empty one-to-one FinSequence of a₁;
existence

proof end;

end;

theorem Th13: :: FINSEQ_5:13

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st dom b₂ = dom b₃ & ( for b₄ being Nat st b₄ in dom b₂ holds
b₂ /. b₄ = b₃ /. b₄ ) holds
b₂ = b₃

proof end;

theorem Th14: :: FINSEQ_5:14

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

proof end;

theorem Th15: :: FINSEQ_5:15

for b₁ being non empty set
for b₂ being FinSequence of b₁ st len b₂ = 1 holds
b₂ = <*(b₂ /. 1)*>

proof end;

theorem Th16: :: FINSEQ_5:16

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds (<*b₂*> ^ b₃) /. 1 = b₂

proof end;

Lemma11: for b₁ being Nat
for b₂ being non empty set
for b₃, b₄ being FinSequence of b₂ st b₁ in dom b₃ holds
(b₃ ^ b₄) /. b₁ = b₃ /. b₁

proof end;

theorem Th17: :: FINSEQ_5:17

canceled;

theorem Th18: :: FINSEQ_5:18

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

proof end;

theorem Th19: :: FINSEQ_5:19

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

proof end;

theorem Th20: :: FINSEQ_5:20

for b₁ being Nat
for b₂ being set
for b₃ being FinSequence of b₂ holds dom (b₃ | b₁) c= dom b₃

proof end;

theorem Th21: :: FINSEQ_5:21

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ holds rng (b₃ | b₁) c= rng b₃

proof end;

theorem Th22: :: FINSEQ_5:22

canceled;

theorem Th23: :: FINSEQ_5:23

for b₁ being set
for b₂ being FinSequence of b₁ st not b₂ is empty holds
b₂ | 1 = <*(b₂ /. 1)*>

proof end;

theorem Th24: :: FINSEQ_5:24

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₁ + 1 = len b₃ holds
b₃ = (b₃ | b₁) ^ <*(b₃ /. (len b₃))*>

proof end;

Lemma17: for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₃ is one-to-one holds
b₃ | b₁ is one-to-one

proof end;

registration

let c₁ be Nat;
let c₂ be non empty set ;
let c₃ be one-to-one FinSequence of c₂;
cluster a₃ | a₁ -> one-to-one ;
coherence by Lemma17;

end;

theorem Th25: :: FINSEQ_5:25

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

proof end;

theorem Th26: :: FINSEQ_5:26

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

proof end;

theorem Th27: :: FINSEQ_5:27

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being set
for b₄ being FinSequence of b₃ st b₂ in rng b₄ holds
(b₄ -| b₂) ^ <*b₂*> = b₄ | (b₂ .. b₄)

proof end;

theorem Th28: :: FINSEQ_5:28

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

proof end;

theorem Th29: :: FINSEQ_5:29

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom (b₄ /^ b₂) holds
b₂ + b₁ in dom b₄

proof end;

theorem Th30: :: FINSEQ_5:30

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom (b₄ /^ b₂) holds
(b₄ /^ b₂) /. b₁ = b₄ /. (b₂ + b₁)

proof end;

theorem Th31: :: FINSEQ_5:31

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

proof end;

theorem Th32: :: FINSEQ_5:32

for b₁ being non empty set
for b₂ being FinSequence of b₁ st not b₂ is empty holds
b₂ = <*(b₂ /. 1)*> ^ (b₂ /^ 1)

proof end;

theorem Th33: :: FINSEQ_5:33

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₁ + 1 = len b₃ holds
b₃ /^ b₁ = <*(b₃ /. (len b₃))*>

proof end;

theorem Th34: :: FINSEQ_5:34

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ + 1 = b₂ & b₂ in dom b₄ holds
<*(b₄ /. b₂)*> ^ (b₄ /^ b₂) = b₄ /^ b₁

proof end;

theorem Th35: :: FINSEQ_5:35

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

proof end;

theorem Th36: :: FINSEQ_5:36

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ holds rng (b₃ /^ b₁) c= rng b₃

proof end;

Lemma25: for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₃ is one-to-one holds
b₃ /^ b₁ is one-to-one

proof end;

registration

let c₁ be Nat;
let c₂ be non empty set ;
let c₃ be one-to-one FinSequence of c₂;
cluster a₃ /^ a₁ -> one-to-one ;
coherence by Lemma25;

end;

theorem Th37: :: FINSEQ_5:37

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₃ is one-to-one holds
rng (b₃ | b₁) misses rng (b₃ /^ b₁)

proof end;

theorem Th38: :: FINSEQ_5:38

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
b₃ |-- b₂ = b₃ /^ (b₂ .. b₃)

proof end;

theorem Th39: :: FINSEQ_5:39

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

proof end;

theorem Th40: :: FINSEQ_5:40

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

proof end;

theorem Th41: :: FINSEQ_5:41

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
b₃ /. (b₂ .. b₃) = b₂

proof end;

theorem Th42: :: FINSEQ_5:42

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₁ in dom b₃ holds
(b₃ /. b₁) .. b₃ <= b₁

proof end;

theorem Th43: :: FINSEQ_5:43

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng (b₄ | b₁) holds
b₃ .. (b₄ | b₁) = b₃ .. b₄

proof end;

theorem Th44: :: FINSEQ_5:44

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₁ in dom b₃ & b₃ is one-to-one holds
(b₃ /. b₁) .. b₃ = b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be set ;
func c₂ -: c₃ -> FinSequence of a₁ equals :: FINSEQ_5:def 1
a₂ | (a₃ .. a₂);
correctness ;

end;

:: deftheorem Def1 defines -: FINSEQ_5:def 1 :

theorem Th45: :: FINSEQ_5:45

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
len (b₃ -: b₂) = b₂ .. b₃

proof end;

theorem Th46: :: FINSEQ_5:46

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng b₄ & b₁ in Seg (b₃ .. b₄) holds
(b₄ -: b₃) /. b₁ = b₄ /. b₁

proof end;

theorem Th47: :: FINSEQ_5:47

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
(b₃ -: b₂) /. 1 = b₃ /. 1

proof end;

theorem Th48: :: FINSEQ_5:48

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
(b₃ -: b₂) /. (b₂ .. b₃) = b₂

proof end;

theorem Th49: :: FINSEQ_5:49

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁
for b₄ being set st b₄ in rng b₃ & b₂ in rng b₃ & b₄ .. b₃ <= b₂ .. b₃ holds
b₄ in rng (b₃ -: b₂)

proof end;

theorem Th50: :: FINSEQ_5:50

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
not b₃ -: b₂ is empty

proof end;

theorem Th51: :: FINSEQ_5:51

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds rng (b₃ -: b₂) c= rng b₃ by Th21;

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be one-to-one FinSequence of c₁;
cluster a₃ -: a₂ -> one-to-one ;
coherence ;

end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Element of c₁;
func c₂ :- c₃ -> FinSequence of a₁ equals :: FINSEQ_5:def 2
<*a₃*> ^ (a₂ /^ (a₃ .. a₂));
correctness ;

end;

:: deftheorem Def2 defines :- FINSEQ_5:def 2 :

theorem Th52: :: FINSEQ_5:52

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
ex b₄ being Nat st
( b₄ + 1 = b₂ .. b₃ & b₃ :- b₂ = b₃ /^ b₄ )

proof end;

theorem Th53: :: FINSEQ_5:53

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
len (b₃ :- b₂) = ((len b₃) - (b₂ .. b₃)) + 1

proof end;

theorem Th54: :: FINSEQ_5:54

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng b₄ & b₁ + 1 in dom (b₄ :- b₃) holds
b₁ + (b₃ .. b₄) in dom b₄

proof end;

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be FinSequence of c₁;
cluster a₃ :- a₂ -> non empty ;
coherence ;

end;

theorem Th55: :: FINSEQ_5:55

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng b₄ & b₁ + 1 in dom (b₄ :- b₃) holds
(b₄ :- b₃) /. (b₁ + 1) = b₄ /. (b₁ + (b₃ .. b₄))

proof end;

theorem Th56: :: FINSEQ_5:56

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds (b₃ :- b₂) /. 1 = b₂ by Th16;

theorem Th57: :: FINSEQ_5:57

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
(b₃ :- b₂) /. (len (b₃ :- b₂)) = b₃ /. (len b₃)

proof end;

theorem Th58: :: FINSEQ_5:58

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
rng (b₃ :- b₂) c= rng b₃

proof end;

theorem Th59: :: FINSEQ_5:59

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ & b₃ is one-to-one holds
b₃ :- b₂ is one-to-one

proof end;

definition

let c₁ be FinSequence;
func Rev c₁ -> FinSequence means :Def3: :: FINSEQ_5:def 3
( len a₂ = len a₁ & ( for b₁ being Nat st b₁ in dom a₂ holds
a₂ . b₁ = a₁ . (((len a₁) - b₁) + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Rev FINSEQ_5:def 3 :

theorem Th60: :: FINSEQ_5:60

for b₁ being FinSequence holds
( dom b₁ = dom (Rev b₁) & rng b₁ = rng (Rev b₁) )

proof end;

theorem Th61: :: FINSEQ_5:61

for b₁ being Nat
for b₂ being FinSequence st b₁ in dom b₂ holds
(Rev b₂) . b₁ = b₂ . (((len b₂) - b₁) + 1)

proof end;

theorem Th62: :: FINSEQ_5:62

for b₁ being FinSequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₂ + b₃ = (len b₁) + 1 holds
b₃ in dom (Rev b₁)

proof end;

registration

let c₁ be empty FinSequence;
cluster Rev a₁ -> empty trivial ;
coherence

proof end;

end;

theorem Th63: :: FINSEQ_5:63

for b₁ being set holds Rev <*b₁*> = <*b₁*>

proof end;

theorem Th64: :: FINSEQ_5:64

for b₁, b₂ being set holds Rev <*b₁,b₂*> = <*b₂,b₁*>

proof end;

theorem Th65: :: FINSEQ_5:65

for b₁ being FinSequence holds
( b₁ . 1 = (Rev b₁) . (len b₁) & b₁ . (len b₁) = (Rev b₁) . 1 )

proof end;

registration

let c₁ be one-to-one FinSequence;
cluster Rev a₁ -> one-to-one ;
coherence

proof end;

end;

theorem Th66: :: FINSEQ_5:66

for b₁ being FinSequence
for b₂ being set holds Rev (b₁ ^ <*b₂*>) = <*b₂*> ^ (Rev b₁)

proof end;

theorem Th67: :: FINSEQ_5:67

for b₁, b₂ being FinSequence holds Rev (b₁ ^ b₂) = (Rev b₂) ^ (Rev b₁)

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
redefine func Rev as Rev c₂ -> FinSequence of a₁;
coherence

proof end;

end;

theorem Th68: :: FINSEQ_5:68

for b₁ being non empty set
for b₂ being FinSequence of b₁ st not b₂ is empty holds
( b₂ /. 1 = (Rev b₂) /. (len b₂) & b₂ /. (len b₂) = (Rev b₂) /. 1 )

proof end;

theorem Th69: :: FINSEQ_5:69

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₁ + b₂ = (len b₄) + 1 holds
b₄ /. b₁ = (Rev b₄) /. b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Element of c₁;
let c₄ be Nat;
func Ins c₂,c₄,c₃ -> FinSequence of a₁ equals :: FINSEQ_5:def 4
((a₂ | a₄) ^ <*a₃*>) ^ (a₂ /^ a₄);
correctness ;

end;

:: deftheorem Def4 defines Ins FINSEQ_5:def 4 :

theorem Th70: :: FINSEQ_5:70

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds Ins b₃,0,b₂ = <*b₂*> ^ b₃

proof end;

theorem Th71: :: FINSEQ_5:71

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st len b₄ <= b₁ holds
Ins b₄,b₁,b₃ = b₄ ^ <*b₃*>

proof end;

theorem Th72: :: FINSEQ_5:72

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ holds len (Ins b₄,b₁,b₃) = (len b₄) + 1

proof end;

theorem Th73: :: FINSEQ_5:73

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ holds rng (Ins b₄,b₁,b₃) = {b₃} \/ (rng b₄)

proof end;

registration

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Nat;
let c₄ be Element of c₁;
cluster Ins a₂,a₃,a₄ -> non empty ;
coherence ;

end;

theorem Th74: :: FINSEQ_5:74

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ holds b₃ in rng (Ins b₄,b₁,b₃)

proof end;

theorem Th75: :: FINSEQ_5:75

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being FinSequence of b₃ st b₁ in dom (b₅ | b₂) holds
(Ins b₅,b₂,b₄) /. b₁ = b₅ /. b₁

proof end;

theorem Th76: :: FINSEQ_5:76

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₁ <= len b₄ holds
(Ins b₄,b₁,b₃) /. (b₁ + 1) = b₃

proof end;

theorem Th77: :: FINSEQ_5:77

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being FinSequence of b₃ st b₁ + 1 <= b₂ & b₂ <= len b₅ holds
(Ins b₅,b₁,b₄) /. (b₂ + 1) = b₅ /. b₂

proof end;

theorem Th78: :: FINSEQ_5:78

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st 1 <= b₁ & not b₄ is empty holds
(Ins b₄,b₁,b₃) /. 1 = b₄ /. 1

proof end;

theorem Th79: :: FINSEQ_5:79

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₄ is one-to-one & not b₃ in rng b₄ holds
Ins b₄,b₁,b₃ is one-to-one

proof end;

theorem Th80: :: FINSEQ_5:80

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

proof end;

theorem Th81: :: FINSEQ_5:81

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

proof end;

theorem Th82: :: FINSEQ_5:82

for b₁ being non empty set holds Rev (<*> b₁) = <*> b₁

proof end;