| Up: | Monoid enumeration |
|---|---|
| Prev: | #1 ⟨a, b | bababbbabba=a⟩ |
| Next: | #3 ⟨a, b | baabababa=a⟩ |
| # | Rule | Proof |
|---|---|---|
| 1. | db ⇒ bc | [6] |
| 2. | dc3 ⇒ c | [9] |
| 3. | ab ⇒ c | [2] |
| 4. | ba ⇒ d | [3] |
| 5. | ca ⇒ ad | [5] |
| 6. | dac ⇒ ac5 | [11] |
| 7. | dadc ⇒ ac3 | [10] |
| 8. | dad2 ⇒ a | [7] |
| 9. | da2 ⇒ a2d4 | [12] |
| 10. | (da)2 ⇒ a2d2 | [8] |
# ab:baababa=a bcd/a ab=c,ba=d custom:1 db=bc dccc=c ab=c ba=d ca=ad dac=accccc dadc=accc dadd=a daa=aadddd dada=aadd
Axiom: baababa=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] baababa=a with [3] ba=d:
Critical pair: dababa=a.
Reduce LHS:
| [2] | d(ab)aba |
| [2] | ⇒ dc(ab)a |
| ⇒ dcca |
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] dcca=a.
Reduce LHS:
| [5] | dc(ca) |
| [5] | ⇒ d(ca)d |
| ⇒ dadd |
Defines rule #8.
Referenced by [8], [9], [10], [12].
Overlap of [7] dadd=a with [7] dadd=a:
Critical pair: aadd=dada.
Flip LHS and RHS.
Defines rule #10.
Referenced by [12].
Overlap of [7] dadd=a with [6] db=bc:
Critical pair: ab=dadbc.
Reduce LHS:
| [2] | (ab) |
| ⇒ c |
Reduce RHS:
| [6] | da(db)c |
| [2] | ⇒ d(ab)cc |
| ⇒ dccc |
Flip LHS and RHS.
Defines rule #2.
Overlap of [7] dadd=a with [9] dccc=c:
Critical pair: accc=dadc.
Flip LHS and RHS.
Defines rule #7.
Referenced by [11].
Overlap of [10] dadc=accc with [9] dccc=c:
Critical pair: accccc=dac.
Flip LHS and RHS.
Defines rule #6.
Overlap of [8] dada=aadd with [7] dadd=a:
Critical pair: aadddd=daa.
Flip LHS and RHS.
Defines rule #9.