Home | Metamath
Proof Explorer Theorem List (p. 145 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pfxres 14401 | Value of the subword extractor for left-anchored subwords. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) = (𝑆 ↾ (0..^𝐿))) | ||
Theorem | pfxf 14402 | A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 prefix 𝐿):(0..^𝐿)⟶𝑉) | ||
Theorem | pfxfn 14403 | Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) Fn (0..^𝐿)) | ||
Theorem | pfxfv 14404 | A symbol in a prefix of a word, indexed using the prefix' indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | pfxlen 14405 | Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐿)) = 𝐿) | ||
Theorem | pfxid 14406 | A word is a prefix of itself. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by AV, 2-May-2020.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix (♯‘𝑆)) = 𝑆) | ||
Theorem | pfxrn 14407 | The range of a prefix of a word is a subset of the set of symbols for the word. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ 𝑉) | ||
Theorem | pfxn0 14408 | A prefix consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ ∧ 𝐿 ≤ (♯‘𝑊)) → (𝑊 prefix 𝐿) ≠ ∅) | ||
Theorem | pfxnd 14409 | The value of a prefix operation for a length argument larger than the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6813). (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (♯‘𝑊) < 𝐿) → (𝑊 prefix 𝐿) = ∅) | ||
Theorem | pfxnd0 14410 | The value of a prefix operation for a length argument not in the range of the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6813). (Contributed by AV, 3-Dec-2022.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∉ (0...(♯‘𝑊))) → (𝑊 prefix 𝐿) = ∅) | ||
Theorem | pfxwrdsymb 14411 | A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) ∈ Word (𝑆 “ (0..^𝐿))) | ||
Theorem | addlenrevpfx 14412 | The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → ((♯‘(𝑊 substr 〈𝑀, (♯‘𝑊)〉)) + (♯‘(𝑊 prefix 𝑀))) = (♯‘𝑊)) | ||
Theorem | addlenpfx 14413 | The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018.) (Revised by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → ((♯‘(𝑊 prefix 𝑀)) + (♯‘(𝑊 substr 〈𝑀, (♯‘𝑊)〉))) = (♯‘𝑊)) | ||
Theorem | pfxfv0 14414 | The first symbol of a prefix is the first symbol of the word. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝐿)‘0) = (𝑊‘0)) | ||
Theorem | pfxtrcfv 14415 | A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 prefix ((♯‘𝑊) − 1))‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | pfxtrcfv0 14416 | The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → ((𝑊 prefix ((♯‘𝑊) − 1))‘0) = (𝑊‘0)) | ||
Theorem | pfxfvlsw 14417 | The last symbol in a nonempty prefix of a word. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 prefix 𝐿)) = (𝑊‘(𝐿 − 1))) | ||
Theorem | pfxeq 14418* | The prefixes of two words are equal iff they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 4-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) | ||
Theorem | pfxtrcfvl 14419 | The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018.) (Revised by AV, 5-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (lastS‘(𝑊 prefix ((♯‘𝑊) − 1))) = (𝑊‘((♯‘𝑊) − 2))) | ||
Theorem | pfxsuffeqwrdeq 14420 | 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.) (Revised by AV, 5-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 = 𝑆 ↔ ((♯‘𝑊) = (♯‘𝑆) ∧ ((𝑊 prefix 𝐼) = (𝑆 prefix 𝐼) ∧ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉))))) | ||
Theorem | pfxsuff1eqwrdeq 14421 | 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 AV, 6-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 1)) = (𝑈 prefix ((♯‘𝑊) − 1)) ∧ (lastS‘𝑊) = (lastS‘𝑈))))) | ||
Theorem | disjwrdpfx 14422* | Sets of words are disjoint if each set contains exactly the extensions of distinct words of a fixed length. Remark: A word 𝑊 is called an "extension" of a word 𝑃 if 𝑃 is a prefix of 𝑊. (Contributed by AV, 29-Jul-2018.) (Revised by AV, 6-May-2020.) |
⊢ Disj 𝑦 ∈ 𝑊 {𝑥 ∈ Word 𝑉 ∣ (𝑥 prefix 𝑁) = 𝑦} | ||
Theorem | ccatpfx 14423 | Concatenating a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → ((𝑆 prefix 𝑌) ++ (𝑆 substr 〈𝑌, 𝑍〉)) = (𝑆 prefix 𝑍)) | ||
Theorem | pfxccat1 14424 | Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by AV, 6-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) prefix (♯‘𝑆)) = 𝑆) | ||
Theorem | pfx1 14425 | The prefix of length one of a nonempty word expressed as a singleton word. (Contributed by AV, 15-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 prefix 1) = 〈“(𝑊‘0)”〉) | ||
Theorem | swrdswrdlem 14426 | Lemma for swrdswrd 14427. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊)))) | ||
Theorem | swrdswrd 14427 | A subword of a subword is a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉))) | ||
Theorem | pfxswrd 14428 | A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018.) (Revised by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝐿 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 substr 〈𝑀, 𝑁〉) prefix 𝐿) = (𝑊 substr 〈𝑀, (𝑀 + 𝐿)〉))) | ||
Theorem | swrdpfx 14429 | A subword of a prefix is a subword. (Contributed by Alexander van der Vekens, 6-Apr-2018.) (Revised by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 prefix 𝑁) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉))) | ||
Theorem | pfxpfx 14430 | A prefix of a prefix is a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 prefix 𝑁) prefix 𝐿) = (𝑊 prefix 𝐿)) | ||
Theorem | pfxpfxid 14431 | A prefix of a prefix with the same length is the original prefix. In other words, the operation "prefix of length 𝑁 " is idempotent. (Contributed by AV, 5-Apr-2018.) (Revised by AV, 8-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 𝑁) prefix 𝑁) = (𝑊 prefix 𝑁)) | ||
Theorem | pfxcctswrd 14432 | The concatenation of the prefix of a word and the rest of the word yields the word itself. (Contributed by AV, 21-Oct-2018.) (Revised by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 𝑀) ++ (𝑊 substr 〈𝑀, (♯‘𝑊)〉)) = 𝑊) | ||
Theorem | lenpfxcctswrd 14433 | The length of the concatenation of the prefix of a word and the rest of the word is the length of the word. (Contributed by AV, 21-Oct-2018.) (Revised by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → (♯‘((𝑊 prefix 𝑀) ++ (𝑊 substr 〈𝑀, (♯‘𝑊)〉))) = (♯‘𝑊)) | ||
Theorem | lenrevpfxcctswrd 14434 | The length of the concatenation of the rest of a word and the prefix of the word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → (♯‘((𝑊 substr 〈𝑀, (♯‘𝑊)〉) ++ (𝑊 prefix 𝑀))) = (♯‘𝑊)) | ||
Theorem | pfxlswccat 14435 | Reconstruct a nonempty word from its prefix and last symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 prefix ((♯‘𝑊) − 1)) ++ 〈“(lastS‘𝑊)”〉) = 𝑊) | ||
Theorem | ccats1pfxeq 14436 | The last symbol of a word concatenated with the word with the last symbol removed results in the word itself. (Contributed by Alexander van der Vekens, 24-Oct-2018.) (Revised by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (♯‘𝑈) = ((♯‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (♯‘𝑊)) → 𝑈 = (𝑊 ++ 〈“(lastS‘𝑈)”〉))) | ||
Theorem | ccats1pfxeqrex 14437* | There exists a symbol such that its concatenation after the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018.) (Revised by AV, 9-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (♯‘𝑈) = ((♯‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (♯‘𝑊)) → ∃𝑠 ∈ 𝑉 𝑈 = (𝑊 ++ 〈“𝑠”〉))) | ||
Theorem | ccatopth 14438 | An opth 5392-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 12-Oct-2022.) |
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (♯‘𝐴) = (♯‘𝐶)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | ccatopth2 14439 | An opth 5392-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (♯‘𝐵) = (♯‘𝐷)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | ccatlcan 14440 | Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → ((𝐶 ++ 𝐴) = (𝐶 ++ 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | ccatrcan 14441 | Concatenation of words is right-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | wrdeqs1cat 14442 | 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, 12-Oct-2022.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅) → 𝑊 = (〈“(𝑊‘0)”〉 ++ (𝑊 substr 〈1, (♯‘𝑊)〉))) | ||
Theorem | cats1un 14443 | 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 14444* | Perform induction over the structure of a word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 12-Oct-2022.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Word 𝐵 → 𝜏) | ||
Theorem | wrd2ind 14445* | Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.) (Proof shortened by AV, 12-Oct-2022.) |
⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (𝜑 ↔ 𝜒)) & ⊢ ((𝑥 = (𝑦 ++ 〈“𝑧”〉) ∧ 𝑤 = (𝑢 ++ 〈“𝑠”〉)) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜌 ↔ 𝜏)) & ⊢ (𝑤 = 𝐵 → (𝜑 ↔ 𝜌)) & ⊢ 𝜓 & ⊢ (((𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝜏) | ||
Theorem | swrdccatfn 14446 | 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 14447 | 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 | pfxccatin12lem4 14448 | Lemma 4 for pfxccatin12 14455. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.) |
⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) | ||
Theorem | pfxccatin12lem2a 14449 | Lemma for pfxccatin12lem2 14453. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 + 𝑀) ∈ (𝐿..^𝑋))) | ||
Theorem | pfxccatin12lem1 14450 | Lemma 1 for pfxccatin12 14455. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.) |
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (𝐾 − (𝐿 − 𝑀)) ∈ (0..^(𝑁 − 𝐿)))) | ||
Theorem | swrdccatin2 14451 | 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 | pfxccatin12lem2c 14452 | Lemma for pfxccatin12lem2 14453 and pfxccatin12lem3 14454. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) | ||
Theorem | pfxccatin12lem2 14453 | Lemma 2 for pfxccatin12 14455. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝐾 − (♯‘(𝐴 substr 〈𝑀, 𝐿〉)))))) | ||
Theorem | pfxccatin12lem3 14454 | Lemma 3 for pfxccatin12 14455. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾))) | ||
Theorem | pfxccatin12 14455 | 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 AV, 9-May-2020.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))) | ||
Theorem | pfxccat3 14456 | 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 AV, 10-May-2020.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈𝑀, 𝑁〉), if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))))) | ||
Theorem | swrdccat 14457 | 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 | pfxccatpfx1 14458 | A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...𝐿)) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 prefix 𝑁)) | ||
Theorem | pfxccatpfx2 14459 | A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020.) |
⊢ 𝐿 = (♯‘𝐴) & ⊢ 𝑀 = (♯‘𝐵) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) | ||
Theorem | pfxccat3a 14460 | 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 AV, 10-May-2020.) |
⊢ 𝐿 = (♯‘𝐴) & ⊢ 𝑀 = (♯‘𝐵) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(𝐿 + 𝑀)) → ((𝐴 ++ 𝐵) prefix 𝑁) = if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))))) | ||
Theorem | swrdccat3blem 14461 | Lemma for swrdccat3b 14462. (Contributed by AV, 30-May-2018.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (♯‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = (𝐴 substr 〈𝑀, (𝐿 + (♯‘𝐵))〉)) | ||
Theorem | swrdccat3b 14462 | 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.) (Proof shortened by AV, 14-Oct-2022.) |
⊢ 𝐿 = (♯‘𝐴) ⇒ ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → ((𝐴 ++ 𝐵) substr 〈𝑀, (𝐿 + (♯‘𝐵))〉) = if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (♯‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)))) | ||
Theorem | pfxccatid 14463 | 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.) (Revised by AV, 10-May-2020.) |
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (♯‘𝐴)) → ((𝐴 ++ 𝐵) prefix 𝑁) = 𝐴) | ||
Theorem | ccats1pfxeqbi 14464 | 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.) (Revised by AV, 10-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (♯‘𝑈) = ((♯‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (♯‘𝑊)) ↔ 𝑈 = (𝑊 ++ 〈“(lastS‘𝑈)”〉))) | ||
Theorem | swrdccatin1d 14465 | 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 14466 | 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 | pfxccatin12d 14467 | The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by AV, 10-May-2020.) |
⊢ (𝜑 → (♯‘𝐴) = 𝐿) & ⊢ (𝜑 → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) & ⊢ (𝜑 → 𝑀 ∈ (0...𝐿)) & ⊢ (𝜑 → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿)))) | ||
Theorem | reuccatpfxs1lem 14468* | Lemma for reuccatpfxs1 14469. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 9-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ 𝑋) ∧ ∀𝑠 ∈ 𝑉 ((𝑊 ++ 〈“𝑠”〉) ∈ 𝑋 → 𝑆 = 𝑠) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑊) + 1))) → (𝑊 = (𝑈 prefix (♯‘𝑊)) → 𝑈 = (𝑊 ++ 〈“𝑆”〉))) | ||
Theorem | reuccatpfxs1 14469* | There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 13-Oct-2022.) |
⊢ Ⅎ𝑣𝑋 ⇒ ⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 prefix (♯‘𝑊)))) | ||
Theorem | reuccatpfxs1v 14470* | There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 10-May-2022.) (Proof shortened by AV, 13-Oct-2022.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑥 ∈ 𝑋 (𝑥 ∈ Word 𝑉 ∧ (♯‘𝑥) = ((♯‘𝑊) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑊 ++ 〈“𝑣”〉) ∈ 𝑋 → ∃!𝑥 ∈ 𝑋 𝑊 = (𝑥 prefix (♯‘𝑊)))) | ||
Syntax | csplice 14471 | Syntax for the word splicing operator. |
class splice | ||
Definition | df-splice 14472* | 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 14473 | 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 14474 | 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 14475 | 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 14476 | 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 14477 | 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 14478 | 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 14479 | 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 〈𝐹, 𝑇, 𝑅〉) = ((𝐴 ++ 𝑅) ++ 𝐶)) | ||
Syntax | creverse 14480 | Syntax for the word reverse operator. |
class reverse | ||
Definition | df-reverse 14481* | 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 14482* | Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ 𝑉 → (reverse‘𝑊) = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ (𝑊‘(((♯‘𝑊) − 1) − 𝑥)))) | ||
Theorem | revcl 14483 | The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘𝑊) ∈ Word 𝐴) | ||
Theorem | revlen 14484 | The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (♯‘(reverse‘𝑊)) = (♯‘𝑊)) | ||
Theorem | revfv 14485 | Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘𝑊))) → ((reverse‘𝑊)‘𝑋) = (𝑊‘(((♯‘𝑊) − 1) − 𝑋))) | ||
Theorem | rev0 14486 | The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ (reverse‘∅) = ∅ | ||
Theorem | revs1 14487 | Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (reverse‘〈“𝑆”〉) = 〈“𝑆”〉 | ||
Theorem | revccat 14488 | Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆))) | ||
Theorem | revrev 14489 | Reversal is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ (𝑊 ∈ Word 𝐴 → (reverse‘(reverse‘𝑊)) = 𝑊) | ||
Syntax | creps 14490 | Extend class notation with words consisting of one repeated symbol. |
class repeatS | ||
Definition | df-reps 14491* | 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 14492* | 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 14493 | 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 14494 | Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 5650. (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = ((0..^𝑁) × {𝑆})) | ||
Theorem | repsf 14495 | 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 14496 | The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝐼) = 𝑆) | ||
Theorem | repsw 14497 | 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 14498 | The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (♯‘(𝑆 repeatS 𝑁)) = 𝑁) | ||
Theorem | repsw0 14499 | The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅) | ||
Theorem | repsdf2 14500* | Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |