⟨a, b | ababaaab=baa⟩

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

#	Rule	Proof
1.	cbcab ⇒ abc	[8]
2.	ba² ⇒ abcab	[3]
3.	ca² ⇒ a²bc²	[7]
4.	(cab)² ⇒ abac	[10]
5.	c(ba)²c ⇒ abc²ab	[15]
6.	c²ab²cab ⇒ a²(bc)²	[9]
7.	a²bcab ⇒ c	[4]
8.	a(bcab)² ⇒ bc	[5]
9.	ca(ba)²c ⇒ abac²ab	[16]
10.	c²(ab)²cab ⇒ a²bcbac	[11]
11.	c²ab(ba)²c ⇒ a²bcbc²ab	[17]
12.	a²(ba)²c ⇒ c²ab	[12]
13.	(abcab)² ⇒ bac	[6]
14.	abcab(ba)²c ⇒ bc²ab	[13]
15.	c²a(ba)³c ⇒ a²bcbac²ab	[18]
16.	abca(ba)³c ⇒ bac²ab	[14]

# ab:ababaaab=baa bc/a abaa=c morph:4/0 cbcab=abc baa=abcab caa=aabcc cabcab=abac cbabac=abccab ccabbcab=aabcbc aabcab=c abcabbcab=bc cababac=abaccab ccababcab=aabcbac ccabbabac=aabcbccab aababac=ccab abcababcab=bac abcabbabac=bccab ccabababac=aabcbaccab abcabababac=baccab