Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-pfx | Structured version Visualization version GIF version |
Description: Define an operation which extracts prefixes of words, i.e. subwords starting at the beginning of a word. Definition in section 9.1 of [AhoHopUll] p. 318. "pfx" is used as label fragment. (Contributed by AV, 2-May-2020.) |
Ref | Expression |
---|---|
df-pfx | ⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpfx 41381 | . 2 class prefix | |
2 | vs | . . 3 setvar 𝑠 | |
3 | vl | . . 3 setvar 𝑙 | |
4 | cvv 3200 | . . 3 class V | |
5 | cn0 11292 | . . 3 class ℕ0 | |
6 | 2 | cv 1482 | . . . 4 class 𝑠 |
7 | cc0 9936 | . . . . 5 class 0 | |
8 | 3 | cv 1482 | . . . . 5 class 𝑙 |
9 | 7, 8 | cop 4183 | . . . 4 class 〈0, 𝑙〉 |
10 | csubstr 13295 | . . . 4 class substr | |
11 | 6, 9, 10 | co 6650 | . . 3 class (𝑠 substr 〈0, 𝑙〉) |
12 | 2, 3, 4, 5, 11 | cmpt2 6652 | . 2 class (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) |
13 | 1, 12 | wceq 1483 | 1 wff prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) |
Colors of variables: wff setvar class |
This definition is referenced by: pfxval 41383 pfx00 41384 pfx0 41385 pfxcl 41386 |
Copyright terms: Public domain | W3C validator |