Definition df-s8 12819

Description: Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-s8

Detailed syntax breakdown of Definition df-s8

Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3		cC	. . 3
4		cD	. . 3
5		cE	. . 3
6		cF	. . 3
7		cG	. . 3
8		cH	. . 3
9	1, 2, 3, 4, 5, 6, 7, 8	cs8 12812	. 2
10	1, 2, 3, 4, 5, 6, 7	cs7 12811	. . 3
11	8	cs1 12537	. . 3
12		cconcat 12536	. . 3
13	10, 11, 12	co 6296	. 2
14	9, 13	wceq 1395	1

This definition is referenced by:  s8eqd  12833  s8cld  12840  s8cli  12849  s8len  12861  s1s7  12876  s4s4  12880