| # | Rule | Proof |
| 1. |
(dc)3b ⇒ c |
[5] |
| 2. |
dc(dcd)2cbd ⇒ cb |
[10] |
| 3. |
(dc)2(d(dc)2)2bc ⇒ c2(dc)2b |
[13] |
| 4. |
(d(dc)2)2(d2c)2dcbd2 ⇒ cdb |
[20] |
| 5. |
cb2 ⇒ (dc)2bd |
[9] |
| 6. |
cbc(dc)2b ⇒ dc(dcd)2cbc |
[11] |
| 7. |
cdbc(dc)2b ⇒ (d(dc)2)2(d2c)2dcbdc |
[22] |
| 8. |
c2dcbdb ⇒ dc(dcd)2c((d2c)2dc)2bd2 |
[29] |
| 9. |
c(dc)2bdb ⇒ (dc)2d2c(dcd)3cbd2 |
[18] |
| 10. |
d(dc)2bdb ⇒ bd |
[16] |
| 11. |
c2((dc)2b)2 ⇒ dc((dcd)2cd)2(dc)2bc |
[15] |
| 12. |
dc(dcd)2(cb)2 ⇒ cbc(dcd)2cbd |
[12] |
| 13. |
dc(dcd)2cbcdb ⇒ cb(dc)2d2c(dcd)3cbd2 |
[21] |
| 14. |
dc(dcd)2cbc2(dc)2b ⇒ cbcdc(d(dc)2)2bc |
[14] |
| 15. |
(d(dc)2)2(d2c)2dcbcdb ⇒ cdbcdcd2c(dcd)3cbd2 |
[27] |
| 16. |
(d(dc)2)2(d2c)2(dcb)2 ⇒ cdbc(dcd)2cbd |
[23] |
| 17. |
(d(dc)2)2(d2c)2dcbdcdb ⇒ cdb(dc)2d2c(dcd)3cbd2 |
[28] |
| 18. |
(d(dc)2)2(d2c)2dcbdc2(dc)2b ⇒ cdbcdc(d(dc)2)2bc |
[24] |
| 19. |
cbcdcbdb ⇒ (dc)2((d2c)2dc)2bd2 |
[19] |
| 20. |
cb(dc)2bdb ⇒ dc(dcd)3cbd2 |
[17] |
| 21. |
cdbcdcbdb ⇒ (d(dc)2)2(d2c)3dcbd2 |
[25] |
| 22. |
cdb(dc)2bdb ⇒ d2c(dcd2c)2bd2 |
[26] |
| 23. |
c(cd)2(cbd)2b ⇒ dc(dcd)2c((d2c)2dc)3bd2 |
[30] |
| 24. |
ab2 ⇒ d |
[3] |
| 25. |
ca ⇒ dc2 |
[8] |
| 26. |
da ⇒ abdcb |
[6] |
| 27. |
ba ⇒ dcb |
[4] |