:: FINSEQ_6 semantic presentation

registration

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

proof end;

end;

registration

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

proof end;

end;

Lemma1: for b₁, b₂ being set holds rng <*b₁,b₂*> = {b₁,b₂}

proof end;

Lemma2: for b₁, b₂, b₃ being set holds rng <*b₁,b₂,b₃*> = {b₁,b₂,b₃}

proof end;

theorem Th1: :: FINSEQ_6:1

canceled;

theorem Th2: :: FINSEQ_6:2

canceled;

theorem Th3: :: FINSEQ_6:3

for b₁ being set
for b₂ being Nat st b₁ c= Seg b₂ & 1 in b₁ holds
(Sgm b₁) . 1 = 1

proof end;

theorem Th4: :: FINSEQ_6:4

for b₁ being Nat
for b₂ being FinSequence st b₁ in dom b₂ & ( for b₃ being Nat st 1 <= b₃ & b₃ < b₁ holds
b₂ . b₃ <> b₂ . b₁ ) holds
(b₂ . b₁) .. b₂ = b₁

proof end;

theorem Th5: :: FINSEQ_6:5

for b₁, b₂ being set holds <*b₁,b₂*> | (Seg 1) = <*b₁*>

proof end;

theorem Th6: :: FINSEQ_6:6

for b₁, b₂, b₃ being set holds <*b₁,b₂,b₃*> | (Seg 1) = <*b₁*>

proof end;

theorem Th7: :: FINSEQ_6:7

for b₁, b₂, b₃ being set holds <*b₁,b₂,b₃*> | (Seg 2) = <*b₁,b₂*>

proof end;

theorem Th8: :: FINSEQ_6:8

for b₁, b₂ being FinSequence
for b₃ being set st b₃ in rng b₁ holds
b₃ .. (b₁ ^ b₂) = b₃ .. b₁

proof end;

theorem Th9: :: FINSEQ_6:9

for b₁, b₂ being FinSequence
for b₃ being set st b₃ in (rng b₁) \ (rng b₂) holds
b₃ .. (b₂ ^ b₁) = (len b₂) + (b₃ .. b₁)

proof end;

theorem Th10: :: FINSEQ_6:10

for b₁, b₂ being FinSequence
for b₃ being set st b₃ in rng b₁ holds
(b₁ ^ b₂) |-- b₃ = (b₁ |-- b₃) ^ b₂

proof end;

theorem Th11: :: FINSEQ_6:11

for b₁, b₂ being FinSequence
for b₃ being set st b₃ in (rng b₁) \ (rng b₂) holds
(b₂ ^ b₁) |-- b₃ = b₁ |-- b₃

proof end;

theorem Th12: :: FINSEQ_6:12

for b₁, b₂ being FinSequence holds b₁ c= b₁ ^ b₂

proof end;

theorem Th13: :: FINSEQ_6:13

for b₁, b₂ being FinSequence
for b₃ being set st b₃ c= dom b₁ holds
(b₁ ^ b₂) | b₃ = b₁ | b₃

proof end;

theorem Th14: :: FINSEQ_6:14

for b₁, b₂ being FinSequence
for b₃ being set st b₃ in rng b₁ holds
(b₁ ^ b₂) -| b₃ = b₁ -| b₃

proof end;

registration

let c₁ be FinSequence;
let c₂ be natural number ;
cluster a₁ | (Seg a₂) -> FinSequence-like ;
coherence by FINSEQ_1:19;

end;

theorem Th15: :: FINSEQ_6:15

for b₁, b₂, b₃ being FinSequence st b₁ c= b₂ holds
b₃ ^ b₁ c= b₃ ^ b₂

proof end;

theorem Th16: :: FINSEQ_6:16

for b₁, b₂ being FinSequence
for b₃ being Nat holds (b₁ ^ b₂) | (Seg ((len b₁) + b₃)) = b₁ ^ (b₂ | (Seg b₃))

proof end;

theorem Th17: :: FINSEQ_6:17

for b₁, b₂ being FinSequence
for b₃ being set st b₃ in (rng b₁) \ (rng b₂) holds
(b₂ ^ b₁) -| b₃ = b₂ ^ (b₁ -| b₃)

proof end;

theorem Th18: :: FINSEQ_6:18

canceled;

theorem Th19: :: FINSEQ_6:19

for b₁, b₂ being FinSequence
for b₃ being set st b₁ ^ b₂ just_once_values b₃ holds
b₃ in (rng b₁) \+\ (rng b₂)

proof end;

theorem Th20: :: FINSEQ_6:20

for b₁, b₂ being FinSequence
for b₃ being set st b₁ ^ b₂ just_once_values b₃ & b₃ in rng b₁ holds
b₁ just_once_values b₃

proof end;

theorem Th21: :: FINSEQ_6:21

for b₁ being FinSequence st not rng b₁ is trivial holds
not b₁ is trivial

proof end;

theorem Th22: :: FINSEQ_6:22

for b₁ being set holds b₁ .. <*b₁*> = 1

proof end;

theorem Th23: :: FINSEQ_6:23

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

proof end;

theorem Th24: :: FINSEQ_6:24

for b₁, b₂ being set st b₁ <> b₂ holds
b₂ .. <*b₁,b₂*> = 2

proof end;

theorem Th25: :: FINSEQ_6:25

for b₁, b₂, b₃ being set holds b₁ .. <*b₁,b₂,b₃*> = 1

proof end;

theorem Th26: :: FINSEQ_6:26

for b₁, b₂, b₃ being set st b₁ <> b₂ holds
b₂ .. <*b₁,b₂,b₃*> = 2

proof end;

theorem Th27: :: FINSEQ_6:27

for b₁, b₂, b₃ being set st b₁ <> b₂ & b₃ <> b₂ holds
b₂ .. <*b₁,b₃,b₂*> = 3

proof end;

theorem Th28: :: FINSEQ_6:28

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

proof end;

theorem Th29: :: FINSEQ_6:29

for b₁ being FinSequence holds Rev (Rev b₁) = b₁

proof end;

theorem Th30: :: FINSEQ_6:30

for b₁, b₂ being set st b₁ <> b₂ holds
<*b₁,b₂*> -| b₂ = <*b₁*>

proof end;

theorem Th31: :: FINSEQ_6:31

for b₁, b₂, b₃ being set st b₁ <> b₂ holds
<*b₁,b₂,b₃*> -| b₂ = <*b₁*>

proof end;

theorem Th32: :: FINSEQ_6:32

for b₁, b₂, b₃ being set st b₁ <> b₂ & b₃ <> b₂ holds
<*b₁,b₃,b₂*> -| b₂ = <*b₁,b₃*>

proof end;

theorem Th33: :: FINSEQ_6:33

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

proof end;

theorem Th34: :: FINSEQ_6:34

for b₁, b₂, b₃ being set st b₁ <> b₂ holds
<*b₁,b₂,b₃*> |-- b₂ = <*b₃*>

proof end;

theorem Th35: :: FINSEQ_6:35

for b₁, b₂, b₃ being set holds <*b₁,b₂,b₃*> |-- b₁ = <*b₂,b₃*>

proof end;

theorem Th36: :: FINSEQ_6:36

for b₁ being set holds
( <*b₁*> |-- b₁ = {} & <*b₁*> -| b₁ = {} )

proof end;

theorem Th37: :: FINSEQ_6:37

for b₁, b₂ being set st b₁ <> b₂ holds
<*b₁,b₂*> |-- b₂ = {}

proof end;

theorem Th38: :: FINSEQ_6:38

for b₁, b₂, b₃ being set st b₁ <> b₂ & b₃ <> b₂ holds
<*b₁,b₃,b₂*> |-- b₂ = {}

proof end;

theorem Th39: :: FINSEQ_6:39

for b₁, b₂ being set
for b₃ being FinSequence st b₁ in rng b₃ & b₂ in rng (b₃ -| b₁) holds
(b₃ -| b₁) -| b₂ = b₃ -| b₂

proof end;

theorem Th40: :: FINSEQ_6:40

for b₁ being set
for b₂, b₃ being FinSequence st not b₁ in rng b₂ holds
b₁ .. ((b₂ ^ <*b₁*>) ^ b₃) = (len b₂) + 1

proof end;

theorem Th41: :: FINSEQ_6:41

for b₁ being set
for b₂ being FinSequence st b₂ just_once_values b₁ holds
(b₁ .. b₂) + (b₁ .. (Rev b₂)) = (len b₂) + 1

proof end;

theorem Th42: :: FINSEQ_6:42

for b₁ being set
for b₂ being FinSequence st b₂ just_once_values b₁ holds
Rev (b₂ -| b₁) = (Rev b₂) |-- b₁

proof end;

theorem Th43: :: FINSEQ_6:43

for b₁ being set
for b₂ being FinSequence st b₂ just_once_values b₁ holds
Rev b₂ just_once_values b₁

proof end;

theorem Th44: :: FINSEQ_6:44

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 Th45: :: FINSEQ_6: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
b₃ :- b₂ = <*b₂*> ^ (b₃ |-- b₂)

proof end;

theorem Th46: :: FINSEQ_6:46

for b₁ being non empty set
for b₂ being FinSequence of b₁ st b₂ <> {} holds
b₂ /. 1 in rng b₂

proof end;

theorem Th47: :: FINSEQ_6:47

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

proof end;

theorem Th48: :: FINSEQ_6:48

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₃ <> {} & b₃ /. 1 = b₂ holds
( b₃ -: b₂ = <*b₂*> & b₃ :- b₂ = b₃ )

proof end;

theorem Th49: :: FINSEQ_6:49

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;

theorem Th50: :: FINSEQ_6:50

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

proof end;

theorem Th51: :: FINSEQ_6:51

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

proof end;

theorem Th52: :: FINSEQ_6:52

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

proof end;

theorem Th53: :: FINSEQ_6:53

for b₁ being non empty set
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
<*b₂,b₃*> -: b₃ = <*b₂,b₃*>

proof end;

theorem Th54: :: FINSEQ_6:54

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ holds
<*b₂,b₃,b₄*> -: b₃ = <*b₂,b₃*>

proof end;

theorem Th55: :: FINSEQ_6:55

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ & b₄ <> b₃ holds
<*b₂,b₄,b₃*> -: b₃ = <*b₂,b₄,b₃*>

proof end;

theorem Th56: :: FINSEQ_6:56

for b₁ being non empty set
for b₂ being Element of b₁ holds
( <*b₂*> :- b₂ = <*b₂*> & <*b₂*> -: b₂ = <*b₂*> )

proof end;

theorem Th57: :: FINSEQ_6:57

for b₁ being non empty set
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
<*b₂,b₃*> :- b₃ = <*b₃*>

proof end;

theorem Th58: :: FINSEQ_6:58

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ holds
<*b₂,b₃,b₄*> :- b₃ = <*b₃,b₄*>

proof end;

theorem Th59: :: FINSEQ_6:59

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ & b₄ <> b₃ holds
<*b₂,b₄,b₃*> :- b₃ = <*b₃*>

proof end;

theorem Th60: :: FINSEQ_6:60

canceled;

theorem Th61: :: FINSEQ_6:61

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₃ .. b₄ > b₁ holds
b₃ .. b₄ = b₁ + (b₃ .. (b₄ /^ b₁))

proof end;

theorem Th62: :: FINSEQ_6:62

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₃ .. b₄ > b₁ holds
b₃ in rng (b₄ /^ b₁)

proof end;

theorem Th63: :: FINSEQ_6:63

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

proof end;

theorem Th64: :: FINSEQ_6:64

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₃ .. b₄ > b₁ holds
(b₄ /^ b₁) -: b₃ = (b₄ -: b₃) /^ b₁

proof end;

theorem Th65: :: FINSEQ_6:65

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

proof end;

theorem Th66: :: FINSEQ_6:66

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

proof end;

theorem Th67: :: FINSEQ_6:67

for b₁ being set
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 rng b₄ & b₁ .. b₄ >= b₃ .. b₄ holds
b₁ in rng (b₄ :- b₃)

proof end;

theorem Th68: :: FINSEQ_6:68

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₁ <= len b₄ & b₁ >= b₃ .. b₄ holds
b₄ /. b₁ in rng (b₄ :- b₃)

proof end;

theorem Th69: :: FINSEQ_6:69

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

proof end;

theorem Th70: :: FINSEQ_6:70

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

proof end;

theorem Th71: :: FINSEQ_6:71

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

proof end;

theorem Th72: :: FINSEQ_6:72

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

proof end;

theorem Th73: :: FINSEQ_6:73

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

proof end;

theorem Th74: :: FINSEQ_6:74

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

proof end;

theorem Th75: :: FINSEQ_6:75

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₃ = (rng (b₃ -: b₂)) \/ (rng (b₃ :- b₂))

proof end;

theorem Th76: :: FINSEQ_6:76

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

proof end;

theorem Th77: :: FINSEQ_6:77

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 Th78: :: FINSEQ_6:78

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

proof end;

theorem Th79: :: FINSEQ_6:79

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 Th80: :: FINSEQ_6:80

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

proof end;

theorem Th81: :: FINSEQ_6:81

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₂) /^ 1) = b₃

proof end;

theorem Th82: :: FINSEQ_6:82

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₂ <> {} holds
(b₂ ^ b₃) /^ 1 = (b₂ /^ 1) ^ b₃

proof end;

theorem Th83: :: FINSEQ_6:83

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ & b₂ .. b₃ <> 1 holds
b₂ in rng (b₃ /^ 1)

proof end;

theorem Th84: :: FINSEQ_6:84

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

proof end;

Lemma77: 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₃ .. b₄ > b₁ holds
b₁ + (b₃ .. (b₄ /^ b₁)) = b₃ .. b₄

proof end;

theorem Th85: :: FINSEQ_6:85

canceled;

theorem Th86: :: FINSEQ_6:86

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

proof end;

theorem Th87: :: FINSEQ_6:87

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

proof end;

theorem Th88: :: FINSEQ_6:88

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₃ .. b₄ > b₁ holds
(b₄ /^ b₁) :- b₃ = b₄ :- b₃

proof end;

theorem Th89: :: FINSEQ_6:89

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

proof end;

theorem Th90: :: FINSEQ_6:90

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

proof end;

theorem Th91: :: FINSEQ_6:91

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

proof end;

theorem Th92: :: FINSEQ_6:92

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₃ just_once_values b₂ holds
Rev (b₃ |-- b₂) = (Rev b₃) -| b₂

proof end;

theorem Th93: :: FINSEQ_6:93

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₃ just_once_values b₂ holds
Rev (b₃ :- b₂) = (Rev b₃) -: b₂

proof end;

theorem Th94: :: FINSEQ_6:94

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₃ just_once_values b₂ holds
Rev (b₃ -: b₂) = (Rev b₃) :- b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
attr a₂ is circular means :Def1: :: FINSEQ_6:def 1
a₂ /. 1 = a₂ /. (len a₂);

end;

:: deftheorem Def1 defines circular FINSEQ_6:def 1 :

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be Element of c₁;
func Rotate c₂,c₃ -> FinSequence of a₁ equals :Def2: :: FINSEQ_6:def 2
(a₂ :- a₃) ^ ((a₂ -: a₃) /^ 1) if a₃ in rng a₂
otherwise a₂;
correctness ;

end;

:: deftheorem Def2 defines Rotate FINSEQ_6:def 2 :

registration

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

proof end;

end;

registration

let c₁ be non empty set ;
cluster non empty trivial circular FinSequence of a₁;
existence

proof end;

cluster non empty non trivial circular FinSequence of a₁;
existence

proof end;

end;

theorem Th95: :: FINSEQ_6:95

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds Rotate b₂,(b₂ /. 1) = b₂

proof end;

registration

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

proof end;

end;

theorem Th96: :: FINSEQ_6:96

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₃ is circular & b₂ in rng b₃ holds
rng (Rotate b₃,b₂) = rng b₃

proof end;

theorem Th97: :: FINSEQ_6:97

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₂ in rng (Rotate b₃,b₂)

proof end;

theorem Th98: :: FINSEQ_6:98

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

proof end;

theorem Th99: :: FINSEQ_6:99

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds Rotate (Rotate b₃,b₂),b₂ = Rotate b₃,b₂

proof end;

theorem Th100: :: FINSEQ_6:100

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

proof end;

theorem Th101: :: FINSEQ_6:101

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

proof end;

theorem Th102: :: FINSEQ_6:102

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

proof end;

theorem Th103: :: FINSEQ_6:103

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

proof end;

theorem Th104: :: FINSEQ_6:104

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

proof end;

theorem Th105: :: FINSEQ_6:105

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

proof end;

theorem Th106: :: FINSEQ_6:106

for b₁ being non empty set
for b₂ being non trivial circular FinSequence of b₁ holds rng (b₂ /^ 1) = rng b₂

proof end;

theorem Th107: :: FINSEQ_6:107

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds rng (b₃ /^ 1) c= rng (Rotate b₃,b₂)

proof end;

theorem Th108: :: FINSEQ_6:108

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

proof end;

theorem Th109: :: FINSEQ_6:109

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

proof end;

theorem Th110: :: FINSEQ_6:110

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being FinSequence of b₁ st b₂ in rng (b₄ /^ 1) & b₄ just_once_values b₂ holds
Rotate (Rotate b₄,b₃),b₂ = Rotate b₄,b₂

proof end;

theorem Th111: :: FINSEQ_6:111

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being FinSequence of b₁ st b₄ is circular & b₄ just_once_values b₂ holds
Rotate (Rotate b₄,b₃),b₂ = Rotate b₄,b₂

proof end;

theorem Th112: :: FINSEQ_6:112

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₃ is circular & b₃ just_once_values b₂ holds
Rev (Rotate b₃,b₂) = Rotate (Rev b₃),b₂

proof end;