Description: 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, ( S prefix L ) is the prefix of the word S of length L . 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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-pfx | |- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cpfx | |- prefix |
|
| 1 | vs | |- s |
|
| 2 | cvv | |- _V |
|
| 3 | vl | |- l |
|
| 4 | cn0 | |- NN0 |
|
| 5 | 1 | cv | |- s |
| 6 | csubstr | |- substr |
|
| 7 | cc0 | |- 0 |
|
| 8 | 3 | cv | |- l |
| 9 | 7 8 | cop | |- <. 0 , l >. |
| 10 | 5 9 6 | co | |- ( s substr <. 0 , l >. ) |
| 11 | 1 3 2 4 10 | cmpo | |- ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) ) |
| 12 | 0 11 | wceq | |- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) ) |