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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csplice | |
|
1 | vs | |
|
2 | cvv | |
|
3 | vb | |
|
4 | 1 | cv | |
5 | cpfx | |
|
6 | c1st | |
|
7 | 3 | cv | |
8 | 7 6 | cfv | |
9 | 8 6 | cfv | |
10 | 4 9 5 | co | |
11 | cconcat | |
|
12 | c2nd | |
|
13 | 7 12 | cfv | |
14 | 10 13 11 | co | |
15 | csubstr | |
|
16 | 8 12 | cfv | |
17 | chash | |
|
18 | 4 17 | cfv | |
19 | 16 18 | cop | |
20 | 4 19 15 | co | |
21 | 14 20 11 | co | |
22 | 1 3 2 2 21 | cmpo | |
23 | 0 22 | wceq | |