#1 ⟨a, b | bababbbabba=a⟩

Up:Monoid enumeration
Next:#2 ⟨a, b | baababa=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. ca ⇒ ac [12]
2. b2a ⇒ c [2]
3. cbac ⇒ abc2 [8]
4. cbabc2 ⇒ ba [4]
5. ba2 ⇒ (ab)2c3 [13]
6. (ba)2c ⇒ aba(bc2)2 [10]
7. b(ab)2c2 ⇒ a [3]
8. c(ba)2 ⇒ abcba [9]
9. cbabcba ⇒ a [6]
10. (ba)3 ⇒ (ab)2c(cb)2a [11]
11. b(ab)2cba ⇒ (ab)2c2 [5]
# ab:bababbbabba=a bc/a bba=c custom:0
ca=ac
bba=c
cbac=abcc
cbabcc=ba
baa=ababccc
babac=ababccbcc
bababcc=a
cbaba=abcba
cbabcba=a
bababa=ababccbcba
bababcba=ababcc

Certificate

[1] bababbbabba=a

Axiom: bababbbabba=a.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #2.

Referenced by [3], [4], [8], [12].

[3] bababcc=a

Overlap of [1] bababbbabba=a with [2] bba=c:

babab bbabba bba

Critical pair: bababcbba=a.

Reduce LHS:

[2]bababc(bba)
⇒ bababcc

Defines rule #7.

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

[4] cbabcc=ba

Overlap of [2] bba=c with [3] bababcc=a:

b ba bababcc

Critical pair: cbabcc=ba.

Defines rule #4.

Referenced by [5], [6], [7], [8], [10], [11], [12], [13].

[5] bababcba=ababcc

Overlap of [3] bababcc=a with [4] cbabcc=ba:

bababc c cbabcc

Critical pair: ababcc=bababcba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [7].

[6] cbabcba=a

Overlap of [4] cbabcc=ba with [4] cbabcc=ba:

cbabc c cbabcc

Critical pair: bababcc=cbabcba.

Reduce LHS:

[3](bababcc)
⇒ a

Flip LHS and RHS.

Defines rule #9.

Referenced by [7], [8], [9].

[7] cbabca=ababcc

Overlap of [4] cbabcc=ba with [6] cbabcba=a:

cbabc c cbabcba

Critical pair: bababcba=cbabca.

Reduce LHS:

[5](bababcba)
⇒ ababcc

Flip LHS and RHS.

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

[8] cbac=abcc

Overlap of [6] cbabcba=a with [4] cbabcc=ba:

cbab cba cbabcc

Critical pair: abcc=cbabba.

Reduce RHS:

[2]cba(bba)
⇒ cbac

Flip LHS and RHS.

Defines rule #3.

Referenced by [10].

[9] cbaba=abcba

Overlap of [6] cbabcba=a with [6] cbabcba=a:

cbab cba cbabcba

Critical pair: abcba=cbaba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [11], [12].

[10] babac=ababccbcc

Overlap of [4] cbabcc=ba with [8] cbac=abcc:

cbabc c cbac

Critical pair: babac=cbabcabcc.

Reduce RHS:

[7](cbabca)bcc
⇒ ababccbcc

Defines rule #6.

[11] bababa=ababccbcba

Overlap of [4] cbabcc=ba with [9] cbaba=abcba:

cbabc c cbaba

Critical pair: bababa=cbabcabcba.

Reduce RHS:

[7](cbabca)bcba
⇒ ababccbcba

Defines rule #10.

[12] ca=ac

Overlap of [9] cbaba=abcba with [3] bababcc=a:

c baba bababcc

Critical pair: abcbabcc=ca.

Reduce LHS:

[4]ab(cbabcc)
[2]⇒ a(bba)
⇒ ac

Flip LHS and RHS.

Defines rule #1.

Referenced by [13].

[13] baa=ababccc

Overlap of [4] cbabcc=ba with [12] ca=ac:

cbabc c ca

Critical pair: baa=cbabcac.

Reduce RHS:

[7](cbabca)c
⇒ ababccc

Defines rule #5.