![]() |
Metamath
Proof Explorer Theorem List (p. 148 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | splcl 14701 | 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 14702 | 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 14703 | 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 14704 | 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 14705 | 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 14706 | 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 14707 | Syntax for the word reverse operator. |
class reverse | ||
Definition | df-reverse 14708* | 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 14709* | Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (π β π β (reverseβπ) = (π₯ β (0..^(β―βπ)) β¦ (πβ(((β―βπ) β 1) β π₯)))) | ||
Theorem | revcl 14710 | The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (π β Word π΄ β (reverseβπ) β Word π΄) | ||
Theorem | revlen 14711 | The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (π β Word π΄ β (β―β(reverseβπ)) = (β―βπ)) | ||
Theorem | revfv 14712 | Reverse of a word at a point. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ ((π β Word π΄ β§ π β (0..^(β―βπ))) β ((reverseβπ)βπ) = (πβ(((β―βπ) β 1) β π))) | ||
Theorem | rev0 14713 | The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ (reverseββ ) = β | ||
Theorem | revs1 14714 | Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (reverseββ¨βπββ©) = β¨βπββ© | ||
Theorem | revccat 14715 | Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ ((π β Word π΄ β§ π β Word π΄) β (reverseβ(π ++ π)) = ((reverseβπ) ++ (reverseβπ))) | ||
Theorem | revrev 14716 | Reversal is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ (π β Word π΄ β (reverseβ(reverseβπ)) = π) | ||
Syntax | creps 14717 | Extend class notation with words consisting of one repeated symbol. |
class repeatS | ||
Definition | df-reps 14718* | 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 14719* | 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 14720 | 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 14721 | Construct a function mapping a half-open range of nonnegative integers to a constant, see also fconstmpt 5738. (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0) β (π repeatS π) = ((0..^π) Γ {π})) | ||
Theorem | repsf 14722 | 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 14723 | The symbols of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0 β§ πΌ β (0..^π)) β ((π repeatS π)βπΌ) = π) | ||
Theorem | repsw 14724 | 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 14725 | The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β0) β (β―β(π repeatS π)) = π) | ||
Theorem | repsw0 14726 | The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018.) |
β’ (π β π β (π repeatS 0) = β ) | ||
Theorem | repsdf2 14727* | Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018.) |
β’ ((π β π β§ π β β0) β (π = (π repeatS π) β (π β Word π β§ (β―βπ) = π β§ βπ β (0..^π)(πβπ) = π))) | ||
Theorem | repswsymball 14728* | All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.) |
β’ ((π β Word π β§ π β π) β (π = (π repeatS (β―βπ)) β βπ β (0..^(β―βπ))(πβπ) = π)) | ||
Theorem | repswsymballbi 14729* | 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 14730 | The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β) β ((π repeatS π)β0) = π) | ||
Theorem | repswlsw 14731 | The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.) |
β’ ((π β π β§ π β β) β (lastSβ(π repeatS π)) = π) | ||
Theorem | repsw1 14732 | The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.) |
β’ (π β π β (π repeatS 1) = β¨βπββ©) | ||
Theorem | repswswrd 14733 | A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption π β€ πΏ is required, because otherwise (πΏ < π): ((π 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 14734 | 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 14735 | 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 14736 | 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 14738. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 17035 for words consisting of identical symbols and cshwshash 17037 for words having lengths which are prime numbers. | ||
Syntax | ccsh 14737 | Extend class notation with Cyclical Shifts. |
class cyclShift | ||
Definition | df-csh 14738* | 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 (β―βπ€)))))) | ||
Theorem | cshfn 14739* | 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 | cshword 14740 | 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 14741 | 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 14742 | 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 14743 | 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 14744 | 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 14745 | Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018.) |
β’ ((π β Word π β§ π β β€) β (π cyclShift π) = (π cyclShift (π β (β―βπ)))) | ||
Theorem | cshwn 14746 | 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 14747 | 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 14748 | 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 14749 | 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 14750 | 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 14751 | 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 14752 | 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 14753 | 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 14754 | 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 14755 | 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 14756 | 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 14757 | 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 14758 | 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 14759 | 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 14760 | 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 14761 | 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 14762 | 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 14763 | 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 14764 | 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 14765 | 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 14766 | 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 14767 | 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 14768 | 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 14769 | 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 14770* | 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 14771* | 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 14772 | 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 14773* | 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.) (Proof shortened by SN, 15-Jan-2025.) |
β’ {π€ β Word π β£ βπ β (0..^(β―βπ))(π cyclShift π) = π€} β V | ||
Theorem | cshwsexaOLD 14774* | Obsolete version of cshwsexa 14773 as of 15-Jan-2025. (Contributed by AV, 8-Jun-2018.) (Revised by Mario Carneiro/AV, 25-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ {π€ β Word π β£ βπ β (0..^(β―βπ))(π cyclShift π) = π€} β V | ||
Theorem | 2cshwcshw 14775* | 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 14776* | 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 14777* | A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlksym 29271 and erclwwlknsym 29320. (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 14778* | A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr 29272 and erclwwlkntr 29321. (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 14779 | 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 14780 | 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 14781 | Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ ((π β Word π΄ β§ πΉ:π΄βΆπ΅) β (πΉ β π) β Word π΅) | ||
Theorem | lenco 14782 | Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ ((π β Word π΄ β§ πΉ:π΄βΆπ΅) β (β―β(πΉ β π)) = (β―βπ)) | ||
Theorem | s1co 14783 | Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ ((π β π΄ β§ πΉ:π΄βΆπ΅) β (πΉ β β¨βπββ©) = β¨β(πΉβπ)ββ©) | ||
Theorem | revco 14784 | Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ ((π β Word π΄ β§ πΉ:π΄βΆπ΅) β (πΉ β (reverseβπ)) = (reverseβ(πΉ β π))) | ||
Theorem | ccatco 14785 | Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ ((π β Word π΄ β§ π β Word π΄ β§ πΉ:π΄βΆπ΅) β (πΉ β (π ++ π)) = ((πΉ β π) ++ (πΉ β π))) | ||
Theorem | cshco 14786 | Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018.) |
β’ ((π β Word π΄ β§ π β β€ β§ πΉ:π΄βΆπ΅) β (πΉ β (π cyclShift π)) = ((πΉ β π) cyclShift π)) | ||
Theorem | swrdco 14787 | Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.) |
β’ ((π β Word π΄ β§ (π β (0...π) β§ π β (0...(β―βπ))) β§ πΉ:π΄βΆπ΅) β (πΉ β (π substr β¨π, πβ©)) = ((πΉ β π) substr β¨π, πβ©)) | ||
Theorem | pfxco 14788 | Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.) |
β’ ((π β Word π΄ β§ π β (0...(β―βπ)) β§ πΉ:π΄βΆπ΅) β (πΉ β (π prefix π)) = ((πΉ β π) prefix π)) | ||
Theorem | lswco 14789 | 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 14790 | Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018.) |
β’ ((π β π΄ β§ π β β0 β§ πΉ:π΄βΆπ΅) β (πΉ β (π repeatS π)) = ((πΉβπ) repeatS π)) | ||
Syntax | cs2 14791 | Syntax for the length 2 word constructor. |
class β¨βπ΄π΅ββ© | ||
Syntax | cs3 14792 | Syntax for the length 3 word constructor. |
class β¨βπ΄π΅πΆββ© | ||
Syntax | cs4 14793 | Syntax for the length 4 word constructor. |
class β¨βπ΄π΅πΆπ·ββ© | ||
Syntax | cs5 14794 | Syntax for the length 5 word constructor. |
class β¨βπ΄π΅πΆπ·πΈββ© | ||
Syntax | cs6 14795 | Syntax for the length 6 word constructor. |
class β¨βπ΄π΅πΆπ·πΈπΉββ© | ||
Syntax | cs7 14796 | Syntax for the length 7 word constructor. |
class β¨βπ΄π΅πΆπ·πΈπΉπΊββ© | ||
Syntax | cs8 14797 | Syntax for the length 8 word constructor. |
class β¨βπ΄π΅πΆπ·πΈπΉπΊπ»ββ© | ||
Definition | df-s2 14798 | Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄π΅ββ© = (β¨βπ΄ββ© ++ β¨βπ΅ββ©) | ||
Definition | df-s3 14799 | Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄π΅πΆββ© = (β¨βπ΄π΅ββ© ++ β¨βπΆββ©) | ||
Definition | df-s4 14800 | Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄π΅πΆπ·ββ© = (β¨βπ΄π΅πΆββ© ++ β¨βπ·ββ©) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |