This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 , 𝑙 ⟩ ) )