Definition df-pfx

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	$$⊢\mathrm{prefix}=\left(s\in \mathrm{V},l\in {\mathbb{N}}_0⟼s\mathrm{substr}⟨0,l⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpfx	$$class\mathrm{prefix}$$
1		vs	$$setvars$$
2		cvv	$$class\mathrm{V}$$
3		vl	$$setvarl$$
4		cn0	$$class{\mathbb{N}}_0$$
5	1	cv	$$setvars$$
6		csubstr	$$class\mathrm{substr}$$
7		cc0	$$class0$$
8	3	cv	$$setvarl$$
9	7 8	cop	$$class⟨0,l⟩$$
10	5 9 6	co	$$class\left(s\mathrm{substr}⟨0,l⟩\right)$$
11	1 3 2 4 10	cmpo	$$class\left(s\in \mathrm{V},l\in {\mathbb{N}}_0⟼s\mathrm{substr}⟨0,l⟩\right)$$
12	0 11	wceq	$$wff\mathrm{prefix}=\left(s\in \mathrm{V},l\in {\mathbb{N}}_0⟼s\mathrm{substr}⟨0,l⟩\right)$$