Metamath Proof Explorer


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 ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )