Definition df-s7

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

	Ref	Expression
Assertion	df-s7	$$⊢⟨“ABCDEFG”⟩=⟨“ABCDEF”⟩\mathrm{++}⟨“G”⟩$$

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