:: On the Decomposition of Finite Sequences :: by Andrzej Trybulec :: :: Received May 24, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users begin registration let x, y, z be set ; cluster<*x,y,z*> -> non trivial ; coherence not <*x,y,z*> is trivial proofend; end; registration let f be non empty FinSequence; cluster Rev f -> non empty ; coherence not Rev f is empty proofend; end; Lm1: for x, y being set holds rng <*x,y*> = {x,y} proofend; Lm2: for x, y, z being set holds rng <*x,y,z*> = {x,y,z} proofend; begin theorem Th1: :: FINSEQ_6:1 for X being set for i being Nat st X c= Seg i & 1 in X holds (Sgm X) . 1 = 1 proofend; theorem Th2: :: FINSEQ_6:2 for k being Nat for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds f . i <> f . k ) holds (f . k) .. f = k proofend; theorem Th3: :: FINSEQ_6:3 for p1, p2 being set holds <*p1,p2*> | (Seg 1) = <*p1*> proofend; theorem Th4: :: FINSEQ_6:4 for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 1) = <*p1*> proofend; theorem Th5: :: FINSEQ_6:5 for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 2) = <*p1,p2*> proofend; theorem Th6: :: FINSEQ_6:6 for f1, f2 being FinSequence for p being set st p in rng f1 holds p .. (f1 ^ f2) = p .. f1 proofend; theorem Th7: :: FINSEQ_6:7 for f2, f1 being FinSequence for p being set st p in (rng f2) \ (rng f1) holds p .. (f1 ^ f2) = (len f1) + (p .. f2) proofend; theorem Th8: :: FINSEQ_6:8 for f1, f2 being FinSequence for p being set st p in rng f1 holds (f1 ^ f2) |-- p = (f1 |-- p) ^ f2 proofend; theorem Th9: :: FINSEQ_6:9 for f2, f1 being FinSequence for p being set st p in (rng f2) \ (rng f1) holds (f1 ^ f2) |-- p = f2 |-- p proofend; theorem Th10: :: FINSEQ_6:10 for f1, f2 being FinSequence holds f1 c= f1 ^ f2 proofend; theorem :: FINSEQ_6:11 for f1, f2 being FinSequence for A being set st A c= dom f1 holds (f1 ^ f2) | A = f1 | A by Th10, GRFUNC_1:27; theorem Th12: :: FINSEQ_6:12 for f1, f2 being FinSequence for p being set st p in rng f1 holds (f1 ^ f2) -| p = f1 -| p proofend; registration let f1 be FinSequence; let i be Nat; clusterf1 | (Seg i) -> FinSequence-like ; coherence f1 | (Seg i) is FinSequence-like by FINSEQ_1:15; end; theorem Th13: :: FINSEQ_6:13 for f1, f2, f3 being FinSequence st f1 c= f2 holds f3 ^ f1 c= f3 ^ f2 proofend; theorem Th14: :: FINSEQ_6:14 for f1, f2 being FinSequence for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i)) proofend; theorem Th15: :: FINSEQ_6:15 for f2, f1 being FinSequence for p being set st p in (rng f2) \ (rng f1) holds (f1 ^ f2) -| p = f1 ^ (f2 -| p) proofend; theorem Th16: :: FINSEQ_6:16 for f1, f2 being FinSequence for p being set st f1 ^ f2 just_once_values p holds p in (rng f1) \+\ (rng f2) proofend; theorem :: FINSEQ_6:17 for f1, f2 being FinSequence for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds f1 just_once_values p proofend; theorem Th18: :: FINSEQ_6:18 for p being set holds p .. <*p*> = 1 proofend; theorem Th19: :: FINSEQ_6:19 for p1, p2 being set holds p1 .. <*p1,p2*> = 1 proofend; theorem Th20: :: FINSEQ_6:20 for p1, p2 being set st p1 <> p2 holds p2 .. <*p1,p2*> = 2 proofend; theorem Th21: :: FINSEQ_6:21 for p1, p2, p3 being set holds p1 .. <*p1,p2,p3*> = 1 proofend; theorem Th22: :: FINSEQ_6:22 for p1, p2, p3 being set st p1 <> p2 holds p2 .. <*p1,p2,p3*> = 2 proofend; theorem Th23: :: FINSEQ_6:23 for p1, p3, p2 being set st p1 <> p3 & p2 <> p3 holds p3 .. <*p1,p2,p3*> = 3 proofend; theorem Th24: :: FINSEQ_6:24 for p being set for f being FinSequence holds Rev (<*p*> ^ f) = (Rev f) ^ <*p*> proofend; theorem :: FINSEQ_6:25 for f being FinSequence holds Rev (Rev f) = f ; theorem Th26: :: FINSEQ_6:26 for x, y being set st x <> y holds <*x,y*> -| y = <*x*> proofend; theorem Th27: :: FINSEQ_6:27 for x, y, z being set st x <> y holds <*x,y,z*> -| y = <*x*> proofend; theorem Th28: :: FINSEQ_6:28 for x, z, y being set st x <> z & y <> z holds <*x,y,z*> -| z = <*x,y*> proofend; theorem :: FINSEQ_6:29 for x, y being set holds <*x,y*> |-- x = <*y*> proofend; theorem Th30: :: FINSEQ_6:30 for x, y, z being set st x <> y holds <*x,y,z*> |-- y = <*z*> proofend; theorem :: FINSEQ_6:31 for x, y, z being set holds <*x,y,z*> |-- x = <*y,z*> proofend; theorem Th32: :: FINSEQ_6:32 for z being set holds ( <*z*> |-- z = {} & <*z*> -| z = {} ) proofend; theorem Th33: :: FINSEQ_6:33 for x, y being set st x <> y holds <*x,y*> |-- y = {} proofend; theorem Th34: :: FINSEQ_6:34 for x, z, y being set st x <> z & y <> z holds <*x,y,z*> |-- z = {} proofend; theorem Th35: :: FINSEQ_6:35 for x, y being set for f being FinSequence st x in rng f & y in rng (f -| x) holds (f -| x) -| y = f -| y proofend; theorem Th36: :: FINSEQ_6:36 for x being set for f1, f2 being FinSequence st not x in rng f1 holds x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1 proofend; theorem Th37: :: FINSEQ_6:37 for x being set for f being FinSequence st f just_once_values x holds (x .. f) + (x .. (Rev f)) = (len f) + 1 proofend; theorem Th38: :: FINSEQ_6:38 for x being set for f being FinSequence st f just_once_values x holds Rev (f -| x) = (Rev f) |-- x proofend; theorem :: FINSEQ_6:39 for x being set for f being FinSequence st f just_once_values x holds Rev f just_once_values x proofend; begin theorem Th40: :: FINSEQ_6:40 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds f -: p = (f -| p) ^ <*p*> proofend; theorem Th41: :: FINSEQ_6:41 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds f :- p = <*p*> ^ (f |-- p) proofend; theorem Th42: :: FINSEQ_6:42 for D being non empty set for f being FinSequence of D st f <> {} holds f /. 1 in rng f proofend; theorem Th43: :: FINSEQ_6:43 for D being non empty set for f being FinSequence of D st f <> {} holds (f /. 1) .. f = 1 proofend; theorem Th44: :: FINSEQ_6:44 for D being non empty set for p being Element of D for f being FinSequence of D st f <> {} & f /. 1 = p holds ( f -: p = <*p*> & f :- p = f ) proofend; theorem Th45: :: FINSEQ_6:45 for D being non empty set for p1 being Element of D for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f proofend; theorem Th46: :: FINSEQ_6:46 for D being non empty set for p1, p2 being Element of D holds <*p1,p2*> /^ 1 = <*p2*> proofend; theorem Th47: :: FINSEQ_6:47 for D being non empty set for p1, p2, p3 being Element of D holds <*p1,p2,p3*> /^ 1 = <*p2,p3*> proofend; theorem Th48: :: FINSEQ_6:48 for k being Nat for D being non empty set for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds f /. i <> f /. k ) holds (f /. k) .. f = k proofend; theorem Th49: :: FINSEQ_6:49 for D being non empty set for p1, p2 being Element of D st p1 <> p2 holds <*p1,p2*> -: p2 = <*p1,p2*> proofend; theorem Th50: :: FINSEQ_6:50 for D being non empty set for p1, p2, p3 being Element of D st p1 <> p2 holds <*p1,p2,p3*> -: p2 = <*p1,p2*> proofend; theorem Th51: :: FINSEQ_6:51 for D being non empty set for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds <*p1,p2,p3*> -: p3 = <*p1,p2,p3*> proofend; theorem :: FINSEQ_6:52 for D being non empty set for p being Element of D holds ( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> ) proofend; theorem Th53: :: FINSEQ_6:53 for D being non empty set for p1, p2 being Element of D st p1 <> p2 holds <*p1,p2*> :- p2 = <*p2*> proofend; theorem Th54: :: FINSEQ_6:54 for D being non empty set for p1, p2, p3 being Element of D st p1 <> p2 holds <*p1,p2,p3*> :- p2 = <*p2,p3*> proofend; theorem Th55: :: FINSEQ_6:55 for D being non empty set for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds <*p1,p2,p3*> :- p3 = <*p3*> proofend; theorem Th56: :: FINSEQ_6:56 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p .. f = k + (p .. (f /^ k)) proofend; theorem Th57: :: FINSEQ_6:57 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds p in rng (f /^ k) proofend; theorem Th58: :: FINSEQ_6:58 for k, i being Nat for D being non empty set for f being FinSequence of D st k < i & i in dom f holds f /. i in rng (f /^ k) proofend; theorem Th59: :: FINSEQ_6:59 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) -: p = (f -: p) /^ k proofend; theorem Th60: :: FINSEQ_6:60 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) -: p = (f -: p) /^ 1 proofend; theorem Th61: :: FINSEQ_6:61 for D being non empty set for p being Element of D for f being FinSequence of D holds p in rng (f :- p) proofend; theorem Th62: :: FINSEQ_6:62 for x being set for D being non empty set for p being Element of D for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds x in rng (f :- p) proofend; theorem Th63: :: FINSEQ_6:63 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds f /. k in rng (f :- p) proofend; theorem Th64: :: FINSEQ_6:64 for D being non empty set for p being Element of D for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) :- p = (f1 :- p) ^ f2 proofend; theorem Th65: :: FINSEQ_6:65 for D being non empty set for p being Element of D for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) :- p = f2 :- p proofend; theorem Th66: :: FINSEQ_6:66 for D being non empty set for p being Element of D for f1, f2 being FinSequence of D st p in rng f1 holds (f1 ^ f2) -: p = f1 -: p proofend; theorem Th67: :: FINSEQ_6:67 for D being non empty set for p being Element of D for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds (f1 ^ f2) -: p = f1 ^ (f2 -: p) proofend; theorem :: FINSEQ_6:68 for D being non empty set for p being Element of D for f being FinSequence of D holds (f :- p) :- p = f :- p proofend; theorem Th69: :: FINSEQ_6:69 for D being non empty set for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds f |-- p2 = (f |-- p1) |-- p2 proofend; theorem Th70: :: FINSEQ_6:70 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds rng f = (rng (f -: p)) \/ (rng (f :- p)) proofend; theorem Th71: :: FINSEQ_6:71 for D being non empty set for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds (f :- p1) :- p2 = f :- p2 proofend; theorem Th72: :: FINSEQ_6:72 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds p .. (f -: p) = p .. f proofend; theorem Th73: :: FINSEQ_6:73 for i being Nat for D being non empty set for f being FinSequence of D holds (f | i) | i = f | i proofend; theorem Th74: :: FINSEQ_6:74 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) -: p = f -: p proofend; theorem Th75: :: FINSEQ_6:75 for D being non empty set for p1, p2 being Element of D for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds (f -: p1) -: p2 = f -: p2 proofend; theorem Th76: :: FINSEQ_6:76 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (f -: p) ^ ((f :- p) /^ 1) = f proofend; theorem Th77: :: FINSEQ_6:77 for D being non empty set for f1, f2 being FinSequence of D st f1 <> {} holds (f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2 proofend; theorem Th78: :: FINSEQ_6:78 for D being non empty set for p2 being Element of D for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds p2 in rng (f /^ 1) proofend; theorem Th79: :: FINSEQ_6:79 for D being non empty set for p being Element of D for f being FinSequence of D holds p .. (f :- p) = 1 proofend; Lm3: for i being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > i holds i + (p .. (f /^ i)) = p .. f proofend; theorem Th80: :: FINSEQ_6:80 for k being Nat for D being non empty set holds (<*> D) /^ k = <*> D proofend; theorem Th81: :: FINSEQ_6:81 for i, k being Nat for D being non empty set for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k proofend; theorem Th82: :: FINSEQ_6:82 for k being Nat for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f > k holds (f /^ k) :- p = f :- p proofend; theorem Th83: :: FINSEQ_6:83 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f & p .. f <> 1 holds (f /^ 1) :- p = f :- p proofend; theorem Th84: :: FINSEQ_6:84 for i, k being Nat for D being non empty set for f being FinSequence of D st i + k = len f holds Rev (f /^ k) = (Rev f) | i proofend; theorem Th85: :: FINSEQ_6:85 for i, k being Nat for D being non empty set for f being FinSequence of D st i + k = len f holds Rev (f | k) = (Rev f) /^ i proofend; theorem Th86: :: FINSEQ_6:86 for D being non empty set for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f |-- p) = (Rev f) -| p proofend; theorem Th87: :: FINSEQ_6:87 for D being non empty set for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f :- p) = (Rev f) -: p proofend; theorem Th88: :: FINSEQ_6:88 for D being non empty set for p being Element of D for f being FinSequence of D st f just_once_values p holds Rev (f -: p) = (Rev f) :- p proofend; begin definition let D be non empty set ; let IT be FinSequence of D; attrIT is circular means :Def1: :: FINSEQ_6:def 1 IT /. 1 = IT /. (len IT); end; :: deftheorem Def1 defines circular FINSEQ_6:def_1_:_ for D being non empty set for IT being FinSequence of D holds ( IT is circular iff IT /. 1 = IT /. (len IT) ); definition let D be non empty set ; let f be FinSequence of D; let p be Element of D; func Rotate (f,p) -> FinSequence of D equals :Def2: :: FINSEQ_6:def 2 (f :- p) ^ ((f -: p) /^ 1) if p in rng f otherwise f; correctness coherence ( ( p in rng f implies (f :- p) ^ ((f -: p) /^ 1) is FinSequence of D ) & ( not p in rng f implies f is FinSequence of D ) ); consistency for b1 being FinSequence of D holds verum; ; end; :: deftheorem Def2 defines Rotate FINSEQ_6:def_2_:_ for D being non empty set for f being FinSequence of D for p being Element of D holds ( ( p in rng f implies Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) ) & ( not p in rng f implies Rotate (f,p) = f ) ); registration let D be non empty set ; let f be non empty FinSequence of D; let p be Element of D; cluster Rotate (f,p) -> non empty ; coherence not Rotate (f,p) is empty proofend; end; registration let D be non empty set ; cluster Relation-like NAT -defined D -valued Function-like V34() 1 -element FinSequence-like FinSubsequence-like circular for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is circular & b1 is 1 -element ) proofend; cluster non trivial Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like circular for FinSequence of D; existence ex b1 being FinSequence of D st ( b1 is circular & not b1 is trivial ) proofend; end; theorem Th89: :: FINSEQ_6:89 for D being non empty set for f being FinSequence of D holds Rotate (f,(f /. 1)) = f proofend; registration let D be non empty set ; let p be Element of D; let f be non empty circular FinSequence of D; cluster Rotate (f,p) -> circular ; coherence Rotate (f,p) is circular proofend; end; theorem :: FINSEQ_6:90 for D being non empty set for p being Element of D for f being FinSequence of D st f is circular & p in rng f holds rng (Rotate (f,p)) = rng f proofend; theorem Th91: :: FINSEQ_6:91 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds p in rng (Rotate (f,p)) proofend; theorem Th92: :: FINSEQ_6:92 for D being non empty set for p being Element of D for f being FinSequence of D st p in rng f holds (Rotate (f,p)) /. 1 = p proofend; theorem Th93: :: FINSEQ_6:93 for D being non empty set for p being Element of D for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p) proofend; theorem :: FINSEQ_6:94 for D being non empty set for p being Element of D holds Rotate (<*p*>,p) = <*p*> proofend; theorem Th95: :: FINSEQ_6:95 for D being non empty set for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p1) = <*p1,p2*> proofend; theorem :: FINSEQ_6:96 for D being non empty set for p1, p2 being Element of D holds Rotate (<*p1,p2*>,p2) = <*p2,p2*> proofend; theorem Th97: :: FINSEQ_6:97 for D being non empty set for p1, p2, p3 being Element of D holds Rotate (<*p1,p2,p3*>,p1) = <*p1,p2,p3*> proofend; theorem :: FINSEQ_6:98 for D being non empty set for p1, p2, p3 being Element of D st p1 <> p2 holds Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*> proofend; theorem :: FINSEQ_6:99 for D being non empty set for p2, p3, p1 being Element of D st p2 <> p3 holds Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> proofend; theorem :: FINSEQ_6:100 for D being non empty set for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f proofend; theorem Th101: :: FINSEQ_6:101 for D being non empty set for p being Element of D for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p)) proofend; theorem Th102: :: FINSEQ_6:102 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proofend; theorem Th103: :: FINSEQ_6:103 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proofend; theorem Th104: :: FINSEQ_6:104 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proofend; theorem :: FINSEQ_6:105 for D being non empty set for p2, p1 being Element of D for f being FinSequence of D st f is circular & f just_once_values p2 holds Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) proofend; theorem :: FINSEQ_6:106 for D being non empty set for p being Element of D for f being FinSequence of D st f is circular & f just_once_values p holds Rev (Rotate (f,p)) = Rotate ((Rev f),p) proofend; begin :: from AMISTD_1, 2007.07.26, A.T. theorem :: FINSEQ_6:107 for D being non empty set for f being trivial FinSequence of D holds ( f is empty or ex x being Element of D st f = <*x*> ) proofend; begin theorem :: FINSEQ_6:108 for i being Nat for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds (p ^ q) . i = q . (i - (len p)) proofend; theorem :: FINSEQ_6:109 for D being non empty set for x being set for f being FinSequence of D st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (f ^ <*x*>) . 1 = f /. 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) & (<*x*> ^ f) . ((len f) + 1) = f /. (len f) ) proofend; theorem Th110: :: FINSEQ_6:110 for f being FinSequence st len f = 1 holds Rev f = f proofend; theorem :: FINSEQ_6:111 for D being non empty set for f being FinSequence of D for k being Nat holds len (f /^ k) = (len f) -' k by RFINSEQ:29; theorem :: FINSEQ_6:112 for D being non empty set for f being FinSequence of D for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1 by FINSEQ_5:80; definition let f be FinSequence; let k1, k2 be Nat; func mid (f,k1,k2) -> FinSequence equals :Def3: :: FINSEQ_6:def 3 (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) if k1 <= k2 otherwise Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)); correctness coherence ( ( k1 <= k2 implies (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) is FinSequence ) & ( not k1 <= k2 implies Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) is FinSequence ) ); consistency for b1 being FinSequence holds verum; ; end; :: deftheorem Def3 defines mid FINSEQ_6:def_3_:_ for f being FinSequence for k1, k2 being Nat holds ( ( k1 <= k2 implies mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) ) & ( not k1 <= k2 implies mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) ) ); definition let D be non empty set ; let f be FinSequence of D; let k1, k2 be Nat; :: original:mid redefine func mid (f,k1,k2) -> FinSequence of D; coherence mid (f,k1,k2) is FinSequence of D proofend; end; theorem :: FINSEQ_6:113 for D being non empty set for f being FinSequence of D for k1, k2 being Element of 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)) proofend; theorem Th114: :: FINSEQ_6:114 for D being non empty set for n, m being Element of NAT for f being FinSequence of D st 1 <= m & m + n <= len f holds (f /^ n) . m = f . (m + n) proofend; theorem Th115: :: FINSEQ_6:115 for D being non empty set for i being Element of NAT for f being FinSequence of D st 1 <= i & i <= len f holds (Rev f) . i = f . (((len f) - i) + 1) proofend; theorem :: FINSEQ_6:116 for D being non empty set for f being FinSequence of D for k being Nat st 1 <= k holds mid (f,1,k) = f | k proofend; theorem :: FINSEQ_6:117 for D being non empty set for f being FinSequence of D for k being Element of NAT st k <= len f holds mid (f,k,(len f)) = f /^ (k -' 1) proofend; theorem Th118: :: FINSEQ_6:118 for D being non empty set for f being FinSequence of D for k1, k2 being Element of 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 Element of 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 Element of NAT st 1 <= i & i <= len (mid (f,k1,k2)) holds (mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) ) proofend; theorem :: FINSEQ_6:119 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT holds rng (mid (f,k1,k2)) c= rng f proofend; theorem :: FINSEQ_6:120 for D being non empty set for f being FinSequence of D st 1 <= len f holds mid (f,1,(len f)) = f proofend; theorem :: FINSEQ_6:121 for D being non empty set for f being FinSequence of D st 1 <= len f holds mid (f,(len f),1) = Rev f proofend; theorem Th122: :: FINSEQ_6:122 for D being non empty set for f being FinSequence of D for k1, k2, i being Element of 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) ) proofend; theorem :: FINSEQ_6:123 for D being non empty set for f being FinSequence of D for k, i being Nat st 1 <= i & i <= k & k <= len f holds (mid (f,1,k)) . i = f . i proofend; theorem :: FINSEQ_6:124 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f holds len (mid (f,k1,k2)) <= len f proofend; theorem Th125: :: FINSEQ_6:125 for D being non empty set for f being FinSequence of D for k being Element of NAT for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k) proofend; theorem :: FINSEQ_6:126 for D being non empty set for f being FinSequence of D for k1, k2 being Element of NAT st k1 < k2 & k1 in dom f holds mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2)) proofend;