| Up: | Monoid enumeration |
|---|---|
| Prev: | #6 ⟨a, b | baababababababa=a⟩ |
| # | Rule | Proof |
|---|---|---|
| 1. | db ⇒ bc | [6] |
| 2. | dc8 ⇒ c | [9] |
| 3. | ab ⇒ c | [2] |
| 4. | ba ⇒ d | [3] |
| 5. | ca ⇒ ad | [5] |
| 6. | dac ⇒ ac50 | [21] |
| 7. | dadc ⇒ ac43 | [19] |
| 8. | dad2c ⇒ ac36 | [17] |
| 9. | dad3c ⇒ ac29 | [15] |
| 10. | dad4c ⇒ ac22 | [13] |
| 11. | dad5c ⇒ ac15 | [11] |
| 12. | dad6c ⇒ ac8 | [10] |
| 13. | dad7 ⇒ a | [7] |
| 14. | da2 ⇒ a2d49 | [22] |
| 15. | (da)2 ⇒ a2d42 | [20] |
| 16. | dad2a ⇒ a2d35 | [18] |
| 17. | dad3a ⇒ a2d28 | [16] |
| 18. | dad4a ⇒ a2d21 | [14] |
| 19. | dad5a ⇒ a2d14 | [12] |
| 20. | dad6a ⇒ a2d7 | [8] |
# ab:baabababababababa=a bcd/a ab=c,ba=d custom:1 db=bc dcccccccc=c ab=c ba=d ca=ad dac=acccccccccccccccccccccccccccccccccccccccccccccccccc dadc=accccccccccccccccccccccccccccccccccccccccccc daddc=acccccccccccccccccccccccccccccccccccc dadddc=accccccccccccccccccccccccccccc daddddc=acccccccccccccccccccccc dadddddc=accccccccccccccc daddddddc=acccccccc daddddddd=a daa=aaddddddddddddddddddddddddddddddddddddddddddddddddd dada=aadddddddddddddddddddddddddddddddddddddddddd dadda=aaddddddddddddddddddddddddddddddddddd daddda=aadddddddddddddddddddddddddddd dadddda=aaddddddddddddddddddddd daddddda=aadddddddddddddd dadddddda=aaddddddd
Axiom: baabababababababa=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] baabababababababa=a with [3] ba=d:
Critical pair: dabababababababa=a.
Reduce LHS:
| [2] | d(ab)ababababababa |
| [2] | ⇒ dc(ab)abababababa |
| [2] | ⇒ dcc(ab)ababababa |
| [2] | ⇒ dccc(ab)abababa |
| [2] | ⇒ dcccc(ab)ababa |
| [2] | ⇒ dccccc(ab)aba |
| [2] | ⇒ dcccccc(ab)a |
| ⇒ dccccccca |
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] dccccccca=a.
Reduce LHS:
| [5] | dcccccc(ca) |
| [5] | ⇒ dccccc(ca)d |
| [5] | ⇒ dcccc(ca)dd |
| [5] | ⇒ dccc(ca)ddd |
| [5] | ⇒ dcc(ca)dddd |
| [5] | ⇒ dc(ca)ddddd |
| [5] | ⇒ d(ca)dddddd |
| ⇒ daddddddd |
Defines rule #13.
Referenced by [8], [9], [10], [12], [14], [16], [18], [20], [22].
Overlap of [7] daddddddd=a with [7] daddddddd=a:
Critical pair: aaddddddd=dadddddda.
Flip LHS and RHS.
Defines rule #20.
Referenced by [12].
Overlap of [7] daddddddd=a with [6] db=bc:
Critical pair: ab=daddddddbc.
Reduce LHS:
| [2] | (ab) |
| ⇒ c |
Reduce RHS:
| [6] | daddddd(db)c |
| [6] | ⇒ dadddd(db)cc |
| [6] | ⇒ daddd(db)ccc |
| [6] | ⇒ dadd(db)cccc |
| [6] | ⇒ dad(db)ccccc |
| [6] | ⇒ da(db)cccccc |
| [2] | ⇒ d(ab)ccccccc |
| ⇒ dcccccccc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [10], [11], [13], [15], [17], [19], [21].
Overlap of [7] daddddddd=a with [9] dcccccccc=c:
Critical pair: acccccccc=daddddddc.
Flip LHS and RHS.
Defines rule #12.
Referenced by [11].
Overlap of [10] daddddddc=acccccccc with [9] dcccccccc=c:
Critical pair: accccccccccccccc=dadddddc.
Flip LHS and RHS.
Defines rule #11.
Referenced by [13].
Overlap of [8] dadddddda=aaddddddd with [7] daddddddd=a:
Critical pair: aadddddddddddddd=daddddda.
Flip LHS and RHS.
Defines rule #19.
Referenced by [14].
Overlap of [11] dadddddc=accccccccccccccc with [9] dcccccccc=c:
Critical pair: acccccccccccccccccccccc=daddddc.
Flip LHS and RHS.
Defines rule #10.
Referenced by [15].
Overlap of [12] daddddda=aadddddddddddddd with [7] daddddddd=a:
Critical pair: aaddddddddddddddddddddd=dadddda.
Flip LHS and RHS.
Defines rule #18.
Referenced by [16].
Overlap of [13] daddddc=acccccccccccccccccccccc with [9] dcccccccc=c:
Critical pair: accccccccccccccccccccccccccccc=dadddc.
Flip LHS and RHS.
Defines rule #9.
Referenced by [17].
Overlap of [14] dadddda=aaddddddddddddddddddddd with [7] daddddddd=a:
Critical pair: aadddddddddddddddddddddddddddd=daddda.
Flip LHS and RHS.
Defines rule #17.
Referenced by [18].
Overlap of [15] dadddc=accccccccccccccccccccccccccccc with [9] dcccccccc=c:
Critical pair: acccccccccccccccccccccccccccccccccccc=daddc.
Flip LHS and RHS.
Defines rule #8.
Referenced by [19].
Overlap of [16] daddda=aadddddddddddddddddddddddddddd with [7] daddddddd=a:
Critical pair: aaddddddddddddddddddddddddddddddddddd=dadda.
Flip LHS and RHS.
Defines rule #16.
Referenced by [20].
Overlap of [17] daddc=acccccccccccccccccccccccccccccccccccc with [9] dcccccccc=c:
Critical pair: accccccccccccccccccccccccccccccccccccccccccc=dadc.
Flip LHS and RHS.
Defines rule #7.
Referenced by [21].
Overlap of [18] dadda=aaddddddddddddddddddddddddddddddddddd with [7] daddddddd=a:
Critical pair: aadddddddddddddddddddddddddddddddddddddddddd=dada.
Flip LHS and RHS.
Defines rule #15.
Referenced by [22].
Overlap of [19] dadc=accccccccccccccccccccccccccccccccccccccccccc with [9] dcccccccc=c:
Critical pair: acccccccccccccccccccccccccccccccccccccccccccccccccc=dac.
Flip LHS and RHS.
Defines rule #6.
Overlap of [20] dada=aadddddddddddddddddddddddddddddddddddddddddd with [7] daddddddd=a:
Critical pair: aaddddddddddddddddddddddddddddddddddddddddddddddddd=daa.
Flip LHS and RHS.
Defines rule #14.