:: by Grzegorz Bancerek and Krzysztof Hryniewiecki

::

:: Received April 1, 1989

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

:: Segments of Natural Numbers

definition

let n be natural Number ;

correctness

coherence

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

;

end;
correctness

coherence

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

;

:: deftheorem defines Seg FINSEQ_1:def 1 :

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

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

end;
:: original: Seg

redefine func Seg n -> Subset of NAT;

coherence

Seg n is Subset of NAT

proof end;

registration
end;

theorem :: FINSEQ_1:8

:: Finite Sequences

:: 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 );

for IT being Relation holds

( IT is FinSequence-like iff ex n being Nat st dom IT = Seg n );

registration
end;

defpred S

( $1 = k & $2 = k + 1 );

registration
end;

registration
end;

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

proof end;

registration
end;

definition

let p be FinSequence;

len p is Element of NAT

for b_{1} being Element of NAT holds

( b_{1} = len p iff Seg b_{1} = dom p )

end;
:: original: len

redefine func len p -> Element of NAT means :Def3: :: FINSEQ_1:def 3

Seg it = dom p;

coherence redefine func len p -> Element of NAT means :Def3: :: FINSEQ_1:def 3

Seg it = dom p;

len p is Element of NAT

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def3 defines len FINSEQ_1:def 3 :

for p being FinSequence

for b_{2} being Element of NAT holds

( b_{2} = len p iff Seg b_{2} = dom p );

for p being FinSequence

for b

( b

definition

let p be FinSequence;

:: original: dom

redefine func dom p -> Subset of NAT;

coherence

dom p is Subset of NAT

end;
:: original: dom

redefine func dom p -> Subset of NAT;

coherence

dom p is Subset of NAT

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)] )

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

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

p . k = q . k ) holds

p = q

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 )

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

:: ::

:: FinSequences of D ::

:: ::

:: deftheorem Def4 defines FinSequence FINSEQ_1:def 4 :

for D being set

for b_{2} being FinSequence holds

( b_{2} is FinSequence of D iff rng b_{2} c= D );

for D being set

for b

( b

registration
end;

Lm2: for D being set

for f being FinSequence of D holds f is PartFunc of NAT,D

proof end;

registration
end;

registration
end;

definition

let D be set ;

:: original: FinSequence

redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D;

coherence

for b_{1} being FinSequence of D holds b_{1} is FinSequence-like PartFunc of NAT,D
by Lm2;

end;
:: original: FinSequence

redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D;

coherence

for b

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

for D being set

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

proof end;

Lm3: for q being FinSequence holds

( q = {} iff len q = 0 )

;

definition
end;

registration
end;

definition

let p, q be FinSequence;

ex b_{1} being FinSequence st

( dom b_{1} = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds

b_{1} . k = p . k ) & ( for k being Nat st k in dom q holds

b_{1} . ((len p) + k) = q . k ) )

for b_{1}, b_{2} being FinSequence st dom b_{1} = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds

b_{1} . k = p . k ) & ( for k being Nat st k in dom q holds

b_{1} . ((len p) + k) = q . k ) & dom b_{2} = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds

b_{2} . k = p . k ) & ( for k being Nat st k in dom q holds

b_{2} . ((len p) + k) = q . k ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( dom b

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :

for p, q being FinSequence

for b_{3} being FinSequence holds

( b_{3} = p ^ q iff ( dom b_{3} = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds

b_{3} . k = p . k ) & ( for k being Nat st k in dom q holds

b_{3} . ((len p) + k) = q . k ) ) );

for p, q being FinSequence

for b

( b

b

b

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))

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))

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 ) )

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 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) )

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;

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;

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 ;

<*x*> is Function ;

compatibility

for b_{1} being Function holds

( b_{1} = <*x*> iff ( dom b_{1} = Seg 1 & b_{1} . 1 = x ) )

end;
:: original: <*

redefine func <*x*> -> Function means :Def8: :: FINSEQ_1:def 8

( dom it = Seg 1 & it . 1 = x );

coherence redefine func <*x*> -> Function means :Def8: :: FINSEQ_1:def 8

( dom it = Seg 1 & it . 1 = x );

<*x*> is Function ;

compatibility

for b

( b

proof end;

:: deftheorem Def8 defines <* FINSEQ_1:def 8 :

for x being object

for b_{2} being Function holds

( b_{2} = <*x*> iff ( dom b_{2} = Seg 1 & b_{2} . 1 = x ) );

for x being object

for b

( b

registration
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 )

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 ;

correctness

coherence

<*x*> ^ <*y*> is set ;

;

let z be object ;

correctness

coherence

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

;

end;
correctness

coherence

<*x*> ^ <*y*> is set ;

;

let z be object ;

correctness

coherence

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

;

:: deftheorem defines <* FINSEQ_1:def 10 :

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

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

registration

let x, y be object ;

coherence

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

let z be object ;

coherence

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

end;
coherence

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

let z be object ;

coherence

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

registration

let x, y be object ;

coherence

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

let z be object ;

coherence

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

end;
coherence

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

let z be object ;

coherence

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

theorem :: FINSEQ_1:43

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 ) )

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 ) )

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

for x being object st p <> {} holds

ex q being FinSequence ex x being object st p = q ^ <*x*>

for x being object 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

end;
let x be Element of D;

:: original: <*

redefine func <*x*> -> FinSequence of D;

coherence

<*x*> is FinSequence of D

proof end;

:: scheme of induction for finite sequences ::

scheme :: FINSEQ_1:sch 3

IndSeq{ P_{1}[ FinSequence] } :

provided

IndSeq{ P

provided

A1:
P_{1}[ {} ]
and

A2: for p being FinSequence

for x being object st P_{1}[p] holds

P_{1}[p ^ <*x*>]

A2: for p being FinSequence

for x being object st P

P

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

ex t being FinSequence st p ^ t = r

proof end;

definition

let D be set ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is FinSequence of D )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is FinSequence of D ) ) & ( for x being object holds

( x in b_{2} iff x is FinSequence of D ) ) holds

b_{1} = b_{2}

end;
func D * -> set means :Def11: :: FINSEQ_1:def 11

for x being object holds

( x in it iff x is FinSequence of D );

existence for x being object holds

( x in it iff x is FinSequence of D );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def11 defines * FINSEQ_1:def 11 :

for D, b_{2} being set holds

( b_{2} = D * iff for x being object holds

( x in b_{2} iff x is FinSequence of D ) );

for D, b

( b

( x in b

scheme :: FINSEQ_1:sch 4

SepSeq{ F_{1}() -> non empty set , P_{1}[ FinSequence] } :

SepSeq{ F

ex X being set st

for x being object holds

( x in X iff ex p being FinSequence st

( p in F_{1}() * & P_{1}[p] & x = p ) )

for x being object holds

( x in X iff ex p being FinSequence st

( p in F

proof end;

:: ::

:: Subsequences ::

:: ::

:: Subsequences ::

:: ::

:: 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 );

for IT being Function holds

( IT is FinSubsequence-like iff ex k being Nat st dom IT c= Seg k );

registration

coherence

for b_{1} being Function st b_{1} is FinSequence-like holds

b_{1} is FinSubsequence-like
;

let p be FinSubsequence;

let X be set ;

coherence

p | X is FinSubsequence-like

X |` p is FinSubsequence-like

end;
for b

b

let p be FinSubsequence;

let X be set ;

coherence

p | X is FinSubsequence-like

proof end;

coherence X |` p is FinSubsequence-like

proof end;

definition

let X be set ;

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

ex b_{1} being FinSequence of NAT st

( rng b_{1} = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b_{1} & k1 = b_{1} . l & k2 = b_{1} . m holds

k1 < k2 ) )

for b_{1}, b_{2} being FinSequence of NAT st rng b_{1} = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b_{1} & k1 = b_{1} . l & k2 = b_{1} . m holds

k1 < k2 ) & rng b_{2} = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b_{2} & k1 = b_{2} . l & k2 = b_{2} . m holds

k1 < k2 ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( rng b

k1 < k2 ) )

proof end;

uniqueness for b

k1 < k2 ) & rng b

k1 < k2 ) holds

b

proof 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_{2} being FinSequence of NAT holds

( b_{2} = Sgm X iff ( rng b_{2} = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b_{2} & k1 = b_{2} . l & k2 = b_{2} . m holds

k1 < k2 ) ) );

for X being set st ex k being Nat st X c= Seg k holds

for b

( b

k1 < k2 ) ) );

:: deftheorem defines Seq FINSEQ_1:def 14 :

for p9 being FinSubsequence holds Seq p9 = p9 * (Sgm (dom p9));

for p9 being FinSubsequence holds Seq p9 = p9 * (Sgm (dom p9));

:: from FINSEQ_5

:: From SPRECT_1

registration

not for b_{1} being FinSequence holds b_{1} is empty
end;

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

existence not for b

proof end;

:: From FUNCT_7, actually from GOBOARD4

registration

let f1 be FinSequence;

let f2 be non empty FinSequence;

coherence

not f1 ^ f2 is empty by Th35;

coherence

not f2 ^ f1 is empty by Th35;

end;
let f2 be non empty FinSequence;

coherence

not f1 ^ f2 is empty by Th35;

coherence

not f2 ^ f1 is empty by Th35;

registration

let x, y be object ;

coherence

not <*x,y*> is empty ;

let z be object ;

coherence

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

end;
coherence

not <*x,y*> is empty ;

let z be object ;

coherence

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

:: from MATRIX_2

:: deftheorem defines | FINSEQ_1:def 15 :

for m being Nat

for p being FinSequence holds p | m = p | (Seg m);

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;
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;

registration

let f be non empty FinSequence;

reducibility

len (f | 1) = 1

f | 1 is 1 -element ;

end;
reducibility

len (f | 1) = 1

proof end;

coherence f | 1 is 1 -element ;

registration
end;

:: from FSM_1

:: from LANG1

definition

let R be Relation;

ex b_{1} being Relation st

for x, y being object holds

( [x,y] in b_{1} 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 b_{1}, b_{2} being Relation st ( for x, y being object holds

( [x,y] in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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 ) ) ) );

ex b

for x, y being object holds

( [x,y] in b

( 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

( [x,y] in b

( 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

( 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

proof end;

:: deftheorem defines [*] FINSEQ_1:def 16 :

for R, b_{2} being Relation holds

( b_{2} = R [*] iff for x, y being object holds

( [x,y] in b_{2} 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 R, b

( b

( [x,y] in b

( 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 ) ) ) ) );

:: 2005.05.13, A.T.

:: from SCMFSA_7, 2005.11.21, A.T.

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

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.

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 )

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 )

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 )

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 )

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 )

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 )

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:74

theorem :: FINSEQ_1:75

:: from PRVECT_1, 2007.03.09, A.T

registration

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is non-empty )
end;

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

existence ex b

( not b

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

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 ;

not for b_{1} being FinSequence of D holds b_{1} is empty

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

existence not for b

proof end;

:: Added by AK, 2007.11.07

definition

let p, q be FinSequence;

( 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;
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 ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds

p . k = q . k ) );

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

p . k = q . k ) ) ) by Th14;

:: 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 ) ) );

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:82

:: from CIRCCOMB, 2009.03.27, A.T.

registration

let n be natural Number ;

ex b_{1} being FinSequence st b_{1} is n -element

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

existence ex b

proof end;

:: from FACIRC_1, 2009.02.16, A.T.

registration

let x be object ;

coherence

<*x*> is 1 -element ;

let y be object ;

coherence

<*x,y*> is 2 -element by Th44;

let z be object ;

coherence

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

end;
coherence

<*x*> is 1 -element ;

let y be object ;

coherence

<*x,y*> is 2 -element by Th44;

let z be object ;

coherence

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

:: new, 2009.08.24, A.T.

definition

let X be set ;

end;
attr X is FinSequence-membered means :Def18: :: FINSEQ_1:def 18

for x being object st x in X holds

x is FinSequence;

for x being object st x in X holds

x is FinSequence;

:: 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 );

for X being set holds

( X is FinSequence-membered iff for x being object st x in X holds

x is FinSequence );

registration
end;

registration
end;

registration
end;

registration

let X be FinSequence-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is FinSequence-like

end;
coherence

for b

proof end;

registration

let X be FinSequence-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is FinSequence-membered
;

end;
coherence

for b

:: from TREES_1, 2009.09.09, A.T.

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

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.

registration

let n, m be natural Number ;

let f be n -element FinSequence;

let g be m -element FinSequence;

coherence

f ^ g is n + m -element

end;
let f be n -element FinSequence;

let g be m -element FinSequence;

coherence

f ^ g is n + m -element

proof end;

:: from JORDAN7, 2010.02.26, A.T

registration

for b_{1} being real-valued FinSequence st b_{1} is increasing holds

b_{1} is one-to-one
end;

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

coherence for b

b

proof end;

:: from AMI_6, 2010.04.07, A.T.

:: from FOMODEL0, 2011.06.12, A.T.

registration

let X be set ;

ex b_{1} being FinSequence st b_{1} is X -valued

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

existence ex b

proof end;

:: new, 2011.10.03, A.K.

registration

let D be FinSequence-membered set ;

let f be D -valued Function;

let x be object ;

coherence

f . x is FinSequence-like

end;
let f be D -valued Function;

let x be object ;

coherence

f . x is FinSequence-like

proof end;

theorem :: FINSEQ_1:91

registration

let A be finite set ;

ex b_{1} being FinSequence of A st

( b_{1} is onto & b_{1} is one-to-one )

end;
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

( b

proof end;

definition
end;

:: deftheorem defines canFS FINSEQ_1:def 19 :

for A being finite set holds canFS A = the one-to-one onto FinSequence of A;

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;
:: original: canFS

redefine func canFS A -> FinSequence of A;

coherence

canFS A is FinSequence of A ;

registration

let A be finite set ;

coherence

for b_{1} being FinSequence of A st b_{1} = canFS A holds

( b_{1} is one-to-one & b_{1} is onto )
;

end;
coherence

for b

( b

:: from PNPROC_1, 2012.02.20, A.T.

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

p = {}

proof 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 ) )

( 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;

registration

ex b_{1} being FinSequence st b_{1} is one-to-one
end;

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

existence ex b

proof end;

registration

let D be set ;

ex b_{1} being FinSequence of D st b_{1} is one-to-one

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

existence ex b

proof end;

registration

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is natural-valued )
end;

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

existence ex b

( not b

proof end;