:: Non-contiguous Substrings and One-to-one Finite Sequences :: by Wojciech A. Trybulec :: :: Received April 8, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, XBOOLE_0, ARYTM_3, CARD_1, XXREAL_0, ARYTM_1, NAT_1, SUBSET_1, TARSKI, RELAT_1, ORDINAL4, FUNCT_1, FINSET_1, FINSEQ_2, FUNCT_2, CARD_3, FUNCOP_1, FINSEQ_3, EQREL_1, ALG_1, FUNCT_6, SETFAM_1, FINSEQ_4, ZFMISC_1, FUNCT_5, PARTFUN1, XCMPLX_0, ORDINAL1; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_2, FINSET_1, NAT_1, FINSEQOP, XXREAL_0, CARD_3, FUNCT_3, FUNCT_5, FUNCT_6, EQREL_1; constructors ENUMSET1, PARTFUN1, WELLORD2, XXREAL_0, REAL_1, NAT_1, INT_1, FINSEQOP, RELSET_1, CARD_3, DOMAIN_1, CARD_2, EQREL_1, FUNCT_6, BINOP_1, FUNCT_3, FUNCT_5, FINSEQ_2; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_1, FINSEQ_2, FUNCOP_1, CARD_3, CARD_2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve p,q,r for FinSequence; reserve u,v,x,y,y1,y2,z for object, A,D,X,Y for set; reserve i,j,k,l,m,n for Nat; theorem :: FINSEQ_3:1 Seg 3 = {1,2,3}; theorem :: FINSEQ_3:2 Seg 4 = {1,2,3,4}; theorem :: FINSEQ_3:3 Seg 5 = {1,2,3,4,5}; theorem :: FINSEQ_3:4 Seg 6 = {1,2,3,4,5,6}; theorem :: FINSEQ_3:5 Seg 7 = {1,2,3,4,5,6,7}; theorem :: FINSEQ_3:6 Seg 8 = {1,2,3,4,5,6,7,8}; theorem :: FINSEQ_3:7 Seg k = {} iff not k in Seg k; theorem :: FINSEQ_3:8 not k + 1 in Seg k; theorem :: FINSEQ_3:9 k <> 0 implies k in Seg(k + n); theorem :: FINSEQ_3:10 k + n in Seg k implies n = 0; theorem :: FINSEQ_3:11 k < n implies k + 1 in Seg n; theorem :: FINSEQ_3:12 k in Seg n & m < k implies k - m in Seg n; theorem :: FINSEQ_3:13 k - n in Seg k iff n < k; theorem :: FINSEQ_3:14 Seg k misses {k + 1}; theorem :: FINSEQ_3:15 Seg(k + 1) \ Seg k = {k + 1}; :: Theorem Seg(k + 1) \ {k + 1} = Seg k is :: proved in RLVECT_1 and has a number 104. theorem :: FINSEQ_3:16 Seg k <> Seg(k + 1); theorem :: FINSEQ_3:17 Seg k = Seg(k + n) implies n = 0; theorem :: FINSEQ_3:18 Seg k c= Seg(k + n); theorem :: FINSEQ_3:19 Seg k, Seg n are_c=-comparable; theorem :: FINSEQ_3:20 for y being object st Seg k = {y} holds k = 1 & y = 1; theorem :: FINSEQ_3:21 Seg k = {x,y} & x <> y implies k = 2 & {x,y} = {1,2}; theorem :: FINSEQ_3:22 x in dom p implies x in dom(p ^ q); theorem :: FINSEQ_3:23 x in dom p implies x is Element of NAT; theorem :: FINSEQ_3:24 x in dom p implies x <> 0; theorem :: FINSEQ_3:25 n in dom p iff 1 <= n & n <= len p; theorem :: FINSEQ_3:26 n in dom p iff n - 1 is Element of NAT & len p - n is Element of NAT; ::$CT 2 theorem :: FINSEQ_3:29 len p = len q iff dom p = dom q; theorem :: FINSEQ_3:30 len p <= len q iff dom p c= dom q; theorem :: FINSEQ_3:31 x in rng p implies 1 in dom p; theorem :: FINSEQ_3:32 rng p <> {} implies 1 in dom p; theorem :: FINSEQ_3:33 {} <> <* x,y *>; theorem :: FINSEQ_3:34 {} <> <* x,y,z *>; theorem :: FINSEQ_3:35 <* x *> <> <* y,z *>; theorem :: FINSEQ_3:36 <* u *> <> <* x,y,z *>; theorem :: FINSEQ_3:37 <* u,v *> <> <* x,y,z *>; theorem :: FINSEQ_3:38 len r = len p + len q & (for k being Nat st k in dom p holds r.k = p.k) & (for k being Nat st k in dom q holds r.(len p + k) = q.k) implies r = p ^ q; theorem :: FINSEQ_3:39 for A being finite set st A c= Seg k holds len(Sgm A) = card A; theorem :: FINSEQ_3:40 for A being finite set st A c= Seg k holds dom(Sgm A) = Seg(card A); theorem :: FINSEQ_3:41 X c= Seg i & k < l & 1 <= n & m <= len(Sgm X) & Sgm(X).m = k & Sgm(X).n = l implies m < n; theorem :: FINSEQ_3:42 X c= Seg i & Y c= Seg j implies ((for m,n being Nat st m in X & n in Y holds m < n) iff Sgm(X \/ Y) = Sgm(X) ^ Sgm(Y)); theorem :: FINSEQ_3:43 Sgm {} = {}; :: The other way of the one above - FINSEQ_1:72. theorem :: FINSEQ_3:44 0 <> n implies Sgm{n} = <* n *>; theorem :: FINSEQ_3:45 0 < n & n < m implies Sgm{n,m} = <* n,m *>; theorem :: FINSEQ_3:46 len(Sgm(Seg k)) = k; theorem :: FINSEQ_3:47 Sgm(Seg(k + n)) | Seg k = Sgm(Seg k); theorem :: FINSEQ_3:48 Sgm(Seg k) = idseq k; theorem :: FINSEQ_3:49 p | Seg n = p iff len p <= n; theorem :: FINSEQ_3:50 idseq(n + k) | Seg n = idseq n; theorem :: FINSEQ_3:51 idseq n | Seg m = idseq m iff m <= n; theorem :: FINSEQ_3:52 idseq n | Seg m = idseq n iff n <= m; theorem :: FINSEQ_3:53 len p = k + l & q = p | Seg k implies len q = k; theorem :: FINSEQ_3:54 len p = k + l & q = p | Seg k implies dom q = Seg k; theorem :: FINSEQ_3:55 len p = k + 1 & q = p | Seg k implies p = q ^ <* p.(k + 1) *>; theorem :: FINSEQ_3:56 p | X is FinSequence iff ex k being Element of NAT st X /\ dom p = Seg k; theorem :: FINSEQ_3:57 card((p ^ q) " A) = card(p " A) + card(q " A); theorem :: FINSEQ_3:58 p " A c= (p ^ q) " A; definition let p,A; func p - A -> FinSequence equals :: FINSEQ_3:def 1 p * Sgm ((dom p) \ p " A); end; theorem :: FINSEQ_3:59 len(p - A) = len p - card(p " A); theorem :: FINSEQ_3:60 len(p - A) <= len p; theorem :: FINSEQ_3:61 len(p - A) = len p implies A misses rng p; theorem :: FINSEQ_3:62 n = len p - card(p " A) implies dom(p - A) = Seg n; theorem :: FINSEQ_3:63 dom(p - A) c= dom p; theorem :: FINSEQ_3:64 dom(p - A) = dom p implies A misses rng p; theorem :: FINSEQ_3:65 rng(p - A) = rng p \ A; theorem :: FINSEQ_3:66 rng(p - A) c= rng p; theorem :: FINSEQ_3:67 rng(p - A) = rng p implies A misses rng p; theorem :: FINSEQ_3:68 p - A = {} iff rng p c= A; theorem :: FINSEQ_3:69 p - A = p iff A misses rng p; theorem :: FINSEQ_3:70 p - {x} = p iff not x in rng p; theorem :: FINSEQ_3:71 p - {} = p; theorem :: FINSEQ_3:72 p - rng p = {}; theorem :: FINSEQ_3:73 (p ^ q) - A = (p - A) ^ (q - A); theorem :: FINSEQ_3:74 {} - A = {}; theorem :: FINSEQ_3:75 <* x *> - A = <* x *> iff not x in A; theorem :: FINSEQ_3:76 <* x *> - A = {} iff x in A; theorem :: FINSEQ_3:77 <* x,y *> - A = {} iff x in A & y in A; theorem :: FINSEQ_3:78 x in A & not y in A implies <* x,y *> - A = <* y *>; theorem :: FINSEQ_3:79 <* x,y *> - A = <* y *> & x <> y implies x in A & not y in A; theorem :: FINSEQ_3:80 not x in A & y in A implies <* x,y *> - A = <* x *>; theorem :: FINSEQ_3:81 <* x,y *> - A = <* x *> & x <> y implies not x in A & y in A; theorem :: FINSEQ_3:82 <* x,y *> - A = <* x,y *> iff not x in A & not y in A; theorem :: FINSEQ_3:83 len p = k + 1 & q = p | Seg k implies (p.(k + 1) in A iff p - A = q - A); theorem :: FINSEQ_3:84 len p = k + 1 & q = p | Seg k implies (not p.(k + 1) in A iff p - A = (q - A) ^ <* p.(k + 1) *>); theorem :: FINSEQ_3:85 n in dom p implies for B being finite set st B = {k where k is Element of NAT : k in dom p & k <= n & p.k in A} holds p.n in A or (p - A).(n - card B) = p.n; theorem :: FINSEQ_3:86 p is FinSequence of D implies p - A is FinSequence of D; theorem :: FINSEQ_3:87 p is one-to-one implies p - A is one-to-one; theorem :: FINSEQ_3:88 p is one-to-one implies len(p - A) = len p - card(A /\ rng p); theorem :: FINSEQ_3:89 for A being finite set st p is one-to-one & A c= rng p holds len (p - A) = len p - card A; theorem :: FINSEQ_3:90 p is one-to-one & x in rng p implies len(p - {x}) = len p - 1; theorem :: FINSEQ_3:91 rng p misses rng q & p is one-to-one & q is one-to-one iff p ^ q is one-to-one; theorem :: FINSEQ_3:92 A c= Seg k implies Sgm A is one-to-one; theorem :: FINSEQ_3:93 <* x *> is one-to-one; theorem :: FINSEQ_3:94 x <> y iff <* x,y *> is one-to-one; theorem :: FINSEQ_3:95 x <> y & y <> z & z <> x iff <* x,y,z *> is one-to-one; theorem :: FINSEQ_3:96 p is one-to-one & rng p = {x} implies len p = 1; theorem :: FINSEQ_3:97 p is one-to-one & rng p = {x} implies p = <* x *>; theorem :: FINSEQ_3:98 p is one-to-one & rng p = {x,y} & x <> y implies len p = 2; theorem :: FINSEQ_3:99 p is one-to-one & rng p = {x,y} & x <> y implies p = <* x,y *> or p = <* y,x *>; theorem :: FINSEQ_3:100 p is one-to-one & rng p = {x,y,z} & <* x,y,z *> is one-to-one implies len p = 3; theorem :: FINSEQ_3:101 p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & x <> z implies len p = 3; begin :: Addenda :: from FSM_1 theorem :: FINSEQ_3:102 for D being non empty set, df being FinSequence of D holds df is non empty implies ex d being Element of D, df1 being FinSequence of D st d = df.1 & df = <*d*>^df1; theorem :: FINSEQ_3:103 for df being FinSequence, d being object holds i in dom df implies (<*d*>^df).(i+1) = df.i; :: from MATRIX_2, 2005.11.16, A.T. definition let i be natural Number; let p be FinSequence; func Del(p,i) -> FinSequence equals :: FINSEQ_3:def 2 p * Sgm ((dom p) \ {i}); end; theorem :: FINSEQ_3:104 for p being FinSequence holds (i in dom p implies ex m being Nat st len p = m + 1 & len Del(p,i) = m) & (not i in dom p implies Del(p,i) = p); theorem :: FINSEQ_3:105 for D being non empty set for p being FinSequence of D holds Del(p,i) is FinSequence of D; :: from MATRLIN, 2005.11.16, A.T. theorem :: FINSEQ_3:106 for p be FinSequence holds rng Del(p,i) c= rng p; :: from GOBOARD1, 2005.11.16, A.T. theorem :: FINSEQ_3:107 n = m + 1 & i in Seg n implies len Sgm(Seg n \ {i}) = m; reserve J for Nat; theorem :: FINSEQ_3:108 for i,k,m,n being Nat st n=m+1 & k in Seg n & i in Seg m holds (1<=i & i 0 & A = {} iff i-tuples_on A = {}; :: from AMISTD_2, 2009.09.08, A.T. registration let i be Nat, D be set; cluster i-tuples_on D -> with_common_domain; end; registration let i be Nat, D be set; cluster i-tuples_on D -> product-like; end; begin :: Moved from ALG_1, 2010.03.17 reserve n for Nat; theorem :: FINSEQ_3:120 for D1,D2 be non empty set, p be FinSequence of D1, f be Function of D1,D2 holds dom(f*p) = dom p & len (f*p) = len p & for n being Nat st n in dom (f*p) holds (f*p).n = f.(p.n); definition let D be non empty set, R be Relation of D; func ExtendRel(R) -> Relation of D* means :: FINSEQ_3:def 3 for x,y be FinSequence of D holds [x,y] in it iff len x = len y & for n st n in dom x holds [x.n,y.n] in R; end; theorem :: FINSEQ_3:121 for D be non empty set holds ExtendRel(id D) = id (D*); definition let D be non empty set, R be Equivalence_Relation of D; let y be FinSequence of Class(R), x be FinSequence of D; pred x is_representatives_FS y means :: FINSEQ_3:def 4 len x = len y & for n st n in dom x holds Class(R,x.n) = y.n; end; theorem :: FINSEQ_3:122 for D be non empty set, R be Equivalence_Relation of D, y be FinSequence of Class(R) ex x be FinSequence of D st x is_representatives_FS y ; :: from FUNCT_6, 2011.04.18, A.T. reserve x,y,y1,y2,z,a,b for object, X,Y,Z,V1,V2 for set, f,g,h,h9,f1,f2 for Function, i for Nat, P for Permutation of X, D,D1,D2,D3 for non empty set, d1 for Element of D1, d2 for Element of D2, d3 for Element of D3; theorem :: FINSEQ_3:123 x in product <*X*> iff ex y st y in X & x = <*y*>; theorem :: FINSEQ_3:124 z in product <*X,Y*> iff ex x,y st x in X & y in Y & z = <*x,y*>; theorem :: FINSEQ_3:125 a in product <*X,Y,Z*> iff ex x,y,z st x in X & y in Y & z in Z & a = <*x,y,z*>; theorem :: FINSEQ_3:126 product <*D*> = 1-tuples_on D; theorem :: FINSEQ_3:127 product <*D1,D2*> = the set of all <*d1,d2*>; theorem :: FINSEQ_3:128 product <*D,D*> = 2-tuples_on D; theorem :: FINSEQ_3:129 product <*D1,D2,D3*> = the set of all <*d1,d2,d3*>; theorem :: FINSEQ_3:130 product <*D,D,D*> = 3-tuples_on D; theorem :: FINSEQ_3:131 for D being set holds product (i |-> D) = i-tuples_on D; registration let f be Function; cluster <*f*> -> Function-yielding; let g be Function; cluster <*f,g*> -> Function-yielding; let h be Function; cluster <*f,g,h*> -> Function-yielding; end; theorem :: FINSEQ_3:132 doms <*f*> = <*dom f*> & rngs <*f*> = <*rng f*>; theorem :: FINSEQ_3:133 doms <*f,g*> = <*dom f, dom g*> & rngs <*f,g*> = <*rng f, rng g *>; theorem :: FINSEQ_3:134 doms <*f,g,h*> = <*dom f, dom g, dom h*> & rngs <*f,g,h*> = <*rng f, rng g, rng h*>; theorem :: FINSEQ_3:135 Union <*X*> = X & meet <*X*> = X; theorem :: FINSEQ_3:136 Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y; theorem :: FINSEQ_3:137 Union <*X,Y,Z*> = X \/ Y \/ Z & meet <*X,Y,Z*> = X /\ Y /\ Z; theorem :: FINSEQ_3:138 x in dom f implies <*f*>..(1,x) = f.x & <*f,g*>..(1,x) = f.x & <*f,g,h *>..(1,x) = f.x; theorem :: FINSEQ_3:139 x in dom g implies <*f,g*>..(2,x) = g.x & <*f,g,h*>..(2,x) = g.x; theorem :: FINSEQ_3:140 x in dom h implies <*f,g,h*>..(3,x) = h.x; theorem :: FINSEQ_3:141 dom <:<*h*>:> = dom h & for x st x in dom h holds <:<*h*>:>.x = <*h.x *>; theorem :: FINSEQ_3:142 dom <:<*f1,f2*>:> = dom f1 /\ dom f2 & for x st x in dom f1 /\ dom f2 holds <:<*f1,f2*>:>.x = <*f1.x,f2.x*>; theorem :: FINSEQ_3:143 dom Frege<*h*> = product <*dom h*> & rng Frege<*h*> = product <*rng h *> & for x st x in dom h holds (Frege<*h*>).<*x*> = <*h.x*>; theorem :: FINSEQ_3:144 dom Frege<*f1,f2*> = product <*dom f1, dom f2*> & rng Frege<*f1, f2*> = product <*rng f1, rng f2*> & for x,y st x in dom f1 & y in dom f2 holds (Frege<*f1,f2*>).<*x,y*> = <*f1.x, f2.y*>; theorem :: FINSEQ_3:145 x in dom f1 & x in dom f2 implies for y1,y2 holds <:f1,f2:>.x = [y1,y2 ] iff <:<*f1,f2*>:>.x = <*y1,y2*>; theorem :: FINSEQ_3:146 x in dom f1 & y in dom f2 implies for y1,y2 holds [:f1,f2:].(x,y) = [ y1,y2] iff (Frege<*f1,f2*>).<*x,y*> = <*y1,y2*>; theorem :: FINSEQ_3:147 Funcs(<*X*>,Y) = <*Funcs(X,Y)*>; theorem :: FINSEQ_3:148 Funcs(<*X,Y*>,Z) = <*Funcs(X,Z), Funcs(Y,Z)*>; theorem :: FINSEQ_3:149 Funcs(X,<*Y*>) = <*Funcs(X,Y)*>; theorem :: FINSEQ_3:150 Funcs(X,<*Y,Z*>) = <*Funcs(X,Y), Funcs(X,Z)*>; ::from JORDAN2C, 2011.07.03, A.T. theorem :: FINSEQ_3:151 for f being FinSequence st rng f={x,y} & len f=2 holds f.1=x & f. 2=y or f.1=y & f.2=x; :: from GLIB_001, 2011.07.30, A.T. theorem :: FINSEQ_3:152 for X being set, k being Element of NAT st X c= Seg k holds for m ,n being Element of NAT st m in dom (Sgm X) & n = (Sgm X).m holds m <= n; registration let i be Nat; let D be finite set; cluster i-tuples_on D -> finite; end; theorem :: FINSEQ_3:153 for p being m-element FinSequence holds len p = m; theorem :: FINSEQ_3:154 for p being n-element FinSequence, q being FinSequence holds (p^q).1 = p.1 & ... & (p^q).n = p.n; reserve n for Nat; theorem :: FINSEQ_3:155 for p being n-element FinSequence, q being m-element FinSequence holds (p^q).(n+(1 qua Nat)) = q.1 & ... & (p^q).(n+m) = q.m; theorem :: FINSEQ_3:156 for p being FinSequence, k being Nat st k in dom p for i being Nat st 1 <= i & i <= k holds i in dom p; :: from PNPROC_1, 2012.02.20, A.T. theorem :: FINSEQ_3:157 for q being FinSubsequence st q = {[i,x]} holds Seq q = <*x*>; theorem :: FINSEQ_3:158 for p being FinSubsequence holds card p = len Seq p; theorem :: FINSEQ_3:159 for q being FinSubsequence st Seq q = <*x*> ex i being Element of NAT st q = {[i,x]};