Definition df-s8 12639

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 12632	. 2
10	1, 2, 3, 4, 5, 6, 7	cs7 12631	. . 3
11	8	cs1 12382	. . 3
12		cconcat 12381	. . 3
13	10, 11, 12	co 6222	. 2
14	9, 13	wceq 1370	1

This definition is referenced by:  s8eqd  12653  s8cld  12660  s8cli  12669  s8len  12681  s1s7  12696  s4s4  12700