| Step |
Hyp |
Ref |
Expression |
| 1 |
|
s2s2 |
|- <" A B C D "> = ( <" A B "> ++ <" C D "> ) |
| 2 |
1
|
eqcomi |
|- ( <" A B "> ++ <" C D "> ) = <" A B C D "> |
| 3 |
2
|
oveq1i |
|- ( ( <" A B "> ++ <" C D "> ) ++ <" E F G "> ) = ( <" A B C D "> ++ <" E F G "> ) |
| 4 |
|
s2cli |
|- <" A B "> e. Word _V |
| 5 |
|
s3cli |
|- <" E F G "> e. Word _V |
| 6 |
|
df-s3 |
|- <" A B C "> = ( <" A B "> ++ <" C "> ) |
| 7 |
|
s1s3 |
|- <" D E F G "> = ( <" D "> ++ <" E F G "> ) |
| 8 |
4 5 6 7
|
cats2cat |
|- ( <" A B C "> ++ <" D E F G "> ) = ( ( <" A B "> ++ <" C D "> ) ++ <" E F G "> ) |
| 9 |
|
s4s3 |
|- <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> ) |
| 10 |
3 8 9
|
3eqtr4ri |
|- <" A B C D E F G "> = ( <" A B C "> ++ <" D E F G "> ) |