![]() |
Metamath
Proof Explorer Theorem List (p. 140 of 435) | < 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: | ![]() (1-28326) |
![]() (28327-29851) |
![]() (29852-43457) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | repsdf2 13901* | Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) | ||
Theorem | repswsymball 13902* | All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑊 = (𝑆 repeatS (♯‘𝑊)) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = 𝑆)) | ||
Theorem | repswsymballbi 13903* | 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 13904 | The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁)‘0) = 𝑆) | ||
Theorem | repswlsw 13905 | The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (lastS‘(𝑆 repeatS 𝑁)) = 𝑆) | ||
Theorem | repsw1 13906 | The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 1) = 〈“𝑆”〉) | ||
Theorem | repswswrd 13907 | 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 | repswpfx 13908 | 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 13909 | 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 13910 | 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 13913. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 16182 for words consisting of identical symbols and cshwshash 16184 for words having lengths which are prime numbers. | ||
Syntax | ccsh 13911 | Extend class notation with Cyclical Shifts. |
class cyclShift | ||
Syntax | ccshOLD 13912 | Obsolete version of ccsh 13911 as of 12-Oct-2022. (New usage is discouraged.) |
class cyclShiftOLD | ||
Definition | df-csh 13913* | 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 (♯‘𝑤)))))) | ||
Definition | df-cshOLD 13914* | Obsolete version of df-csh 13913 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by Mario Carneiro/ Alexander van der Vekens/Gerard Lang, 17-Nov-2018.) (New usage is discouraged.) |
⊢ cyclShiftOLD = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr 〈(𝑛 mod (♯‘𝑤)), (♯‘𝑤)〉) ++ (𝑤 substr 〈0, (𝑛 mod (♯‘𝑤))〉)))) | ||
Theorem | cshfn 13915* | 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 | cshfnOLD 13916* | Obsolete version of cshfn 13915 as of 12-Oct-2022. (Contributed by AV, 20-May-2018.) (Revised by AV, 17-Nov-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShiftOLD 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (♯‘𝑊))〉)))) | ||
Theorem | cshword 13917 | 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 13918 | 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 | cshnzOLD 13919 | Obsolete version of cshnz 13918 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 21-May-2018.) (Revised by AV, 17-Nov-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ 𝑁 ∈ ℤ → (𝑊 cyclShiftOLD 𝑁) = ∅) | ||
Theorem | 0csh0 13920 | 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 | 0csh0OLD 13921 | Obsolete version of cshnz 13918 as of 12-Oct-2022. (Contributed by AV, 25-Oct-2018.) (Revised by AV, 17-Nov-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∅ cyclShiftOLD 𝑁) = ∅ | ||
Theorem | cshw0 13922 | 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 13923 | 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 13924 | Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 − (♯‘𝑊)))) | ||
Theorem | cshwn 13925 | 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 13926 | 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 13927 | 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 13928 | 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 13929 | 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 13930 | 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 13931 | 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 13932 | 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 13933 | 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 13934 | 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 13935 | 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 13936 | 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 13937 | 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 13938 | 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 13939 | 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 13940 | 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 13941 | 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 13942 | 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 13943 | 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 13944 | 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 13945 | 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 13946 | 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 13947 | 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 13948 | 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 13949* | 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 13950* | 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 13951 | 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 13952* | 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 13953* | 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 13954* | 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 13955* | A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlksym 27366 and erclwwlknsym 27423. (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 13956* | A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr 27367 and erclwwlkntr 27424. (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 13957 | 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 13958 | 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 13959 | Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) | ||
Theorem | lenco 13960 | Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊)) | ||
Theorem | s1co 13961 | Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 〈“𝑆”〉) = 〈“(𝐹‘𝑆)”〉) | ||
Theorem | revco 13962 | Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊))) | ||
Theorem | ccatco 13963 | Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇))) | ||
Theorem | cshco 13964 | Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) = ((𝐹 ∘ 𝑊) cyclShift 𝑁)) | ||
Theorem | swrdco 13965 | Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) = ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)) | ||
Theorem | pfxco 13966 | Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 prefix 𝑁)) = ((𝐹 ∘ 𝑊) prefix 𝑁)) | ||
Theorem | lswco 13967 | 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 13968 | Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 repeatS 𝑁)) = ((𝐹‘𝑆) repeatS 𝑁)) | ||
Syntax | cs2 13969 | Syntax for the length 2 word constructor. |
class 〈“𝐴𝐵”〉 | ||
Syntax | cs3 13970 | Syntax for the length 3 word constructor. |
class 〈“𝐴𝐵𝐶”〉 | ||
Syntax | cs4 13971 | Syntax for the length 4 word constructor. |
class 〈“𝐴𝐵𝐶𝐷”〉 | ||
Syntax | cs5 13972 | Syntax for the length 5 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸”〉 | ||
Syntax | cs6 13973 | Syntax for the length 6 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 | ||
Syntax | cs7 13974 | Syntax for the length 7 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 | ||
Syntax | cs8 13975 | Syntax for the length 8 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 | ||
Definition | df-s2 13976 | Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) | ||
Definition | df-s3 13977 | Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | ||
Definition | df-s4 13978 | Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) | ||
Definition | df-s5 13979 | Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸”〉) | ||
Definition | df-s6 13980 | Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹”〉) | ||
Definition | df-s7 13981 | Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ++ 〈“𝐺”〉) | ||
Definition | df-s8 13982 | Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ++ 〈“𝐻”〉) | ||
Theorem | cats1cld 13983 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑇 ∈ Word 𝐴) | ||
Theorem | cats1co 13984 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ∘ 𝑆) = 𝑈) & ⊢ 𝑉 = (𝑈 ++ 〈“(𝐹‘𝑋)”〉) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝑇) = 𝑉) | ||
Theorem | cats1cli 13985 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V ⇒ ⊢ 𝑇 ∈ Word V | ||
Theorem | cats1fvn 13986 | The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (♯‘𝑆) = 𝑀 ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑇‘𝑀) = 𝑋) | ||
Theorem | cats1fv 13987 | A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (♯‘𝑆) = 𝑀 & ⊢ (𝑌 ∈ 𝑉 → (𝑆‘𝑁) = 𝑌) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑁 < 𝑀 ⇒ ⊢ (𝑌 ∈ 𝑉 → (𝑇‘𝑁) = 𝑌) | ||
Theorem | cats1len 13988 | The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (♯‘𝑆) = 𝑀 & ⊢ (𝑀 + 1) = 𝑁 ⇒ ⊢ (♯‘𝑇) = 𝑁 | ||
Theorem | cats1cat 13989 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝐴 ∈ Word V & ⊢ 𝑆 ∈ Word V & ⊢ 𝐶 = (𝐵 ++ 〈“𝑋”〉) & ⊢ 𝐵 = (𝐴 ++ 𝑆) ⇒ ⊢ 𝐶 = (𝐴 ++ 𝑇) | ||
Theorem | cats2cat 13990 | Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) |
⊢ 𝐵 ∈ Word V & ⊢ 𝐷 ∈ Word V & ⊢ 𝐴 = (𝐵 ++ 〈“𝑋”〉) & ⊢ 𝐶 = (〈“𝑌”〉 ++ 𝐷) ⇒ ⊢ (𝐴 ++ 𝐶) = ((𝐵 ++ 〈“𝑋𝑌”〉) ++ 𝐷) | ||
Theorem | s2eqd 13991 | Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵”〉 = 〈“𝑁𝑂”〉) | ||
Theorem | s3eqd 13992 | Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 = 〈“𝑁𝑂𝑃”〉) | ||
Theorem | s4eqd 13993 | Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉 = 〈“𝑁𝑂𝑃𝑄”〉) | ||
Theorem | s5eqd 13994 | Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸”〉 = 〈“𝑁𝑂𝑃𝑄𝑅”〉) | ||
Theorem | s6eqd 13995 | Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆”〉) | ||
Theorem | s7eqd 13996 | Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) & ⊢ (𝜑 → 𝐺 = 𝑇) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆𝑇”〉) | ||
Theorem | s8eqd 13997 | Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) & ⊢ (𝜑 → 𝐺 = 𝑇) & ⊢ (𝜑 → 𝐻 = 𝑈) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆𝑇𝑈”〉) | ||
Theorem | s3eq2 13998 | Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.) |
⊢ (𝐵 = 𝐷 → 〈“𝐴𝐵𝐶”〉 = 〈“𝐴𝐷𝐶”〉) | ||
Theorem | s2cld 13999 | A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵”〉 ∈ Word 𝑋) | ||
Theorem | s3cld 14000 | A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |