:: On the Decomposition of Finite Sequences :: by Andrzej Trybulec :: :: Received May 24, 1995 :: Copyright (c) 1995-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, ZFMISC_1, XBOOLE_0, FINSEQ_5, RELAT_1, ORDINAL4, NAT_1, TARSKI, FUNCT_1, XXREAL_0, SUBSET_1, ARYTM_3, FINSEQ_4, ARYTM_1, CARD_1, RFINSEQ, PARTFUN1, FINSEQ_6, JORDAN3, INT_1, FINSET_1, GRAPH_2, ORDINAL1, FUNCT_4, FUNCT_7; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, FINSET_1, XCMPLX_0, XXREAL_0, XXREAL_2, FUNCT_4, ZFMISC_1, REAL_1, INT_1, NAT_1, NAT_D, RELAT_1, FUNCT_7, PARTFUN1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_4, RFINSEQ, FINSEQ_5; constructors XXREAL_0, NAT_1, INT_1, PARTFUN1, FINSEQ_4, RFINSEQ, BINARITH, FINSEQ_5, REAL_1, RELSET_1, NAT_D, ENUMSET1, CARD_1, WELLORD2, FUNCT_4, MEMBERED, XXREAL_2, FUNCT_7; registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, FINSEQ_5, ORDINAL1, NAT_1, CARD_1, XXREAL_0, FINSET_1, VALUED_0, NUMBERS, MEMBERED, XXREAL_2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve x,y,z for set; registration let x,y,z; cluster <*x,y,z*> -> non trivial; end; registration let f be non empty FinSequence; cluster Rev f -> non empty; end; begin reserve f,f1,f2,f3 for FinSequence, p,p1,p2,p3 for set, i,k for Nat; theorem :: FINSEQ_6:1 for X being set, i st X c= Seg i & 1 in X holds (Sgm X).1 = 1; theorem :: FINSEQ_6:2 for f being FinSequence holds k in dom f & (for i st 1 <= i & i < k holds f.i <> f.k) implies (f.k)..f = k; theorem :: FINSEQ_6:3 <*p1,p2*>| Seg 1 = <*p1*>; theorem :: FINSEQ_6:4 <*p1,p2,p3*>| Seg 1 = <*p1*>; theorem :: FINSEQ_6:5 <*p1,p2,p3*>| Seg 2 = <*p1,p2*>; theorem :: FINSEQ_6:6 p in rng f1 implies p..(f1^f2) = p..f1; theorem :: FINSEQ_6:7 p in rng f2 \ rng f1 implies p..(f1^f2) = len f1 + p..f2; theorem :: FINSEQ_6:8 p in rng f1 implies (f1^f2)|--p = (f1|--p)^f2; theorem :: FINSEQ_6:9 p in rng f2 \ rng f1 implies (f1^f2)|--p = f2|--p; theorem :: FINSEQ_6:10 f1 c= f1^f2; theorem :: FINSEQ_6:11 for A being set st A c= dom f1 holds (f1^f2)|A = f1 | A; theorem :: FINSEQ_6:12 p in rng f1 implies (f1^f2)-|p = f1-|p; registration let f1; let i be Nat; cluster f1|Seg i -> FinSequence-like; end; theorem :: FINSEQ_6:13 f1 c= f2 implies f3^f1 c= f3^f2; theorem :: FINSEQ_6:14 (f1^f2)|Seg(len f1 + i) = f1^(f2|Seg i); theorem :: FINSEQ_6:15 p in rng f2 \ rng f1 implies (f1^f2)-|p = f1^(f2-|p); theorem :: FINSEQ_6:16 f1^f2 just_once_values p implies p in rng f1 \+\ rng f2; theorem :: FINSEQ_6:17 f1^f2 just_once_values p & p in rng f1 implies f1 just_once_values p; theorem :: FINSEQ_6:18 p..<*p*> = 1; theorem :: FINSEQ_6:19 p1..<*p1,p2*> = 1; theorem :: FINSEQ_6:20 p1 <> p2 implies p2..<*p1,p2*> = 2; theorem :: FINSEQ_6:21 p1..<*p1,p2,p3*> = 1; theorem :: FINSEQ_6:22 p1 <> p2 implies p2..<*p1,p2,p3*> = 2; theorem :: FINSEQ_6:23 p1 <> p3 & p2 <> p3 implies p3..<*p1,p2,p3*> = 3; theorem :: FINSEQ_6:24 for f being FinSequence holds Rev(<*p*>^f) = Rev f ^ <*p*>; theorem :: FINSEQ_6:25 for f being FinSequence holds Rev Rev f = f; theorem :: FINSEQ_6:26 x <> y implies <*x,y*> -| y = <*x*>; theorem :: FINSEQ_6:27 x <> y implies <*x,y,z*> -| y = <*x*>; theorem :: FINSEQ_6:28 x <> z & y <> z implies <*x,y,z*> -| z = <*x,y*>; theorem :: FINSEQ_6:29 <*x,y*>|--x = <*y*>; theorem :: FINSEQ_6:30 x <> y implies <*x,y,z*>|--y = <*z*>; theorem :: FINSEQ_6:31 <*x,y,z*>|--x = <*y,z*>; theorem :: FINSEQ_6:32 <*z*>|--z = {} & <*z*>-|z = {}; theorem :: FINSEQ_6:33 x <> y implies <*x,y*> |-- y = {}; theorem :: FINSEQ_6:34 x <> z & y <> z implies <*x,y,z*> |-- z = {}; theorem :: FINSEQ_6:35 x in rng f & y in rng(f-|x) implies f-|x-|y = f-|y; theorem :: FINSEQ_6:36 not x in rng f1 implies x..(f1^<*x*>^f2) = len f1 + 1; theorem :: FINSEQ_6:37 f just_once_values x implies x..f + x..Rev f = len f + 1; theorem :: FINSEQ_6:38 f just_once_values x implies Rev(f-|x) = Rev f |--x; theorem :: FINSEQ_6:39 f just_once_values x implies Rev f just_once_values x; begin reserve D for non empty set, p,p1,p2,p3 for Element of D, f,f1,f2 for FinSequence of D; theorem :: FINSEQ_6:40 p in rng f implies f-:p = (f -| p)^<*p*>; theorem :: FINSEQ_6:41 p in rng f implies f:-p = <*p*>^(f |-- p); theorem :: FINSEQ_6:42 f <> {} implies f/.1 in rng f; theorem :: FINSEQ_6:43 f <> {} implies f/.1..f = 1; theorem :: FINSEQ_6:44 f <> {} & f/.1 = p implies f-:p = <*p*> & f:-p = f; theorem :: FINSEQ_6:45 (<*p1*>^f)/^1 = f; theorem :: FINSEQ_6:46 <*p1,p2*>/^1 = <*p2*>; theorem :: FINSEQ_6:47 <*p1,p2,p3*>/^1 = <*p2,p3*>; theorem :: FINSEQ_6:48 k in dom f & (for i st 1 <= i & i < k holds f/.i <> f/.k) implies f/.k..f = k; theorem :: FINSEQ_6:49 p1 <> p2 implies <*p1,p2*>-:p2 = <*p1,p2*>; theorem :: FINSEQ_6:50 p1 <> p2 implies <*p1,p2,p3*>-:p2 = <*p1,p2*>; theorem :: FINSEQ_6:51 p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>-:p3 = <*p1,p2,p3*>; theorem :: FINSEQ_6:52 <*p*>:-p = <*p*> & <*p*>-:p = <*p*>; theorem :: FINSEQ_6:53 p1 <> p2 implies <*p1,p2*>:-p2 = <*p2*>; theorem :: FINSEQ_6:54 p1 <> p2 implies <*p1,p2,p3*>:-p2 = <*p2,p3*>; theorem :: FINSEQ_6:55 p1 <> p3 & p2 <> p3 implies <*p1,p2,p3*>:-p3 = <*p3*>; theorem :: FINSEQ_6:56 p in rng f & p..f > k implies p..f = k + p..(f/^k); theorem :: FINSEQ_6:57 p in rng f & p..f > k implies p in rng(f/^k); theorem :: FINSEQ_6:58 k < i & i in dom f implies f/.i in rng(f/^k); theorem :: FINSEQ_6:59 p in rng f & p..f > k implies (f/^k)-:p = (f-:p)/^k; theorem :: FINSEQ_6:60 p in rng f & p..f <> 1 implies (f/^1)-:p = (f-:p)/^1; theorem :: FINSEQ_6:61 p in rng(f:-p); theorem :: FINSEQ_6:62 x in rng f & p in rng f & x..f >= p..f implies x in rng(f:-p); theorem :: FINSEQ_6:63 p in rng f & k <= len f & k >= p..f implies f/.k in rng(f:-p); theorem :: FINSEQ_6:64 p in rng f1 implies (f1^f2):-p = (f1:-p)^f2; theorem :: FINSEQ_6:65 p in rng f2 \ rng f1 implies (f1^f2):-p = f2:-p; theorem :: FINSEQ_6:66 p in rng f1 implies (f1^f2)-:p = f1-:p; theorem :: FINSEQ_6:67 p in rng f2 \ rng f1 implies (f1^f2)-:p = f1^(f2-:p); theorem :: FINSEQ_6:68 f:-p:-p = f:-p; theorem :: FINSEQ_6:69 p1 in rng f & p2 in rng f \ rng(f-:p1) implies f|--p2 = f|--p1 |--p2; theorem :: FINSEQ_6:70 p in rng f implies rng f = rng(f-:p) \/ rng(f:-p); theorem :: FINSEQ_6:71 p1 in rng f & p2 in rng f \ rng(f-:p1) implies f:-p1:-p2 = f:-p2; theorem :: FINSEQ_6:72 p in rng f implies p..(f-:p) = p..f; theorem :: FINSEQ_6:73 f|i|i = f|i; theorem :: FINSEQ_6:74 p in rng f implies f-:p-:p = f-:p; theorem :: FINSEQ_6:75 p1 in rng f & p2 in rng(f-:p1) implies f-:p1-:p2 = f-:p2; theorem :: FINSEQ_6:76 p in rng f implies (f-:p)^((f:-p)/^1) = f; theorem :: FINSEQ_6:77 f1 <> {} implies (f1^f2)/^1 = (f1/^1)^f2; theorem :: FINSEQ_6:78 p2 in rng f & p2..f <> 1 implies p2 in rng(f/^1); theorem :: FINSEQ_6:79 p..(f:-p) = 1; theorem :: FINSEQ_6:80 <*>D/^k = <*>D; theorem :: FINSEQ_6:81 f/^(i+k) = f/^i/^k; theorem :: FINSEQ_6:82 p in rng f & p..f > k implies (f/^k):-p = f:-p; theorem :: FINSEQ_6:83 p in rng f & p..f <> 1 implies (f/^1):-p = f:-p; theorem :: FINSEQ_6:84 i + k = len f implies Rev(f/^k) = Rev f|i; theorem :: FINSEQ_6:85 i + k = len f implies Rev(f|k) = Rev f/^i; theorem :: FINSEQ_6:86 f just_once_values p implies Rev(f|--p) = Rev f -|p; theorem :: FINSEQ_6:87 f just_once_values p implies Rev(f:-p) = Rev f -:p; theorem :: FINSEQ_6:88 f just_once_values p implies Rev(f-:p) = Rev f :-p; begin :: rotation, circular definition let D be non empty set; let IT be FinSequence of D; attr IT is circular means :: FINSEQ_6:def 1 IT/.1 = IT/.len IT; end; definition let D,f,p; func Rotate(f,p) -> FinSequence of D equals :: FINSEQ_6:def 2 (f:-p)^((f-:p)/^1) if p in rng f otherwise f; end; registration let D; let f be non empty FinSequence of D, p be Element of D; cluster Rotate(f,p) -> non empty; end; registration let D; cluster circular 1-element for FinSequence of D; cluster circular non trivial for FinSequence of D; end; theorem :: FINSEQ_6:89 Rotate(f,f/.1) = f; registration let D,p; let f be circular non empty FinSequence of D; cluster Rotate(f,p) -> circular; end; theorem :: FINSEQ_6:90 f is circular & p in rng f implies rng Rotate(f,p) = rng f; theorem :: FINSEQ_6:91 p in rng f implies p in rng Rotate(f,p); theorem :: FINSEQ_6:92 p in rng f implies (Rotate(f,p))/.1 = p; theorem :: FINSEQ_6:93 Rotate(Rotate(f,p),p) = Rotate(f,p); theorem :: FINSEQ_6:94 Rotate(<*p*>,p) = <*p*>; theorem :: FINSEQ_6:95 Rotate(<*p1,p2*>,p1) = <*p1,p2*>; theorem :: FINSEQ_6:96 Rotate(<*p1,p2*>,p2) = <*p2,p2*>; theorem :: FINSEQ_6:97 Rotate(<*p1,p2,p3*>,p1) = <*p1,p2,p3*>; theorem :: FINSEQ_6:98 p1 <> p2 implies Rotate(<*p1,p2,p3*>,p2) = <*p2,p3,p2*>; theorem :: FINSEQ_6:99 p2 <> p3 implies Rotate(<*p1,p2,p3*>,p3) = <*p3,p2,p3*>; theorem :: FINSEQ_6:100 for f being circular non trivial FinSequence of D holds rng(f/^1) = rng f; theorem :: FINSEQ_6:101 rng(f/^1) c= rng Rotate(f,p); theorem :: FINSEQ_6:102 p2 in rng f \ rng(f-:p1) implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2); theorem :: FINSEQ_6:103 p2..f <> 1 & p2 in rng f \ rng(f:-p1) implies Rotate(Rotate(f, p1),p2) = Rotate(f,p2); theorem :: FINSEQ_6:104 p2 in rng(f/^1) & f just_once_values p2 implies Rotate(Rotate(f ,p1),p2) = Rotate(f,p2); theorem :: FINSEQ_6:105 f is circular & f just_once_values p2 implies Rotate(Rotate(f,p1),p2) = Rotate(f,p2); theorem :: FINSEQ_6:106 f is circular & f just_once_values p implies Rev Rotate(f,p) = Rotate( Rev f,p); begin :: Addenda :: from AMISTD_1, 2007.07.26, A.T. theorem :: FINSEQ_6:107 for f being trivial FinSequence of D holds f is empty or ex x being Element of D st f = <*x*>; begin :: from JORDAN3, 2010.02.25, A.T. reserve D for non empty set; theorem :: FINSEQ_6:108 for i be Nat for p,q being FinSequence st len p).1=f.1 & (f^<*x*>).1=f/.1 & (<*x*>^f).(len f +1)=f.len f & (<*x*>^f).(len f +1)=f/.len f; theorem :: FINSEQ_6:110 for f being FinSequence st len f=1 holds Rev f=f; theorem :: FINSEQ_6:111 for f being FinSequence of D,k being Nat holds len (f/^k)=len f-'k; definition let f be FinSequence,k1,k2 be Nat; func mid(f,k1,k2) -> FinSequence equals :: FINSEQ_6:def 3 (f/^(k1-'1))|(k2-'k1+1) if k1<=k2 otherwise Rev ((f/^(k2-'1))|(k1-'k2+1)); end; definition let D; let f be FinSequence of D,k1,k2 be Nat; redefine func mid(f,k1,k2) -> FinSequence of D; end; ::$CT theorem :: FINSEQ_6:113 for f being FinSequence of D,k1,k2 being Nat st 1<=k1 & k1<=len f & 1<=k2 & k2<=len f holds Rev mid(f,k1,k2)=mid(Rev f,len f-'k2+1, len f-'k1+1); theorem :: FINSEQ_6:114 for n,m being Nat,f being FinSequence st 1<= m & m+n<=len f holds (f/^n).m=f.(m+n); theorem :: FINSEQ_6:115 for i being Nat, f being FinSequence st 1<=i & i<=len f holds (Rev f).i=f.(len f -i+1); theorem :: FINSEQ_6:116 for f being FinSequence, k being Nat st 1<=k holds mid(f,1,k)=f|k; theorem :: FINSEQ_6:117 for f being FinSequence,k being Nat st k<=len f holds mid(f,k,len f)=f/^(k-'1); theorem :: FINSEQ_6:118 for f being FinSequence,k1,k2 being Nat st 1<=k1 & k1<=len f & 1<=k2 & k2<=len f holds mid(f,k1,k2).1=f.k1 & (k1<=k2 implies len mid(f,k1,k2) = k2 -' k1 +1 & for i being Nat st 1<=i & i<=len mid(f,k1,k2) holds mid(f,k1,k2).i=f.(i+k1-'1)) & (k1>k2 implies len mid(f,k1,k2) = k1 -' k2 +1 & for i being Nat st 1<=i & i<=len mid(f,k1,k2) holds mid(f,k1,k2).i=f.(k1-'i+1)); theorem :: FINSEQ_6:119 for f being FinSequence,k1,k2 being Nat holds rng mid(f,k1,k2) c= rng f; theorem :: FINSEQ_6:120 for f being FinSequence st 1<=len f holds mid(f,1,len f)=f; theorem :: FINSEQ_6:121 for f being FinSequence of D st 1<=len f holds mid(f,len f,1)=Rev f; theorem :: FINSEQ_6:122 for f being FinSequence, k1,k2,i being Nat st 1 <=k1 & k1<=k2 & k2<=len f & 1<=i & (i<=k2-'k1+1 or i<=k2-k1+1 or i<=k2+1-k1) holds mid(f,k1,k2).i=f.(i+k1-'1) & mid(f,k1,k2).i=f.(i-'1+k1) & mid(f,k1,k2).i= f.(i+k1-1) & mid(f,k1,k2).i=f.(i-1+k1); theorem :: FINSEQ_6:123 for f being FinSequence,k,i being Nat st 1<=i & i<=k & k<=len f holds mid(f,1,k).i=f.i; theorem :: FINSEQ_6:124 for f being FinSequence, k1,k2 being Nat holds len mid(f,k1,k2)<=len f; theorem :: FINSEQ_6:125 for f being FinSequence, k being Nat, p being set holds (<*p*>^f)|(k+1) = <*p*>^(f|k); theorem :: FINSEQ_6:126 for p being FinSequence, k1,k2 being Nat st k1 < k2 & k1 in dom p holds mid(p,k1,k2) = <*p.k1*> ^ mid(p,k1+1,k2); begin :: from GRAPH_2, 2018.04.10 reserve p, q for FinSequence, X, Y, x, y for set, D for non empty set, i, j, k, l, m, n, r for Nat; theorem :: FINSEQ_6:127 for m,k,n being Nat holds m+1<=k & k<=n iff ex i being Nat st m<=i & i FinSequence means :: FINSEQ_6:def 4 len it +m = n+1 & for i being Nat st i; theorem :: FINSEQ_6:133 (1, len p)-cut p = p; theorem :: FINSEQ_6:134 m<=n & n<=r & r<=len p implies (m+1, n)-cut p ^ (n+1, r)-cut p = (m+1, r)-cut p; theorem :: FINSEQ_6:135 m<=len p implies (1, m)-cut p ^ (m+1, len p)-cut p = p; theorem :: FINSEQ_6:136 m<=n & n<=len p implies (1, m)-cut p ^ (m+1, n)-cut p ^ (n+1, len p) -cut p = p; theorem :: FINSEQ_6:137 rng ((m,n)-cut p) c= rng p; definition let D be set, p be FinSequence of D, m, n be Nat; redefine func (m, n)-cut p -> FinSequence of D; end; theorem :: FINSEQ_6:138 1<=m & m<=n & n<=len p implies ((m,n)-cut p).1 = p.m & ((m,n) -cut p).len ((m,n)-cut p)=p.n; begin :: The glueing catenation definition let p, q be FinSequence; func p ^' q -> FinSequence equals :: FINSEQ_6:def 5 p^(2, len q)-cut q; end; theorem :: FINSEQ_6:139 q<>{} implies len (p^'q) +1 = len p + len q; theorem :: FINSEQ_6:140 1<=k & k<=len p implies (p^'q).k=p.k; theorem :: FINSEQ_6:141 1<=k & k FinSequence of D; end; theorem :: FINSEQ_6:144 p<>{} & q<>{} & p.len p = q.1 implies rng (p^'q) = rng p \/ rng q; begin :: Two valued alternating finsequences definition let f be FinSequence; attr f is TwoValued means :: FINSEQ_6:def 6 card rng f = 2; end; theorem :: FINSEQ_6:145 p is TwoValued iff len p >1 & ex x,y being object st x<>y & rng p = {x, y}; definition let f be FinSequence; attr f is Alternating means :: FINSEQ_6:def 7 for i being Nat st 1<=i & (i+1)<=len f holds f.i <> f.(i+1); end; registration cluster TwoValued Alternating for FinSequence; end; reserve a, a1, a2 for TwoValued Alternating FinSequence; theorem :: FINSEQ_6:146 len a1 = len a2 & rng a1 = rng a2 & a1.1 = a2.1 implies a1 = a2; theorem :: FINSEQ_6:147 a1<>a2 & len a1 = len a2 & rng a1 = rng a2 implies for i st 1<=i & i<=len a1 holds a1.i<>a2.i; theorem :: FINSEQ_6:148 a1<>a2 & len a1 = len a2 & rng a1 = rng a2 implies for a st len a=len a1 & rng a=rng a1 holds a=a1 or a=a2; theorem :: FINSEQ_6:149 X <> Y & n > 1 implies ex a1 st rng a1 = {X, Y} & len a1 = n & a1.1 = X; begin :: Finite subsequences of finite sequences registration let X; let fs be FinSequence of X; cluster -> FinSubsequence-like for Subset of fs; end; theorem :: FINSEQ_6:150 for f being FinSubsequence, g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg=f*g & fh=f*h & fgh=f*(g^h) holds fgh = fg^fh; reserve fs, fs1, fs2 for FinSequence of X, fss, fss2 for Subset of fs; theorem :: FINSEQ_6:151 dom fss c= dom fs & rng fss c= rng fs; theorem :: FINSEQ_6:152 fs is Subset of fs; theorem :: FINSEQ_6:153 fss|Y is Subset of fs; theorem :: FINSEQ_6:154 for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss|rng((Sgm dom fss)|dom fss1) holds Seq fss2 = fs2; begin :: Addenda :: from AMISTD_1, 2006.01.12, A.T. theorem :: FINSEQ_6:155 for f1 being non empty FinSequence of D, f2 being FinSequence of D holds (f1^'f2)/.1 = f1/.1; theorem :: FINSEQ_6:156 for f1 being FinSequence of D, f2 being non trivial FinSequence of D holds (f1^'f2)/.len(f1^'f2) = f2/.len f2; theorem :: FINSEQ_6:157 for f being FinSequence holds f^'{} = f; theorem :: FINSEQ_6:158 for f being FinSequence holds f^'<*x*> = f; theorem :: FINSEQ_6:159 :: GRAPH_2:14 for f1, f2 being FinSequence of D holds 1<=n & n<=len f1 implies (f1^' f2)/.n = f1/.n; theorem :: FINSEQ_6:160 :: GRAPH_2:15 for f1, f2 being FinSequence of D holds 1<=n & n Nat means :: FINSEQ_6:def 8 ex X being finite non empty Subset of INT st X = rng ((m,n)-cut F) & it+1 = (min X)..(m,n)-cut F +m; end; reserve F, F1 for FinSequence of INT, k, m, n, ma for Nat; theorem :: FINSEQ_6:161 1 <= m & m <= n & n <= len F implies (ma = min_at(F, m, n) iff m <= ma & ma <= n & (for i being Nat st m <= i & i <= n holds F.ma <= F.i) & for i being Nat st m <= i & i < ma holds F.ma < F.i); theorem :: FINSEQ_6:162 1 <= m & m <= len F implies min_at(F, m, m) = m; definition let F be FinSequence of INT, m, n be Nat; pred F is_non_decreasing_on m, n means :: FINSEQ_6:def 9 for i, j being Nat st m <= i & i <= j & j <= n holds F.i <= F.j; end; definition let F be FinSequence of INT, n be Nat; pred F is_split_at n means :: FINSEQ_6:def 10 for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds F.i <= F.j; end; theorem :: FINSEQ_6:163 k+1 <= len F & ma = min_at(F, k+1, len F) & F is_split_at k & F is_non_decreasing_on 1, k & F1 = F+*(k+1, F.ma)+*(ma, F.(k+1)) implies F1 is_non_decreasing_on 1, k+1; theorem :: FINSEQ_6:164 k+1 <= len F & ma = min_at(F, k+1, len F) & F is_split_at k & F1 = F+* (k+1, F.ma)+*(ma, F.(k+1)) implies F1 is_split_at k+1; :: from SCPISORT, 2011.02.13 theorem :: FINSEQ_6:165 for f being FinSequence of INT,m,n be Nat st m >= n holds f is_non_decreasing_on m,n; begin :: from REVROT_1 reserve i,j,k,m,n for Nat, D for non empty set, p for Element of D, f for FinSequence of D; definition let D be non empty set; let f be FinSequence of D; redefine attr f is constant means :: FINSEQ_6:def 11 for n,m st n in dom f & m in dom f holds f/.n=f/.m; end; theorem :: FINSEQ_6:166 for D being non empty set, f being FinSequence of D st f just_once_values f/.len f holds f/.len f..f = len f; theorem :: FINSEQ_6:167 for D being non empty set, f being FinSequence of D holds f /^ len f = {}; theorem :: FINSEQ_6:168 for D being non empty set, f being non empty FinSequence of D holds f/.len f in rng f; definition let D be non empty set, f be FinSequence of D, y be set; redefine pred f just_once_values y means :: FINSEQ_6:def 12 ex x being set st x in dom f & y = f/.x & for z being set st z in dom f & z <> x holds f/.z <> y; end; theorem :: FINSEQ_6:169 for D being non empty set, f being FinSequence of D st f just_once_values f/.len f holds f-:f/.len f = f; theorem :: FINSEQ_6:170 for D being non empty set, f being FinSequence of D st f just_once_values f/.len f holds f:-f/.len f = <*f/.len f*>; theorem :: FINSEQ_6:171 1 <= len (f:-p); theorem :: FINSEQ_6:172 for D being non empty set, p being Element of D, f being FinSequence of D st p in rng f holds len(f:-p) <= len f; theorem :: FINSEQ_6:173 for D being non empty set, f being circular non empty FinSequence of D holds Rev f is circular; begin :: About Rotation reserve D for non empty set, p for Element of D, f for FinSequence of D; theorem :: FINSEQ_6:174 p in rng f & 1 <= i & i <= len(f:-p) implies (Rotate(f,p))/.i = f /.(i -' 1 + p..f); theorem :: FINSEQ_6:175 p in rng f & p..f <= i & i <= len f implies f/.i = (Rotate(f,p)) /.(i+1 -' p..f); theorem :: FINSEQ_6:176 p in rng f implies (Rotate(f,p))/.len(f:-p) = f/.len f; theorem :: FINSEQ_6:177 p in rng f & len(f:-p) < i & i <= len f implies (Rotate(f,p))/.i = f/.(i + p..f -' len f); theorem :: FINSEQ_6:178 p in rng f & 1 < i & i <= p..f implies f/.i = (Rotate(f,p))/.(i + len f -' p..f); theorem :: FINSEQ_6:179 len Rotate(f,p) = len f; theorem :: FINSEQ_6:180 dom Rotate(f,p) = dom f; theorem :: FINSEQ_6:181 for D being non empty set, f being circular FinSequence of D, p be Element of D st for i st 1 < i & i < len f holds f/.i <> f/.1 holds Rotate( Rotate(f,p),f/.1) = f; begin :: Rotating circular reserve f for circular FinSequence of D; theorem :: FINSEQ_6:182 p in rng f & len(f:-p) <= i & i <= len f implies (Rotate(f,p))/. i = f/.(i + p..f -' len f); theorem :: FINSEQ_6:183 p in rng f & 1 <= i & i <= p..f implies f/.i = (Rotate(f,p))/.(i + len f -' p..f); registration let D be non trivial set; cluster non constant circular for FinSequence of D; end; registration let D be non trivial set, p be Element of D; let f be non constant circular FinSequence of D; cluster Rotate(f,p) -> non constant; end;