Definition df-s8

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

	Ref	Expression
Assertion	df-s8	$$⊢⟨“ABCDEFGH”⟩=⟨“ABCDEFG”⟩\mathrm{++}⟨“H”⟩$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cC	$$classC$$
3		cD	$$classD$$
4		cE	$$classE$$
5		cF	$$classF$$
6		cG	$$classG$$
7		cH	$$classH$$
8	0 1 2 3 4 5 6 7	cs8	$$class⟨“ABCDEFGH”⟩$$
9	0 1 2 3 4 5 6	cs7	$$class⟨“ABCDEFG”⟩$$
10		cconcat	$$class\mathrm{++}$$
11	7	cs1	$$class⟨“H”⟩$$
12	9 11 10	co	$$class\left(⟨“ABCDEFG”⟩\mathrm{++}⟨“H”⟩\right)$$
13	8 12	wceq	$$wff⟨“ABCDEFGH”⟩=⟨“ABCDEFG”⟩\mathrm{++}⟨“H”⟩$$