⟨a, b | aabbbbaa=ab⟩

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 = abbb
Reduction order:
- Right-to-left shortlex with a < c < b
Certificate: derivations of all rewriting rules from the defining relations.
Morphocompletion: how the auxiliary generators were found.

#	Rule	Proof
1.	ab³ ⇒ c	[2]
2.	acba² ⇒ ab	[3]
3.	c²ba² ⇒ cb	[11]
4.	acbac ⇒ cb	[4]
5.	acbab ⇒ cb²a²	[7]
6.	a(cb)² ⇒ cb²ac	[8]
7.	cb⁴ ⇒ c²bac	[13]
8.	abcba² ⇒ ab²	[5]
9.	(cb)²a² ⇒ cb²	[12]
10.	abcbac ⇒ cb²	[6]
11.	abcbab ⇒ cb³a²	[18]
12.	c²bacb ⇒ (cb)²ac	[14]
13.	ab(cb)² ⇒ cb³ac	[19]
14.	cb²aca² ⇒ acb²	[27]
15.	ab²cba² ⇒ c	[9]
16.	cb²cba² ⇒ cb³	[15]
17.	ab²cbac ⇒ cb³	[10]
18.	ab²cbab ⇒ c²baca²	[21]
19.	(cb)²acb ⇒ cb²cbac	[17]
20.	ab²(cb)² ⇒ c²b(ac)²	[26]
21.	cb²a²b² ⇒ acbc	[22]
22.	(cb)²aca² ⇒ c²bab	[23]
23.	cb³aca² ⇒ abcb²	[32]
24.	cb³cba² ⇒ c²bac	[16]
25.	(cb)²(ac)² ⇒ c(cb)²	[28]
26.	(cb)²acab ⇒ c²bcb²a²	[40]
27.	cb²(ac)²b ⇒ acb²cbac	[34]
28.	cb²cbacb ⇒ cb³cbac	[20]
29.	(cb)²ac²b ⇒ c²bcb²ac	[41]
30.	cb³a²b² ⇒ a(bc)²	[38]
31.	cb²acb³ ⇒ acbc²bac	[31]
32.	c²b(ac)²a² ⇒ ab²cb²	[33]
33.	cb²(ac)²a² ⇒ ac²bab	[43]
34.	cb²cbaca² ⇒ (cb)²ab	[24]
35.	cb²(ac)³ ⇒ ac(cb)²	[48]
36.	cb²cb(ac)² ⇒ (cb)³	[29]
37.	cb²a(ca)²b ⇒ ac²bcb²a²	[60]
38.	cb²cbacab ⇒ (cb)³ba²	[52]
39.	cb³(ac)²b ⇒ a(bcb)²ac	[47]
40.	cb³cbacb ⇒ (c²ba)²c	[35]
41.	cb²acac²b ⇒ ac²bcb²ac	[61]
42.	cb²cbac²b ⇒ (cb)³bac	[53]
43.	c²baca²b² ⇒ ab(bc)²	[39]
44.	cb³acb³ ⇒ abcbc²bac	[42]
45.	cb³(ac)²a² ⇒ abc²bab	[45]
46.	cb³cbaca² ⇒ cb²cbab	[25]
47.	cb³(ac)³ ⇒ abc(cb)²	[50]
48.	cb³cb(ac)² ⇒ cb²(cb)²	[30]
49.	cb³a(ca)²b ⇒ abc²bcb²a²	[63]
50.	cb³cbacab ⇒ cb(bc)²b²a²	[67]
51.	c²b(ac)³b ⇒ a(b²c)²bac	[55]
52.	cb³acac²b ⇒ abc²bcb²ac	[70]
53.	cb³cbac²b ⇒ cb(bc)²b²ac	[68]
54.	c²b(ac)²b³ ⇒ ab²cbc²bac	[54]
55.	c²b(ac)³a² ⇒ ab²c²bab	[56]
56.	(c²ba)²ca² ⇒ cb³cbab	[36]
57.	cb²ac²baca² ⇒ acbc²bab	[44]
58.	c²b(ac)⁴ ⇒ ab²c(cb)²	[58]
59.	(c²ba)²cac ⇒ cb³(cb)²	[37]
60.	cb²ac²b(ac)² ⇒ a(cbc)²b	[49]
61.	c²ba(ca)³b ⇒ ab²c²bcb²a²	[65]
62.	(c²ba)²cab ⇒ cb³cbcb²a²	[74]
63.	cb²ac²bacab ⇒ a(cbc)²b²a²	[62]
64.	c²b(ac)³cb ⇒ ab²c²bcb²ac	[72]
65.	c²b(ac²b)² ⇒ cb³cbcb²ac	[75]
66.	cb²(ac²b)² ⇒ a(cbc)²b²ac	[69]
67.	cb³ac²baca² ⇒ abcbc²bab	[46]
68.	cb³ac²b(ac)² ⇒ ab(cbc)²b	[51]
69.	cb³ac²bacab ⇒ ab(cbc)²b²a²	[64]
70.	cb³(ac²b)² ⇒ ab(cbc)²b²ac	[71]
71.	(c²baca)²a ⇒ ab²cbc²bab	[57]
72.	c(cb(ac)²)² ⇒ ab²(cbc)²b	[59]
73.	(c²baca)²b ⇒ ab²(cbc)²b²a²	[66]
74.	c²bac(ac²b)² ⇒ ab²(cbc)²b²ac	[73]

Up:	Monoids with two generators and one relation
Prev:	#2008 ⟨a, b \| aabbbbaa=aa⟩
Next:	#2010 ⟨a, b \| aabbbbaa=bb⟩

#2009 ⟨a, b | aabbbbaa=ab⟩

Quick links

Properties

Rewriting system