:: Some Properties of Restrictions of Finite Sequences :: by Czes\law Byli\'nski :: :: Received January 25, 1995 :: Copyright (c) 1995-2016 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, NAT_1, XXREAL_0, ARYTM_1, ARYTM_3, SUBSET_1, FINSEQ_1, CARD_1, FUNCT_1, RELAT_1, FINSEQ_4, ZFMISC_1, XBOOLE_0, ORDINAL4, TARSKI, PARTFUN1, RFINSEQ, FINSEQ_5; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, ZFMISC_1, RFINSEQ, NAT_D, XXREAL_0; constructors XXREAL_0, NAT_1, INT_1, PARTFUN1, FINSEQ_4, ZFMISC_1, RFINSEQ, NAT_D, REAL_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve i,j,k,n for Nat; theorem :: FINSEQ_5:1 for i, n being Nat holds i <= n implies n - i + 1 is Element of NAT; theorem :: FINSEQ_5:2 for i,n being Nat holds i in Seg n implies n - i + 1 in Seg n; theorem :: FINSEQ_5:3 for f being Function, x,y being object st f"{y} = {x} holds x in dom f & y in rng f & f.x = y; theorem :: FINSEQ_5:4 for f being Function holds f is one-to-one iff for x being set st x in dom f holds f"{f.x} = {x}; theorem :: FINSEQ_5:5 for f being Function, y1,y2 being object st f is one-to-one & y1 in rng f & f"{y1} = f"{y2} holds y1 = y2; registration let x be object; cluster <*x*> -> trivial; let y be object; cluster <*x,y*> -> non trivial; end; registration cluster one-to-one non empty for FinSequence; end; theorem :: FINSEQ_5:6 for f being non empty FinSequence holds 1 in dom f & len f in dom f; theorem :: FINSEQ_5:7 for f being non empty FinSequence ex i being Nat st i+1 = len f; theorem :: FINSEQ_5:8 for x being object, f being FinSequence holds len(<*x*>^f) = 1 + len f; theorem :: FINSEQ_5:9 for f being FinSequence, p,q being set st p in rng f & q in rng f & p..f = q..f holds p = q; theorem :: FINSEQ_5:10 for f,g being FinSequence st n+1 in dom f & g = f|Seg n holds f| Seg(n+1) = g^<*f.(n+1)*>; theorem :: FINSEQ_5:11 for f being one-to-one FinSequence st i in dom f holds (f.i)..f = i; reserve D for non empty set, p for Element of D, f,g for FinSequence of D; registration let D be non empty set; cluster one-to-one non empty for FinSequence of D; end; :: FINSEQ_1:17 theorem :: FINSEQ_5:12 dom f = dom g & (for i st i in dom f holds f/.i = g/.i) implies f = g; :: FINSEQ_1:18 theorem :: FINSEQ_5:13 len f = len g & (for k st 1 <= k & k <= len f holds f/.k = g/.k) implies f = g; theorem :: FINSEQ_5:14 len f = 1 implies f = <*f/.1*>; theorem :: FINSEQ_5:15 for D being non empty set, p being Element of D, f being FinSequence of D holds (<*p*>^f)/.1 = p; theorem :: FINSEQ_5:16 for f being FinSequence, i being Nat holds len(f|i) <= len f; theorem :: FINSEQ_5:17 for f being FinSequence, i being Nat holds len(f|i) <= i; theorem :: FINSEQ_5:18 for f being FinSequence, i being Nat holds dom(f|i) c= dom f; theorem :: FINSEQ_5:19 for f being FinSequence, i being Nat holds rng(f|i) c= rng f; theorem :: FINSEQ_5:20 for D being set, f being FinSequence of D st f is non empty holds f|1 = <*f/.1*>; theorem :: FINSEQ_5:21 i+1 = len f implies f = (f|i)^<*f/.len f*>; registration let i,D; let f be one-to-one FinSequence of D; cluster f|i -> one-to-one; end; theorem :: FINSEQ_5:22 for D being set, f, g being FinSequence of D st i <= len f holds (f^g)|i = f|i; theorem :: FINSEQ_5:23 for D being set, f, g being FinSequence of D holds (f^g)|(len f) = f; theorem :: FINSEQ_5:24 for D being set, f being FinSequence of D st p in rng f holds (f-|p)^ <*p*> = f|(p..f); theorem :: FINSEQ_5:25 len(f/^i) <= len f; reserve D for set, f for FinSequence of D; theorem :: FINSEQ_5:26 i in dom(f/^n) implies n+i in dom f; theorem :: FINSEQ_5:27 i in dom(f/^n) implies (f/^n)/.i = f/.(n+i); theorem :: FINSEQ_5:28 f/^0 = f; reserve D for non empty set, p for Element of D, f,g for FinSequence of D; theorem :: FINSEQ_5:29 f is non empty implies f = <*f/.1*>^(f/^1); theorem :: FINSEQ_5:30 i+1 = len f implies f/^i = <*f/.len f*>; theorem :: FINSEQ_5:31 j+1 = i & i in dom f implies <*f/.i*>^(f/^i) = f/^j; theorem :: FINSEQ_5:32 for D being set, f being FinSequence of D holds len f <= i implies f/^i is empty; theorem :: FINSEQ_5:33 rng(f/^n) c= rng f; registration let i,D; let f be one-to-one FinSequence of D; cluster f/^i -> one-to-one; end; theorem :: FINSEQ_5:34 f is one-to-one implies rng(f|n) misses rng(f/^n); theorem :: FINSEQ_5:35 p in rng f implies f |-- p = f/^(p..f); theorem :: FINSEQ_5:36 (f^g)/^(len f + i) = g/^i; theorem :: FINSEQ_5:37 (f^g)/^(len f) = g; theorem :: FINSEQ_5:38 p in rng f implies f/.(p..f) = p; theorem :: FINSEQ_5:39 i in dom f implies f/.i..f <= i; theorem :: FINSEQ_5:40 p in rng(f|i) implies p..(f|i) = p..f; theorem :: FINSEQ_5:41 i in dom f & f is one-to-one implies f/.i..f = i; definition let D, f; let p be set; func f-:p -> FinSequence of D equals :: FINSEQ_5:def 1 f|(p..f); end; theorem :: FINSEQ_5:42 p in rng f implies len(f-:p) = p..f; theorem :: FINSEQ_5:43 p in rng f & i in Seg(p..f) implies (f-:p)/.i = f/.i; theorem :: FINSEQ_5:44 p in rng f implies (f-:p)/.1 = f/.1; theorem :: FINSEQ_5:45 p in rng f implies (f-:p)/.(p..f) = p; theorem :: FINSEQ_5:46 for x being set holds x in rng f & p in rng f & x..f<=p..f implies x in rng(f-:p); theorem :: FINSEQ_5:47 p in rng f implies f-:p is non empty; theorem :: FINSEQ_5:48 rng(f-:p) c= rng f; registration let D,p; let f be one-to-one FinSequence of D; cluster f-:p -> one-to-one; end; definition let D, f, p; func f:-p -> FinSequence of D equals :: FINSEQ_5:def 2 <*p*>^(f/^p..f); end; theorem :: FINSEQ_5:49 p in rng f implies ex i being Element of NAT st i+1 = p..f & f:- p = f/^i; theorem :: FINSEQ_5:50 p in rng f implies len (f:-p) = len f - p..f + 1; theorem :: FINSEQ_5:51 p in rng f & j+1 in dom(f:-p) implies j+p..f in dom f; registration let D,p,f; cluster f:-p -> non empty; end; theorem :: FINSEQ_5:52 p in rng f & j+1 in dom(f:-p) implies (f:-p)/.(j+1) = f/.(j+p..f ); theorem :: FINSEQ_5:53 (f:-p)/.1 = p; theorem :: FINSEQ_5:54 p in rng f implies (f:-p)/.(len(f:-p)) = f/.len f; theorem :: FINSEQ_5:55 p in rng f implies rng(f:-p) c= rng f; theorem :: FINSEQ_5:56 p in rng f & f is one-to-one implies f:-p is one-to-one; reserve i for Nat; definition let f be FinSequence; func Rev f -> FinSequence means :: FINSEQ_5:def 3 len it = len f & for i st i in dom it holds it.i = f.(len f - i + 1); involutiveness; end; theorem :: FINSEQ_5:57 for f being FinSequence holds dom f = dom Rev f & rng f = rng Rev f; theorem :: FINSEQ_5:58 for f being FinSequence st i in dom f holds (Rev f).i = f.(len f - i + 1); theorem :: FINSEQ_5:59 for f being FinSequence, i,j being Nat st i in dom f & i+j = len f + 1 holds j in dom Rev f; registration let f be empty FinSequence; cluster Rev f -> empty; end; theorem :: FINSEQ_5:60 for x being object holds Rev <*x*> = <*x*>; theorem :: FINSEQ_5:61 for x1,x2 being object holds Rev <*x1,x2*> = <*x2,x1*>; theorem :: FINSEQ_5:62 for f being FinSequence holds f.1 = (Rev f).(len f) & f.(len f) = (Rev f).1; registration let f be one-to-one FinSequence; cluster Rev f -> one-to-one; end; theorem :: FINSEQ_5:63 for f being FinSequence, x being object holds Rev(f^<*x*>) = <*x*>^ (Rev f); theorem :: FINSEQ_5:64 for f,g being FinSequence holds Rev(f^g) = (Rev g)^(Rev f); definition let D be set, f be FinSequence of D; redefine func Rev f -> FinSequence of D; end; theorem :: FINSEQ_5:65 f is non empty implies f/.1 = (Rev f)/.len f & f/.len f = (Rev f)/.1; theorem :: FINSEQ_5:66 i in dom f & i+j = len f + 1 implies f/.i = (Rev f)/.j; definition let D,f,p; let n be Nat; func Ins(f,n,p) -> FinSequence of D equals :: FINSEQ_5:def 4 (f|n)^<*p*>^(f/^n); end; theorem :: FINSEQ_5:67 Ins(f,0,p) = <*p*>^f; theorem :: FINSEQ_5:68 len f <= n implies Ins(f,n,p) = f^<*p*>; theorem :: FINSEQ_5:69 len(Ins(f,n,p)) = len f + 1; theorem :: FINSEQ_5:70 rng Ins(f,n,p) = {p} \/ rng f; registration let D,f,n,p; cluster Ins(f,n,p) -> non empty; end; theorem :: FINSEQ_5:71 p in rng Ins(f,n,p); theorem :: FINSEQ_5:72 i in dom(f|n) implies (Ins(f,n,p))/.i = f/.i; theorem :: FINSEQ_5:73 n <= len f implies (Ins(f,n,p))/.(n+1) = p; theorem :: FINSEQ_5:74 n+1 <= i & i <= len f implies (Ins(f,n,p))/.(i+1) = f/.i; theorem :: FINSEQ_5:75 1 <= n & f is non empty implies (Ins(f,n,p))/.1 = f/.1; theorem :: FINSEQ_5:76 f is one-to-one & not p in rng f implies Ins(f,n,p) is one-to-one; begin :: Addenda :: from JORDAN4, 2005.11.16, A.T. theorem :: FINSEQ_5:77 for i1,i2 be Nat st i1<=i2 holds (f|i1)|i2=f|i1 & (f|i2)|i1=f|i1; theorem :: FINSEQ_5:78 for i be Nat holds (<*>D)|i=<*>D; theorem :: FINSEQ_5:79 Rev <*>D = <*>D; :: from AMISTD_1, 2006.03,15, A.T. registration cluster non trivial for FinSequence; end; :: from JORDAN3, 2007.03.09, A.T theorem :: FINSEQ_5:80 for f being FinSequence of D,l1,l2 being Nat holds (f/^l1)|(l2-'l1)=(f |l2)/^l1; :: from JORDAN8, 2007.03.18, A.T. reserve D for set, f for FinSequence of D; theorem :: FINSEQ_5:81 len f >= 2 implies f|2 = <*f/.1,f/.2*>; theorem :: FINSEQ_5:82 k+1 <= len f implies f|(k+1) = f|k^<*f/.(k+1)*>; :: from JORDAN3, 2007.03.18, A.T. theorem :: FINSEQ_5:83 for D being set, p be FinSequence of D for i be Nat st i < len p holds p|(i+1) = p|i ^ <*p.(i+1)*>; :: from POLYNOM4, 2007.03.18, A.T. theorem :: FINSEQ_5:84 for D be non empty set for p be FinSequence of D for n be Nat st 1 <= n & n <= len p holds p = (p|(n-'1))^<*p.n*>^(p/^n);