Home | Metamath
Proof Explorer Theorem List (p. 134 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | swrdspsleq 13301* | Two words have a common subword (starting at the same position with the same length) iff they have the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Proof shortened by AV, 7-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) | ||
Theorem | swrdtrcfvl 13302 | The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018.) (Proof shortened by Mario Carneiro/AV, 14-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → ( lastS ‘(𝑊 substr 〈0, ((#‘𝑊) − 1)〉)) = (𝑊‘((#‘𝑊) − 2))) | ||
Theorem | swrds1 13303 | Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) | ||
Theorem | swrdlsw 13304 | Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑊)”〉) | ||
Theorem | 2swrdeqwrdeq 13305 | Two words are equal if and only if they have the same prefix and the same suffix. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑆 ↔ ((#‘𝑊) = (#‘𝑆) ∧ ((𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉) ∧ (𝑊 substr 〈𝐼, (#‘𝑊)〉) = (𝑆 substr 〈𝐼, (#‘𝑊)〉))))) | ||
Theorem | 2swrd1eqwrdeq 13306 | Two (nonempty) words are equal if and only if they have the same prefix and the same single symbol suffix. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Revised by Mario Carneiro/AV, 23-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 1)〉) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) | ||
Theorem | disjxwrd 13307* | Sets of words are disjoint if each set contains extensions of distinct words of a fixed length. (Contributed by AV, 29-Jul-2018.) (Proof shortened by AV, 7-May-2020.) |
⊢ Disj 𝑦 ∈ 𝑊 {𝑥 ∈ Word 𝑉 ∣ (𝑥 substr 〈0, 𝑁〉) = 𝑦} | ||
Theorem | ccatswrd 13308 | Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(#‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) = (𝑆 substr 〈𝑋, 𝑍〉)) | ||
Theorem | swrdccat1 13309 | Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈0, (#‘𝑆)〉) = 𝑆) | ||
Theorem | swrdccat2 13310 | Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(#‘𝑆), ((#‘𝑆) + (#‘𝑇))〉) = 𝑇) | ||
Theorem | swrdswrdlem 13311 | Lemma for swrdswrd 13312. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(#‘𝑊)))) | ||
Theorem | swrdswrd 13312 | A subword of a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉))) | ||
Theorem | swrd0swrd 13313 | A prefix of a subword. (Contributed by AV, 2-Apr-2018.) (Proof shortened by AV, 21-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝐿 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈0, 𝐿〉) = (𝑊 substr 〈𝑀, (𝑀 + 𝐿)〉))) | ||
Theorem | swrdswrd0 13314 | A subword of a prefix. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉))) | ||
Theorem | swrd0swrd0 13315 | A prefix of a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 substr 〈0, 𝑁〉) substr 〈0, 𝐿〉) = (𝑊 substr 〈0, 𝐿〉)) | ||
Theorem | swrd0swrdid 13316 | A prefix of a prefix with the same length is the prefix. (Contributed by AV, 5-Apr-2018.) (Proof shortened by AV, 14-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝑊 substr 〈0, 𝑁〉) substr 〈0, 𝑁〉) = (𝑊 substr 〈0, 𝑁〉)) | ||
Theorem | wrdcctswrd 13317 | The concatenation of two parts of a word yields the word itself. (Contributed by AV, 21-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((𝑊 substr 〈0, 𝑀〉) ++ (𝑊 substr 〈𝑀, (#‘𝑊)〉)) = 𝑊) | ||
Theorem | lencctswrd 13318 | The length of two concatenated parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘((𝑊 substr 〈0, 𝑀〉) ++ (𝑊 substr 〈𝑀, (#‘𝑊)〉))) = (#‘𝑊)) | ||
Theorem | lenrevcctswrd 13319 | The length of two reversely concatenated parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘((𝑊 substr 〈𝑀, (#‘𝑊)〉) ++ (𝑊 substr 〈0, 𝑀〉))) = (#‘𝑊)) | ||
Theorem | swrdccatwrd 13320 | Reconstruct a nonempty word from its prefix and last symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ++ 〈“( lastS ‘𝑊)”〉) = 𝑊) | ||
Theorem | ccats1swrdeq 13321 | The last symbol of a word concatenated with the subword of the word having length less by 1 than the word results in the word itself. (Contributed by Alexander van der Vekens, 24-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 substr 〈0, (#‘𝑊)〉) → 𝑈 = (𝑊 ++ 〈“( lastS ‘𝑈)”〉))) | ||
Theorem | ccatopth 13322 | An opth 4871-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | ccatopth2 13323 | An opth 4871-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐵) = (#‘𝐷)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | ccatlcan 13324 | Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → ((𝐶 ++ 𝐴) = (𝐶 ++ 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | ccatrcan 13325 | Concatenation of words is right-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | wrdeqs1cat 13326 | Decompose a nonempty word by separating off the first symbol. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅) → 𝑊 = (〈“(𝑊‘0)”〉 ++ (𝑊 substr 〈1, (#‘𝑊)〉))) | ||
Theorem | cats1un 13327 | Express a word with an extra symbol as the union of the word and the new value. (Contributed by Mario Carneiro, 28-Feb-2016.) |
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉) = (𝐴 ∪ {〈(#‘𝐴), 𝐵〉})) | ||
Theorem | wrdind 13328* | Perform induction over the structure of a word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Word 𝐵 → 𝜏) | ||
Theorem | wrd2ind 13329* | Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.) |
⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (𝜑 ↔ 𝜒)) & ⊢ ((𝑥 = (𝑦 ++ 〈“𝑧”〉) ∧ 𝑤 = (𝑢 ++ 〈“𝑠”〉)) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜌 ↔ 𝜏)) & ⊢ (𝑤 = 𝐵 → (𝜑 ↔ 𝜌)) & ⊢ 𝜓 & ⊢ (((𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (#‘𝑦) = (#‘𝑢)) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (#‘𝐴) = (#‘𝐵)) → 𝜏) | ||
Theorem | ccats1swrdeqrex 13330* | There exists a symbol such that its concatenation with the subword obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018.) (Proof shortened by AV, 24-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 substr 〈0, (#‘𝑊)〉) → ∃𝑠 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑠”〉))) | ||
Theorem | reuccats1lem 13331* | Lemma for reuccats1 13332. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Proof shortened by AV, 15-Jan-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋 ∧ (𝑊 ++ 〈“𝑆”〉) ∈ 𝑋) ∧ (∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1)))) → (𝑊 = (𝑈 substr 〈0, (#‘𝑊)〉) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))) | ||
Theorem | reuccats1 13332* | A set of words having the length of a given word increased by 1 contains a unique word with the given word as prefix if there is a unique symbol which extends the given word to be a word of the set. (Contributed by Alexander van der Vekens, 6-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 substr 〈0, (#‘𝑊)〉))) | ||
Theorem | swrdccatfn 13333 | The subword of a concatenation as function. (Contributed by Alexander van der Vekens, 27-May-2018.) |
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) | ||
Theorem | swrdccatin1 13334 | The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) |
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) | ||
Theorem | swrdccatin12lem1 13335 | Lemma 1 for swrdccatin12 13342. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.) |
⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) | ||
Theorem | swrdccatin12lem2a 13336 | Lemma 1 for swrdccatin12lem2 13340. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋))) | ||
Theorem | swrdccatin12lem2b 13337 | Lemma 2 for swrdccatin12lem2 13340. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^((𝑁 − 𝐿) − 0)))) | ||
Theorem | swrdccatin2 13338 | The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉))) | ||
Theorem | swrdccatin12lem2c 13339 | Lemma for swrdccatin12lem2 13340 and swrdccatin12lem3 13341. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) | ||
Theorem | swrdccatin12lem2 13340 | Lemma 2 for swrdccatin12 13342. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐵 substr 〈0, (𝑁 − 𝐿)〉)‘(𝐾 − (#‘(𝐴 substr 〈𝑀, 𝐿〉)))))) | ||
Theorem | swrdccatin12lem3 13341 | Lemma 3 for swrdccatin12 13342. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾))) | ||
Theorem | swrdccatin12 13342 | The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)))) | ||
Theorem | swrdccat3 13343 | The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 28-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈𝑀, 𝑁〉), if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)))))) | ||
Theorem | swrdccat 13344 | The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)〉) ++ (𝐵 substr 〈if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)〉)))) | ||
Theorem | swrdccat3a 13345 | A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 29-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(𝐿 + (#‘𝐵))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))))) | ||
Theorem | swrdccat3blem 13346 | Lemma for swrdccat3b 13347. (Contributed by AV, 30-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ (𝐿 + (#‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = (𝐴 substr 〈𝑀, (𝐿 + (#‘𝐵))〉)) | ||
Theorem | swrdccat3b 13347 | A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 30-May-2018.) |
⊢ 𝐿 = (#‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑀 ∈ (0...(𝐿 + (#‘𝐵))) → ((𝐴 ++ 𝐵) substr 〈𝑀, (𝐿 + (#‘𝐵))〉) = if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)))) | ||
Theorem | swrdccatid 13348 | A prefix of a concatenation of length of the first concatenated word is the first word itself. (Contributed by Alexander van der Vekens, 20-Sep-2018.) |
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = 𝐴) | ||
Theorem | ccats1swrdeqbi 13349 | A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. (Contributed by AV, 24-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 substr 〈0, (#‘𝑊)〉) ↔ 𝑈 = (𝑊 ++ 〈“( lastS ‘𝑈)”〉))) | ||
Theorem | swrdccatin1d 13350 | The subword of a concatenation of two words within the first of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.) |
⊢ (𝜑 → (#‘𝐴) = 𝐿) & ⊢ (𝜑 → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) & ⊢ (𝜑 → 𝑀 ∈ (0...𝑁)) & ⊢ (𝜑 → 𝑁 ∈ (0...𝐿)) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)) | ||
Theorem | swrdccatin2d 13351 | The subword of a concatenation of two words within the second of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.) |
⊢ (𝜑 → (#‘𝐴) = 𝐿) & ⊢ (𝜑 → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) & ⊢ (𝜑 → 𝑀 ∈ (𝐿...𝑁)) & ⊢ (𝜑 → 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉)) | ||
Theorem | swrdccatin12d 13352 | 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 13353 | Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) | ||
Theorem | splcl 13354 | Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) ∈ Word 𝐴) | ||
Theorem | splid 13355 | 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 13356 | The length of a splice. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(#‘𝑆))) & ⊢ (𝜑 → 𝑅 ∈ Word 𝐴) ⇒ ⊢ (𝜑 → (#‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = ((#‘𝑆) + ((#‘𝑅) − (𝑇 − 𝐹)))) | ||
Theorem | splfv1 13357 | 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 13358 | 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 13359 | 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 13360* | Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ 𝑉 → (reverse‘𝑊) = (𝑥 ∈ (0..^(#‘𝑊)) ↦ (𝑊‘(((#‘𝑊) − 1) − 𝑥)))) | ||
Theorem | revcl 13361 | The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) | ||
Theorem | revlen 13362 | The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (#‘(reverse‘𝑊)) = (#‘𝑊)) | ||
Theorem | revfv 13363 | Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(#‘𝑊))) → ((reverse‘𝑊)‘𝑋) = (𝑊‘(((#‘𝑊) − 1) − 𝑋))) | ||
Theorem | rev0 13364 | The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (reverse‘∅) = ∅ | ||
Theorem | revs1 13365 | Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (reverse‘〈“𝑆”〉) = 〈“𝑆”〉 | ||
Theorem | revccat 13366 | Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆))) | ||
Theorem | revrev 13367 | Reversion is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊) | ||
Theorem | reps 13368* | 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 13369 | 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 13370 | Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 5085. (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = ((0..^𝑁) × {𝑆})) | ||
Theorem | repsf 13371 | 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 13372 | The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝐼) = 𝑆) | ||
Theorem | repsw 13373 | 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 13374 | The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (#‘(𝑆 repeatS 𝑁)) = 𝑁) | ||
Theorem | repsw0 13375 | The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅) | ||
Theorem | repsdf2 13376* | Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) | ||
Theorem | repswsymball 13377* | All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑊 = (𝑆 repeatS (#‘𝑊)) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = 𝑆)) | ||
Theorem | repswsymballbi 13378* | 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 13379 | The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁)‘0) = 𝑆) | ||
Theorem | repswlsw 13380 | The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ( lastS ‘(𝑆 repeatS 𝑁)) = 𝑆) | ||
Theorem | repsw1 13381 | The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 1) = 〈“𝑆”〉) | ||
Theorem | repswswrd 13382 | 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 13383 | 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 13384 | 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 13386. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 15647 for words consisting of identical symbols and cshwshash 15649 for words having lengths which are prime numbers. | ||
Syntax | ccsh 13385 | Extend class notation with Cyclical Shifts. |
class cyclShift | ||
Definition | df-csh 13386* | 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 13387* | 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 13388 | 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 13389 | 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 13390 | 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 13391 | 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 13392 | Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (#‘𝑊)))) | ||
Theorem | cshwsublen 13393 | Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 − (#‘𝑊)))) | ||
Theorem | cshwn 13394 | 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 13395 | 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 13396 | 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 13397 | 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 13398 | 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 13399 | 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 13400 | 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 (#‘𝑊)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |