| Up: | Monoid enumeration |
|---|---|
| Prev: | #4 ⟨a, b | baababababa=a⟩ |
| Next: | #6 ⟨a, b | baababababababa=a⟩ |
| # | Rule | Proof |
|---|---|---|
| 1. | db ⇒ bc | [6] |
| 2. | dc6 ⇒ c | [9] |
| 3. | ab ⇒ c | [2] |
| 4. | ba ⇒ d | [3] |
| 5. | ca ⇒ ad | [5] |
| 6. | dac ⇒ ac26 | [17] |
| 7. | dadc ⇒ ac21 | [15] |
| 8. | dad2c ⇒ ac16 | [13] |
| 9. | dad3c ⇒ ac11 | [11] |
| 10. | dad4c ⇒ ac6 | [10] |
| 11. | dad5 ⇒ a | [7] |
| 12. | da2 ⇒ a2d25 | [18] |
| 13. | (da)2 ⇒ a2d20 | [16] |
| 14. | dad2a ⇒ a2d15 | [14] |
| 15. | dad3a ⇒ a2d10 | [12] |
| 16. | dad4a ⇒ a2d5 | [8] |
# ab:baabababababa=a bcd/a ab=c,ba=d custom:1 db=bc dcccccc=c ab=c ba=d ca=ad dac=acccccccccccccccccccccccccc dadc=accccccccccccccccccccc daddc=acccccccccccccccc dadddc=accccccccccc daddddc=acccccc daddddd=a daa=aaddddddddddddddddddddddddd dada=aadddddddddddddddddddd dadda=aaddddddddddddddd daddda=aadddddddddd dadddda=aaddddd
Axiom: baabababababa=a.
Referenced by [4].
Axiom: ab=c.
Defines rule #3.
Referenced by [4], [5], [6], [9].
Axiom: ba=d.
Defines rule #4.
Overlap of [1] baabababababa=a with [3] ba=d:
Critical pair: dabababababa=a.
Reduce LHS:
| [2] | d(ab)ababababa |
| [2] | ⇒ dc(ab)abababa |
| [2] | ⇒ dcc(ab)ababa |
| [2] | ⇒ dccc(ab)aba |
| [2] | ⇒ dcccc(ab)a |
| ⇒ dccccca |
Referenced by [7].
Overlap of [2] ab=c with [3] ba=d:
Critical pair: ca=ad.
Defines rule #5.
Referenced by [7].
Overlap of [3] ba=d with [2] ab=c:
Critical pair: db=bc.
Defines rule #1.
Referenced by [9].
Simplify [4] dccccca=a.
Reduce LHS:
| [5] | dcccc(ca) |
| [5] | ⇒ dccc(ca)d |
| [5] | ⇒ dcc(ca)dd |
| [5] | ⇒ dc(ca)ddd |
| [5] | ⇒ d(ca)dddd |
| ⇒ daddddd |
Defines rule #11.
Referenced by [8], [9], [10], [12], [14], [16], [18].
Overlap of [7] daddddd=a with [7] daddddd=a:
Critical pair: aaddddd=dadddda.
Flip LHS and RHS.
Defines rule #16.
Referenced by [12].
Overlap of [7] daddddd=a with [6] db=bc:
Critical pair: ab=daddddbc.
Reduce LHS:
| [2] | (ab) |
| ⇒ c |
Reduce RHS:
| [6] | daddd(db)c |
| [6] | ⇒ dadd(db)cc |
| [6] | ⇒ dad(db)ccc |
| [6] | ⇒ da(db)cccc |
| [2] | ⇒ d(ab)ccccc |
| ⇒ dcccccc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [10], [11], [13], [15], [17].
Overlap of [7] daddddd=a with [9] dcccccc=c:
Critical pair: acccccc=daddddc.
Flip LHS and RHS.
Defines rule #10.
Referenced by [11].
Overlap of [10] daddddc=acccccc with [9] dcccccc=c:
Critical pair: accccccccccc=dadddc.
Flip LHS and RHS.
Defines rule #9.
Referenced by [13].
Overlap of [8] dadddda=aaddddd with [7] daddddd=a:
Critical pair: aadddddddddd=daddda.
Flip LHS and RHS.
Defines rule #15.
Referenced by [14].
Overlap of [11] dadddc=accccccccccc with [9] dcccccc=c:
Critical pair: acccccccccccccccc=daddc.
Flip LHS and RHS.
Defines rule #8.
Referenced by [15].
Overlap of [12] daddda=aadddddddddd with [7] daddddd=a:
Critical pair: aaddddddddddddddd=dadda.
Flip LHS and RHS.
Defines rule #14.
Referenced by [16].
Overlap of [13] daddc=acccccccccccccccc with [9] dcccccc=c:
Critical pair: accccccccccccccccccccc=dadc.
Flip LHS and RHS.
Defines rule #7.
Referenced by [17].
Overlap of [14] dadda=aaddddddddddddddd with [7] daddddd=a:
Critical pair: aadddddddddddddddddddd=dada.
Flip LHS and RHS.
Defines rule #13.
Referenced by [18].
Overlap of [15] dadc=accccccccccccccccccccc with [9] dcccccc=c:
Critical pair: acccccccccccccccccccccccccc=dac.
Flip LHS and RHS.
Defines rule #6.
Overlap of [16] dada=aadddddddddddddddddddd with [7] daddddd=a:
Critical pair: aaddddddddddddddddddddddddd=daa.
Flip LHS and RHS.
Defines rule #12.