P. 148 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14701-14800   *Has distinct variable group(s)

Type	Label	Description
Statement
5.7.11  Splicing words (substring replacement)
Syntax	csplice 14701	Syntax for the word splicing operator.
class splice
Definition	df-splice 14702*	Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by AV, 14-Oct-2022.)
⊢ splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)))
Theorem	splval 14703	Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by AV, 11-May-2020.) (Revised by AV, 15-Oct-2022.)
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))
Theorem	splcl 14704	Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) ∈ Word 𝐴)
Theorem	splid 14705	Splicing a subword for the same subword makes no difference. (Contributed by Stefan O'Rear, 20-Aug-2015.) (Proof shortened by AV, 14-Oct-2022.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(♯‘𝑆)))) → (𝑆 splice ⟨𝑋, 𝑌, (𝑆 substr ⟨𝑋, 𝑌⟩)⟩) = 𝑆)
Theorem	spllen 14706	The length of a splice. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝐴)    ⇒   ⊢ (𝜑 → (♯‘(𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)) = ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹))))
Theorem	splfv1 14707	Symbols to the left of a splice are unaffected. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ (0..^𝐹))    ⇒   ⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘𝑋) = (𝑆‘𝑋))
Theorem	splfv2a 14708	Symbols within the replacement region of a splice, expressed using the coordinates of the replacement region. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘𝑅)))    ⇒   ⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘(𝐹 + 𝑋)) = (𝑅‘𝑋))
Theorem	splval2 14709	Value of a splice, assuming the input word 𝑆 has already been decomposed into its pieces. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ Word 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ Word 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝑋)    &   ⊢ (𝜑 → 𝑆 = ((𝐴 ++ 𝐵) ++ 𝐶))    &   ⊢ (𝜑 → 𝐹 = (♯‘𝐴))    &   ⊢ (𝜑 → 𝑇 = (𝐹 + (♯‘𝐵)))    ⇒   ⊢ (𝜑 → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = ((𝐴 ++ 𝑅) ++ 𝐶))
5.7.12  Reversing words
Syntax	creverse 14710	Syntax for the word reverse operator.
class reverse
Definition	df-reverse 14711*	Define an operation which reverses the order of symbols in a word. This operation is also known as "word reversal" and "word mirroring". (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ reverse = (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(♯‘𝑠)) ↦ (𝑠‘(((♯‘𝑠) − 1) − 𝑥))))
Theorem	revval 14712*	Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ (𝑊 ∈ 𝑉 → (reverse‘𝑊) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ (𝑊‘(((♯‘𝑊) − 1) − 𝑥))))
Theorem	revcl 14713	The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴)
Theorem	revlen 14714	The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ (𝑊 ∈ Word 𝐴 → (♯‘(reverse‘𝑊)) = (♯‘𝑊))
Theorem	revfv 14715	Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘𝑋) = (𝑊‘(((♯‘𝑊) − 1) − 𝑋)))
Theorem	rev0 14716	The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ (reverse‘∅) = ∅
Theorem	revs1 14717	Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (reverse‘⟨“𝑆”⟩) = ⟨“𝑆”⟩
Theorem	revccat 14718	Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆)))
Theorem	revrev 14719	Reversal is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊)
5.7.13  Repeated symbol words
Syntax	creps 14720	Extend class notation with words consisting of one repeated symbol.
class repeatS
Definition	df-reps 14721*	Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018.)
⊢ repeatS = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
Theorem	reps 14722*	Construct a function mapping a half-open range of nonnegative integers to a constant. (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = (𝑥 ∈ (0..^𝑁) ↦ 𝑆))
Theorem	repsundef 14723	A function mapping a half-open range of nonnegative integers with an upper bound not being a nonnegative integer to a constant is the empty set (in the meaning of "undefined"). (Contributed by AV, 5-Nov-2018.)
⊢ (𝑁 ∉ ℕ0 → (𝑆 repeatS 𝑁) = ∅)
Theorem	repsconst 14724	Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 5738. (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = ((0..^𝑁) × {𝑆}))
Theorem	repsf 14725	The constructed function mapping a half-open range of nonnegative integers to a constant is a function. (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁):(0..^𝑁)⟶𝑉)
Theorem	repswsymb 14726	The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝐼) = 𝑆)
Theorem	repsw 14727	A function mapping a half-open range of nonnegative integers to a constant is a word consisting of one symbol repeated several times ("repeated symbol word"). (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) ∈ Word 𝑉)
Theorem	repswlen 14728	The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (♯‘(𝑆 repeatS 𝑁)) = 𝑁)
Theorem	repsw0 14729	The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅)
Theorem	repsdf2 14730*	Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆)))
Theorem	repswsymball 14731*	All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑊 = (𝑆 repeatS (♯‘𝑊)) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = 𝑆))
Theorem	repswsymballbi 14732*	A word is a "repeated symbol word" iff each of its symbols equals the first symbol of the word. (Contributed by AV, 10-Nov-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
Theorem	repswfsts 14733	The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁)‘0) = 𝑆)
Theorem	repswlsw 14734	The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (lastS‘(𝑆 repeatS 𝑁)) = 𝑆)
Theorem	repsw1 14735	The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 1) = ⟨“𝑆”⟩)
Theorem	repswswrd 14736	A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption 𝑁 ≤ 𝐿 is required, because otherwise (𝐿 < 𝑁): ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = ∅, but for M < N (𝑆 repeatS (𝑁 − 𝑀))) ≠ ∅! The proof is relatively long because the border cases (𝑀 = 𝑁, ¬ (𝑀..^𝑁) ⊆ (0..^𝐿) must have been considered. (Contributed by AV, 6-Nov-2018.)
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁 − 𝑀)))
Theorem	repswpfx 14737	A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿))
Theorem	repswccat 14738	The concatenation of two "repeated symbol words" with the same symbol is again a "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑆 repeatS 𝑁) ++ (𝑆 repeatS 𝑀)) = (𝑆 repeatS (𝑁 + 𝑀)))
Theorem	repswrevw 14739	The reverse of a "repeated symbol word". (Contributed by AV, 6-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (reverse‘(𝑆 repeatS 𝑁)) = (𝑆 repeatS 𝑁))
5.7.14  Cyclical shifts of words A word/string can be regarded as "necklace" by connecting the two ends of the word/string together (see Wikipedia "Necklace (combinatorics)", https://en.wikipedia.org/wiki/Necklace_(combinatorics)). Two strings are regarded as the same necklace if one string can be rotated/circularly shifted/cyclically shifted to obtain the second string. To cope with words in the sense of necklaces, the rotation/cyclic shift cyclShift is defined as the basic operation, see df-csh 14741. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 17038 for words consisting of identical symbols and cshwshash 17040 for words having lengths which are prime numbers.
Syntax	ccsh 14740	Extend class notation with Cyclical Shifts.
class cyclShift
Definition	df-csh 14741*	Perform a cyclical shift for an arbitrary class. Meaningful only for words 𝑤 ∈ Word 𝑆 or at least functions over half-open ranges of nonnegative integers. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by Mario Carneiro/Alexander van der Vekens/ Gerard Lang, 17-Nov-2018.) (Revised by AV, 4-Nov-2022.)
⊢ cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))
Theorem	cshfn 14742*	Perform a cyclical shift for a function over a half-open range of nonnegative integers. (Contributed by AV, 20-May-2018.) (Revised by AV, 17-Nov-2018.) (Revised by AV, 4-Nov-2022.)
⊢ ((𝑊 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))))
Theorem	cshword 14743	Perform a cyclical shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by AV, 12-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
Theorem	cshnz 14744	A cyclical shift is the empty set if the number of shifts is not an integer. (Contributed by Alexander van der Vekens, 21-May-2018.) (Revised by AV, 17-Nov-2018.)
⊢ (¬ 𝑁 ∈ ℤ → (𝑊 cyclShift 𝑁) = ∅)
Theorem	0csh0 14745	Cyclically shifting an empty set/word always results in the empty word/set. (Contributed by AV, 25-Oct-2018.) (Revised by AV, 17-Nov-2018.)
⊢ (∅ cyclShift 𝑁) = ∅
Theorem	cshw0 14746	A word cyclically shifted by 0 is the word itself. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 26-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 0) = 𝑊)
Theorem	cshwmodn 14747	Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018.) (Proof shortened by AV, 16-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (♯‘𝑊))))
Theorem	cshwsublen 14748	Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 − (♯‘𝑊))))
Theorem	cshwn 14749	A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 26-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift (♯‘𝑊)) = 𝑊)
Theorem	cshwcl 14750	A cyclically shifted word is a word over the same set as for the original word. (Contributed by AV, 16-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 27-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 𝑁) ∈ Word 𝑉)
Theorem	cshwlen 14751	The length of a cyclically shifted word is the same as the length of the original word. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 27-Oct-2018.) (Proof shortened by AV, 16-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (♯‘(𝑊 cyclShift 𝑁)) = (♯‘𝑊))
Theorem	cshwf 14752	A cyclically shifted word is a function from a half-open range of integers of the same length as the word as domain to the set of symbols for the word. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁):(0..^(♯‘𝑊))⟶𝐴)
Theorem	cshwfn 14753	A cyclically shifted word is a function with a half-open range of integers of the same length as the word as domain. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) Fn (0..^(♯‘𝑊)))
Theorem	cshwrn 14754	The range of a cyclically shifted word is a subset of the set of symbols for the word. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) ⊆ 𝑉)
Theorem	cshwidxmod 14755	The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 13-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) (Proof shortened by AV, 12-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
Theorem	cshwidxmodr 14756	The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 17-Mar-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((𝐼 − 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼))
Theorem	cshwidx0mod 14757	The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N (modulo the length of the word) of the original word. (Contributed by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘(𝑁 mod (♯‘𝑊))))
Theorem	cshwidx0 14758	The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N of the original word. (Contributed by AV, 15-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘𝑁))
Theorem	cshwidxm1 14759	The symbol at index ((n-N)-1) of a word of length n (not 0) cyclically shifted by N positions is the symbol at index (n-1) of the original word. (Contributed by AV, 23-Mar-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((♯‘𝑊) − 𝑁) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
Theorem	cshwidxm 14760	The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((♯‘𝑊) − 𝑁)) = (𝑊‘0))
Theorem	cshwidxn 14761	The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((♯‘𝑊) − 1)) = (𝑊‘(𝑁 − 1)))
Theorem	cshf1 14762	Cyclically shifting a word which contains a symbol at most once results in a word which contains a symbol at most once. (Contributed by AV, 14-Mar-2021.)
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))–1-1→𝐴)
Theorem	cshinj 14763	If a word is injectiv (regarded as function), the cyclically shifted word is also injective. (Contributed by AV, 14-Mar-2021.)
⊢ ((𝐹 ∈ Word 𝐴 ∧ Fun ◡𝐹 ∧ 𝑆 ∈ ℤ) → (𝐺 = (𝐹 cyclShift 𝑆) → Fun ◡𝐺))
Theorem	repswcshw 14764	A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018.) (Proof shortened by AV, 16-Oct-2022.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁))
Theorem	2cshw 14765	Cyclically shifting a word two times. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 4-Jun-2018.) (Revised by AV, 31-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁)))
Theorem	2cshwid 14766	Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift ((♯‘𝑊) − 𝑁)) = 𝑊)
Theorem	lswcshw 14767	The last symbol of a word cyclically shifted by N positions is the symbol at index (N-1) of the original word. (Contributed by AV, 21-Mar-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 cyclShift 𝑁)) = (𝑊‘(𝑁 − 1)))
Theorem	2cshwcom 14768	Cyclically shifting a word two times is commutative. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by Mario Carneiro/AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift 𝑀) = ((𝑊 cyclShift 𝑀) cyclShift 𝑁))
Theorem	cshwleneq 14769	If the results of cyclically shifting two words are equal, the length of the two words was equal. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (♯‘𝑊) = (♯‘𝑈))
Theorem	3cshw 14770	Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by AV, 6-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (((𝑊 cyclShift 𝑀) cyclShift 𝑁) cyclShift ((♯‘𝑊) − 𝑀)))
Theorem	cshweqdif2 14771	If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 6-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀) → (𝑈 cyclShift (𝑀 − 𝑁)) = 𝑊))
Theorem	cshweqdifid 14772	If cyclically shifting a word by two positions results in the same word, cyclically shifting the word by the difference of these two positions results in the original word itself. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑊 cyclShift 𝑁) = (𝑊 cyclShift 𝑀) → (𝑊 cyclShift (𝑀 − 𝑁)) = 𝑊))
Theorem	cshweqrep 14773*	If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ∀𝑗 ∈ ℕ0 (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊)))))
Theorem	cshw1 14774*	If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Proof shortened by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
Theorem	cshw1repsw 14775	If cyclically shifting a word by 1 position results in the word itself, the word is a "repeated symbol word". Remark: also "valid" for an empty word! (Contributed by AV, 8-Nov-2018.) (Proof shortened by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))
Theorem	cshwsexa 14776*	The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by AV, 8-Jun-2018.) (Revised by Mario Carneiro/AV, 25-Oct-2018.) (Proof shortened by SN, 15-Jan-2025.)
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
Theorem	cshwsexaOLD 14777*	Obsolete version of cshwsexa 14776 as of 15-Jan-2025. (Contributed by AV, 8-Jun-2018.) (Revised by Mario Carneiro/AV, 25-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
Theorem	2cshwcshw 14778*	If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018.) (Revised by AV, 12-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
Theorem	scshwfzeqfzo 14779*	For a nonempty word the sets of shifted words, expressd by a finite interval of integers or by a half-open integer range are identical. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (♯‘𝑋)) → {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛)})
Theorem	cshwcshid 14780*	A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlksym 29312 and erclwwlknsym 29361. (Contributed by AV, 8-Apr-2018.) (Revised by AV, 11-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
⊢ (𝜑 → 𝑦 ∈ Word 𝑉)    &   ⊢ (𝜑 → (♯‘𝑥) = (♯‘𝑦))    ⇒   ⊢ (𝜑 → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ∃𝑛 ∈ (0...(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)))
Theorem	cshwcsh2id 14781*	A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr 29313 and erclwwlkntr 29362. (Contributed by AV, 9-Apr-2018.) (Revised by AV, 11-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
⊢ (𝜑 → 𝑧 ∈ Word 𝑉)    &   ⊢ (𝜑 → ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)))    ⇒   ⊢ (𝜑 → (((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
Theorem	cshimadifsn 14782	The image of a cyclically shifted word under its domain without its left bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐽) “ (1..^𝑁)))
Theorem	cshimadifsn0 14783	The image of a cyclically shifted word under its domain without its upper bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
5.7.15  Mapping words by a function
Theorem	wrdco 14784	Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵)
Theorem	lenco 14785	Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊))
Theorem	s1co 14786	Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ ⟨“𝑆”⟩) = ⟨“(𝐹‘𝑆)”⟩)
Theorem	revco 14787	Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊)))
Theorem	ccatco 14788	Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)))
Theorem	cshco 14789	Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) = ((𝐹 ∘ 𝑊) cyclShift 𝑁))
Theorem	swrdco 14790	Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr ⟨𝑀, 𝑁⟩)) = ((𝐹 ∘ 𝑊) substr ⟨𝑀, 𝑁⟩))
Theorem	pfxco 14791	Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 prefix 𝑁)) = ((𝐹 ∘ 𝑊) prefix 𝑁))
Theorem	lswco 14792	Mapping of (nonempty) words commutes with the "last symbol" operation. This theorem would not hold if 𝑊 = ∅, (𝐹‘∅) ≠ ∅ and ∅ ∈ 𝐴, because then (lastS‘(𝐹 ∘ 𝑊)) = (lastS‘∅) = ∅ ≠ (𝐹‘∅) = (𝐹(lastS‘𝑊)). (Contributed by AV, 11-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ∧ 𝐹:𝐴⟶𝐵) → (lastS‘(𝐹 ∘ 𝑊)) = (𝐹‘(lastS‘𝑊)))
Theorem	repsco 14793	Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 repeatS 𝑁)) = ((𝐹‘𝑆) repeatS 𝑁))
5.7.16  Longer string literals
Syntax	cs2 14794	Syntax for the length 2 word constructor.
class ⟨“𝐴𝐵”⟩
Syntax	cs3 14795	Syntax for the length 3 word constructor.
class ⟨“𝐴𝐵𝐶”⟩
Syntax	cs4 14796	Syntax for the length 4 word constructor.
class ⟨“𝐴𝐵𝐶𝐷”⟩
Syntax	cs5 14797	Syntax for the length 5 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸”⟩
Syntax	cs6 14798	Syntax for the length 6 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩
Syntax	cs7 14799	Syntax for the length 7 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩
Syntax	cs8 14800	Syntax for the length 8 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩