:: FINSEQ_5 semantic presentation

theorem Th1: :: FINSEQ_5:1

for i, n being Nat st i <= n holds
(n - i) + 1 is Nat

proof end;

theorem Th2: :: FINSEQ_5:2

for i, n being Nat st i in Seg n holds
(n - i) + 1 in Seg n

proof end;

theorem Th3: :: FINSEQ_5:3

for f being Function
for x, y being set st f " {y} = {x} holds
( x in dom f & y in rng f & f . x = y )

proof end;

theorem :: FINSEQ_5:4

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

proof end;

theorem :: FINSEQ_5:5

for f being Function
for y1, y2 being set st f is one-to-one & y1 in rng f & y2 in rng f & f " {y1} = f " {y2} holds
y1 = y2

proof end;

registration

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

end;

registration

let x be set ;
cluster <*x*> -> trivial ;
coherence

proof end;

let y be set ;
cluster <*x,y*> -> non trivial ;
coherence

proof end;

end;

registration

cluster non empty one-to-one set ;
existence

proof end;

end;

theorem Th6: :: FINSEQ_5:6

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

proof end;

theorem :: FINSEQ_5:7

for f being non empty FinSequence ex i being Nat st i + 1 = len f

proof end;

theorem Th8: :: FINSEQ_5:8

for x being set
for f being FinSequence holds len (<*x*> ^ f) = 1 + (len f)

proof end;

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

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

proof end;

theorem :: FINSEQ_5:9

canceled;

theorem :: FINSEQ_5:10

for f being FinSequence
for p, q being set st p in rng f & q in rng f & p .. f = q .. f holds
p = q

proof end;

theorem Th11: :: FINSEQ_5:11

for n being Nat
for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds
f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>

proof end;

theorem Th12: :: FINSEQ_5:12

for i being Nat
for f being one-to-one FinSequence st i in dom f holds
(f . i) .. f = i

proof end;

registration

let D be non empty set ;
cluster non empty one-to-one FinSequence of D;
existence

proof end;

end;

theorem :: FINSEQ_5:13

for D being non empty set
for f, g being FinSequence of D st dom f = dom g & ( for i being Nat st i in dom f holds
f /. i = g /. i ) holds
f = g

proof end;

theorem Th14: :: FINSEQ_5:14

for D being non empty set
for f, g being FinSequence of D st len f = len g & ( for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ) holds
f = g

proof end;

theorem Th15: :: FINSEQ_5:15

for D being non empty set
for f being FinSequence of D st len f = 1 holds
f = <*(f /. 1)*>

proof end;

theorem Th16: :: FINSEQ_5:16

for D being non empty set
for p being Element of D
for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p

proof end;

Lm1: for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i

proof end;

theorem :: FINSEQ_5:17

canceled;

theorem Th18: :: FINSEQ_5:18

for i being Nat
for D being set
for f being FinSequence of D holds len (f | i) <= len f

proof end;

theorem Th19: :: FINSEQ_5:19

for i being Nat
for D being set
for f being FinSequence of D holds len (f | i) <= i

proof end;

theorem Th20: :: FINSEQ_5:20

for i being Nat
for D being set
for f being FinSequence of D holds dom (f | i) c= dom f

proof end;

theorem Th21: :: FINSEQ_5:21

for i being Nat
for D being non empty set
for f being FinSequence of D holds rng (f | i) c= rng f

proof end;

theorem :: FINSEQ_5:22

canceled;

theorem Th23: :: FINSEQ_5:23

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

proof end;

theorem :: FINSEQ_5:24

for i being Nat
for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f = (f | i) ^ <*(f /. (len f))*>

proof end;

Lm2: for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one

proof end;

registration

let i be Nat;
let D be non empty set ;
let f be one-to-one FinSequence of D;
cluster f | i -> one-to-one ;
coherence by Lm2;

end;

theorem Th25: :: FINSEQ_5:25

for i being Nat
for D being set
for f, g being FinSequence of D st i <= len f holds
(f ^ g) | i = f | i

proof end;

theorem :: FINSEQ_5:26

for D being set
for f, g being FinSequence of D holds (f ^ g) | (len f) = f

proof end;

theorem :: FINSEQ_5:27

for D being non empty set
for p being Element of D
for D being set
for f being FinSequence of D st p in rng f holds
(f -| p) ^ <*p*> = f | (p .. f)

proof end;

theorem :: FINSEQ_5:28

for i being Nat
for D being non empty set
for f being FinSequence of D holds len (f /^ i) <= len f

proof end;

theorem Th29: :: FINSEQ_5:29

for i, n being Nat
for D being non empty set
for f being FinSequence of D st i in dom (f /^ n) holds
n + i in dom f

proof end;

theorem Th30: :: FINSEQ_5:30

for i, n being Nat
for D being non empty set
for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)

proof end;

theorem Th31: :: FINSEQ_5:31

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

proof end;

theorem :: FINSEQ_5:32

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

proof end;

theorem :: FINSEQ_5:33

for i being Nat
for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f /^ i = <*(f /. (len f))*>

proof end;

theorem Th34: :: FINSEQ_5:34

for j, i being Nat
for D being non empty set
for f being FinSequence of D st j + 1 = i & i in dom f holds
<*(f /. i)*> ^ (f /^ i) = f /^ j

proof end;

theorem Th35: :: FINSEQ_5:35

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

proof end;

theorem Th36: :: FINSEQ_5:36

for n being Nat
for D being non empty set
for f being FinSequence of D holds rng (f /^ n) c= rng f

proof end;

Lm3: for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f /^ i is one-to-one

proof end;

registration

let i be Nat;
let D be non empty set ;
let f be one-to-one FinSequence of D;
cluster f /^ i -> one-to-one ;
coherence by Lm3;

end;

theorem Th37: :: FINSEQ_5:37

for n being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)

proof end;

theorem :: FINSEQ_5:38

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
f |-- p = f /^ (p .. f)

proof end;

theorem Th39: :: FINSEQ_5:39

for i being Nat
for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i

proof end;

theorem :: FINSEQ_5:40

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

proof end;

theorem Th41: :: FINSEQ_5:41

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
f /. (p .. f) = p

proof end;

theorem Th42: :: FINSEQ_5:42

for i being Nat
for D being non empty set
for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i

proof end;

theorem :: FINSEQ_5:43

for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng (f | i) holds
p .. (f | i) = p .. f

proof end;

theorem :: FINSEQ_5:44

for i being Nat
for D being non empty set
for f being FinSequence of D st i in dom f & f is one-to-one holds
(f /. i) .. f = i

proof end;

definition

let D be non empty set ;
let f be FinSequence of D;
let p be set ;
func f -: p -> FinSequence of D equals :: FINSEQ_5:def 1
f | (p .. f);
correctness ;

end;

:: deftheorem defines -: FINSEQ_5:def 1 :

theorem Th45: :: FINSEQ_5:45

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
len (f -: p) = p .. f

proof end;

theorem Th46: :: FINSEQ_5:46

for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds
(f -: p) /. i = f /. i

proof end;

theorem :: FINSEQ_5:47

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f -: p) /. 1 = f /. 1

proof end;

theorem :: FINSEQ_5:48

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f -: p) /. (p .. f) = p

proof end;

theorem :: FINSEQ_5:49

for D being non empty set
for p being Element of D
for f being FinSequence of D
for x being set st x in rng f & p in rng f & x .. f <= p .. f holds
x in rng (f -: p)

proof end;

theorem :: FINSEQ_5:50

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
not f -: p is empty

proof end;

theorem :: FINSEQ_5:51

for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (f -: p) c= rng f by Th21;

registration

let D be non empty set ;
let p be Element of D;
let f be one-to-one FinSequence of D;
cluster f -: p -> one-to-one ;
coherence ;

end;

definition

let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
func f :- p -> FinSequence of D equals :: FINSEQ_5:def 2
<*p*> ^ (f /^ (p .. f));
correctness ;

end;

:: deftheorem defines :- FINSEQ_5:def 2 :

theorem Th52: :: FINSEQ_5:52

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
ex i being Nat st
( i + 1 = p .. f & f :- p = f /^ i )

proof end;

theorem Th53: :: FINSEQ_5:53

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
len (f :- p) = ((len f) - (p .. f)) + 1

proof end;

theorem Th54: :: FINSEQ_5:54

for j being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f

proof end;

registration

let D be non empty set ;
let p be Element of D;
let f be FinSequence of D;
cluster f :- p -> non empty ;
coherence ;

end;

theorem Th55: :: FINSEQ_5:55

for j being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))

proof end;

theorem :: FINSEQ_5:56

for D being non empty set
for p being Element of D
for f being FinSequence of D holds (f :- p) /. 1 = p by Th16;

theorem :: FINSEQ_5:57

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f :- p) /. (len (f :- p)) = f /. (len f)

proof end;

theorem :: FINSEQ_5:58

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
rng (f :- p) c= rng f

proof end;

theorem :: FINSEQ_5:59

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & f is one-to-one holds
f :- p is one-to-one

proof end;

definition

let f be FinSequence;
func Rev f -> FinSequence means :Def3: :: FINSEQ_5:def 3
( len it = len f & ( for i being Nat st i in dom it holds
it . i = f . (((len f) - i) + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Rev FINSEQ_5:def 3 :

theorem Th60: :: FINSEQ_5:60

for f being FinSequence holds
( dom f = dom (Rev f) & rng f = rng (Rev f) )

proof end;

theorem Th61: :: FINSEQ_5:61

for i being Nat
for f being FinSequence st i in dom f holds
(Rev f) . i = f . (((len f) - i) + 1)

proof end;

theorem Th62: :: FINSEQ_5:62

for f being FinSequence
for i, j being Nat st i in dom f & i + j = (len f) + 1 holds
j in dom (Rev f)

proof end;

registration

let f be empty FinSequence;
cluster Rev f -> empty trivial ;
coherence

proof end;

end;

theorem :: FINSEQ_5:63

for x being set holds Rev <*x*> = <*x*>

proof end;

theorem :: FINSEQ_5:64

for x1, x2 being set holds Rev <*x1,x2*> = <*x2,x1*>

proof end;

theorem Th65: :: FINSEQ_5:65

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

proof end;

registration

let f be one-to-one FinSequence;
cluster Rev f -> one-to-one ;
coherence

proof end;

end;

theorem Th66: :: FINSEQ_5:66

for f being FinSequence
for x being set holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f)

proof end;

theorem :: FINSEQ_5:67

for f, g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f)

proof end;

definition

let D be non empty set ;
let f be FinSequence of D;
:: original: Rev
redefine func Rev f -> FinSequence of D;
coherence

proof end;

end;

theorem :: FINSEQ_5:68

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

proof end;

theorem :: FINSEQ_5:69

for i, j being Nat
for D being non empty set
for f being FinSequence of D st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j

proof end;

definition

let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
let n be Nat;
func Ins f,n,p -> FinSequence of D equals :: FINSEQ_5:def 4
((f | n) ^ <*p*>) ^ (f /^ n);
correctness ;

end;

:: deftheorem defines Ins FINSEQ_5:def 4 :

theorem :: FINSEQ_5:70

for D being non empty set
for p being Element of D
for f being FinSequence of D holds Ins f,0,p = <*p*> ^ f

proof end;

theorem Th71: :: FINSEQ_5:71

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins f,n,p = f ^ <*p*>

proof end;

theorem :: FINSEQ_5:72

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds len (Ins f,n,p) = (len f) + 1

proof end;

theorem Th73: :: FINSEQ_5:73

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (Ins f,n,p) = {p} \/ (rng f)

proof end;

registration

let D be non empty set ;
let f be FinSequence of D;
let n be Nat;
let p be Element of D;
cluster Ins f,n,p -> non empty ;
coherence ;

end;

theorem :: FINSEQ_5:74

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (Ins f,n,p)

proof end;

theorem Th75: :: FINSEQ_5:75

for i, n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st i in dom (f | n) holds
(Ins f,n,p) /. i = f /. i

proof end;

theorem :: FINSEQ_5:76

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins f,n,p) /. (n + 1) = p

proof end;

theorem :: FINSEQ_5:77

for n, i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st n + 1 <= i & i <= len f holds
(Ins f,n,p) /. (i + 1) = f /. i

proof end;

theorem :: FINSEQ_5:78

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins f,n,p) /. 1 = f /. 1

proof end;

theorem :: FINSEQ_5:79

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins f,n,p is one-to-one

proof end;

theorem :: FINSEQ_5:80

for D being non empty set
for f being FinSequence of D
for i1, i2 being Nat st i1 <= i2 holds
( (f | i1) | i2 = f | i1 & (f | i2) | i1 = f | i1 )

proof end;

theorem :: FINSEQ_5:81

for i being Nat
for D being non empty set holds (<*> D) | i = <*> D

proof end;

theorem :: FINSEQ_5:82

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

proof end;