:: FINSEQ_7 semantic presentation

theorem Th1: :: FINSEQ_7:1

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

proof end;

theorem Th2: :: FINSEQ_7:2

for b₁ being Nat
for b₂, b₃, b₄ being FinSequence st len b₃ = len b₄ & len b₃ < b₁ & b₁ <= len (b₃ ^ b₂) holds
(b₃ ^ b₂) . b₁ = (b₄ ^ b₂) . b₁

proof end;

theorem Th3: :: FINSEQ_7:3

for b₁ being Nat
for b₂, b₃ being FinSequence st 1 <= b₁ & b₁ <= len b₂ holds
b₂ . b₁ = (b₃ ^ b₂) . ((len b₃) + b₁)

proof end;

theorem Th4: :: FINSEQ_7:4

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

proof end;

Lemma2: for b₁, b₂ being Nat holds (b₁ -' b₂) -' 1 = (b₁ -' 1) -' b₂

proof end;

notation

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Nat;
let c₄ be Element of c₁;
synonym Replace c₂,c₃,c₄ for c₁ +* c₂,c₃;

end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Nat;
let c₄ be Element of c₁;
redefine func Replace as Replace c₂,c₃,c₄ -> FinSequence of a₁ equals :Def1: :: FINSEQ_7:def 1
((a₂ | (a₃ -' 1)) ^ <*a₄*>) ^ (a₂ /^ a₃) if ( 1 <= a₃ & a₃ <= len a₂ )
otherwise a₂;
compatibility

proof end;

correctness

proof end;

end;

:: deftheorem Def1 defines Replace FINSEQ_7:def 1 :

theorem Th5: :: FINSEQ_7:5

canceled;

theorem Th6: :: FINSEQ_7:6

canceled;

theorem Th7: :: FINSEQ_7:7

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

proof end;

theorem Th8: :: FINSEQ_7:8

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

proof end;

theorem Th9: :: FINSEQ_7:9

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Element of b₁
for b₄ being Nat st 1 <= b₄ & b₄ <= len b₂ holds
b₃ in rng (Replace b₂,b₄,b₃)

proof end;

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

proof end;

theorem Th10: :: FINSEQ_7:10

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

proof end;

theorem Th11: :: FINSEQ_7:11

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

proof end;

theorem Th12: :: FINSEQ_7:12

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

proof end;

theorem Th13: :: FINSEQ_7:13

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Nat st 1 <= b₅ & b₅ < b₆ & b₆ <= len b₂ holds
Replace (Replace b₂,b₆,b₃),b₅,b₄ = ((((b₂ | (b₅ -' 1)) ^ <*b₄*>) ^ ((b₂ /^ b₅) | ((b₆ -' b₅) -' 1))) ^ <*b₃*>) ^ (b₂ /^ b₆)

proof end;

theorem Th14: :: FINSEQ_7:14

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds Replace <*b₂*>,1,b₃ = <*b₃*>

proof end;

theorem Th15: :: FINSEQ_7:15

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds Replace <*b₂,b₃*>,1,b₄ = <*b₄,b₃*>

proof end;

theorem Th16: :: FINSEQ_7:16

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds Replace <*b₂,b₃*>,2,b₄ = <*b₂,b₄*>

proof end;

theorem Th17: :: FINSEQ_7:17

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁ holds Replace <*b₂,b₃,b₄*>,1,b₅ = <*b₅,b₃,b₄*>

proof end;

theorem Th18: :: FINSEQ_7:18

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁ holds Replace <*b₂,b₃,b₄*>,2,b₅ = <*b₂,b₅,b₄*>

proof end;

theorem Th19: :: FINSEQ_7:19

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁ holds Replace <*b₂,b₃,b₄*>,3,b₅ = <*b₂,b₃,b₅*>

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃, c₄ be Nat;
func Swap c₂,c₃,c₄ -> FinSequence of a₁ equals :Def2: :: FINSEQ_7:def 2
Replace (Replace a₂,a₃,(a₂ /. a₄)),a₄,(a₂ /. a₃) if ( 1 <= a₃ & a₃ <= len a₂ & 1 <= a₄ & a₄ <= len a₂ )
otherwise a₂;
correctness ;

end;

:: deftheorem Def2 defines Swap FINSEQ_7:def 2 :

theorem Th20: :: FINSEQ_7:20

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

proof end;

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

proof end;

theorem Th21: :: FINSEQ_7:21

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat holds Swap b₂,b₃,b₃ = b₂

proof end;

theorem Th22: :: FINSEQ_7:22

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat holds Swap (Swap b₂,b₃,b₄),b₄,b₃ = b₂

proof end;

theorem Th23: :: FINSEQ_7:23

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat holds Swap b₂,b₃,b₄ = Swap b₂,b₄,b₃

proof end;

theorem Th24: :: FINSEQ_7:24

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat holds rng (Swap b₂,b₃,b₄) = rng b₂

proof end;

theorem Th25: :: FINSEQ_7:25

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds Swap <*b₂,b₃*>,1,2 = <*b₃,b₂*>

proof end;

theorem Th26: :: FINSEQ_7:26

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds Swap <*b₂,b₃,b₄*>,1,2 = <*b₃,b₂,b₄*>

proof end;

theorem Th27: :: FINSEQ_7:27

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds Swap <*b₂,b₃,b₄*>,1,3 = <*b₄,b₃,b₂*>

proof end;

theorem Th28: :: FINSEQ_7:28

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds Swap <*b₂,b₃,b₄*>,2,3 = <*b₂,b₄,b₃*>

proof end;

theorem Th29: :: FINSEQ_7:29

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ < b₄ & b₄ <= len b₂ holds
Swap b₂,b₃,b₄ = ((((b₂ | (b₃ -' 1)) ^ <*(b₂ /. b₄)*>) ^ ((b₂ /^ b₃) | ((b₄ -' b₃) -' 1))) ^ <*(b₂ /. b₃)*>) ^ (b₂ /^ b₄)

proof end;

theorem Th30: :: FINSEQ_7:30

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st 1 < b₃ & b₃ <= len b₂ holds
Swap b₂,1,b₃ = ((<*(b₂ /. b₃)*> ^ ((b₂ /^ 1) | (b₃ -' 2))) ^ <*(b₂ /. 1)*>) ^ (b₂ /^ b₃)

proof end;

theorem Th31: :: FINSEQ_7:31

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

proof end;

Lemma19: for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄, b₅ being Nat st b₃ <> b₄ & b₅ <> b₄ holds
(Swap b₂,b₃,b₅) . b₄ = b₂ . b₄

proof end;

theorem Th32: :: FINSEQ_7:32

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

proof end;

theorem Th33: :: FINSEQ_7:33

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

proof end;

theorem Th34: :: FINSEQ_7:34

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

proof end;

theorem Th35: :: FINSEQ_7:35

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Element of b₁
for b₄, b₅, b₆ being Nat st b₄ <> b₅ & b₆ <> b₅ & 1 <= b₄ & b₄ <= len b₂ & 1 <= b₆ & b₆ <= len b₂ & 1 <= b₅ & b₅ <= len b₂ holds
Swap (Replace b₂,b₅,b₃),b₄,b₆ = Replace (Swap b₂,b₄,b₆),b₅,b₃

proof end;

theorem Th36: :: FINSEQ_7:36

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

proof end;

theorem Th37: :: FINSEQ_7:37

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

proof end;