:: Segments of Natural Numbers and Finite Sequences
:: by Grzegorz Bancerek and Krzysztof Hryniewiecki
::
:: Received April 1, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

:: Segments of Natural Numbers

definition

let n be natural Number ;

func Seg n -> set equals :: FINSEQ_1:def 1
{ k where k is Nat : ( 1 <= k & k <= n ) } ;

correctness
coherence
{ k where k is Nat : ( 1 <= k & k <= n ) } is set ;
;

end;

:: deftheorem defines Seg FINSEQ_1:def 1 :
for n being natural Number holds Seg n = { k where k is Nat : ( 1 <= k & k <= n ) } ;

definition

let n be Nat;
:: original: Seg
redefine func Seg n -> Subset of NAT;
coherence
Seg n is Subset of NAT

proof end;

end;

theorem Th1: :: FINSEQ_1:1

for a, b being natural Number holds
( a in Seg b iff ( 1 <= a & a <= b ) )

proof end;

registration

let n be natural zero Number ;

cluster Seg n -> empty ;

coherence
Seg n is empty

proof end;

end;

theorem Th2: :: FINSEQ_1:2

( Seg 1 = {1} & Seg 2 = {1,2} )

proof end;

theorem Th3: :: FINSEQ_1:3

for a being natural Number holds
( a = 0 or a in Seg a )

proof end;

registration

let n be natural non zero Number ;

cluster Seg n -> non empty ;

coherence
not Seg n is empty by Th3;

end;

theorem :: FINSEQ_1:4

for a being natural Number holds a + 1 in Seg (a + 1) by Th3;

theorem Th5: :: FINSEQ_1:5

for a, b being natural Number holds
( a <= b iff Seg a c= Seg b )

proof end;

theorem Th6: :: FINSEQ_1:6

for a, b being natural Number st Seg a = Seg b holds
a = b

proof end;

theorem Th7: :: FINSEQ_1:7

for a, c being natural Number st c <= a holds
Seg c = (Seg a) /\ (Seg c) by Th5, XBOOLE_1:28;

theorem :: FINSEQ_1:8

for a, c being natural Number st Seg c = (Seg c) /\ (Seg a) holds
c <= a by Th6, Th7;

theorem Th9: :: FINSEQ_1:9

for a being natural Number holds (Seg a) \/ {(a + 1)} = Seg (a + 1)

proof end;

theorem :: FINSEQ_1:10

for k being natural Number holds Seg k = (Seg (k + 1)) \ {(k + 1)}

proof end;

:: Finite Sequences

definition

let IT be Relation;

attr IT is FinSequence-like means :Def2: :: FINSEQ_1:def 2
ex n being Nat st dom IT = Seg n;

end;

:: deftheorem Def2 defines FinSequence-like FINSEQ_1:def 2 :
for IT being Relation holds
( IT is FinSequence-like iff ex n being Nat st dom IT = Seg n );

registration

cluster Relation-like empty -> FinSequence-like for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is FinSequence-like

proof end;

end;

definition

mode FinSequence is FinSequence-like Function;

end;

defpred S₁[ object , object ] means ex k being Nat st
( $1 = k & $2 = k + 1 );

registration

let n be natural Number ;

cluster Seg n -> finite ;

coherence
Seg n is finite

proof end;

end;

registration

cluster Relation-like Function-like FinSequence-like -> finite for set ;

coherence
for b₁ being Function st b₁ is FinSequence-like holds
b₁ is finite

proof end;

end;

Lm1: for n being Nat holds Seg n,n are_equipotent

proof end;

registration

let n be natural Number ;

cluster Seg n -> n -element ;

coherence
Seg n is n -element

proof end;

end;

notation

let p be FinSequence;
synonym len p for card p;

end;

definition

let p be FinSequence;

:: original: len
redefine func len p -> Element of NAT means :Def3: :: FINSEQ_1:def 3
Seg it = dom p;

coherence
len p is Element of NAT

proof end;

compatibility
for b₁ being Element of NAT holds
( b₁ = len p iff Seg b₁ = dom p )

proof end;

end;

:: deftheorem Def3 defines len FINSEQ_1:def 3 :
for p being FinSequence
for b₂ being Element of NAT holds
( b₂ = len p iff Seg b₂ = dom p );

definition

let p be FinSequence;
:: original: dom
redefine func dom p -> Subset of NAT;
coherence
dom p is Subset of NAT

proof end;

end;

theorem :: FINSEQ_1:11

for f being Function st ex k being Nat st dom f c= Seg k holds
ex p being FinSequence st f c= p

proof end;

scheme :: FINSEQ_1:sch 1
SeqEx{ F₁() -> Nat, P₁[ object , object ] } :

ex p being FinSequence st
( dom p = Seg F₁() & ( for k being Nat st k in Seg F₁() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in Seg F₁() holds
ex x being object st P₁[k,x]

proof end;

scheme :: FINSEQ_1:sch 2
SeqLambda{ F₁() -> Nat, F₂( object ) -> object } :

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_1:12

for z being object
for p being FinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )

proof end;

theorem :: FINSEQ_1:13

for p, q being FinSequence st dom p = dom q & ( for k being Nat st k in dom p holds
p . k = q . k ) holds
p = q ;

theorem Th14: :: FINSEQ_1:14

for p, q being FinSequence st len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) holds
p = q

proof end;

theorem Th15: :: FINSEQ_1:15

for a being natural Number
for p being FinSequence holds p | (Seg a) is FinSequence

proof end;

theorem :: FINSEQ_1:16

for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence

proof end;

theorem Th17: :: FINSEQ_1:17

for a being natural Number
for p, q being FinSequence st a <= len p & q = p | (Seg a) holds
( len q = a & dom q = Seg a )

proof end;

:: ::
:: FinSequences of D ::
:: ::

definition

let D be set ;

mode FinSequence of D -> FinSequence means :Def4: :: FINSEQ_1:def 4
rng it c= D;

existence
ex b₁ being FinSequence st rng b₁ c= D

proof end;

end;

:: deftheorem Def4 defines FinSequence FINSEQ_1:def 4 :
for D being set
for b₂ being FinSequence holds
( b₂ is FinSequence of D iff rng b₂ c= D );

registration

let D be set ;

cluster -> D -valued for FinSequence of D;

coherence
for b₁ being FinSequence of D holds b₁ is D -valued

proof end;

end;

Lm2: for D being set
for f being FinSequence of D holds f is PartFunc of NAT,D

proof end;

registration

cluster Relation-like empty -> FinSequence-like for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is FinSequence-like ;

end;

registration

let D be set ;

cluster Relation-like Function-like FinSequence-like for Element of bool [:NAT,D:];

existence
ex b₁ being PartFunc of NAT,D st b₁ is FinSequence-like

proof end;

end;

definition

let D be set ;
:: original: FinSequence
redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D;
coherence
for b₁ being FinSequence of D holds b₁ is FinSequence-like PartFunc of NAT,D by Lm2;

end;

theorem Th18: :: FINSEQ_1:18

for a being natural Number
for D being set
for p being FinSequence of D holds p | (Seg a) is FinSequence of D

proof end;

theorem :: FINSEQ_1:19

for a being natural Number
for D being non empty set ex p being FinSequence of D st len p = a

proof end;

Lm3: for q being FinSequence holds
( q = {} iff len q = 0 )
;

theorem :: FINSEQ_1:20

for p being FinSequence holds
( p <> {} iff len p >= 1 )

proof end;

definition

let x be object ;

func <*x*> -> set equals :: FINSEQ_1:def 5
{[1,x]};

coherence
{[1,x]} is set ;

end;

:: deftheorem defines <* FINSEQ_1:def 5 :
for x being object holds <*x*> = {[1,x]};

definition

let D be set ;

func <*> D -> FinSequence of D equals :: FINSEQ_1:def 6
{} ;

coherence
{} is FinSequence of D

proof end;

end;

:: deftheorem defines <*> FINSEQ_1:def 6 :
for D being set holds <*> D = {} ;

registration

let D be set ;

cluster <*> D -> empty ;

coherence
<*> D is empty ;

end;

registration

let D be set ;

cluster Relation-like D -valued Function-like empty finite FinSequence-like for FinSequence of D;

existence
ex b₁ being FinSequence of D st b₁ is empty

proof end;

end;

definition

let p, q be FinSequence;

func p ^ q -> FinSequence means :Def7: :: FINSEQ_1:def 7
( dom it = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
it . k = p . k ) & ( for k being Nat st k in dom q holds
it . ((len p) + k) = q . k ) );

existence
ex b₁ being FinSequence st
( dom b₁ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₁ . k = p . k ) & ( for k being Nat st k in dom q holds
b₁ . ((len p) + k) = q . k ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st dom b₁ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₁ . k = p . k ) & ( for k being Nat st k in dom q holds
b₁ . ((len p) + k) = q . k ) & dom b₂ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₂ . k = p . k ) & ( for k being Nat st k in dom q holds
b₂ . ((len p) + k) = q . k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :
for p, q being FinSequence
for b₃ being FinSequence holds
( b₃ = p ^ q iff ( dom b₃ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₃ . k = p . k ) & ( for k being Nat st k in dom q holds
b₃ . ((len p) + k) = q . k ) ) );

theorem Th21: :: FINSEQ_1:21

for p, q being FinSequence holds p = (p ^ q) | (dom p)

proof end;

theorem Th22: :: FINSEQ_1:22

for p, q being FinSequence holds len (p ^ q) = (len p) + (len q)

proof end;

theorem Th23: :: FINSEQ_1:23

for p, q being FinSequence
for k being Nat st (len p) + 1 <= k & k <= (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))

proof end;

theorem Th24: :: FINSEQ_1:24

for p, q being FinSequence
for k being Nat st len p < k & k <= len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))

proof end;

theorem Th25: :: FINSEQ_1:25

for p, q being FinSequence
for k being Nat holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )

proof end;

theorem Th26: :: FINSEQ_1:26

for p, q being FinSequence holds dom p c= dom (p ^ q)

proof end;

theorem Th27: :: FINSEQ_1:27

for x being object
for p, q being FinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )

proof end;

theorem Th28: :: FINSEQ_1:28

for k being Nat
for p, q being FinSequence st k in dom q holds
(len p) + k in dom (p ^ q)

proof end;

theorem Th29: :: FINSEQ_1:29

for p, q being FinSequence holds rng p c= rng (p ^ q)

proof end;

theorem Th30: :: FINSEQ_1:30

for p, q being FinSequence holds rng q c= rng (p ^ q)

proof end;

theorem Th31: :: FINSEQ_1:31

for p, q being FinSequence holds rng (p ^ q) = (rng p) \/ (rng q)

proof end;

theorem Th32: :: FINSEQ_1:32

for p, q, r being FinSequence holds (p ^ q) ^ r = p ^ (q ^ r)

proof end;

theorem :: FINSEQ_1:33

for p, q, r being FinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q

proof end;

theorem Th34: :: FINSEQ_1:34

for p being FinSequence holds
( p ^ {} = p & {} ^ p = p )

proof end;

theorem Th35: :: FINSEQ_1:35

for p, q being FinSequence st p ^ q = {} holds
( p = {} & q = {} )

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

proof end;

end;

Lm4: for x, y, x1, y1 being object st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )

proof end;

definition

let x be object ;

:: original: <*
redefine func <*x*> -> Function means :Def8: :: FINSEQ_1:def 8
( dom it = Seg 1 & it . 1 = x );

coherence
<*x*> is Function ;
compatibility
for b₁ being Function holds
( b₁ = <*x*> iff ( dom b₁ = Seg 1 & b₁ . 1 = x ) )

proof end;

end;

:: deftheorem Def8 defines <* FINSEQ_1:def 8 :
for x being object
for b₂ being Function holds
( b₂ = <*x*> iff ( dom b₂ = Seg 1 & b₂ . 1 = x ) );

registration

let x be object ;

cluster <*x*> -> Relation-like Function-like ;

coherence
( <*x*> is Function-like & <*x*> is Relation-like ) ;

end;

registration

let x be object ;

cluster <*x*> -> FinSequence-like ;

coherence
<*x*> is FinSequence-like by Def8;

end;

theorem Th36: :: FINSEQ_1:36

for p, q being FinSequence
for D being set st p ^ q is FinSequence of D holds
( p is FinSequence of D & q is FinSequence of D )

proof end;

definition

let x, y be object ;

func <*x,y*> -> set equals :: FINSEQ_1:def 9
<*x*> ^ <*y*>;

correctness
coherence
<*x*> ^ <*y*> is set ;
;
let z be object ;

func <*x,y,z*> -> set equals :: FINSEQ_1:def 10
(<*x*> ^ <*y*>) ^ <*z*>;

correctness
coherence
(<*x*> ^ <*y*>) ^ <*z*> is set ;
;

end;

:: deftheorem defines <* FINSEQ_1:def 9 :
for x, y being object holds <*x,y*> = <*x*> ^ <*y*>;

:: deftheorem defines <* FINSEQ_1:def 10 :
for x, y, z being object holds <*x,y,z*> = (<*x*> ^ <*y*>) ^ <*z*>;

registration

let x, y be object ;

cluster <*x,y*> -> Relation-like Function-like ;

coherence
( <*x,y*> is Function-like & <*x,y*> is Relation-like ) ;
let z be object ;

cluster <*x,y,z*> -> Relation-like Function-like ;

coherence
( <*x,y,z*> is Function-like & <*x,y,z*> is Relation-like ) ;

end;

registration

let x, y be object ;

cluster <*x,y*> -> FinSequence-like ;

coherence
<*x,y*> is FinSequence-like ;
let z be object ;

cluster <*x,y,z*> -> FinSequence-like ;

coherence
<*x,y,z*> is FinSequence-like ;

end;

theorem :: FINSEQ_1:37

for x being object holds <*x*> = {[1,x]} ;

theorem Th38: :: FINSEQ_1:38

for p being FinSequence
for x being object holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )

proof end;

theorem Th39: :: FINSEQ_1:39

for p being FinSequence
for x being object holds
( p = <*x*> iff ( len p = 1 & rng p = {x} ) )

proof end;

theorem Th40: :: FINSEQ_1:40

for p being FinSequence
for x being object holds
( p = <*x*> iff ( len p = 1 & p . 1 = x ) )

proof end;

theorem :: FINSEQ_1:41

for p being FinSequence
for x being object holds (<*x*> ^ p) . 1 = x

proof end;

theorem Th42: :: FINSEQ_1:42

for p being FinSequence
for x being object holds (p ^ <*x*>) . ((len p) + 1) = x

proof end;

theorem :: FINSEQ_1:43

for x, y, z being object holds
( <*x,y,z*> = <*x*> ^ <*y,z*> & <*x,y,z*> = <*x,y*> ^ <*z*> ) by Th32;

theorem Th44: :: FINSEQ_1:44

for p being FinSequence
for x, y being object holds
( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )

proof end;

theorem Th45: :: FINSEQ_1:45

for p being FinSequence
for x, y, z being object holds
( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )

proof end;

theorem Th46: :: FINSEQ_1:46

for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being object st p = q ^ <*x*>

proof end;

definition

let D be non empty set ;
let x be Element of D;
:: original: <*
redefine func <*x*> -> FinSequence of D;
coherence
<*x*> is FinSequence of D

proof end;

end;

:: scheme of induction for finite sequences ::

scheme :: FINSEQ_1:sch 3
IndSeq{ P₁[ FinSequence] } :

for p being FinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being FinSequence
for x being object st P₁[p] holds
P₁[p ^ <*x*>]

proof end;

theorem :: FINSEQ_1:47

for p, q, r, s being FinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being FinSequence st p ^ t = r

proof end;

registration

cluster Relation-like Function-like FinSequence-like -> NAT -defined for set ;

coherence
for b₁ being FinSequence holds b₁ is NAT -defined

proof end;

end;

definition

let D be set ;

func D * -> set means :Def11: :: FINSEQ_1:def 11
for x being object holds
( x in it iff x is FinSequence of D );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff x is FinSequence of D )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff x is FinSequence of D ) ) & ( for x being object holds
( x in b₂ iff x is FinSequence of D ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines * FINSEQ_1:def 11 :
for D, b₂ being set holds
( b₂ = D * iff for x being object holds
( x in b₂ iff x is FinSequence of D ) );

registration

let D be set ;

cluster D * -> non empty ;

coherence
not D * is empty

proof end;

end;

theorem :: FINSEQ_1:48

for p, q being FinSequence st rng p = rng q & p is one-to-one & q is one-to-one holds
len p = len q

proof end;

theorem :: FINSEQ_1:49

for D being set holds {} in D *

proof end;

scheme :: FINSEQ_1:sch 4
SepSeq{ F₁() -> non empty set , P₁[ FinSequence] } :

ex X being set st
for x being object holds
( x in X iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) )

proof end;

:: ::
:: Subsequences ::
:: ::

definition

let IT be Function;

attr IT is FinSubsequence-like means :Def12: :: FINSEQ_1:def 12
ex k being Nat st dom IT c= Seg k;

end;

:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def 12 :
for IT being Function holds
( IT is FinSubsequence-like iff ex k being Nat st dom IT c= Seg k );

registration

cluster Relation-like Function-like FinSubsequence-like for set ;

existence
ex b₁ being Function st b₁ is FinSubsequence-like

proof end;

end;

definition

mode FinSubsequence is FinSubsequence-like Function;

end;

registration

cluster Relation-like Function-like FinSequence-like -> FinSubsequence-like for set ;

coherence
for b₁ being Function st b₁ is FinSequence-like holds
b₁ is FinSubsequence-like ;
let p be FinSubsequence;
let X be set ;

cluster p | X -> FinSubsequence-like ;

coherence
p | X is FinSubsequence-like

proof end;

cluster X |` p -> FinSubsequence-like ;

coherence
X |` p is FinSubsequence-like

proof end;

end;

registration

cluster Relation-like Function-like FinSubsequence-like -> NAT -defined for set ;

coherence
for b₁ being FinSubsequence holds b₁ is NAT -defined

proof end;

end;

definition

let X be set ;
given k being Nat such that A1: X c= Seg k ;

func Sgm X -> FinSequence of NAT means :Def13: :: FINSEQ_1:def 13
( rng it = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len it & k1 = it . l & k2 = it . m holds
k1 < k2 ) );

existence
ex b₁ being FinSequence of NAT st
( rng b₁ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st rng b₁ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) & rng b₂ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines Sgm FINSEQ_1:def 13 :
for X being set st ex k being Nat st X c= Seg k holds
for b₂ being FinSequence of NAT holds
( b₂ = Sgm X iff ( rng b₂ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) ) );

theorem Th50: :: FINSEQ_1:50

for p9 being FinSubsequence holds rng (Sgm (dom p9)) = dom p9

proof end;

definition

let p9 be FinSubsequence;

func Seq p9 -> Function equals :: FINSEQ_1:def 14
p9 * (Sgm (dom p9));

coherence
p9 * (Sgm (dom p9)) is Function ;

end;

:: deftheorem defines Seq FINSEQ_1:def 14 :
for p9 being FinSubsequence holds Seq p9 = p9 * (Sgm (dom p9));

registration

let p9 be FinSubsequence;

cluster Seq p9 -> FinSequence-like ;

coherence
Seq p9 is FinSequence-like

proof end;

end;

theorem :: FINSEQ_1:51

for X being set st ex k being Nat st X c= Seg k holds
( Sgm X = {} iff X = {} )

proof end;

theorem :: FINSEQ_1:52

for D being set holds
( D is finite iff ex p being FinSequence st D = rng p )

proof end;

theorem :: FINSEQ_1:53

for m, n being Nat st Seg n, Seg m are_equipotent holds
n = m

proof end;

theorem :: FINSEQ_1:54

for n being Nat holds Seg n,n are_equipotent by Lm1;

theorem :: FINSEQ_1:55

for n being Nat holds card (Seg n) = card n by Lm1, CARD_1:5;

theorem Th56: :: FINSEQ_1:56

for X being set st X is finite holds
ex n being Nat st X, Seg n are_equipotent

proof end;

theorem :: FINSEQ_1:57

for n being Nat holds card (Seg n) = n by Lm1, CARD_1:def 2;

:: from FINSEQ_5

registration

let x be object ;

cluster <*x*> -> non empty ;

coherence
not <*x*> is empty ;

end;

:: From SPRECT_1

registration

cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like for set ;

existence
not for b₁ being FinSequence holds b₁ is empty

proof end;

end;

:: From FUNCT_7, actually from GOBOARD4

registration

let f1 be FinSequence;
let f2 be non empty FinSequence;

cluster f1 ^ f2 -> non empty ;

coherence
not f1 ^ f2 is empty by Th35;

cluster f2 ^ f1 -> non empty ;

coherence
not f2 ^ f1 is empty by Th35;

end;

registration

let x, y be object ;

cluster <*x,y*> -> non empty ;

coherence
not <*x,y*> is empty ;
let z be object ;

cluster <*x,y,z*> -> non empty ;

coherence
not <*x,y,z*> is empty ;

end;

:: from MATRIX_2

scheme :: FINSEQ_1:sch 5
SeqDEx{ F₁() -> non empty set , F₂() -> Nat, P₁[ object , object ] } :

ex p being FinSequence of F₁() st
( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₁[k,x]

proof end;

definition

let m be Nat;
let p be FinSequence;

func p | m -> FinSequence equals :: FINSEQ_1:def 15
p | (Seg m);

coherence
p | (Seg m) is FinSequence by Th15;

end;

:: deftheorem defines | FINSEQ_1:def 15 :
for m being Nat
for p being FinSequence holds p | m = p | (Seg m);

definition

let D be set ;
let m be Nat;
let p be FinSequence of D;
:: original: |
redefine func p | m -> FinSequence of D;
coherence
p | m is FinSequence of D by Th18;

end;

registration

let f be FinSequence;

cluster f | 0 -> empty ;

coherence
f | 0 is empty ;

end;

theorem Th58: :: FINSEQ_1:58

for i being Nat
for q being FinSequence st len q <= i holds
q | i = q

proof end;

theorem Th59: :: FINSEQ_1:59

for i being Nat
for q being FinSequence st i <= len q holds
len (q | i) = i

proof end;

registration

let f be non empty FinSequence;

reduce len (f | 1) to 1;

reducibility
len (f | 1) = 1

proof end;

cluster f | 1 -> 1 -element ;

coherence
f | 1 is 1 -element ;

end;

registration

let p be non empty FinSequence;
let n be non zero Nat;

cluster p | n -> non empty ;

coherence
not p | n is empty

proof end;

end;

:: from FSM_1

theorem :: FINSEQ_1:60

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

proof end;

theorem :: FINSEQ_1:61

for n, i, m being Nat st i > 0 & i + m in Seg (n + m) holds
( i in Seg n & i in Seg (n + m) )

proof end;

:: from LANG1

definition

let R be Relation;

func R [*] -> Relation means :: FINSEQ_1:def 16
for x, y being object holds
( [x,y] in it iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) );

existence
ex b₁ being Relation st
for x, y being object holds
( [x,y] in b₁ iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation st ( for x, y being object holds
( [x,y] in b₁ iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) & ( for x, y being object holds
( [x,y] in b₂ iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines [*] FINSEQ_1:def 16 :
for R, b₂ being Relation holds
( b₂ = R [*] iff for x, y being object holds
( [x,y] in b₂ iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) );

theorem :: FINSEQ_1:62

for D1, D2 being set st D1 c= D2 holds
D1 * c= D2 *

proof end;

:: 2005.05.13, A.T.

registration

let D be set ;

cluster D * -> functional ;

coherence
D * is functional by Def11;

end;

:: from SCMFSA_7, 2005.11.21, A.T.

theorem :: FINSEQ_1:63

for p, q being FinSequence st p c= q holds
len p <= len q

proof end;

theorem :: FINSEQ_1:64

for p, q being FinSequence
for i being Nat st 1 <= i & i <= len p holds
(p ^ q) . i = p . i

proof end;

theorem :: FINSEQ_1:65

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

proof end;

:: from GRAPH_2, 2006.01.09, A.T.

scheme :: FINSEQ_1:sch 6
FinSegRng{ F₁() -> Nat, F₂( set ) -> set , P₁[ set ] } :

{ F₂(i) where i is Nat : ( i <= F₁() & P₁[i] ) } is finite

proof end;

Lm5: for n being Nat
for x being object st x in Seg n holds
not not x = 1 & ... & not x = n

proof end;

theorem Th66: :: FINSEQ_1:66

for x1, x2, x3, x4 being set
for p being FinSequence st p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> holds
( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )

proof end;

theorem Th67: :: FINSEQ_1:67

for x1, x2, x3, x4, x5 being set
for p being FinSequence st p = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> holds
( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )

proof end;

theorem Th68: :: FINSEQ_1:68

for x1, x2, x3, x4, x5, x6 being set
for p being FinSequence st p = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*> holds
( len p = 6 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 )

proof end;

theorem Th69: :: FINSEQ_1:69

for x1, x2, x3, x4, x5, x6, x7 being set
for p being FinSequence st p = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*> holds
( len p = 7 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 )

proof end;

theorem Th70: :: FINSEQ_1:70

for x1, x2, x3, x4, x5, x6, x7, x8 being set
for p being FinSequence st p = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*> holds
( len p = 8 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 )

proof end;

theorem :: FINSEQ_1:71

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set
for p being FinSequence st p = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*> holds
( len p = 9 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 )

proof end;

:: from SCMFSA_7, 2006.03.14, A.T.

theorem :: FINSEQ_1:72

for p being FinSequence holds p | (Seg 0) = {} ;

theorem :: FINSEQ_1:73

for f, g being FinSequence holds f | (Seg 0) = g | (Seg 0) ;

theorem :: FINSEQ_1:74

for D being non empty set
for x being Element of D holds <*x*> is FinSequence of D ;

theorem :: FINSEQ_1:75

for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D ;

theorem :: FINSEQ_1:76

for a, b being object st <*a*> = <*b*> holds
a = b

proof end;

theorem :: FINSEQ_1:77

for a, b, c, d being object st <*a,b*> = <*c,d*> holds
( a = c & b = d )

proof end;

theorem :: FINSEQ_1:78

for a, b, c, d, e, f being object st <*a,b,c*> = <*d,e,f*> holds
( a = d & b = e & c = f )

proof end;

:: from PRVECT_1, 2007.03.09, A.T

registration

cluster Relation-like non-empty NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st
( not b₁ is empty & b₁ is non-empty )

proof end;

end;

theorem Th79: :: FINSEQ_1:79

for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= len p

proof end;

theorem :: FINSEQ_1:80

for n being Nat
for p, r being FinSequence st r = p | (Seg n) holds
ex q being FinSequence st p = r ^ q

proof end;

:: from GOBOARD1, PRALG_1, 2007.04.06, A.T

registration

let D be non empty set ;

cluster Relation-like NAT -defined D -valued Function-like non empty finite FinSequence-like FinSubsequence-like for FinSequence of D;

existence
not for b₁ being FinSequence of D holds b₁ is empty

proof end;

end;

registration

let D be non empty set ;

cluster Relation-like NAT -defined D -valued Function-like non empty finite FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st
( not b₁ is empty & b₁ is D -valued )

proof end;

end;

:: Added by AK, 2007.11.07

definition

let p, q be FinSequence;

redefine pred p = q means :: FINSEQ_1:def 17
( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) );

compatibility
( p = q iff ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) ) ) by Th14;

end;

:: deftheorem defines = FINSEQ_1:def 17 :
for p, q being FinSequence holds
( p = q iff ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) ) );

:: from GROEB_2, 2008.10.08, A.T.

theorem :: FINSEQ_1:81

for x, y, z being object holds
( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> )

proof end;

theorem :: FINSEQ_1:82

for p being FinSequence
for n, m being Nat st m <= n holds
(p | n) | m = p | m by Th5, RELAT_1:74;

theorem :: FINSEQ_1:83

for n being Nat holds Seg n = (n + 1) \ {0}

proof end;

:: from CIRCCOMB, 2009.03.27, A.T.

registration

let n be natural Number ;

cluster Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st b₁ is n -element

proof end;

end;

:: from FACIRC_1, 2009.02.16, A.T.

registration

let x be object ;

cluster <*x*> -> 1 -element ;

coherence
<*x*> is 1 -element ;
let y be object ;

cluster <*x,y*> -> 2 -element ;

coherence
<*x,y*> is 2 -element by Th44;
let z be object ;

cluster <*x,y,z*> -> 3 -element ;

coherence
<*x,y,z*> is 3 -element by Th45;

end;

:: new, 2009.08.24, A.T.

definition

let X be set ;

attr X is FinSequence-membered means :Def18: :: FINSEQ_1:def 18
for x being object st x in X holds
x is FinSequence;

end;

:: deftheorem Def18 defines FinSequence-membered FINSEQ_1:def 18 :
for X being set holds
( X is FinSequence-membered iff for x being object st x in X holds
x is FinSequence );

registration

cluster empty -> FinSequence-membered for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is FinSequence-membered ;

end;

registration

cluster non empty FinSequence-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is FinSequence-membered )

proof end;

end;

registration

let X be set ;

cluster X * -> FinSequence-membered ;

coherence
X * is FinSequence-membered by Def11;

end;

theorem :: FINSEQ_1:84

for x being object
for D being set
for f being Function st f in D * & x in dom f holds
f . x in D

proof end;

registration

cluster FinSequence-membered -> functional for set ;

coherence
for b₁ being set st b₁ is FinSequence-membered holds
b₁ is functional ;

end;

theorem :: FINSEQ_1:85

for X being FinSequence-membered set ex Y being non empty set st X c= Y *

proof end;

registration

let X be FinSequence-membered set ;

cluster -> FinSequence-like for Element of X;

coherence
for b₁ being Element of X holds b₁ is FinSequence-like

proof end;

end;

registration

let X be FinSequence-membered set ;

cluster -> FinSequence-membered for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is FinSequence-membered ;

end;

:: from TREES_1, 2009.09.09, A.T.

theorem :: FINSEQ_1:86

for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= n

proof end;

theorem :: FINSEQ_1:87

for p, q being FinSequence st ( p = p ^ q or p = q ^ p ) holds
q = {}

proof end;

theorem :: FINSEQ_1:88

for x being object
for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )

proof end;

:: missing, 2009.09.26, A.T.

theorem Th88: :: FINSEQ_1:89

for n being Nat
for f being b₁ -element FinSequence holds dom f = Seg n

proof end;

registration

let n, m be natural Number ;
let f be n -element FinSequence;
let g be m -element FinSequence;

cluster f ^ g -> n + m -element ;

coherence
f ^ g is n + m -element

proof end;

end;

:: from JORDAN7, 2010.02.26, A.T

registration

cluster Relation-like Function-like real-valued increasing FinSequence-like -> one-to-one real-valued for set ;

coherence
for b₁ being real-valued FinSequence st b₁ is increasing holds
b₁ is one-to-one

proof end;

end;

:: from AMI_6, 2010.04.07, A.T.

theorem :: FINSEQ_1:90

for x, y being object st x in dom <*y*> holds
x = 1

proof end;

:: from FOMODEL0, 2011.06.12, A.T.

registration

let X be set ;

cluster Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st b₁ is X -valued

proof end;

end;

:: new, 2011.10.03, A.K.

registration

let D be FinSequence-membered set ;
let f be D -valued Function;
let x be object ;

cluster f . x -> FinSequence-like ;

coherence
f . x is FinSequence-like

proof end;

end;

theorem :: FINSEQ_1:91

for n being Nat
for x being object st x in Seg n holds
not not x = 1 & ... & not x = n by Lm5;

theorem :: FINSEQ_1:92

for x, y being object holds dom <*x,y*> = {1,2}

proof end;

registration

let A be finite set ;

cluster Relation-like NAT -defined A -valued Function-like one-to-one onto finite FinSequence-like FinSubsequence-like for FinSequence of A;

existence
ex b₁ being FinSequence of A st
( b₁ is onto & b₁ is one-to-one )

proof end;

end;

definition

let A be finite set ;

func canFS A -> FinSequence equals :: FINSEQ_1:def 19
the one-to-one onto FinSequence of A;

coherence
the one-to-one onto FinSequence of A is FinSequence ;

end;

:: deftheorem defines canFS FINSEQ_1:def 19 :
for A being finite set holds canFS A = the one-to-one onto FinSequence of A;

definition

let A be finite set ;
:: original: canFS
redefine func canFS A -> FinSequence of A;
coherence
canFS A is FinSequence of A ;

end;

registration

let A be finite set ;

cluster canFS A -> one-to-one onto for FinSequence of A;

coherence
for b₁ being FinSequence of A st b₁ = canFS A holds
( b₁ is one-to-one & b₁ is onto ) ;

end;

theorem Th92: :: FINSEQ_1:93

for A being finite set holds len (canFS A) = card A

proof end;

registration

let A be non empty finite set ;

cluster canFS A -> non empty ;

coherence
not canFS A is empty

proof end;

end;

theorem :: FINSEQ_1:94

for a being object holds canFS {a} = <*a*>

proof end;

theorem :: FINSEQ_1:95

for A being finite set holds (canFS A) " is Function of A,(Seg (card A))

proof end;

:: from PNPROC_1, 2012.02.20, A.T.

theorem :: FINSEQ_1:96

for i being Nat
for x being object st i > 0 holds
{[i,x]} is FinSubsequence

proof end;

Lm6: for p being FinSubsequence st Seq p = {} holds
p = {}

proof end;

theorem :: FINSEQ_1:97

for q being FinSubsequence holds
( q = {} iff Seq q = {} ) by Lm6;

registration

cluster Relation-like Function-like FinSubsequence-like -> finite for set ;

coherence
for b₁ being FinSubsequence holds b₁ is finite

proof end;

end;

theorem :: FINSEQ_1:98

for x1, x2, y1, y2 being set holds
( not {[x1,y1],[x2,y2]} is FinSequence or ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )

proof end;

theorem :: FINSEQ_1:99

for x1, x2 being set holds <*x1,x2*> = {[1,x1],[2,x2]}

proof end;

theorem :: FINSEQ_1:100

for q being FinSubsequence holds dom (Seq q) = dom (Sgm (dom q))

proof end;

theorem :: FINSEQ_1:101

for q being FinSubsequence holds rng q = rng (Seq q)

proof end;

registration

cluster Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st b₁ is one-to-one

proof end;

end;

registration

let D be set ;

cluster Relation-like NAT -defined D -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like for FinSequence of D;

existence
ex b₁ being FinSequence of D st b₁ is one-to-one

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like non empty finite natural-valued FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st
( not b₁ is empty & b₁ is natural-valued )

proof end;

end;