JOURNAL OF FORMALIZED MATHEMATICSVolume2,Released1990,Published2003Inst.of Computer Science,Univ.of BiałystokFinite Sequences andTuples of Elements of a Non-empty SetsCzesław Byli´n skiWarsaw UniversityBiałystokSummary.Thefirst part of the article is a continuation of[4].Next,we define the identity sequence of natural numbers and the constant sequences.The main part of this articleis the definition of tuples.The element of a set of all sequences of the length n of D is calleda tuple of a non-empty set D and it is denoted by element of D n.Also some basic facts abouttuples of a non-empty set are proved.MML Identifier:FINSEQ_2.WWW:/JFM/Vol2/finseq_2.htmlThe articles[13],[12],[9],[16],[2],[3],[14],[11],[1],[15],[17],[6],[8],[7],[4],[5],and[10] provide the notation and terminology for this paper.For simplicity,we adopt the following convention:i,j,l are natural numbers,k is a natural number,A,a,b,x,x1,x2,x3are sets,D,D′,E are non empty sets,d,d1,d2,d3are elements of D, d′,d′1,d′2,d′3are elements of D′,and p,q,r arefinite sequences.One can prove the following propositions:(1)min(i,j)is a natural number and max(i,j)is a natural number.(2)If l=min(i,j),then Seg i∩Seg j=Seg l.(3)If i≤j,then max(0,i−j)=0.(4)If j≤i,then max(0,i−j)=i−j.(5)max(0,i−j)is a natural number.(6)min(0,i)=0and min(i,0)=0and max(0,i)=i and max(i,0)=i.(8)1If i∈Seg(l+1),then i∈Seg l or i=l+1.(9)If i∈Seg l,then i∈Seg(l+j).(10)If len p=i and len q=i and for every j such that j∈Seg i holds p(j)=q(j),then p=q.(11)If b∈rng p,then there exists i such that i∈dom p and p(i)=b.(13)2For every set D and for everyfinite sequence p of elements of D such that i∈dom p holdsp(i)∈D.(14)For every set D such that for every i such that i∈dom p holds p(i)∈D holds p is afinitesequence of elements of D.(15) d1,d2 is afinite sequence of elements of D.(16) d1,d2,d3 is afinite sequence of elements of D.(18)3If i∈dom p,then i∈dom(p q).(19)len(p a )=len p+1.(20)If p a =q b ,then p=q and a=b.(21)If len p=i+1,then there exist q,a such that p=q a .(22)Let p be afinite sequence of elements of D.Suppose len p=0.Then there exists afinitesequence q of elements of D and there exists d such that p=q d .(23)If q=p↾Seg i and len p≤i,then p=q.(24)If q=p↾Seg i,then len q=min(i,len p).(25)If len r=i+j,then there exist p,q such that len p=i and len q=j and r=p q.(26)Let r be afinite sequence of elements of D.Suppose len r=i+j.Then there existfinitesequences p,q of elements of D such that len p=i and len q=j and r=p q.In this article we present several logical schemes.The scheme SeqLambdaD deals with a natural number A,a non empty set B,and a unary functor F yielding an element of B,and states that: There exists afinite sequence z of elements of B such that len z=A and for every jsuch that j∈Seg A holds z(j)=F(j)for all values of the parameters.The scheme IndSeqD deals with a non empty set A and a unary predicate P,and states that: For everyfinite sequence p of elements of A holds P[p]provided the parameters meet the following conditions:•P[εA],and•For everyfinite sequence p of elements of A and for every element x of A such that P[p]holds P[p x ].One can prove the following propositions:(27)For every non empty subset D′of D holds everyfinite sequence of elements of D′is afinitesequence of elements of D.(28)Every function from Seg i into D is afinite sequence of elements of D.(30)4Everyfinite sequence p of elements of D is a function from dom p into D.(31)For every function f from N into D holds f↾Seg i is afinite sequence of elements of D.(32)For every function f from N into D such that q=f↾Seg i holds len q=i.(33)For every function f such that rng p⊆dom f and q=f·p holds len q=len p.(34)Suppose D=Seg i.Let p be afinite sequence and q be afinite sequence of elements of D.If i≤len p,then p·q is afinite sequence.(35)Suppose D=Seg i.Let p be afinite sequence of elements of D′and q be afinite sequenceof elements of D.If i≤len p,then p·q is afinite sequence of elements of D′.(36)Let A,D be sets,p be afinite sequence of elements of A,and f be a function from A intoD.Then f·p is afinite sequence of elements of D.(37)Let p be afinite sequence of elements of A and f be a function from A into D′.If q=f·p,then len q=len p.(38)For every function f from A into D′holds f·εA=εD′.(39)Let p be afinite sequence of elements of D and f be a function from D into D′.If p= x1 ,then f·p= f(x1) .(40)Let p be afinite sequence of elements of D and f be a function from D into D′.If p= x1,x2 ,then f·p= f(x1),f(x2) .(41)Let p be afinite sequence of elements of D and f be a function from D into D′.If p= x1,x2,x3 ,then f·p= f(x1),f(x2),f(x3) .(42)For every function f from Seg i into Seg j such that if j=0,then i=0and j≤len p holdsp·f is afinite sequence.(43)For every function f from Seg i into Seg i such that i≤len p holds p·f is afinite sequence.(44)For every function f from dom p into dom p holds p·f is afinite sequence.(45)For every function f from Seg i into Seg i such that rng f=Seg i and i≤len p and q=p·fholds len q=i.(46)For every function f from dom p into dom p such that rng f=dom p and q=p·f holdslen q=len p.(47)For every permutation f of Seg i such that i≤len p and q=p·f holds len q=i.(48)For every permutation f of dom p such that q=p·f holds len q=len p.(49)Let p be afinite sequence of elements of D and f be a function from Seg i into Seg j.Suppose if j=0,then i=0and j≤len p.Then p·f is afinite sequence of elements of D.(50)Let p be afinite sequence of elements of D and f be a function from Seg i into Seg i.Ifi≤len p,then p·f is afinite sequence of elements of D.(51)Let p be afinite sequence of elements of D and f be a function from dom p into dom p.Then p·f is afinite sequence of elements of D.(52)id Seg k is afinite sequence of elements of N.Let i be a natural number.The functor idseq(i)yielding afinite sequence is defined by: (Def.1)idseq(i)=id Seg i.The following propositions are true:(54)5domidseq(k)=Seg k.(55)lenidseq(k)=k.(56)If j∈Seg i,then(idseq(i))(j)=j.(57)If i=0,then for every element k of Seg i holds(idseq(i))(k)=k.(58)idseq(0)=/0.(59)idseq(1)= 1 .(60)idseq(i+1)=(idseq(i)) i+1 .(61)idseq(2)= 1,2 .(62)idseq(3)= 1,2,3 .(63)p·idseq(k)=p↾Seg k.(64)If len p≤k,then p·idseq(k)=p.(65)idseq(k)is a permutation of Seg k.(66)Seg k−→a is afinite sequence.Let i be a natural number and let a be a set.The functor i→a yielding afinite sequence is defined as follows:(Def.2)i→a=Seg i−→a.We now state a number of propositions:(68)6dom(k→a)=Seg k.(69)len(k→a)=k.(70)If b∈Seg k,then(k→a)(b)=a.(71)If k=0,then for every element w of Seg k holds(k→d)(w)=d.(72)0→a=/0.(73)1→a= a .(74)(i+1)→a=(i→a) a .(75)2→a= a,a .(76)3→a= a,a,a .(77)k→d is afinite sequence of elements of D.(78)For every function F such that[:rng p,rng q:]⊆dom F holds F◦(p,q)is afinite sequence.(79)For every function F such that[:rng p,rng q:]⊆dom F and r=F◦(p,q)holds len r=min(len p,len q).(80)For every function F such that[:{a},rng p:]⊆dom F holds F◦(a,p)is afinite sequence.(81)For every function F such that[:{a},rng p:]⊆dom F and r=F◦(a,p)holds len r=len p.(82)For every function F such that[:rng p,{a}:]⊆dom F holds F◦(p,a)is afinite sequence.(83)For every function F such that[:rng p,{a}:]⊆dom F and r=F◦(p,a)holds len r=len p.(84)Let F be a function from[:D,D′:]into E,p be afinite sequence of elements of D,and q beafinite sequence of elements of D′.Then F◦(p,q)is afinite sequence of elements of E.(85)Let F be a function from[:D,D′:]into E,p be afinite sequence of elements of D,and q beafinite sequence of elements of D′.If r=F◦(p,q),then len r=min(len p,len q).(86)Let F be a function from[:D,D′:]into E,p be afinite sequence of elements of D,and q beafinite sequence of elements of D′.If len p=len q and r=F◦(p,q),then len r=len p and len r=len q.(87)Let F be a function from[:D,D′:]into E,p be afinite sequence of elements of D,and p′be afinite sequence of elements of D′.Then F◦(εD,p′)=εE and F◦(p,εD′)=εE.(88)Let F be a function from[:D,D′:]into E,p be afinite sequence of elements of D,and q beafinite sequence of elements of D′.If p= d1 and q= d′1 ,then F◦(p,q)= F(d1,d′1) .(89)Let F be a function from[:D,D′:]into E,p be afinite sequence of elements of D,and q beafinite sequence of elements of D′.If p= d1,d2 and q= d′1,d′2 ,then F◦(p,q)= F(d1, d′1),F(d2,d′2) .(90)Let F be a function from[:D,D′:]into E,p be afinite sequence of elements of D,and qbe afinite sequence of elements of D′.If p= d1,d2,d3 and q= d′1,d′2,d′3 ,then F◦(p, q)= F(d1,d′1),F(d2,d′2),F(d3,d′3) .(91)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D′.ThenF◦(d,p)is afinite sequence of elements of E.(92)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D′.Ifr=F◦(d,p),then len r=len p.(93)For every function F from[:D,D′:]into E holds F◦(d,εD′)=εE.(94)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D′.Ifp= d′1 ,then F◦(d,p)= F(d,d′1) .(95)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D′.Ifp= d′1,d′2 ,then F◦(d,p)= F(d,d′1),F(d,d′2) .(96)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D′.Ifp= d′1,d′2,d′3 ,then F◦(d,p)= F(d,d′1),F(d,d′2),F(d,d′3) .(97)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D.ThenF◦(p,d′)is afinite sequence of elements of E.(98)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D.Ifr=F◦(p,d′),then len r=len p.(99)For every function F from[:D,D′:]into E holds F◦(εD,d′)=εE.(100)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D.If p= d1 ,then F◦(p,d′)= F(d1,d′) .(101)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D.If p= d1,d2 ,then F◦(p,d′)= F(d1,d′),F(d2,d′) .(102)Let F be a function from[:D,D′:]into E and p be afinite sequence of elements of D.If p= d1,d2,d3 ,then F◦(p,d′)= F(d1,d′),F(d2,d′),F(d3,d′) .Let D be a set.A set is called a set offinite sequences of D if:(Def.3)If a∈it,then a is afinite sequence of elements of D.Let D be a set.Note that there exists a set offinite sequences of D which is non empty.Let D be a set.A non empty set offinite sequences of D is a non empty set offinite sequences of D.We now state the proposition(104)7For every set D holds D∗is a non empty set offinite sequences of D.Let D be a set.Then D∗is a non empty set offinite sequences of D.We now state the proposition(105)For every set D and for every non empty set D′offinite sequences of D holds D′⊆D∗.Let D be a set and let S be a non empty set offinite sequences of D.We see that the element of S is afinite sequence of elements of D.The following proposition is true(107)8For every non empty subset D′of D holds every non empty set offinite sequences of D′isa non empty set offinite sequences of D.Let i be a natural number and let D be a set.The functor D i yields a set offinite sequences of D and is defined by:(Def.4)D i={s;s ranges over elements of D∗:len s=i}.Let i be a natural number and let us consider D.Note that D i is non empty.We now state a number of propositions:(109)9For every element z of D i holds len z=i.(110)For every set D holds everyfinite sequence z of elements of D is an element of D len z. (111)D i=D Seg i.(112)For every set D holds D0={εD}.(113)For every set D and for every element z of D0holds z=εD.(114)For every set D holdsεD is an element of D0.(115)For every element z of D0and for every element t of D i holds z t=t and t z=t. (116)D1={ d }.(117)For every element z of D1there exists d such that z= d .(118) d is an element of D1.(119)D2={ d1,d2 }.(120)For every element z of D2there exist d1,d2such that z= d1,d2 .(121) d1,d2 is an element of D2.(122)D3={ d1,d2,d3 }.(123)For every element z of D3there exist d1,d2,d3such that z= d1,d2,d3 .(124) d1,d2,d3 is an element of D3.(125)D i+j={z t:z ranges over elements of D i,t ranges over elements of D j}.(126)For every element s of D i+j there exists an element z of D i and there exists an element t ofD j such that s=z t.(127)For every element z of D i and for every element t of D j holds z t is an element of D i+j.{D i}.(128)D∗=(129)For every non empty subset D′of D holds every element of D′i is an element of D i. (130)If D i=D j,then i=j.(131)idseq(i)is an element of N i.(132)i→d is an element of D i.(133)For every element z of D i and for every function f from D into D′holds f·z is an element of D′i.(134)Let z be an element of D i and f be a function from Seg i into Seg i.If rng f=Seg i,then z·f is an element of D i.(135)For every element z of D i and for every permutation f of Seg i holds z·f is an element ofD i.(136)For every element z of D i and for every d holds(z d )(i+1)=d.(137)For every element z of D i+1there exists an element t of D i and there exists d such that z=t d .(138)For every element z of D i holds z·idseq(i)=z.(139)For all elements z1,z2of D i such that for every j such that j∈Seg i holds z1(j)=z2(j) holds z1=z2.(140)Let F be a function from[:D,D′:]into E,z1be an element of D i,and z2be an element of D′i.Then F◦(z1,z2)is an element of E i.(141)For every function F from[:D,D′:]into E and for every element z of D′i holds F◦(d,z)is an element of E i.(142)For every function F from[:D,D′:]into E and for every element z of D i holds F◦(z,d′)is an element of E i.(143)(i+j)→x=(i→x) (j→x).(144)For all i,D and for every element x of D i holds dom x=Seg i.(145)For every function f and for all sets x,y such that x∈dom f and y∈dom f holds f· x, y = f(x),f(y) .(146)For every function f and for all sets x,y,z such that x∈dom f and y∈dom f and z∈dom f holds f· x,y,z = f(x),f(y),f(z) .(147)rng x1,x2 ={x1,x2}.(148)rng x1,x2,x3 ={x1,x2,x3}.R EFERENCES[1]Grzegorz Bancerek.The fundamental properties of natural numbers.Journal of Formalized Mathematics,1,1989.http://mizar.org/JFM/Vol1/nat_1.html.[2]Grzegorz Bancerek.The ordinal numbers.Journal of Formalized Mathematics,1,1989./JFM/Vol1/ordinal1.html.[3]Grzegorz Bancerek.Sequences of ordinal numbers.Journal of Formalized Mathematics,1,1989./JFM/Vol1/ordinal2.html.[4]Grzegorz Bancerek and Krzysztof Hryniewiecki.Segments of natural numbers andfinite sequences.Journal of Formalized Mathematics,1,1989./JFM/Vol1/finseq_1.html.[5]Czesław Byli´n ski.Binary operations.Journal of Formalized Mathematics,1,1989./JFM/Vol1/binop_1.html.[6]Czesław Byli´n ski.Functions and their basic properties.Journal of Formalized Mathematics,1,1989./JFM/Vol1/funct_1.html.[7]Czesław Byli´n ski.Functions from a set to a set.Journal of Formalized Mathematics,1,1989./JFM/Vol1/funct_2.html.[8]Czesław Byli´n ski.Partial functions.Journal of Formalized Mathematics,1,1989./JFM/Vol1/partfun1.html.[9]Czesław Byli´n ski.Some basic properties of sets.Journal of Formalized Mathematics,1,1989./JFM/Vol1/zfmisc_1.html.[10]Andrzej Trybulec.Binary operations applied to functions.Journal of Formalized Mathematics,1,1989./JFM/Vol1/funcop_1.html.[11]Andrzej Trybulec.Domains and their Cartesian products.Journal of Formalized Mathematics,1,1989./JFM/Vol1/domain_1.html.[12]Andrzej Trybulec.Enumerated sets.Journal of Formalized Mathematics,1,1989./JFM/Vol1/enumset1.html.[13]Andrzej Trybulec.Tarski Grothendieck set theory.Journal of Formalized Mathematics,Axiomatics,1989./JFM/Axiomatics/tarski.html.[14]Andrzej Trybulec.Subsets of real numbers.Journal of Formalized Mathematics,Addenda,2003./JFM/Addenda/numbers.html.[15]Andrzej Trybulec and Czesław Byli´n ski.Some properties of real numbers operations:min,max,square,and square root.Journal ofFormalized Mathematics,1,1989./JFM/Vol1/square_1.html.[16]Zinaida Trybulec.Properties of subsets.Journal of Formalized Mathematics,1,1989./JFM/Vol1/subset_1.html.[17]Edmund Woronowicz.Relations and their basic properties.Journal of Formalized Mathematics,1,1989./JFM/Vol1/relat_1.html.Received March1,1990Published January2,2004。
