#5077 ⟨a, b | aaabbaa=baaa⟩

Contents

Properties
Rewriting system

Properties

Sum of relation sides is 11
Infinite non-cancellative non-commutative monoid
Element a has infinite order
Not right cancellative, because right multiplication by d is not injective:
- ca ⋅ d = ad² and ad ⋅ d = ad², however ca ≠ ad

Rewriting system

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 = abb
2. d = aacac
Reduction order:
- Right-to-left recursive path with deg(a) = deg(d) = 0, a < d; deg(c) = deg(b) = 1, c < b
Certificate: derivations of all rewriting rules from the defining relations.
Morphocompletion: how the auxiliary generators were found.

#	Rule	Proof
1.	a³dad² ⇒ dad	[24]
2.	a³dada² ⇒ da³	[28]
3.	a²(ad)³ ⇒ da²d	[30]
4.	a³(da)²c ⇒ da²c	[25]
5.	a³dcd ⇒ d²	[33]
6.	a³dadcd ⇒ dacd	[34]
7.	cad ⇒ ad²	[12]
8.	cd² ⇒ ada²dcd	[35]
9.	ca³ ⇒ ada²	[23]
10.	ca²d ⇒ (ad)²	[21]
11.	cdad ⇒ (ada)²d²	[27]
12.	cda³ ⇒ (ada)²da²	[29]
13.	cda²d ⇒ ada(ad)³	[31]
14.	bd ⇒ dac	[10]
15.	bad ⇒ a²cd	[7]
16.	ba³ ⇒ a²ca²	[4]
17.	ba²d ⇒ a³d²	[20]
18.	a(ac)² ⇒ d	[3]
19.	ad(ac)² ⇒ cd	[11]
20.	ca²c ⇒ adac	[14]
21.	cda²c ⇒ (ada)²dac	[26]
22.	c²d ⇒ ad²(ac)²	[19]
23.	cacd ⇒ adcd	[32]
24.	(cd)² ⇒ (ada)²d²(ac)²	[37]
25.	cdacd ⇒ (ada)²dcd	[36]
26.	ba²c ⇒ d	[6]
27.	a³dadbcd ⇒ dabcd	[44]
28.	a³(da)²bcd ⇒ da²bcd	[46]
29.	bacd ⇒ a³d²(ac)²	[22]
30.	ab² ⇒ c	[2]
31.	a²cd(ac)² ⇒ bcd	[16]
32.	cbcd ⇒ a(dac)²ac	[41]
33.	cabcd ⇒ adbcd	[42]
34.	cdbcd ⇒ (ada)²(dac)²ac	[48]
35.	ca²bcd ⇒ adabcd	[43]
36.	cdabcd ⇒ (ada)²dbcd	[45]
37.	cda²bcd ⇒ (ada)²dabcd	[47]
38.	b²cd ⇒ d²(ac)²	[40]
39.	babcd ⇒ a³(dac)²ac	[38]
40.	ba²bcd ⇒ a³dbcd	[39]

# ab:aaabbaa=baaa reversed:ad/cb abb=c,aacac=d morph:3/2,5/1
aaadadd=dad
aaadadaa=daaa
aaadadad=daad
aaadadac=daac
aaadcd=dd
aaadadcd=dacd
cad=add
cdd=adaadcd
caaa=adaa
caad=adad
cdad=adaadadd
cdaaa=adaadadaa
cdaad=adaadadad
bd=dac
bad=aacd
baaa=aacaa
baad=aaadd
aacac=d
adacac=cd
caac=adac
cdaac=adaadadac
ccd=addacac
cacd=adcd
cdcd=adaadaddacac
cdacd=adaadadcd
baac=d
aaadadbcd=dabcd
aaadadabcd=daabcd
bacd=aaaddacac
abb=c
aacdacac=bcd
cbcd=adacdacac
cabcd=adbcd
cdbcd=adaadadacdacac
caabcd=adabcd
cdabcd=adaadadbcd
cdaabcd=adaadadabcd
bbcd=ddacac
babcd=aaadacdacac
baabcd=aaadbcd