Definition df-s4

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

	Ref	Expression
Assertion	df-s4	$$⊢⟨“ABCD”⟩=⟨“ABC”⟩\mathrm{++}⟨“D”⟩$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cC	$$classC$$
3		cD	$$classD$$
4	0 1 2 3	cs4	$$class⟨“ABCD”⟩$$
5	0 1 2	cs3	$$class⟨“ABC”⟩$$
6		cconcat	$$class\mathrm{++}$$
7	3	cs1	$$class⟨“D”⟩$$
8	5 7 6	co	$$class\left(⟨“ABC”⟩\mathrm{++}⟨“D”⟩\right)$$
9	4 8	wceq	$$wff⟨“ABCD”⟩=⟨“ABC”⟩\mathrm{++}⟨“D”⟩$$