| Step |
Hyp |
Ref |
Expression |
| 1 |
|
s1s2 |
|- <" A B C "> = ( <" A "> ++ <" B C "> ) |
| 2 |
1
|
eqcomi |
|- ( <" A "> ++ <" B C "> ) = <" A B C "> |
| 3 |
2
|
oveq1i |
|- ( ( <" A "> ++ <" B C "> ) ++ <" D E F G "> ) = ( <" A B C "> ++ <" D E F G "> ) |
| 4 |
|
s1cli |
|- <" A "> e. Word _V |
| 5 |
|
s4cli |
|- <" D E F G "> e. Word _V |
| 6 |
|
df-s2 |
|- <" A B "> = ( <" A "> ++ <" B "> ) |
| 7 |
|
s1s4 |
|- <" C D E F G "> = ( <" C "> ++ <" 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 |
|
s3s4 |
|- <" 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 "> ) |