#6 ⟨a, b | baababababababa=a⟩

Quick links

Properties
Rewriting system
Certificate

Properties

Presentation has sum-of-sides 16
Infinite non-commutative monoid

Rewriting system

Format:	Pretty Plain
Word to reduce:
	Tips: Lowercase letters stand for generators. Spaces are ignored. Numbers repeat the previous letter, e.g. `b90`.
Reduction strategy:	Leftmost Rightmost
Path to normal form:	1 1

Reduction order:
- Left-to-right recursive path with deg(b) = deg(c) = deg(d) = 0, b < c < d; deg(a) = 1
Auxiliary generator: ab=c
Auxiliary generator: ba=d

#	Rule	Proof
1.	db ⇒ bc	[6]
2.	dc⁷ ⇒ c	[9]
3.	ab ⇒ c	[2]
4.	ba ⇒ d	[3]
5.	ca ⇒ ad	[5]
6.	dac ⇒ ac³⁷	[19]
7.	dadc ⇒ ac³¹	[17]
8.	dad²c ⇒ ac²⁵	[15]
9.	dad³c ⇒ ac¹⁹	[13]
10.	dad⁴c ⇒ ac¹³	[11]
11.	dad⁵c ⇒ ac⁷	[10]
12.	dad⁶ ⇒ a	[7]
13.	da² ⇒ a²d³⁶	[20]
14.	(da)² ⇒ a²d³⁰	[18]
15.	dad²a ⇒ a²d²⁴	[16]
16.	dad³a ⇒ a²d¹⁸	[14]
17.	dad⁴a ⇒ a²d¹²	[12]
18.	dad⁵a ⇒ a²d⁶	[8]

# ab:baababababababa=a bcd/a ab=c,ba=d custom:1
db=bc
dccccccc=c
ab=c
ba=d
ca=ad
dac=accccccccccccccccccccccccccccccccccccc
dadc=accccccccccccccccccccccccccccccc
daddc=accccccccccccccccccccccccc
dadddc=accccccccccccccccccc
daddddc=accccccccccccc
dadddddc=accccccc
dadddddd=a
daa=aadddddddddddddddddddddddddddddddddddd
dada=aadddddddddddddddddddddddddddddd
dadda=aadddddddddddddddddddddddd
daddda=aadddddddddddddddddd
dadddda=aadddddddddddd
daddddda=aadddddd

Certificate

[1] baababababababa=a

Axiom: baababababababa=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] dcccccca=a

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

1 baababababababa ba

Critical pair: dababababababa=a.

Reduce LHS:

[2]	d(ab)abababababa
[2]	⇒ dc(ab)ababababa
[2]	⇒ dcc(ab)abababa
[2]	⇒ dccc(ab)ababa
[2]	⇒ dcccc(ab)aba
[2]	⇒ dccccc(ab)a
	⇒ dcccccca

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

Simplify [4] dcccccca=a.

Reduce LHS:

[5]	dccccc(ca)
[5]	⇒ dcccc(ca)d
[5]	⇒ dccc(ca)dd
[5]	⇒ dcc(ca)ddd
[5]	⇒ dc(ca)dddd
[5]	⇒ d(ca)ddddd
	⇒ dadddddd

Defines rule #12.

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

[8] daddddda=aadddddd

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

daddddd d dadddddd

Critical pair: aadddddd=daddddda.

Flip LHS and RHS.

Defines rule #18.

Referenced by [12].

[9] dccccccc=c

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

daddddd d db

Critical pair: ab=dadddddbc.

Reduce LHS:

[2]	(ab)
	⇒ c

Reduce RHS:

[6]	dadddd(db)c
[6]	⇒ daddd(db)cc
[6]	⇒ dadd(db)ccc
[6]	⇒ dad(db)cccc
[6]	⇒ da(db)ccccc
[2]	⇒ d(ab)cccccc
	⇒ dccccccc

Flip LHS and RHS.

Defines rule #2.

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

[10] dadddddc=accccccc

Overlap of [7] dadddddd=a with [9] dccccccc=c:

daddddd d dccccccc

Critical pair: accccccc=dadddddc.

Flip LHS and RHS.

Defines rule #11.

Referenced by [11].

[11] daddddc=accccccccccccc

Overlap of [10] dadddddc=accccccc with [9] dccccccc=c:

dadddd dc dccccccc

Critical pair: accccccccccccc=daddddc.

Flip LHS and RHS.

Defines rule #10.

Referenced by [13].

[12] dadddda=aadddddddddddd

Overlap of [8] daddddda=aadddddd with [7] dadddddd=a:

dadddd da dadddddd

Critical pair: aadddddddddddd=dadddda.

Flip LHS and RHS.

Defines rule #17.

Referenced by [14].

[13] dadddc=accccccccccccccccccc

Overlap of [11] daddddc=accccccccccccc with [9] dccccccc=c:

daddd dc dccccccc

Critical pair: accccccccccccccccccc=dadddc.

Flip LHS and RHS.

Defines rule #9.

Referenced by [15].

[14] daddda=aadddddddddddddddddd

Overlap of [12] dadddda=aadddddddddddd with [7] dadddddd=a:

daddd da dadddddd

Critical pair: aadddddddddddddddddd=daddda.

Flip LHS and RHS.

Defines rule #16.

Referenced by [16].

[15] daddc=accccccccccccccccccccccccc

Overlap of [13] dadddc=accccccccccccccccccc with [9] dccccccc=c:

dadd dc dccccccc

Critical pair: accccccccccccccccccccccccc=daddc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [17].

[16] dadda=aadddddddddddddddddddddddd

Overlap of [14] daddda=aadddddddddddddddddd with [7] dadddddd=a:

dadd da dadddddd

Critical pair: aadddddddddddddddddddddddd=dadda.

Flip LHS and RHS.

Defines rule #15.

Referenced by [18].

[17] dadc=accccccccccccccccccccccccccccccc

Overlap of [15] daddc=accccccccccccccccccccccccc with [9] dccccccc=c:

dad dc dccccccc

Critical pair: accccccccccccccccccccccccccccccc=dadc.

Flip LHS and RHS.

Defines rule #7.

Referenced by [19].

[18] dada=aadddddddddddddddddddddddddddddd

Overlap of [16] dadda=aadddddddddddddddddddddddd with [7] dadddddd=a:

dad da dadddddd

Critical pair: aadddddddddddddddddddddddddddddd=dada.

Flip LHS and RHS.

Defines rule #14.

Referenced by [20].

[19] dac=accccccccccccccccccccccccccccccccccccc

Overlap of [17] dadc=accccccccccccccccccccccccccccccc with [9] dccccccc=c:

da dc dccccccc

Critical pair: accccccccccccccccccccccccccccccccccccc=dac.

Flip LHS and RHS.

Defines rule #6.

[20] daa=aadddddddddddddddddddddddddddddddddddd

Overlap of [18] dada=aadddddddddddddddddddddddddddddd with [7] dadddddd=a:

da da dadddddd

Critical pair: aadddddddddddddddddddddddddddddddddddd=daa.

Flip LHS and RHS.

Defines rule #13.

Up:	Monoid enumeration
Prev:	#5 ⟨a, b \| baabababababa=a⟩
Next:	#7 ⟨a, b \| baabababababababa=a⟩