Definition df-s4

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

	Ref	Expression
Assertion	df-s4	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3		cD	⊢ 𝐷
4	0 1 2 3	cs4	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
5	0 1 2	cs3	⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩
6		cconcat	⊢ ++
7	3	cs1	⊢ ⟨“ 𝐷 ”⟩
8	5 7 6	co	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )
9	4 8	wceq	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )