Metamath Proof Explorer


Theorem s4s4

Description: Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s4s4
|- <" A B C D E F G H "> = ( <" A B C D "> ++ <" E F G H "> )

Proof

Step Hyp Ref Expression
1 df-s4
 |-  <" E F G H "> = ( <" E F G "> ++ <" H "> )
2 s4cli
 |-  <" A B C D "> e. Word _V
3 s3cli
 |-  <" E F G "> e. Word _V
4 df-s8
 |-  <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
5 s4s3
 |-  <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> )
6 1 2 3 4 5 cats1cat
 |-  <" A B C D E F G H "> = ( <" A B C D "> ++ <" E F G H "> )