#5109 ⟨a, b | aaabbba=baaa⟩

Quick links

Properties
Rewriting system

Properties

Presentation has sum-of-sides 11
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:
- Right-to-left recursive path with deg(a) = deg(f) = 0, a < f; deg(e) = 1; deg(d) = deg(c) = deg(b) = 2, d < c < b
Auxiliary generators:
1. bbba=c
2. ccc=d
3. dadad=e
4. eaa=f
Certificate: derivations of all rewriting rules from the defining relations.

#	Rule	Proof
1.	a³f³ ⇒ fa²	[23]
2.	a³f²e ⇒ f	[13]
3.	ef ⇒ faf²e	[15]
4.	ea² ⇒ f	[5]
5.	eaf ⇒ fa²f²e	[16]
6.	df ⇒ a³fa²f³af²e²	[22]
7.	da² ⇒ a³e	[12]
8.	daf ⇒ fa²e	[14]
9.	dae ⇒ ead	[8]
10.	cf ⇒ a(a²f)²af²e²	[20]
11.	ca² ⇒ a³d	[11]
12.	caf ⇒ a⁶(faf²)²e²	[21]
13.	bf ⇒ a⁵(afa)²f³(af³a)²f²e³	[26]
14.	baf ⇒ a⁹f(af³)³a²f³af²e³	[28]
15.	ba³ ⇒ a³c	[6]
16.	ba²f ⇒ a⁹fa(af³)³a²f³af²e³	[29]
17.	dc ⇒ cd	[7]
18.	d(ad)² ⇒ e	[4]
19.	(da)²ce ⇒ ec(ad)²	[24]
20.	c³ ⇒ d	[3]
21.	b³a ⇒ c	[2]
22.	(da)²cd ⇒ ec	[9]
23.	(da)²c²e ⇒ ec²(ad)²	[27]
24.	(da)²c²d ⇒ ec²	[25]

# ab:aaabbba=baaa reversed:af/e/dcb bbba=c,ccc=d,dadad=e,eaa=f custom:0
aaafff=faa
aaaffe=f
ef=faffe
eaa=f
eaf=faaffe
df=aaafaafffaffee
daa=aaae
daf=faae
dae=ead
cf=aaafaafaffee
caa=aaad
caf=aaaaaafafffaffee
bf=aaaaaafaafafffafffaafffaffeee
baf=aaaaaaaaafafffafffafffaafffaffeee
baaa=aaac
baaf=aaaaaaaaafaafffafffafffaafffaffeee
dc=cd
dadad=e
dadace=ecadad
ccc=d
bbba=c
dadacd=ec
dadacce=eccadad
dadaccd=ecc