⟨a, b | aaabbba=baaa⟩

Up:

Format:	Pretty Plain
Word:
	Enter a word above to compute its normal form. Tips: Lowercase letters stand for generators. Spaces are ignored. Numbers repeat the previous letter, e.g. `b90`.
Strategy:	Leftmost Rightmost
Result:	1 1

Auxiliary generators:
1. c = bbba
2. d = ccc
3. e = dadad
4. f = eaa
Reduction order:
- Right-to-left recursive path with deg(a) = deg(f) = 0, a < f; deg(e) = 1; deg(d) = deg(c) = 2, d < c; deg(b) = 3
Certificate: derivations of all rewriting rules from the defining relations.

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

# ab:aaabbba=baaa reversed:af/e/dc/b 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 dc=cd dadad=e dadace=ecadad ccc=d dadacd=ec dadacce=eccadad dadaccd=ecc bf=aaaaaafaafafffafffaafffaffeee baf=aaaaaaaaafafffafffafffaafffaffeee baaa=aaac baaf=aaaaaaaaafaafffafffafffaafffaffeee bbba=c

Up:	Monoid enumeration
Prev:	#5108 ⟨a, b \| aaabbba=abbb⟩
Next:	#5110 ⟨a, b \| aaabbba=baab⟩

#5109 ⟨a, b | aaabbba=baaa⟩

Contents

Properties

Rewriting system