:: by Andrzej Trybulec

::

:: Received May 24, 1995

:: Copyright (c) 1995-2019 Association of Mizar Users

Lm1: for x, y being set holds rng <*x,y*> = {x,y}

proof end;

Lm2: for x, y, z being set holds rng <*x,y,z*> = {x,y,z}

proof end;

theorem Th2: :: FINSEQ_6:2

for k being Nat

for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds

f . i <> f . k ) holds

(f . k) .. f = k

for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds

f . i <> f . k ) holds

(f . k) .. f = k

proof end;

theorem Th7: :: FINSEQ_6:7

for f1, f2 being FinSequence

for p being set st p in (rng f2) \ (rng f1) holds

p .. (f1 ^ f2) = (len f1) + (p .. f2)

for p being set st p in (rng f2) \ (rng f1) holds

p .. (f1 ^ f2) = (len f1) + (p .. f2)

proof end;

theorem Th9: :: FINSEQ_6:9

for f1, f2 being FinSequence

for p being set st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) |-- p = f2 |-- p

for p being set st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) |-- p = f2 |-- p

proof end;

theorem :: FINSEQ_6:11

for f1, f2 being FinSequence

for A being set st A c= dom f1 holds

(f1 ^ f2) | A = f1 | A by Th10, GRFUNC_1:27;

for A being set st A c= dom f1 holds

(f1 ^ f2) | A = f1 | A by Th10, GRFUNC_1:27;

registration
end;

theorem Th14: :: FINSEQ_6:14

for f1, f2 being FinSequence

for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))

for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))

proof end;

theorem Th15: :: FINSEQ_6:15

for f1, f2 being FinSequence

for p being set st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) -| p = f1 ^ (f2 -| p)

for p being set st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) -| p = f1 ^ (f2 -| p)

proof end;

theorem Th16: :: FINSEQ_6:16

for f1, f2 being FinSequence

for p being set st f1 ^ f2 just_once_values p holds

p in (rng f1) \+\ (rng f2)

for p being set st f1 ^ f2 just_once_values p holds

p in (rng f1) \+\ (rng f2)

proof end;

theorem :: FINSEQ_6:17

for f1, f2 being FinSequence

for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds

f1 just_once_values p

for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds

f1 just_once_values p

proof end;

theorem Th35: :: FINSEQ_6:35

for x, y being set

for f being FinSequence st x in rng f & y in rng (f -| x) holds

(f -| x) -| y = f -| y

for f being FinSequence st x in rng f & y in rng (f -| x) holds

(f -| x) -| y = f -| y

proof end;

theorem Th36: :: FINSEQ_6:36

for x being set

for f1, f2 being FinSequence st not x in rng f1 holds

x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1

for f1, f2 being FinSequence st not x in rng f1 holds

x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1

proof end;

theorem Th37: :: FINSEQ_6:37

for x being set

for f being FinSequence st f just_once_values x holds

(x .. f) + (x .. (Rev f)) = (len f) + 1

for f being FinSequence st f just_once_values x holds

(x .. f) + (x .. (Rev f)) = (len f) + 1

proof end;

theorem Th40: :: FINSEQ_6:40

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) ^ <*p*>

for p being Element of D

for f being FinSequence of D st p in rng f holds

f -: p = (f -| p) ^ <*p*>

proof end;

theorem Th41: :: FINSEQ_6: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 = <*p*> ^ (f |-- p)

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 Th44: :: FINSEQ_6:44

for D being non empty set

for p being Element of D

for f being FinSequence of D st f <> {} & f /. 1 = p holds

( f -: p = <*p*> & f :- p = f )

for p being Element of D

for f being FinSequence of D st f <> {} & f /. 1 = p holds

( f -: p = <*p*> & f :- p = f )

proof end;

theorem Th45: :: FINSEQ_6:45

for D being non empty set

for p1 being Element of D

for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f

for p1 being Element of D

for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f

proof end;

theorem Th48: :: FINSEQ_6:48

for k being Nat

for D being non empty set

for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds

f /. i <> f /. k ) holds

(f /. k) .. f = k

for D being non empty set

for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds

f /. i <> f /. k ) holds

(f /. k) .. f = k

proof end;

theorem Th49: :: FINSEQ_6:49

for D being non empty set

for p1, p2 being Element of D st p1 <> p2 holds

<*p1,p2*> -: p2 = <*p1,p2*>

for p1, p2 being Element of D st p1 <> p2 holds

<*p1,p2*> -: p2 = <*p1,p2*>

proof end;

theorem Th50: :: FINSEQ_6:50

for D being non empty set

for p1, p2, p3 being Element of D st p1 <> p2 holds

<*p1,p2,p3*> -: p2 = <*p1,p2*>

for p1, p2, p3 being Element of D st p1 <> p2 holds

<*p1,p2,p3*> -: p2 = <*p1,p2*>

proof end;

theorem Th51: :: FINSEQ_6:51

for D being non empty set

for p1, p2, p3 being Element of D st p1 <> p3 & p2 <> p3 holds

<*p1,p2,p3*> -: p3 = <*p1,p2,p3*>

for p1, p2, p3 being Element of D st p1 <> p3 & p2 <> p3 holds

<*p1,p2,p3*> -: p3 = <*p1,p2,p3*>

proof end;

theorem :: FINSEQ_6:52

for D being non empty set

for p being Element of D holds

( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> )

for p being Element of D holds

( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> )

proof end;

theorem Th54: :: FINSEQ_6:54

for D being non empty set

for p1, p2, p3 being Element of D st p1 <> p2 holds

<*p1,p2,p3*> :- p2 = <*p2,p3*>

for p1, p2, p3 being Element of D st p1 <> p2 holds

<*p1,p2,p3*> :- p2 = <*p2,p3*>

proof end;

theorem Th55: :: FINSEQ_6:55

for D being non empty set

for p1, p2, p3 being Element of D st p1 <> p3 & p2 <> p3 holds

<*p1,p2,p3*> :- p3 = <*p3*>

for p1, p2, p3 being Element of D st p1 <> p3 & p2 <> p3 holds

<*p1,p2,p3*> :- p3 = <*p3*>

proof end;

theorem Th56: :: FINSEQ_6:56

for k 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 & p .. f > k holds

p .. f = k + (p .. (f /^ k))

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p .. f = k + (p .. (f /^ k))

proof end;

theorem Th57: :: FINSEQ_6:57

for k 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 & p .. f > k holds

p in rng (f /^ k)

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p in rng (f /^ k)

proof end;

theorem Th58: :: FINSEQ_6:58

for i, k being Nat

for D being non empty set

for f being FinSequence of D st k < i & i in dom f holds

f /. i in rng (f /^ k)

for D being non empty set

for f being FinSequence of D st k < i & i in dom f holds

f /. i in rng (f /^ k)

proof end;

theorem Th59: :: FINSEQ_6:59

for k 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 & p .. f > k holds

(f /^ k) -: p = (f -: p) /^ k

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

(f /^ k) -: p = (f -: p) /^ k

proof end;

theorem Th60: :: FINSEQ_6:60

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) -: p = (f -: p) /^ 1

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) -: p = (f -: p) /^ 1

proof end;

theorem Th61: :: FINSEQ_6:61

for D being non empty set

for p being Element of D

for f being FinSequence of D holds p in rng (f :- p)

for p being Element of D

for f being FinSequence of D holds p in rng (f :- p)

proof end;

theorem Th62: :: FINSEQ_6:62

for x being set

for D being non empty set

for p being Element of D

for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds

x in rng (f :- p)

for D being non empty set

for p being Element of D

for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds

x in rng (f :- p)

proof end;

theorem Th63: :: FINSEQ_6:63

for k 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 & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

proof end;

theorem Th64: :: FINSEQ_6:64

for D being non empty set

for p being Element of D

for f1, f2 being FinSequence of D st p in rng f1 holds

(f1 ^ f2) :- p = (f1 :- p) ^ f2

for p being Element of D

for f1, f2 being FinSequence of D st p in rng f1 holds

(f1 ^ f2) :- p = (f1 :- p) ^ f2

proof end;

theorem Th65: :: FINSEQ_6:65

for D being non empty set

for p being Element of D

for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) :- p = f2 :- p

for p being Element of D

for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) :- p = f2 :- p

proof end;

theorem Th66: :: FINSEQ_6:66

for D being non empty set

for p being Element of D

for f1, f2 being FinSequence of D st p in rng f1 holds

(f1 ^ f2) -: p = f1 -: p

for p being Element of D

for f1, f2 being FinSequence of D st p in rng f1 holds

(f1 ^ f2) -: p = f1 -: p

proof end;

theorem Th67: :: FINSEQ_6:67

for D being non empty set

for p being Element of D

for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) -: p = f1 ^ (f2 -: p)

for p being Element of D

for f1, f2 being FinSequence of D st p in (rng f2) \ (rng f1) holds

(f1 ^ f2) -: p = f1 ^ (f2 -: p)

proof end;

theorem :: FINSEQ_6:68

for D being non empty set

for p being Element of D

for f being FinSequence of D holds (f :- p) :- p = f :- p

for p being Element of D

for f being FinSequence of D holds (f :- p) :- p = f :- p

proof end;

theorem Th69: :: FINSEQ_6:69

for D being non empty set

for p1, p2 being Element of D

for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds

f |-- p2 = (f |-- p1) |-- p2

for p1, p2 being Element of D

for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds

f |-- p2 = (f |-- p1) |-- p2

proof end;

theorem Th70: :: FINSEQ_6:70

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 = (rng (f -: p)) \/ (rng (f :- p))

for p being Element of D

for f being FinSequence of D st p in rng f holds

rng f = (rng (f -: p)) \/ (rng (f :- p))

proof end;

theorem Th71: :: FINSEQ_6:71

for D being non empty set

for p1, p2 being Element of D

for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds

(f :- p1) :- p2 = f :- p2

for p1, p2 being Element of D

for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds

(f :- p1) :- p2 = f :- p2

proof end;

theorem Th72: :: FINSEQ_6:72

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f holds

p .. (f -: p) = p .. f

for p being Element of D

for f being FinSequence of D st p in rng f holds

p .. (f -: p) = p .. f

proof end;

theorem :: FINSEQ_6:73

theorem Th74: :: FINSEQ_6:74

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

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 Th75: :: FINSEQ_6:75

for D being non empty set

for p1, p2 being Element of D

for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds

(f -: p1) -: p2 = f -: p2

for p1, p2 being Element of D

for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds

(f -: p1) -: p2 = f -: p2

proof end;

theorem Th76: :: FINSEQ_6:76

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) /^ 1) = f

for p being Element of D

for f being FinSequence of D st p in rng f holds

(f -: p) ^ ((f :- p) /^ 1) = f

proof end;

theorem Th77: :: FINSEQ_6:77

for D being non empty set

for f1, f2 being FinSequence of D st f1 <> {} holds

(f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2

for f1, f2 being FinSequence of D st f1 <> {} holds

(f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2

proof end;

theorem Th78: :: FINSEQ_6:78

for D being non empty set

for p2 being Element of D

for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds

p2 in rng (f /^ 1)

for p2 being Element of D

for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds

p2 in rng (f /^ 1)

proof end;

theorem Th79: :: FINSEQ_6:79

for D being non empty set

for p being Element of D

for f being FinSequence of D holds p .. (f :- p) = 1

for p being Element of D

for f being FinSequence of D holds p .. (f :- p) = 1

proof end;

Lm3: 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 & p .. f > i holds

i + (p .. (f /^ i)) = p .. f

proof end;

theorem Th81: :: FINSEQ_6:81

for i, k being Nat

for D being non empty set

for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k

for D being non empty set

for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k

proof end;

theorem Th82: :: FINSEQ_6:82

for k 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 & p .. f > k holds

(f /^ k) :- p = f :- p

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

(f /^ k) :- p = f :- p

proof end;

theorem Th83: :: FINSEQ_6:83

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) :- p = f :- p

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) :- p = f :- p

proof end;

theorem Th84: :: FINSEQ_6:84

for i, k being Nat

for D being non empty set

for f being FinSequence of D st i + k = len f holds

Rev (f /^ k) = (Rev f) | i

for D being non empty set

for f being FinSequence of D st i + k = len f holds

Rev (f /^ k) = (Rev f) | i

proof end;

theorem Th85: :: FINSEQ_6:85

for i, k being Nat

for D being non empty set

for f being FinSequence of D st i + k = len f holds

Rev (f | k) = (Rev f) /^ i

for D being non empty set

for f being FinSequence of D st i + k = len f holds

Rev (f | k) = (Rev f) /^ i

proof end;

theorem Th86: :: FINSEQ_6:86

for D being non empty set

for p being Element of D

for f being FinSequence of D st f just_once_values p holds

Rev (f |-- p) = (Rev f) -| p

for p being Element of D

for f being FinSequence of D st f just_once_values p holds

Rev (f |-- p) = (Rev f) -| p

proof end;

theorem Th87: :: FINSEQ_6:87

for D being non empty set

for p being Element of D

for f being FinSequence of D st f just_once_values p holds

Rev (f :- p) = (Rev f) -: p

for p being Element of D

for f being FinSequence of D st f just_once_values p holds

Rev (f :- p) = (Rev f) -: p

proof end;

theorem Th88: :: FINSEQ_6:88

for D being non empty set

for p being Element of D

for f being FinSequence of D st f just_once_values p holds

Rev (f -: p) = (Rev f) :- p

for p being Element of D

for f being FinSequence of D st f just_once_values p holds

Rev (f -: p) = (Rev f) :- p

proof end;

:: deftheorem Def1A defines circular FINSEQ_6:def 1 :

for D being non empty set

for IT being FinSequence of D holds

( IT is circular iff IT /. 1 = IT /. (len IT) );

for D being non empty set

for IT being FinSequence of D holds

( IT is circular iff IT /. 1 = IT /. (len IT) );

definition

let D be non empty set ;

let f be FinSequence of D;

let p be Element of D;

coherence

( ( p in rng f implies (f :- p) ^ ((f -: p) /^ 1) is FinSequence of D ) & ( not p in rng f implies f is FinSequence of D ) );

consistency

for b_{1} being FinSequence of D holds verum;

;

end;
let f be FinSequence of D;

let p be Element of D;

func Rotate (f,p) -> FinSequence of D equals :Def2: :: FINSEQ_6:def 2

(f :- p) ^ ((f -: p) /^ 1) if p in rng f

otherwise f;

correctness (f :- p) ^ ((f -: p) /^ 1) if p in rng f

otherwise f;

coherence

( ( p in rng f implies (f :- p) ^ ((f -: p) /^ 1) is FinSequence of D ) & ( not p in rng f implies f is FinSequence of D ) );

consistency

for b

;

:: deftheorem Def2 defines Rotate FINSEQ_6:def 2 :

for D being non empty set

for f being FinSequence of D

for p being Element of D holds

( ( p in rng f implies Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) ) & ( not p in rng f implies Rotate (f,p) = f ) );

for D being non empty set

for f being FinSequence of D

for p being Element of D holds

( ( p in rng f implies Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) ) & ( not p in rng f implies Rotate (f,p) = f ) );

registration

let D be non empty set ;

let f be non empty FinSequence of D;

let p be Element of D;

coherence

not Rotate (f,p) is empty

end;
let f be non empty FinSequence of D;

let p be Element of D;

coherence

not Rotate (f,p) is empty

proof end;

registration

let D be non empty set ;

ex b_{1} being FinSequence of D st

( b_{1} is circular & b_{1} is 1 -element )

ex b_{1} being FinSequence of D st

( b_{1} is circular & not b_{1} is trivial )

end;
cluster Relation-like omega -defined D -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like circular for FinSequence of D;

existence ex b

( b

proof end;

cluster Relation-like omega -defined D -valued non trivial Function-like finite FinSequence-like FinSubsequence-like circular for FinSequence of D;

existence ex b

( b

proof end;

registration

let D be non empty set ;

let p be Element of D;

let f be non empty circular FinSequence of D;

coherence

Rotate (f,p) is circular

end;
let p be Element of D;

let f be non empty circular FinSequence of D;

coherence

Rotate (f,p) is circular

proof end;

theorem Th90: :: FINSEQ_6:90

for D being non empty set

for p being Element of D

for f being FinSequence of D st f is circular & p in rng f holds

rng (Rotate (f,p)) = rng f

for p being Element of D

for f being FinSequence of D st f is circular & p in rng f holds

rng (Rotate (f,p)) = rng f

proof end;

theorem Th91: :: FINSEQ_6:91

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f holds

p in rng (Rotate (f,p))

for p being Element of D

for f being FinSequence of D st p in rng f holds

p in rng (Rotate (f,p))

proof end;

theorem Th92: :: FINSEQ_6:92

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. 1 = p

for p being Element of D

for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. 1 = p

proof end;

theorem Th93: :: FINSEQ_6:93

for D being non empty set

for p being Element of D

for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p)

for p being Element of D

for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p)

proof end;

theorem Th97: :: FINSEQ_6:97

for D being non empty set

for p1, p2, p3 being Element of D holds Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*>

for p1, p2, p3 being Element of D holds Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*>

proof end;

theorem :: FINSEQ_6:98

for D being non empty set

for p1, p2, p3 being Element of D st p1 <> p2 holds

Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*>

for p1, p2, p3 being Element of D st p1 <> p2 holds

Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*>

proof end;

theorem :: FINSEQ_6:99

for D being non empty set

for p1, p2, p3 being Element of D st p2 <> p3 holds

Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>

for p1, p2, p3 being Element of D st p2 <> p3 holds

Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>

proof end;

theorem :: FINSEQ_6:100

for D being non empty set

for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f

for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f

proof end;

theorem Th101: :: FINSEQ_6:101

for D being non empty set

for p being Element of D

for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p))

for p being Element of D

for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p))

proof end;

theorem Th102: :: FINSEQ_6:102

for D being non empty set

for p1, p2 being Element of D

for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

for p1, p2 being Element of D

for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

proof end;

theorem Th103: :: FINSEQ_6:103

for D being non empty set

for p1, p2 being Element of D

for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

for p1, p2 being Element of D

for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

proof end;

theorem Th104: :: FINSEQ_6:104

for D being non empty set

for p1, p2 being Element of D

for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

for p1, p2 being Element of D

for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

proof end;

theorem :: FINSEQ_6:105

for D being non empty set

for p1, p2 being Element of D

for f being FinSequence of D st f is circular & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

for p1, p2 being Element of D

for f being FinSequence of D st f is circular & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

proof end;

theorem :: FINSEQ_6:106

for D being non empty set

for p being Element of D

for f being FinSequence of D st f is circular & f just_once_values p holds

Rev (Rotate (f,p)) = Rotate ((Rev f),p)

for p being Element of D

for f being FinSequence of D st f is circular & f just_once_values p holds

Rev (Rotate (f,p)) = Rotate ((Rev f),p)

proof end;

:: from AMISTD_1, 2007.07.26, A.T.

theorem :: FINSEQ_6:107

for D being non empty set

for f being trivial FinSequence of D holds

( f is empty or ex x being Element of D st f = <*x*> )

for f being trivial FinSequence of D holds

( f is empty or ex x being Element of D st f = <*x*> )

proof end;

theorem :: FINSEQ_6:108

for i being Nat

for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds

(p ^ q) . i = q . (i - (len p))

for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds

(p ^ q) . i = q . (i - (len p))

proof end;

theorem :: FINSEQ_6:109

for D being non empty set

for x being set

for f being FinSequence of D st 1 <= len f holds

( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )

for x being set

for f being FinSequence of D st 1 <= len f holds

( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) )

proof end;

theorem :: FINSEQ_6:111

for D being non empty set

for f being FinSequence of D

for k being Nat holds len (f /^ k) = (len f) -' k by RFINSEQ:29;

for f being FinSequence of D

for k being Nat holds len (f /^ k) = (len f) -' k by RFINSEQ:29;

definition

let f be FinSequence;

let k1, k2 be Nat;

coherence

( ( k1 <= k2 implies (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is FinSequence ) & ( not k1 <= k2 implies Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is FinSequence ) );

consistency

for b_{1} being FinSequence holds verum;

;

end;
let k1, k2 be Nat;

func mid (f,k1,k2) -> FinSequence equals :Def3: :: FINSEQ_6:def 3

(f /^ (k1 -' 1)) | ((k2 -' k1) + 1) if k1 <= k2

otherwise Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1));

correctness (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) if k1 <= k2

otherwise Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1));

coherence

( ( k1 <= k2 implies (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is FinSequence ) & ( not k1 <= k2 implies Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is FinSequence ) );

consistency

for b

;

:: deftheorem Def3 defines mid FINSEQ_6:def 3 :

for f being FinSequence

for k1, k2 being Nat holds

( ( k1 <= k2 implies mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) ) & ( not k1 <= k2 implies mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) );

for f being FinSequence

for k1, k2 being Nat holds

( ( k1 <= k2 implies mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) ) & ( not k1 <= k2 implies mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) );

definition

let D be non empty set ;

let f be FinSequence of D;

let k1, k2 be Nat;

:: original: mid

redefine func mid (f,k1,k2) -> FinSequence of D;

coherence

mid (f,k1,k2) is FinSequence of D

end;
let f be FinSequence of D;

let k1, k2 be Nat;

:: original: mid

redefine func mid (f,k1,k2) -> FinSequence of D;

coherence

mid (f,k1,k2) is FinSequence of D

proof end;

::$CT

theorem :: FINSEQ_6:113

for D being non empty set

for f being FinSequence of D

for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds

Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))

for f being FinSequence of D

for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds

Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))

proof end;

theorem Th113: :: FINSEQ_6:114

for n, m being Nat

for f being FinSequence st 1 <= m & m + n <= len f holds

(f /^ n) . m = f . (m + n)

for f being FinSequence st 1 <= m & m + n <= len f holds

(f /^ n) . m = f . (m + n)

proof end;

theorem Th114: :: FINSEQ_6:115

for i being Nat

for f being FinSequence st 1 <= i & i <= len f holds

(Rev f) . i = f . (((len f) - i) + 1)

for f being FinSequence st 1 <= i & i <= len f holds

(Rev f) . i = f . (((len f) - i) + 1)

proof end;

theorem Th117: :: FINSEQ_6:118

for f being FinSequence

for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds

( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )

for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds

( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )

proof end;

theorem :: FINSEQ_6:121

for D being non empty set

for f being FinSequence of D st 1 <= len f holds

mid (f,(len f),1) = Rev f

for f being FinSequence of D st 1 <= len f holds

mid (f,(len f),1) = Rev f

proof end;

theorem Th121: :: FINSEQ_6:122

for f being FinSequence

for k1, k2, i being Nat st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds

( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) )

for k1, k2, i being Nat st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds

( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) )

proof end;

theorem :: FINSEQ_6:123

for f being FinSequence

for k, i being Nat st 1 <= i & i <= k & k <= len f holds

(mid (f,1,k)) . i = f . i

for k, i being Nat st 1 <= i & i <= k & k <= len f holds

(mid (f,1,k)) . i = f . i

proof end;

theorem Th124: :: FINSEQ_6:125

for f being FinSequence

for k being Nat

for p being set holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)

for k being Nat

for p being set holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)

proof end;

Th126: for D being non empty set

for f being FinSequence of D

for k1, k2 being Nat st k1 < k2 & k1 in dom f holds

mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2))

proof end;

theorem :: FINSEQ_6:126

for p being FinSequence

for k1, k2 being Nat st k1 < k2 & k1 in dom p holds

mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))

for k1, k2 being Nat st k1 < k2 & k1 in dom p holds

mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))

proof end;

theorem Th1: :: FINSEQ_6:127

for m, k, n being Nat holds

( ( m + 1 <= k & k <= n ) iff ex i being Nat st

( m <= i & i < n & k = i + 1 ) )

( ( m + 1 <= k & k <= n ) iff ex i being Nat st

( m <= i & i < n & k = i + 1 ) )

proof end;

theorem :: FINSEQ_6:128

for p, q being FinSequence

for n being Nat st q = p | (Seg n) holds

( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

for n being Nat st q = p | (Seg n) holds

( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

proof end;

theorem Th3: :: FINSEQ_6:129

for X, Y being set

for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds

(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds

(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

proof end;

Lm1: for m, n being Nat

for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds

card F = n + 1

proof end;

theorem :: FINSEQ_6:131

for m, n, l being Nat st 1 <= l & l <= n holds

(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l

(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l

proof end;

definition

let p be FinSequence;

let m, n be Nat;

for b_{1} being FinSequence holds verum
;

existence

( ( 1 <= m & m <= n & n <= len p implies ex b_{1} being FinSequence st

( (len b_{1}) + m = n + 1 & ( for i being Nat st i < len b_{1} holds

b_{1} . (i + 1) = p . (m + i) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ex b_{1} being FinSequence st b_{1} = {} ) )

for b_{1}, b_{2} being FinSequence holds

( ( 1 <= m & m <= n & n <= len p & (len b_{1}) + m = n + 1 & ( for i being Nat st i < len b_{1} holds

b_{1} . (i + 1) = p . (m + i) ) & (len b_{2}) + m = n + 1 & ( for i being Nat st i < len b_{2} holds

b_{2} . (i + 1) = p . (m + i) ) implies b_{1} = b_{2} ) & ( ( not 1 <= m or not m <= n or not n <= len p ) & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

end;
let m, n be Nat;

func (m,n) -cut p -> FinSequence means :Def1: :: FINSEQ_6:def 4

( (len it) + m = n + 1 & ( for i being Nat st i < len it holds

it . (i + 1) = p . (m + i) ) ) if ( 1 <= m & m <= n & n <= len p )

otherwise it = {} ;

consistency ( (len it) + m = n + 1 & ( for i being Nat st i < len it holds

it . (i + 1) = p . (m + i) ) ) if ( 1 <= m & m <= n & n <= len p )

otherwise it = {} ;

for b

existence

( ( 1 <= m & m <= n & n <= len p implies ex b

( (len b

b

proof end;

uniqueness for b

( ( 1 <= m & m <= n & n <= len p & (len b

b

b

proof end;

:: deftheorem Def1 defines -cut FINSEQ_6:def 4 :

for p being FinSequence

for m, n being Nat

for b_{4} being FinSequence holds

( ( 1 <= m & m <= n & n <= len p implies ( b_{4} = (m,n) -cut p iff ( (len b_{4}) + m = n + 1 & ( for i being Nat st i < len b_{4} holds

b_{4} . (i + 1) = p . (m + i) ) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ( b_{4} = (m,n) -cut p iff b_{4} = {} ) ) );

for p being FinSequence

for m, n being Nat

for b

( ( 1 <= m & m <= n & n <= len p implies ( b

b

Lm2: for p being FinSequence

for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds

( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds

((m,n) -cut p) . (i + 1) = p . (m + i) ) )

proof end;

theorem Th8: :: FINSEQ_6:134

for p being FinSequence

for m, n, r being Nat st m <= n & n <= r & r <= len p holds

(((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p

for m, n, r being Nat st m <= n & n <= r & r <= len p holds

(((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p

proof end;

theorem :: FINSEQ_6:135

for p being FinSequence

for m being Nat st m <= len p holds

((1,m) -cut p) ^ (((m + 1),(len p)) -cut p) = p

for m being Nat st m <= len p holds

((1,m) -cut p) ^ (((m + 1),(len p)) -cut p) = p

proof end;

theorem :: FINSEQ_6:136

for p being FinSequence

for m, n being Nat st m <= n & n <= len p holds

(((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p

for m, n being Nat st m <= n & n <= len p holds

(((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p

proof end;

definition

let D be set ;

let p be FinSequence of D;

let m, n be Nat;

:: original: -cut

redefine func (m,n) -cut p -> FinSequence of D;

coherence

(m,n) -cut p is FinSequence of D

end;
let p be FinSequence of D;

let m, n be Nat;

:: original: -cut

redefine func (m,n) -cut p -> FinSequence of D;

coherence

(m,n) -cut p is FinSequence of D

proof end;

theorem :: FINSEQ_6:138

for p being FinSequence

for m, n being Nat st 1 <= m & m <= n & n <= len p holds

( ((m,n) -cut p) . 1 = p . m & ((m,n) -cut p) . (len ((m,n) -cut p)) = p . n )

for m, n being Nat st 1 <= m & m <= n & n <= len p holds

( ((m,n) -cut p) . 1 = p . m & ((m,n) -cut p) . (len ((m,n) -cut p)) = p . n )

proof end;

definition
end;

:: deftheorem defines ^' FINSEQ_6:def 5 :

for p, q being FinSequence holds p ^' q = p ^ ((2,(len q)) -cut q);

for p, q being FinSequence holds p ^' q = p ^ ((2,(len q)) -cut q);

theorem Th15: :: FINSEQ_6:141

for p, q being FinSequence

for k being Nat st 1 <= k & k < len q holds

(p ^' q) . ((len p) + k) = q . (k + 1)

for k being Nat st 1 <= k & k < len q holds

(p ^' q) . ((len p) + k) = q . (k + 1)

proof end;

definition

let D be set ;

let p, q be FinSequence of D;

:: original: ^'

redefine func p ^' q -> FinSequence of D;

coherence

p ^' q is FinSequence of D

end;
let p, q be FinSequence of D;

:: original: ^'

redefine func p ^' q -> FinSequence of D;

coherence

p ^' q is FinSequence of D

proof end;

theorem :: FINSEQ_6:144

for p, q being FinSequence st p <> {} & q <> {} & p . (len p) = q . 1 holds

rng (p ^' q) = (rng p) \/ (rng q)

rng (p ^' q) = (rng p) \/ (rng q)

proof end;

:: deftheorem defines TwoValued FINSEQ_6:def 6 :

for f being FinSequence holds

( f is TwoValued iff card (rng f) = 2 );

for f being FinSequence holds

( f is TwoValued iff card (rng f) = 2 );

Lm3: now :: thesis: ( len <*1,2*> > 1 & 1 <> 2 & rng <*1,2*> = {1,2} )

set p = <*1,2*>;

2 > 1 ;

hence len <*1,2*> > 1 by FINSEQ_1:44; :: thesis: ( 1 <> 2 & rng <*1,2*> = {1,2} )

thus 1 <> 2 ; :: thesis: rng <*1,2*> = {1,2}

thus rng <*1,2*> = (rng <*1*>) \/ (rng <*2*>) by FINSEQ_1:31

.= {1} \/ (rng <*2*>) by FINSEQ_1:38

.= {1} \/ {2} by FINSEQ_1:38

.= {1,2} by ENUMSET1:1 ; :: thesis: verum

end;
2 > 1 ;

hence len <*1,2*> > 1 by FINSEQ_1:44; :: thesis: ( 1 <> 2 & rng <*1,2*> = {1,2} )

thus 1 <> 2 ; :: thesis: rng <*1,2*> = {1,2}

thus rng <*1,2*> = (rng <*1*>) \/ (rng <*2*>) by FINSEQ_1:31

.= {1} \/ (rng <*2*>) by FINSEQ_1:38

.= {1} \/ {2} by FINSEQ_1:38

.= {1,2} by ENUMSET1:1 ; :: thesis: verum

theorem Th19: :: FINSEQ_6:145

for p being FinSequence holds

( p is TwoValued iff ( len p > 1 & ex x, y being object st

( x <> y & rng p = {x,y} ) ) )

( p is TwoValued iff ( len p > 1 & ex x, y being object st

( x <> y & rng p = {x,y} ) ) )

proof end;

then Lm4: <*1,2*> is TwoValued

by Lm3;

Lm5: now :: thesis: for i being Nat st 1 <= i & i + 1 <= len <*1,2*> holds

<*1,2*> . i <> <*1,2*> . (i + 1)

<*1,2*> . i <> <*1,2*> . (i + 1)

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len <*1,2*> implies <*1,2*> . i <> <*1,2*> . (i + 1) )

set p = <*1,2*>;

assume that

A1: 1 <= i and

A2: i + 1 <= len <*1,2*> ; :: thesis: <*1,2*> . i <> <*1,2*> . (i + 1)

i + 1 <= 1 + 1 by A2, FINSEQ_1:44;

then i <= 1 by XREAL_1:6;

then A3: i = 1 by A1, XXREAL_0:1;

then <*1,2*> . i = 1 by FINSEQ_1:44;

hence <*1,2*> . i <> <*1,2*> . (i + 1) by A3, FINSEQ_1:44; :: thesis: verum

end;
set p = <*1,2*>;

assume that

A1: 1 <= i and

A2: i + 1 <= len <*1,2*> ; :: thesis: <*1,2*> . i <> <*1,2*> . (i + 1)

i + 1 <= 1 + 1 by A2, FINSEQ_1:44;

then i <= 1 by XREAL_1:6;

then A3: i = 1 by A1, XXREAL_0:1;

then <*1,2*> . i = 1 by FINSEQ_1:44;

hence <*1,2*> . i <> <*1,2*> . (i + 1) by A3, FINSEQ_1:44; :: thesis: verum

:: deftheorem Def4 defines Alternating FINSEQ_6:def 7 :

for f being FinSequence holds

( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds

f . i <> f . (i + 1) );

for f being FinSequence holds

( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds

f . i <> f . (i + 1) );

Lm6: <*1,2*> is Alternating

by Lm5;

registration

ex b_{1} being FinSequence st

( b_{1} is TwoValued & b_{1} is Alternating )
by Lm4, Lm6;

end;

cluster Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like TwoValued Alternating for set ;

existence ex b

( b

theorem Th20: :: FINSEQ_6:146

for a1, a2 being TwoValued Alternating FinSequence st len a1 = len a2 & rng a1 = rng a2 & a1 . 1 = a2 . 1 holds

a1 = a2

a1 = a2

proof end;

theorem Th21: :: FINSEQ_6:147

for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds

for i being Nat st 1 <= i & i <= len a1 holds

a1 . i <> a2 . i

for i being Nat st 1 <= i & i <= len a1 holds

a1 . i <> a2 . i

proof end;

theorem :: FINSEQ_6:148

for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds

for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds

a = a2

for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds

a = a2

proof end;

theorem :: FINSEQ_6:149

for X, Y being set

for n being Nat st X <> Y & n > 1 holds

ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

for n being Nat st X <> Y & n > 1 holds

ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

proof end;

registration

let X be set ;

let fs be FinSequence of X;

coherence

for b_{1} being Subset of fs holds b_{1} is FinSubsequence-like

end;
let fs be FinSequence of X;

coherence

for b

proof end;

theorem :: FINSEQ_6:150

for f being FinSubsequence

for g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) holds

fgh = fg ^ fh

for g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) holds

fgh = fg ^ fh

proof end;

theorem :: FINSEQ_6:151

for X being set

for fs being FinSequence of X

for fss being Subset of fs holds

( dom fss c= dom fs & rng fss c= rng fs ) by RELAT_1:11;

for fs being FinSequence of X

for fss being Subset of fs holds

( dom fss c= dom fs & rng fss c= rng fs ) by RELAT_1:11;

theorem :: FINSEQ_6:153

for X, Y being set

for fs being FinSequence of X

for fss being Subset of fs holds fss | Y is Subset of fs

for fs being FinSequence of X

for fss being Subset of fs holds fss | Y is Subset of fs

proof end;

theorem :: FINSEQ_6:154

for X being set

for fs, fs1, fs2 being FinSequence of X

for fss, fss2 being Subset of fs

for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds

Seq fss2 = fs2

for fs, fs1, fs2 being FinSequence of X

for fss, fss2 being Subset of fs

for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds

Seq fss2 = fs2

proof end;

:: from AMISTD_1, 2006.01.12, A.T.

theorem :: FINSEQ_6:155

for D being non empty set

for f1 being non empty FinSequence of D

for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1

for f1 being non empty FinSequence of D

for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1

proof end;

theorem :: FINSEQ_6:156

for D being non empty set

for f1 being FinSequence of D

for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)

for f1 being FinSequence of D

for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)

proof end;

theorem :: FINSEQ_6:159

for D being non empty set

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds

(f1 ^' f2) /. n = f1 /. n

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds

(f1 ^' f2) /. n = f1 /. n

proof end;

theorem :: FINSEQ_6:160

for D being non empty set

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds

(f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds

(f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)

proof end;

:: from SFMASTR3, 2007.07.26, A.T.

definition

let F be FinSequence of INT ;

let m, n be Nat;

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len F ;

ex b_{1} being Nat ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{1} + 1 = ((min X) .. ((m,n) -cut F)) + m )

for b_{1}, b_{2} being Nat st ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{1} + 1 = ((min X) .. ((m,n) -cut F)) + m ) & ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{2} + 1 = ((min X) .. ((m,n) -cut F)) + m ) holds

b_{1} = b_{2}
;

end;
let m, n be Nat;

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len F ;

func min_at (F,m,n) -> Nat means :Def11: :: FINSEQ_6:def 8

ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & it + 1 = ((min X) .. ((m,n) -cut F)) + m );

existence ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & it + 1 = ((min X) .. ((m,n) -cut F)) + m );

ex b

( X = rng ((m,n) -cut F) & b

proof end;

uniqueness for b

( X = rng ((m,n) -cut F) & b

( X = rng ((m,n) -cut F) & b

b

:: deftheorem Def11 defines min_at FINSEQ_6:def 8 :

for F being FinSequence of INT

for m, n being Nat st 1 <= m & m <= n & n <= len F holds

for b_{4} being Nat holds

( b_{4} = min_at (F,m,n) iff ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{4} + 1 = ((min X) .. ((m,n) -cut F)) + m ) );

for F being FinSequence of INT

for m, n being Nat st 1 <= m & m <= n & n <= len F holds

for b

( b

( X = rng ((m,n) -cut F) & b

theorem Th59: :: FINSEQ_6:161

for F being FinSequence of INT

for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds

( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds

( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

proof end;

definition

let F be FinSequence of INT ;

let m, n be Nat;

end;
let m, n be Nat;

pred F is_non_decreasing_on m,n means :: FINSEQ_6:def 9

for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j;

for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j;

:: deftheorem defines is_non_decreasing_on FINSEQ_6:def 9 :

for F being FinSequence of INT

for m, n being Nat holds

( F is_non_decreasing_on m,n iff for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j );

for F being FinSequence of INT

for m, n being Nat holds

( F is_non_decreasing_on m,n iff for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j );

:: deftheorem defines is_split_at FINSEQ_6:def 10 :

for F being FinSequence of INT

for n being Nat holds

( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds

F . i <= F . j );

for F being FinSequence of INT

for n being Nat holds

( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds

F . i <= F . j );

theorem :: FINSEQ_6:163

for F, F1 being FinSequence of INT

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_non_decreasing_on 1,k + 1

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_non_decreasing_on 1,k + 1

proof end;

theorem :: FINSEQ_6:164

for F, F1 being FinSequence of INT

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_split_at k + 1

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_split_at k + 1

proof end;

:: from SCPISORT, 2011.02.13

definition

let D be non empty set ;

let f be FinSequence of D;

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f /. n = f /. m )

end;
let f be FinSequence of D;

:: original: constant

redefine attr f is constant means :Def1: :: FINSEQ_6:def 11

for n, m being Nat st n in dom f & m in dom f holds

f /. n = f /. m;

compatibility redefine attr f is constant means :Def1: :: FINSEQ_6:def 11

for n, m being Nat st n in dom f & m in dom f holds

f /. n = f /. m;

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f /. n = f /. m )

proof end;

:: deftheorem Def1 defines constant FINSEQ_6:def 11 :

for D being non empty set

for f being FinSequence of D holds

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f /. n = f /. m );

for D being non empty set

for f being FinSequence of D holds

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f /. n = f /. m );

theorem Th1: :: FINSEQ_6:166

for D being non empty set

for f being FinSequence of D st f just_once_values f /. (len f) holds

(f /. (len f)) .. f = len f

for f being FinSequence of D st f just_once_values f /. (len f) holds

(f /. (len f)) .. f = len f

proof end;

theorem :: FINSEQ_6:167

definition

let D be non empty set ;

let f be FinSequence of D;

let y be set ;

( f just_once_values y iff ex x being set st

( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds

f /. z <> y ) ) )

end;
let f be FinSequence of D;

let y be set ;

:: original: just_once_values

redefine pred f just_once_values y means :: FINSEQ_6:def 12

ex x being set st

( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds

f /. z <> y ) );

compatibility redefine pred f just_once_values y means :: FINSEQ_6:def 12

ex x being set st

( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds

f /. z <> y ) );

( f just_once_values y iff ex x being set st

( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds

f /. z <> y ) ) )

proof end;

:: deftheorem defines just_once_values FINSEQ_6:def 12 :

for D being non empty set

for f being FinSequence of D

for y being set holds

( f just_once_values y iff ex x being set st

( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds

f /. z <> y ) ) );

for D being non empty set

for f being FinSequence of D

for y being set holds

( f just_once_values y iff ex x being set st

( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds

f /. z <> y ) ) );

theorem Th4: :: FINSEQ_6:169

for D being non empty set

for f being FinSequence of D st f just_once_values f /. (len f) holds

f -: (f /. (len f)) = f

for f being FinSequence of D st f just_once_values f /. (len f) holds

f -: (f /. (len f)) = f

proof end;

theorem Th5: :: FINSEQ_6:170

for D being non empty set

for f being FinSequence of D st f just_once_values f /. (len f) holds

f :- (f /. (len f)) = <*(f /. (len f))*>

for f being FinSequence of D st f just_once_values f /. (len f) holds

f :- (f /. (len f)) = <*(f /. (len f))*>

proof end;

theorem Th6: :: FINSEQ_6:171

for D being non empty set

for p being Element of D

for f being FinSequence of D holds 1 <= len (f :- p)

for p being Element of D

for f being FinSequence of D holds 1 <= len (f :- p)

proof end;

theorem :: FINSEQ_6:172

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

for p being Element of D

for f being FinSequence of D st p in rng f holds

len (f :- p) <= len f

proof end;

theorem Th9: :: FINSEQ_6:174

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 & 1 <= i & i <= len (f :- p) holds

(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f))

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds

(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f))

proof end;

theorem Th10: :: FINSEQ_6:175

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 & p .. f <= i & i <= len f holds

f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds

f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

proof end;

theorem :: FINSEQ_6:176

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

for p being Element of D

for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

proof end;

NAT27: for i, j being Nat st j < i holds

(i -' (j + 1)) + 1 = i -' j

proof end;

theorem Th12: :: FINSEQ_6:177

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 & len (f :- p) < i & i <= len f holds

(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds

(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))

proof end;

theorem :: FINSEQ_6:178

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 & 1 < i & i <= p .. f holds

f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))

for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & 1 < i & i <= p .. f holds

f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))

proof end;

theorem Th14: :: FINSEQ_6:179

for D being non empty set

for p being Element of D

for f being FinSequence of D holds len (Rotate (f,p)) = len f

for p being Element of D

for f being FinSequence of D holds len (Rotate (f,p)) = len f

proof end;

theorem Th15: :: FINSEQ_6:180

for D being non empty set

for p being Element of D

for f being FinSequence of D holds dom (Rotate (f,p)) = dom f

for p being Element of D

for f being FinSequence of D holds dom (Rotate (f,p)) = dom f

proof end;

theorem :: FINSEQ_6:181

for D being non empty set

for f being circular FinSequence of D

for p being Element of D st ( for i being Nat st 1 < i & i < len f holds

f /. i <> f /. 1 ) holds

Rotate ((Rotate (f,p)),(f /. 1)) = f

for f being circular FinSequence of D

for p being Element of D st ( for i being Nat st 1 < i & i < len f holds

f /. i <> f /. 1 ) holds

Rotate ((Rotate (f,p)),(f /. 1)) = f

proof end;

theorem Th17: :: FINSEQ_6:182

for i being Nat

for D being non empty set

for p being Element of D

for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds

(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))

for D being non empty set

for p being Element of D

for f being circular FinSequence of D st p in rng f & len (f :- p) <= i & i <= len f holds

(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))

proof end;

theorem Th18: :: FINSEQ_6:183

for i being Nat

for D being non empty set

for p being Element of D

for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds

f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))

for D being non empty set

for p being Element of D

for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds

f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))

proof end;

registration

let D be non trivial set ;

ex b_{1} being FinSequence of D st

( b_{1} is V25() & b_{1} is circular )

end;
cluster Relation-like omega -defined D -valued Function-like V25() finite FinSequence-like FinSubsequence-like circular for FinSequence of D;

existence ex b

( b

proof end;

registration

let D be non trivial set ;

let p be Element of D;

let f be V25() circular FinSequence of D;

coherence

not Rotate (f,p) is constant

end;
let p be Element of D;

let f be V25() circular FinSequence of D;

coherence

not Rotate (f,p) is constant

proof end;