List of theorems referencing the symbol SHIFTED_SEQ
(375) Theorem 324: [Double shifting can be emulated by a single shift] ((M in Za) & (N in Za)) •imp (shifted_seq(shifted_seq(F,M),N) = shifted_seq(F,M •PLUS N))
(377) Theorem 326: [Shift-by-0 is the identity map on sequences] (Is_map(F) & (domain(F) •incin Za)) •imp (shifted_seq(F,0) = F)
(378) Theorem 327: [Form of a shifted sequence] ((M in Za) & (domain(F) •incin Za)) •imp (shifted_seq(F,M) = {[car(x) •MINUS M,cdr(x)]: x in F | car(x) incs M})
(380) Theorem 329: ((F in Fin_seqs(S)) & (M in Za)) •imp (((F •ON M) in Fin_seqs(S)) & (shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) = (#F •MINUS M)))
(384) Theorem 333: [Concatenation of shifted sequences] ((F in Fin_seqs(S)) & (M in domain(F))) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (F = concat((F •ON M), shifted_seq(F,M))))
(390) Theorem 335: (M in Za) •imp (shifted_seq(F,M) in Subseqs(F))
(391) Theorem 336: ((F in Fin_seqs(S)) & (M in Za)) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) in next(domain(F))))
(392) Theorem 337: ((domain(F) = Za) & (M in Za)) •imp (domain(shifted_seq(F,M)) = Za)
(679) Theorem 528: ((F in RaSeq) & (N in Za) & (I in Za)) •imp ((shifted_seq(F,N)~[I]) = (F~[N •PLUS I]))
(698) Theorem 547: ((F in RaSeq) & (M = arb({h in Za | (FORALL i in (Za - h) | (F~[i]) /= Ra_0)}))) •imp (Ras_Recip(F) = Ras_Recip(shifted_seq(F,M)))
(699) Theorem 548: ((F in RaCauchy) & (M in Za)) •imp ((shifted_seq(F,M) in RaCauchy) & Ra_eqseq(F,shifted_seq(F,M)))
(731) Theorem 580: [All terms of a Cauchy sequence not equivalent to zero have the same sign beyond a certain point] ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS n in Za | shifted_seq(Ras_ABS(F),n) = if ((F~[n]) •Ra_GE Ra_0) then shifted_seq(F,n) else shifted_seq(Ras_Rev(F),n) end if)