#2617 ⟨a, b | abbaab=aaba⟩

Quick links

Properties
Rewriting system

Properties

Presentation has sum-of-sides 10
Infinite non-cancellative non-commutative monoid
Not left cancellative, because left multiplication by a is not injective:
- a ⋅ b²a²b = a²ba and a ⋅ aba = a²ba, however b²a²b ≠ aba
Enveloping group: ⟨a, b | aabab^-1abb⟩

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

Auxiliary generators:
1. c = ab
2. d = cbcb
Reduction order:
- Left-to-right recursive path with deg(b) = 0; deg(c) = deg(a) = deg(d) = 1, c < a < d
Certificate: derivations of all rewriting rules from the defining relations.
Morphocompletion: how the auxiliary generators were found.

#	Rule	Proof
1.	ab ⇒ c	[2]
2.	(cb)² ⇒ d	[3]
3.	dcb ⇒ cbd	[6]
4.	ac² ⇒ cbacb	[7]
5.	aca ⇒ cbac	[5]
6.	cbacb²cb ⇒ acd	[9]
7.	dacb²cb ⇒ cbacd	[10]
8.	cbacb²ac ⇒ dacba	[8]
9.	dacbc²b ⇒ cbacb²ad	[13]
10.	dacbac ⇒ acdacb	[15]
11.	dacb²ac ⇒ cbdacba	[11]
12.	dacba² ⇒ acdac	[14]
13.	(da)²cb² ⇒ acdad	[25]
14.	acdacbc ⇒ (da)²cb	[18]
15.	acdacb³cb ⇒ da²cd	[21]
16.	acdacba ⇒ (da)²c	[12]
17.	acdacb³ac ⇒ (da)²cba	[19]
18.	dacbcacb²cb ⇒ cbacb²a²cd	[17]
19.	(dacb)²c ⇒ ac(da)²cb	[23]
20.	(dacb)²b²cb ⇒ acda²cd	[26]
21.	(dacb)²a ⇒ ac(da)²c	[22]
22.	dacbcacb²ac ⇒ cbacb²adacba	[16]
23.	dacbadacbc ⇒ cbacb²(da)²cb	[24]
24.	dacbadacb³cb ⇒ cbacb²da²cd	[27]
25.	(dacba)² ⇒ cbacb²(da)²c	[20]
26.	(dacb)²b²ac ⇒ ac(da)²cba	[28]
27.	dacbadacb³ac ⇒ cbacb²(da)²cba	[29]

# ab:abbaab=aaba b/cad ab=c,cbcb=d morph:2/1,4/1
ab=c
cbcb=d
dcb=cbd
acc=cbacb
aca=cbac
cbacbbcb=acd
dacbbcb=cbacd
cbacbbac=dacba
dacbccb=cbacbbad
dacbac=acdacb
dacbbac=cbdacba
dacbaa=acdac
dadacbb=acdad
acdacbc=dadacb
acdacbbbcb=daacd
acdacba=dadac
acdacbbbac=dadacba
dacbcacbbcb=cbacbbaacd
dacbdacbc=acdadacb
dacbdacbbbcb=acdaacd
dacbdacba=acdadac
dacbcacbbac=cbacbbadacba
dacbadacbc=cbacbbdadacb
dacbadacbbbcb=cbacbbdaacd
dacbadacba=cbacbbdadac
dacbdacbbbac=acdadacba
dacbadacbbbac=cbacbbdadacba