![]() |
Metamath
Proof Explorer Theorem List (p. 139 of 443) | < 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-28474) |
![]() (28475-29999) |
![]() (30000-44271) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ccat2s1fvw 13801 | Extract a symbol of a word from the concatenation of the word with two single symbols. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 13-Jan-2020.) (Proof shortened by AV, 1-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (♯‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | ccat2s1fst 13802 | The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘0) = (𝑊‘0)) | ||
Syntax | csubstr 13803 | Syntax for the subword operator. |
class substr | ||
Definition | df-substr 13804* | Define an operation which extracts portions (called subwords or substrings) of words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅)) | ||
Theorem | swrdnznd 13805 | The value of a subword operation for noninteger arguments is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6529). (Contributed by AV, 2-Dec-2022.) (New usage is discouraged.) |
⊢ (¬ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅) | ||
Theorem | swrdval 13806* | Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅)) | ||
Theorem | swrd00 13807 | A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ (𝑆 substr 〈𝑋, 𝑋〉) = ∅ | ||
Theorem | swrdcl 13808 | Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝐹, 𝐿〉) ∈ Word 𝐴) | ||
Theorem | swrdval2 13809* | Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈𝐹, 𝐿〉) = (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹)))) | ||
Theorem | swrd0valOLD 13810 | Obsolete version of pfxres 13861 as of 12-Oct-2022. (Contributed by Stefan O'Rear, 24-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈0, 𝐿〉) = (𝑆 ↾ (0..^𝐿))) | ||
Theorem | swrd0lenOLD 13811 | Obsolete version of pfxlen 13865 as of 12-Oct-2022. (Contributed by Stefan O'Rear, 24-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈0, 𝐿〉)) = 𝐿) | ||
Theorem | swrdlen 13812 | Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝐹, 𝐿〉)) = (𝐿 − 𝐹)) | ||
Theorem | swrdfv 13813 | A symbol in an extracted subword, indexed using the subword's indices. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ∧ 𝑋 ∈ (0..^(𝐿 − 𝐹))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘𝑋) = (𝑆‘(𝑋 + 𝐹))) | ||
Theorem | swrdfv0 13814 | The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0..^𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘0) = (𝑆‘𝐹)) | ||
Theorem | swrdf 13815 | A subword of a word is a function from a half-open range of nonnegative integers of the same length as the subword to the set of symbols for the original word. (Contributed by AV, 13-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈𝑀, 𝑁〉):(0..^(𝑁 − 𝑀))⟶𝑉) | ||
Theorem | swrdvalfn 13816 | Value of the subword extractor as function with domain. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈𝐹, 𝐿〉) Fn (0..^(𝐿 − 𝐹))) | ||
Theorem | swrd0fOLD 13817 | Obsolete version of pfxf 13862 as of 12-Oct-2022. (Contributed by AV, 2-May-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈0, 𝑁〉):(0..^𝑁)⟶𝑉) | ||
Theorem | swrdidOLD 13818 | Obsolete version of pfxid 13866 as of 12-Oct-2022. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof shortened by AV, 2-May-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈0, (♯‘𝑆)〉) = 𝑆) | ||
Theorem | swrdrn 13819 | The range of a subword of a word is a subset of the set of symbols for the word. (Contributed by AV, 13-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ 𝑉) | ||
Theorem | swrdn0OLD 13820 | Obsolete version of pfxn0 13868 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Proof shortened by AV, 2-May-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝑊)) → (𝑊 substr 〈0, 𝑁〉) ≠ ∅) | ||
Theorem | swrdlend 13821 | The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) (Proof shortened by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ 𝐹 → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | ||
Theorem | swrdnd 13822 | The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) (Proof shortened by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑊) < 𝐿) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | ||
Theorem | swrdnd2 13823 | Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | ||
Theorem | swrdnnn0nd 13824 | The value of a subword operation for arguments not being nonnegative integers is the empty set. (Contributed by AV, 2-Dec-2022.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ ¬ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅) | ||
Theorem | swrdnd0 13825 | The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022.) |
⊢ (𝑆 ∈ Word 𝑉 → (¬ (𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | ||
Theorem | swrd0 13826 | A subword of an empty set is always the empty set. (Contributed by AV, 31-Mar-2018.) (Revised by AV, 20-Oct-2018.) (Proof shortened by AV, 2-May-2020.) |
⊢ (∅ substr 〈𝐹, 𝐿〉) = ∅ | ||
Theorem | swrdrlen 13827 | Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr 〈𝐼, (♯‘𝑊)〉)) = ((♯‘𝑊) − 𝐼)) | ||
Theorem | swrd0len0OLD 13828 | Obsolete as of 12-Oct-2022. Use pfxlen 13865 instead. (Contributed by AV, 4-Aug-2018.) (Proof shortened by AV, 14-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 substr 〈0, 𝑁〉)) = 𝑁) | ||
Theorem | addlenrevswrdOLD 13829 | Obsolete version of addlenrevpfx 13872 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → ((♯‘(𝑊 substr 〈𝑀, (♯‘𝑊)〉)) + (♯‘(𝑊 substr 〈0, 𝑀〉))) = (♯‘𝑊)) | ||
Theorem | addlenswrdOLD 13830 | Obsolete version of addlenpfx 13873 as of 12-Oct-2022. (Contributed by AV, 21-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → ((♯‘(𝑊 substr 〈0, 𝑀〉)) + (♯‘(𝑊 substr 〈𝑀, (♯‘𝑊)〉))) = (♯‘𝑊)) | ||
Theorem | swrd0fvOLD 13831 | Obsolete version of pfxfv 13864 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 substr 〈0, 𝐿〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | swrd0fv0OLD 13832 | Obsolete version of pfxfv0 13874 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (1...(♯‘𝑊))) → ((𝑊 substr 〈0, 𝐼〉)‘0) = (𝑊‘0)) | ||
Theorem | swrdtrcfvOLD 13833 | Obsolete version of pfxtrcfv 13875 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 substr 〈0, ((♯‘𝑊) − 1)〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | swrdtrcfv0OLD 13834 | Obsolete version of pfxtrcfv0 13876 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → ((𝑊 substr 〈0, ((♯‘𝑊) − 1)〉)‘0) = (𝑊‘0)) | ||
Theorem | swrd0fvlswOLD 13835 | Obsolete version of pfxfvlsw 13877 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 substr 〈0, 𝐿〉)) = (𝑊‘(𝐿 − 1))) | ||
Theorem | swrdeqOLD 13836* | Obsolete version of pfxeq 13878 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr 〈0, 𝑀〉) = (𝑈 substr 〈0, 𝑁〉) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) | ||
Theorem | swrdlen2 13837 | Length of an extracted subword. (Contributed by AV, 5-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (♯‘(𝑆 substr 〈𝐹, 𝐿〉)) = (𝐿 − 𝐹)) | ||
Theorem | swrdfv2 13838 | A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.) |
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘𝑋)) | ||
Theorem | swrdwrdsymb 13839 | A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁))) | ||
Theorem | swrdsb0eq 13840 | Two subwords with the same bounds are equal if the range is not valid. (Contributed by AV, 4-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝑀) → (𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉)) | ||
Theorem | swrdsbslen 13841 | Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉))) | ||
Theorem | swrdspsleq 13842* | 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 | swrdtrcfvlOLD 13843 | Obsolete version of pfxtrcfvl 13879 as of 12-Oct-2022. (Contributed by AV, 16-Jun-2018.) (Proof shortened by Mario Carneiro/AV, 14-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (lastS‘(𝑊 substr 〈0, ((♯‘𝑊) − 1)〉)) = (𝑊‘((♯‘𝑊) − 2))) | ||
Theorem | swrds1 13844 | Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) | ||
Theorem | swrdlsw 13845 | Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr 〈((♯‘𝑊) − 1), (♯‘𝑊)〉) = 〈“(lastS‘𝑊)”〉) | ||
Theorem | 2swrdeqwrdeqOLD 13846 | Obsolete version of pfxsuffeqwrdeq 13880 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 = 𝑆 ↔ ((♯‘𝑊) = (♯‘𝑆) ∧ ((𝑊 substr 〈0, 𝐼〉) = (𝑆 substr 〈0, 𝐼〉) ∧ (𝑊 substr 〈𝐼, (♯‘𝑊)〉) = (𝑆 substr 〈𝐼, (♯‘𝑊)〉))))) | ||
Theorem | 2swrd1eqwrdeqOLD 13847 | Obsolete version of pfxsuff1eqwrdeq 13881 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Revised by Mario Carneiro/AV, 23-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 substr 〈0, ((♯‘𝑊) − 1)〉) = (𝑈 substr 〈0, ((♯‘𝑊) − 1)〉) ∧ (lastS‘𝑊) = (lastS‘𝑈))))) | ||
Theorem | disjxwrdOLD 13848* | Obsolete version of disjwrdpfx 13882 as of 12-Oct-2022. (Contributed by AV, 29-Jul-2018.) (Proof shortened by AV, 7-May-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Disj 𝑦 ∈ 𝑊 {𝑥 ∈ Word 𝑉 ∣ (𝑥 substr 〈0, 𝑁〉) = 𝑦} | ||
Theorem | ccatswrd 13849 | Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr 〈𝑋, 𝑌〉) ++ (𝑆 substr 〈𝑌, 𝑍〉)) = (𝑆 substr 〈𝑋, 𝑍〉)) | ||
Theorem | swrdccat1OLD 13850 | Obsolete version of pfxccat1 13884 as of 12-Oct-2022. (Contributed by Mario Carneiro, 27-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈0, (♯‘𝑆)〉) = 𝑆) | ||
Theorem | swrdccat2 13851 | Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr 〈(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))〉) = 𝑇) | ||
Syntax | cpfx 13852 | Syntax for the prefix operator. |
class prefix | ||
Definition | df-pfx 13853* | Define an operation which extracts prefixes of words, i.e. subwords (or substrings) starting at the beginning of a word (or string). In other words, (𝑆 prefix 𝐿) is the prefix of the word 𝑆 of length 𝐿. Definition in Section 9.1 of [AhoHopUll] p. 318. See also Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix. (Contributed by AV, 2-May-2020.) |
⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) | ||
Theorem | pfxnndmnd 13854 | The value of a prefix operation for out-of-domain arguments. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6529). (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.) |
⊢ (¬ (𝑆 ∈ V ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = ∅) | ||
Theorem | pfxval 13855 | Value of a prefix operation. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr 〈0, 𝐿〉)) | ||
Theorem | pfx00 13856 | The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 prefix 0) = ∅ | ||
Theorem | pfx0 13857 | A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.) |
⊢ (∅ prefix 𝐿) = ∅ | ||
Theorem | pfxval0 13858 | Value of a prefix operation. This theorem should only be used in proofs if 𝐿 ∈ ℕ0 is not available. Otherwise (and usually), pfxval 13855 should be used. (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) = (𝑆 substr 〈0, 𝐿〉)) | ||
Theorem | pfxcl 13859 | Closure of the prefix extractor. (Contributed by AV, 2-May-2020.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) ∈ Word 𝐴) | ||
Theorem | pfxmpt 13860* | Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) = (𝑥 ∈ (0..^𝐿) ↦ (𝑆‘𝑥))) | ||
Theorem | pfxres 13861 | 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 13862 | 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 13863 | Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) Fn (0..^𝐿)) | ||
Theorem | pfxfv 13864 | 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 13865 | Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐿)) = 𝐿) | ||
Theorem | pfxid 13866 | 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 13867 | 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 13868 | 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 13869 | 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 6529). (Contributed by AV, 3-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (♯‘𝑊) < 𝐿) → (𝑊 prefix 𝐿) = ∅) | ||
Theorem | pfxnd0 13870 | 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 6529). (Contributed by AV, 3-Dec-2022.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∉ (0...(♯‘𝑊))) → (𝑊 prefix 𝐿) = ∅) | ||
Theorem | pfxwrdsymb 13871 | 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 13872 | 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 13873 | 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 13874 | 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 13875 | 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 13876 | 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 13877 | 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 13878* | 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 13879 | 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 13880 | 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 13881 | 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 13882* | 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 13883 | 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 13884 | 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 13885 | 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 13886 | Lemma for swrdswrd 13887. (Contributed by Alexander van der Vekens, 4-Apr-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊)))) | ||
Theorem | swrdswrd 13887 | 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 | swrd0swrdOLD 13888 | Obsolete proof of pfxswrd 13889 as of 12-Oct-2022. (Contributed by AV, 2-Apr-2018.) (Proof shortened by AV, 21-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝐿 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈0, 𝐿〉) = (𝑊 substr 〈𝑀, (𝑀 + 𝐿)〉))) | ||
Theorem | pfxswrd 13889 | 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 | swrdswrd0OLD 13890 | Obsolete proof of swrdpfx 13891 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 6-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉))) | ||
Theorem | swrdpfx 13891 | 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 | swrd0swrd0OLD 13892 | Obsolete proof of pfxpfx 13893 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝐿 ∈ (0...𝑁)) → ((𝑊 substr 〈0, 𝑁〉) substr 〈0, 𝐿〉) = (𝑊 substr 〈0, 𝐿〉)) | ||
Theorem | pfxpfx 13893 | 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 | swrd0swrdidOLD 13894 | Obsolete proof of pfxpfxid 13895 as of 12-Oct-2022. (Contributed by AV, 5-Apr-2018.) (Proof shortened by AV, 14-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ((𝑊 substr 〈0, 𝑁〉) substr 〈0, 𝑁〉) = (𝑊 substr 〈0, 𝑁〉)) | ||
Theorem | pfxpfxid 13895 | 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 13896 | 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 | wrdcctswrdOLD 13897 | Obsolete proof of pfxcctswrd 13896 as of 12-Oct-2022. (Contributed by AV, 21-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → ((𝑊 substr 〈0, 𝑀〉) ++ (𝑊 substr 〈𝑀, (♯‘𝑊)〉)) = 𝑊) | ||
Theorem | lenpfxcctswrd 13898 | 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 | lencctswrdOLD 13899 | Obsolete proof of lenpfxcctswrd 13898 as of 12-Oct-2022. (Contributed by AV, 21-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → (♯‘((𝑊 substr 〈0, 𝑀〉) ++ (𝑊 substr 〈𝑀, (♯‘𝑊)〉))) = (♯‘𝑊)) | ||
Theorem | lenrevpfxcctswrd 13900 | 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 𝑀))) = (♯‘𝑊)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |