Home | Metamath
Proof Explorer Theorem List (p. 136 of 426) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | swrdccatin12d 13501 | The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.) |
⊢ (𝜑 → (#‘𝐴) = 𝐿) & ⊢ (𝜑 → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) & ⊢ (𝜑 → 𝑀 ∈ (0...𝐿)) & ⊢ (𝜑 → 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) | ||
Theorem | splval 13502 | Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) | ||
Theorem | splcl 13503 | Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) ∈ Word 𝐴) | ||
Theorem | splid 13504 | Splicing a subword for the same subword makes no difference. (Contributed by Stefan O'Rear, 20-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(#‘𝑆)))) → (𝑆 splice 〈𝑋, 𝑌, (𝑆 substr 〈𝑋, 𝑌〉)〉) = 𝑆) | ||
Theorem | spllen 13505 | The length of a splice. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(#‘𝑆))) & ⊢ (𝜑 → 𝑅 ∈ Word 𝐴) ⇒ ⊢ (𝜑 → (#‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = ((#‘𝑆) + ((#‘𝑅) − (𝑇 − 𝐹)))) | ||
Theorem | splfv1 13506 | Symbols to the left of a splice are unaffected. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(#‘𝑆))) & ⊢ (𝜑 → 𝑅 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ (0..^𝐹)) ⇒ ⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘𝑋) = (𝑆‘𝑋)) | ||
Theorem | splfv2a 13507 | Symbols within the replacement region of a splice, expressed using the coordinates of the replacement region. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(#‘𝑆))) & ⊢ (𝜑 → 𝑅 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ (0..^(#‘𝑅))) ⇒ ⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘(𝐹 + 𝑋)) = (𝑅‘𝑋)) | ||
Theorem | splval2 13508 | Value of a splice, assuming the input word 𝑆 has already been decomposed into its pieces. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ (𝜑 → 𝐴 ∈ Word 𝑋) & ⊢ (𝜑 → 𝐵 ∈ Word 𝑋) & ⊢ (𝜑 → 𝐶 ∈ Word 𝑋) & ⊢ (𝜑 → 𝑅 ∈ Word 𝑋) & ⊢ (𝜑 → 𝑆 = ((𝐴 ++ 𝐵) ++ 𝐶)) & ⊢ (𝜑 → 𝐹 = (#‘𝐴)) & ⊢ (𝜑 → 𝑇 = (𝐹 + (#‘𝐵))) ⇒ ⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = ((𝐴 ++ 𝑅) ++ 𝐶)) | ||
Theorem | revval 13509* | Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ 𝑉 → (reverse‘𝑊) = (𝑥 ∈ (0..^(#‘𝑊)) ↦ (𝑊‘(((#‘𝑊) − 1) − 𝑥)))) | ||
Theorem | revcl 13510 | The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) | ||
Theorem | revlen 13511 | The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (#‘(reverse‘𝑊)) = (#‘𝑊)) | ||
Theorem | revfv 13512 | Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘𝑋) = (𝑊‘(((#‘𝑊) − 1) − 𝑋))) | ||
Theorem | rev0 13513 | The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (reverse‘∅) = ∅ | ||
Theorem | revs1 13514 | Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (reverse‘〈“𝑆”〉) = 〈“𝑆”〉 | ||
Theorem | revccat 13515 | Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆))) | ||
Theorem | revrev 13516 | Reversion is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊) | ||
Theorem | reps 13517* | 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 13518 | 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 13519 | Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 5163. (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = ((0..^𝑁) × {𝑆})) | ||
Theorem | repsf 13520 | 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 13521 | The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝐼) = 𝑆) | ||
Theorem | repsw 13522 | 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 13523 | The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (#‘(𝑆 repeatS 𝑁)) = 𝑁) | ||
Theorem | repsw0 13524 | The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅) | ||
Theorem | repsdf2 13525* | Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) | ||
Theorem | repswsymball 13526* | All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑊 = (𝑆 repeatS (#‘𝑊)) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = 𝑆)) | ||
Theorem | repswsymballbi 13527* | 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 13528 | The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁)‘0) = 𝑆) | ||
Theorem | repswlsw 13529 | The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ( lastS ‘(𝑆 repeatS 𝑁)) = 𝑆) | ||
Theorem | repsw1 13530 | The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 1) = 〈“𝑆”〉) | ||
Theorem | repswswrd 13531 | A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ): ((𝑆 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 | repswccat 13532 | 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 13533 | The reverse of a "repeated symbol word". (Contributed by AV, 6-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (reverse‘(𝑆 repeatS 𝑁)) = (𝑆 repeatS 𝑁)) | ||
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 13535. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 15809 for words consisting of identical symbols and cshwshash 15811 for words having lengths which are prime numbers. | ||
Syntax | ccsh 13534 | Extend class notation with Cyclical Shifts. |
class cyclShift | ||
Definition | df-csh 13535* | 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.) |
⊢ cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr 〈(𝑛 mod (#‘𝑤)), (#‘𝑤)〉) ++ (𝑤 substr 〈0, (𝑛 mod (#‘𝑤))〉)))) | ||
Theorem | cshfn 13536* | 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.) |
⊢ ((𝑊 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) | ||
Theorem | cshword 13537 | Perform a cyclical shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by AV, 17-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) | ||
Theorem | cshnz 13538 | 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 13539 | 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 13540 | 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 13541 | Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (#‘𝑊)))) | ||
Theorem | cshwsublen 13542 | Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 − (#‘𝑊)))) | ||
Theorem | cshwn 13543 | 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 13544 | 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 13545 | 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.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) | ||
Theorem | cshwf 13546 | 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 13547 | 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 13548 | 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 13549 | 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.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))) | ||
Theorem | cshwidxmodr 13550 | 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 13551 | 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 13552 | 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 13553 | 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 13554 | 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 13555 | 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 13556 | 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 13557 | 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 13558 | A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁)) | ||
Theorem | 2cshw 13559 | 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 13560 | 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 13561 | 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 13562 | 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 13563 | 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 13564 | 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 13565 | 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 13566 | 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 13567* | 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 13568* | 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 13569 | 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 13570* | 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.) |
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V | ||
Theorem | 2cshwcshw 13571* | 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 13572* | 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 13573* | A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlkssym 26935 and erclwwlksnsym 26947. (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 13574* | A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlkstr 26936 and erclwwlksntr 26948. (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 13575 | 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 13576 | 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)))) | ||
Theorem | wrdco 13577 | Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) | ||
Theorem | lenco 13578 | Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) | ||
Theorem | s1co 13579 | Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 〈“𝑆”〉) = 〈“(𝐹‘𝑆)”〉) | ||
Theorem | revco 13580 | Mapping of words commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊))) | ||
Theorem | ccatco 13581 | Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇))) | ||
Theorem | cshco 13582 | Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) = ((𝐹 ∘ 𝑊) cyclShift 𝑁)) | ||
Theorem | swrdco 13583 | Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) = ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)) | ||
Theorem | lswco 13584 | 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 13585 | Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 repeatS 𝑁)) = ((𝐹‘𝑆) repeatS 𝑁)) | ||
Syntax | cs2 13586 | Syntax for the length 2 word constructor. |
class 〈“𝐴𝐵”〉 | ||
Syntax | cs3 13587 | Syntax for the length 3 word constructor. |
class 〈“𝐴𝐵𝐶”〉 | ||
Syntax | cs4 13588 | Syntax for the length 4 word constructor. |
class 〈“𝐴𝐵𝐶𝐷”〉 | ||
Syntax | cs5 13589 | Syntax for the length 5 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸”〉 | ||
Syntax | cs6 13590 | Syntax for the length 6 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 | ||
Syntax | cs7 13591 | Syntax for the length 7 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 | ||
Syntax | cs8 13592 | Syntax for the length 8 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 | ||
Definition | df-s2 13593 | Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) | ||
Definition | df-s3 13594 | Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | ||
Definition | df-s4 13595 | Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) | ||
Definition | df-s5 13596 | Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸”〉) | ||
Definition | df-s6 13597 | Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹”〉) | ||
Definition | df-s7 13598 | Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ++ 〈“𝐺”〉) | ||
Definition | df-s8 13599 | Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ++ 〈“𝐻”〉) | ||
Theorem | cats1cld 13600 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑇 ∈ Word 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |