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 = (s \in V, l \in ℕ_{0} ⟼ s substr ⟨0, l⟩)$

Detailed syntax breakdown

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