Definition df-s3

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

	Ref	Expression
Assertion	df-s3	$$⊢⟨“ABC”⟩=⟨“AB”⟩\mathrm{++}⟨“C”⟩$$

Detailed syntax breakdown

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