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	⊢ prefix = ( 𝑠 ∈ V , 𝑙 ∈ ℕ0 ↦ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpfx	⊢ prefix
1		vs	⊢ 𝑠
2		cvv	⊢ V
3		vl	⊢ 𝑙
4		cn0	⊢ ℕ0
5	1	cv	⊢ 𝑠
6		csubstr	⊢ substr
7		cc0	⊢ 0
8	3	cv	⊢ 𝑙
9	7 8	cop	⊢ ⟨ 0 , 𝑙 ⟩
10	5 9 6	co	⊢ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ )
11	1 3 2 4 10	cmpo	⊢ ( 𝑠 ∈ V , 𝑙 ∈ ℕ0 ↦ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) )
12	0 11	wceq	⊢ prefix = ( 𝑠 ∈ V , 𝑙 ∈ ℕ0 ↦ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) )