# Metamath Proof Explorer

## Table of Contents - 5.7. Words over a set

This section is about words (or strings) over a set (alphabet) defined as finite sequences of symbols (or characters) being elements of the alphabet. Although it is often required that the underlying set/alphabet be nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word, see, for example, s1cli: . Note that the empty word (i.e. the empty set) is the only word over an empty alphabet, see 0wrd0.

The set of words over is the free monoid over , where the monoid law is concatenation and the monoid unit is the empty word.

Besides the definition of words themselves, several operations on words are defined in this section: <table border="1" id="word-operations"> <tr> <th>Name</th><th>Reference</th><th>Explanation</th><th>Example</th> <th>Remarks</th></tr> <tr> <td>Length (or size) of a word </td><td> df-hash: </td> <td>Operation which determines the number of the symbols within the word.</td> <td> </td> <td> This is not a special definition for words, but for arbitrary sets.</td></tr> <tr> <td>First symbol of a word </td><td> df-fv: </td> <td>Operation which extracts the first symbol of a word. The result is the symbol at the first place in the sequence representing the word.</td> <td> </td> <td> This is not a special definition for words, but for arbitrary functions with a half-open range of nonnegative integers as domain.</td></tr> <tr> <td>Last symbol of a word </td><td> df-lsw: </td> <td>Operation which extracts the last symbol of a word. The result is the symbol at the last place in the sequence representing the word.</td> <td> </td> <td> Note that the index of the last symbol is less by 1 than the length of the word.</td></tr> <tr> <td>Subword (or substring) of a word </td> <td> df-substr: </td> <td>Operation which extracts a portion of a word. The result is a consecutive, reindexed part of the sequence representing the word.</td> <td> </td> <td> Note that the last index of the range defining the subword is greater by 1 than the index of the last symbol of the subword in the sequence of the original word.</td></tr> <tr> <td>Concatenation of two words </td> <td> df-concat: </td> <td>Operation combining two words to one new word. The result is a combined, reindexed sequence build from the sequences representing the two words.</td> <td> </td> <td> Note that the index of the first symbol of the second concatenated word is the length of the first word in the concatenation.</td></tr> <tr> <td>Reversal of a word </td> <td> df-reverse: </td> <td>Operation which reverses the order of symbols in a word.</td> <td> </td> <td> </td></tr> <tr> <td>Cyclical shift of a word </td> <td> df-csh: </td> <td>Operation cyclically shifting the symbols by a number of positions.</td> <td> </td> <td> </td></tr> <tr> <td>Splicing of a word </td> <td> df-splice: </td> <td>Operation which replaces portions of words.</td> <td> </td> <td> </td></tr> <tr> <td>Singleton word </td> <td> df-s1: </td> <td>Constructor building a word of length 1 from a symbol.</td> <td> </td> <td> </td></tr> </table> Conventions: <ul> <li>Words are usually represented by class variable , if two words are involved by and , or by and .</li> <li>The alphabets are usually represented by class variable (because any arbitrary set can be an alphabet), sometimes also by (especially as codomain of the function representing a word, because the alphabet is the set of symbols).</li> <li>The symbols are usually represented by class variables or , if two symbols are involved by and , or by and .</li> <li>The indices of the sequence representing a word are usually represented by class variable , if two indices are involved (especially for subwords) by and , or by and .</li> <li>The length of a word is usually represented by class variables or .</li> <li>The number of position to cyclically shift a word is usually represented by class variables or .</li></ul>

1. Definitions and basic theorems
2. Last symbol of a word
3. Concatenations of words
4. Singleton words
5. Concatenations with singleton words
6. Subwords/substrings
7. Prefixes of a word
8. Subwords of subwords
9. Subwords and concatenations
10. Subwords of concatenations
11. Splicing words (substring replacement)
12. Reversing words
13. Repeated symbol words
14. Cyclical shifts of words
15. Mapping words by a function
16. Longer string literals