Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-word | Structured version Visualization version GIF version |
Description: Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ0 so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 equipped with concatenation is the free monoid over 𝑆, and the monoid unit is the empty word (see frmdval 18132). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
df-word | ⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cS | . . 3 class 𝑆 | |
2 | 1 | cword 13955 | . 2 class Word 𝑆 |
3 | cc0 10615 | . . . . . 6 class 0 | |
4 | vl | . . . . . . 7 setvar 𝑙 | |
5 | 4 | cv 1541 | . . . . . 6 class 𝑙 |
6 | cfzo 13124 | . . . . . 6 class ..^ | |
7 | 3, 5, 6 | co 7170 | . . . . 5 class (0..^𝑙) |
8 | vw | . . . . . 6 setvar 𝑤 | |
9 | 8 | cv 1541 | . . . . 5 class 𝑤 |
10 | 7, 1, 9 | wf 6335 | . . . 4 wff 𝑤:(0..^𝑙)⟶𝑆 |
11 | cn0 11976 | . . . 4 class ℕ0 | |
12 | 10, 4, 11 | wrex 3054 | . . 3 wff ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆 |
13 | 12, 8 | cab 2716 | . 2 class {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} |
14 | 2, 13 | wceq 1542 | 1 wff Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} |
Colors of variables: wff setvar class |
This definition is referenced by: iswrd 13957 wrdval 13958 nfwrd 13984 csbwrdg 13985 |
Copyright terms: Public domain | W3C validator |