Definition df-s6

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

	Ref	Expression
Assertion	df-s6	$$⊢⟨“ABCDEF”⟩=⟨“ABCDE”⟩\mathrm{++}⟨“F”⟩$$

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	0 1 2 3 4 5	cs6	$$class⟨“ABCDEF”⟩$$
7	0 1 2 3 4	cs5	$$class⟨“ABCDE”⟩$$
8		cconcat	$$class\mathrm{++}$$
9	5	cs1	$$class⟨“F”⟩$$
10	7 9 8	co	$$class\left(⟨“ABCDE”⟩\mathrm{++}⟨“F”⟩\right)$$
11	6 10	wceq	$$wff⟨“ABCDEF”⟩=⟨“ABCDE”⟩\mathrm{++}⟨“F”⟩$$