df-splice

Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by AV, 14-Oct-2022)

		Ref	Expression
	Assertion	df-splice	$⊢ splice = (s \in V, b \in V ⟼ ((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b)) ++ (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩))$

Step	Hyp	Ref	Expression
0		csplice	$class splice$
1		vs	$setvar s$
2		cvv	$class V$
3		vb	$setvar b$
4	1	cv	$setvar s$
5		cpfx	$class prefix$
6		c1st	$class 1^{st}$
7	3	cv	$setvar b$
8	7 6	cfv	$class 1^{st} (b)$
9	8 6	cfv	$class 1^{st} (1^{st} (b))$
10	4 9 5	co	$class (s prefix 1^{st} (1^{st} (b)))$
11		cconcat	$class ++$
12		c2nd	$class 2^{nd}$
13	7 12	cfv	$class 2^{nd} (b)$
14	10 13 11	co	$class ((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b))$
15		csubstr	$class substr$
16	8 12	cfv	$class 2^{nd} (1^{st} (b))$
17		chash	$class \|.\|$
18	4 17	cfv	$class \|s\|$
19	16 18	cop	$class ⟨2^{nd} (1^{st} (b)), \|s\|⟩$
20	4 19 15	co	$class (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩)$
21	14 20 11	co	$class (((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b)) ++ (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩))$
22	1 3 2 2 21	cmpo	$class (s \in V, b \in V ⟼ ((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b)) ++ (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩))$
23	0 22	wceq	$wff splice = (s \in V, b \in V ⟼ ((s prefix 1^{st} (1^{st} (b))) ++ 2^{nd} (b)) ++ (s substr ⟨2^{nd} (1^{st} (b)), \|s\|⟩))$

Metamath Proof Explorer