#4 ⟨a, b | baababababa=a⟩

Up:Monoid enumeration
Prev:#3 ⟨a, b | baabababa=a⟩
Next:#5 ⟨a, b | baabababababa=a⟩

Quick links

  1. Properties
  2. Rewriting system
  3. Certificate

Properties

Rewriting system

Format:
Word to reduce:
Tips:
  • Lowercase letters stand for generators.
  • Spaces are ignored.
  • Numbers repeat the previous letter, e.g. b90.
Reduction strategy:
Path to normal form: 1 
1
#RuleProof
1. db ⇒ bc [6]
2. dc5 ⇒ c [9]
3. ab ⇒ c [2]
4. ba ⇒ d [3]
5. ca ⇒ ad [5]
6. dac ⇒ ac17 [15]
7. dadc ⇒ ac13 [13]
8. dad2c ⇒ ac9 [11]
9. dad3c ⇒ ac5 [10]
10. dad4 ⇒ a [7]
11. da2 ⇒ a2d16 [16]
12. (da)2 ⇒ a2d12 [14]
13. dad2a ⇒ a2d8 [12]
14. dad3a ⇒ a2d4 [8]
# ab:baababababa=a bcd/a ab=c,ba=d custom:1
db=bc
dccccc=c
ab=c
ba=d
ca=ad
dac=accccccccccccccccc
dadc=accccccccccccc
daddc=accccccccc
dadddc=accccc
dadddd=a
daa=aadddddddddddddddd
dada=aadddddddddddd
dadda=aadddddddd
daddda=aadddd

Certificate

[1] baababababa=a

Axiom: baababababa=a.

Referenced by [4].

[2] ab=c

Axiom: ab=c.

Defines rule #3.

Referenced by [4], [5], [6], [9].

[3] ba=d

Axiom: ba=d.

Defines rule #4.

Referenced by [4], [5], [6].

[4] dcccca=a

Overlap of [1] baababababa=a with [3] ba=d:

1 baababababa ba

Critical pair: dababababa=a.

Reduce LHS:

[2]d(ab)abababa
[2]⇒ dc(ab)ababa
[2]⇒ dcc(ab)aba
[2]⇒ dccc(ab)a
⇒ dcccca

Referenced by [7].

[5] ca=ad

Overlap of [2] ab=c with [3] ba=d:

a b ba

Critical pair: ca=ad.

Defines rule #5.

Referenced by [7].

[6] db=bc

Overlap of [3] ba=d with [2] ab=c:

b a ab

Critical pair: db=bc.

Defines rule #1.

Referenced by [9].

[7] dadddd=a

Simplify [4] dcccca=a.

Reduce LHS:

[5]dccc(ca)
[5]⇒ dcc(ca)d
[5]⇒ dc(ca)dd
[5]⇒ d(ca)ddd
⇒ dadddd

Defines rule #10.

Referenced by [8], [9], [10], [12], [14], [16].

[8] daddda=aadddd

Overlap of [7] dadddd=a with [7] dadddd=a:

daddd d dadddd

Critical pair: aadddd=daddda.

Flip LHS and RHS.

Defines rule #14.

Referenced by [12].

[9] dccccc=c

Overlap of [7] dadddd=a with [6] db=bc:

daddd d db

Critical pair: ab=dadddbc.

Reduce LHS:

[2](ab)
⇒ c

Reduce RHS:

[6]dadd(db)c
[6]⇒ dad(db)cc
[6]⇒ da(db)ccc
[2]⇒ d(ab)cccc
⇒ dccccc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11], [13], [15].

[10] dadddc=accccc

Overlap of [7] dadddd=a with [9] dccccc=c:

daddd d dccccc

Critical pair: accccc=dadddc.

Flip LHS and RHS.

Defines rule #9.

Referenced by [11].

[11] daddc=accccccccc

Overlap of [10] dadddc=accccc with [9] dccccc=c:

dadd dc dccccc

Critical pair: accccccccc=daddc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [13].

[12] dadda=aadddddddd

Overlap of [8] daddda=aadddd with [7] dadddd=a:

dadd da dadddd

Critical pair: aadddddddd=dadda.

Flip LHS and RHS.

Defines rule #13.

Referenced by [14].

[13] dadc=accccccccccccc

Overlap of [11] daddc=accccccccc with [9] dccccc=c:

dad dc dccccc

Critical pair: accccccccccccc=dadc.

Flip LHS and RHS.

Defines rule #7.

Referenced by [15].

[14] dada=aadddddddddddd

Overlap of [12] dadda=aadddddddd with [7] dadddd=a:

dad da dadddd

Critical pair: aadddddddddddd=dada.

Flip LHS and RHS.

Defines rule #12.

Referenced by [16].

[15] dac=accccccccccccccccc

Overlap of [13] dadc=accccccccccccc with [9] dccccc=c:

da dc dccccc

Critical pair: accccccccccccccccc=dac.

Flip LHS and RHS.

Defines rule #6.

[16] daa=aadddddddddddddddd

Overlap of [14] dada=aadddddddddddd with [7] dadddd=a:

da da dadddd

Critical pair: aadddddddddddddddd=daa.

Flip LHS and RHS.

Defines rule #11.