#4342 ⟨a, b | abbabaaab=ba⟩

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(d) = deg(e) = deg(f) = 0, d < e < f; deg(c) = 1; deg(a) = 2; deg(b) = 3
Auxiliary generators:
1. ba=c
2. bcc=d
3. aab=e
4. cedec=f
Certificate: derivations of all rewriting rules from the defining relations.
Morphocompletion: how the auxiliary generators were found.

#	Rule	Proof
1.	cd² ⇒ dfedec	[28]
2.	ecfe ⇒ c	[22]
3.	cdf ⇒ dfe²dec	[29]
4.	ced² ⇒ f²edec	[30]
5.	cded ⇒ d²ec	[12]
6.	cedf ⇒ f²e²dec	[31]
7.	cdef ⇒ (de)²c	[15]
8.	c(ed)² ⇒ fdec	[16]
9.	cedef ⇒ fedec	[17]
10.	cdc ⇒ dfe	[25]
11.	cedc ⇒ f²e	[26]
12.	cdec ⇒ d	[11]
13.	cedec ⇒ f	[5]
14.	cde²cfd ⇒ dcfedec	[35]
15.	cede²cfd ⇒ fcfedec	[37]
16.	c²fe ⇒ ecfc	[27]
17.	cde²cf² ⇒ dcfe²dec	[36]
18.	cede²cf² ⇒ fcfe²dec	[38]
19.	cde²cfc ⇒ dcfe	[33]
20.	cede²cfc ⇒ fcfe	[34]
21.	ad ⇒ ecf	[20]
22.	af ⇒ ec²e²dec	[21]
23.	aed ⇒ e²c²efed(ec)³	[43]
24.	ac ⇒ ec²e	[19]
25.	aecd ⇒ e²c²efed(ec)²	[42]
26.	aecf ⇒ ec²	[24]
27.	ae²cfd ⇒ e²c²efe²def	[47]
28.	ae²cf² ⇒ e²c²ef(e²dec)²	[48]
29.	ae²cfc ⇒ e²c²efe²dece	[44]
30.	aec²d ⇒ e²c²efedec	[39]
31.	aec²e ⇒ ea	[23]
32.	aec²f ⇒ e²c²efe²dec	[40]
33.	a(ec)²fd ⇒ e²c²e(fe)²dec	[45]
34.	a(ec)²f² ⇒ e²c²(ef)²e²dec	[46]
35.	aec³ ⇒ e²c²efe	[32]
36.	a(ec)²fc ⇒ e²c²e(fe)²	[41]
37.	a²b ⇒ e	[4]
38.	bd ⇒ d²(ec)²	[14]
39.	be ⇒ cab	[9]
40.	bf ⇒ cde²dec	[18]
41.	bc ⇒ cde	[8]
42.	ba ⇒ c	[2]

# ab:abbabaaab=ba reversed:def/c/a/b ba=c,bcc=d,aab=e,cedec=f morph:2/0,3/1,3/1,5/1
cdd=dfedec
ecfe=c
cdf=dfeedec
cedd=ffedec
cded=ddec
cedf=ffeedec
cdef=dedec
ceded=fdec
cedef=fedec
cdc=dfe
cedc=ffe
cdec=d
cedec=f
cdeecfd=dcfedec
cedeecfd=fcfedec
ccfe=ecfc
cdeecff=dcfeedec
cedeecff=fcfeedec
cdeecfc=dcfe
cedeecfc=fcfe
ad=ecf
af=ecceedec
aed=eeccefedececec
ac=ecce
aecd=eeccefedecec
aecf=ecc
aeecfd=eeccefeedef
aeecff=eeccefeedeceedec
aeecfc=eeccefeedece
aeccd=eeccefedec
aecce=ea
aeccf=eeccefeedec
aececfd=eeccefefedec
aececff=eeccefefeedec
aeccc=eeccefe
aececfc=eeccefefe
aab=e
bd=ddecec
be=cab
bf=cdeedec
bc=cde
ba=c