#3 ⟨a, b | baabababa=a⟩

Up:Monoid enumeration
Prev:#2 ⟨a, b | baababa=a⟩
Next:#4 ⟨a, b | baababababa=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. dc4 ⇒ c [9]
3. ab ⇒ c [2]
4. ba ⇒ d [3]
5. ca ⇒ ad [5]
6. dac ⇒ ac10 [13]
7. dadc ⇒ ac7 [11]
8. dad2c ⇒ ac4 [10]
9. dad3 ⇒ a [7]
10. da2 ⇒ a2d9 [14]
11. (da)2 ⇒ a2d6 [12]
12. dad2a ⇒ a2d3 [8]
# ab:baabababa=a bcd/a ab=c,ba=d custom:1
db=bc
dcccc=c
ab=c
ba=d
ca=ad
dac=acccccccccc
dadc=accccccc
daddc=acccc
daddd=a
daa=aaddddddddd
dada=aadddddd
dadda=aaddd

Certificate

[1] baabababa=a

Axiom: baabababa=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] dccca=a

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

1 baabababa ba

Critical pair: dabababa=a.

Reduce LHS:

[2]d(ab)ababa
[2]⇒ dc(ab)aba
[2]⇒ dcc(ab)a
⇒ dccca

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] daddd=a

Simplify [4] dccca=a.

Reduce LHS:

[5]dcc(ca)
[5]⇒ dc(ca)d
[5]⇒ d(ca)dd
⇒ daddd

Defines rule #9.

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

[8] dadda=aaddd

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

dadd d daddd

Critical pair: aaddd=dadda.

Flip LHS and RHS.

Defines rule #12.

Referenced by [12].

[9] dcccc=c

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

dadd d db

Critical pair: ab=daddbc.

Reduce LHS:

[2](ab)
⇒ c

Reduce RHS:

[6]dad(db)c
[6]⇒ da(db)cc
[2]⇒ d(ab)ccc
⇒ dcccc

Flip LHS and RHS.

Defines rule #2.

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

[10] daddc=acccc

Overlap of [7] daddd=a with [9] dcccc=c:

dadd d dcccc

Critical pair: acccc=daddc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [11].

[11] dadc=accccccc

Overlap of [10] daddc=acccc with [9] dcccc=c:

dad dc dcccc

Critical pair: accccccc=dadc.

Flip LHS and RHS.

Defines rule #7.

Referenced by [13].

[12] dada=aadddddd

Overlap of [8] dadda=aaddd with [7] daddd=a:

dad da daddd

Critical pair: aadddddd=dada.

Flip LHS and RHS.

Defines rule #11.

Referenced by [14].

[13] dac=acccccccccc

Overlap of [11] dadc=accccccc with [9] dcccc=c:

da dc dcccc

Critical pair: acccccccccc=dac.

Flip LHS and RHS.

Defines rule #6.

[14] daa=aaddddddddd

Overlap of [12] dada=aadddddd with [7] daddd=a:

da da daddd

Critical pair: aaddddddddd=daa.

Flip LHS and RHS.

Defines rule #10.