⟨a, b | ababbba=bbab⟩

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

#	Rule	Proof
1.	b²ab ⇒ abc	[3]
2.	ab³a ⇒ c	[2]
3.	(ab)²c ⇒ cb	[5]
4.	abcb²a ⇒ b²c	[6]
5.	abcbab ⇒ b²a²bc	[7]
6.	(abc)² ⇒ b²cb	[8]
7.	cb³a ⇒ ab³c	[4]
8.	ab³cb ⇒ cbabc	[11]
9.	abc²b²a ⇒ b⁴c	[9]
10.	b⁴a²bc ⇒ abc²bab	[15]
11.	ab⁵c ⇒ cbcb²a	[19]
12.	(ab)³b²c ⇒ cb⁴a	[13]
13.	b⁴cb ⇒ abc²abc	[10]
14.	a(bcb)² ⇒ b²cbabc	[12]
15.	b⁶c ⇒ abc³b²a	[18]
16.	b²a²bc²bab ⇒ abab³cabc	[16]
17.	abcb⁴c ⇒ b(bc)²b²a	[21]
18.	abcabab³c ⇒ b²cb⁴a	[14]
19.	abcb³cb ⇒ b²a²bc²abc	[17]
20.	abcb⁵c ⇒ b²a²bc³b²a	[20]
21.	b⁴a²bab³c ⇒ abc²bab⁴a	[25]
22.	b²a²bab³cabc ⇒ abcba²bc²bab	[22]
23.	c(ba)²b³cabc ⇒ ab³cabc²bab	[24]
24.	b²a²bcab³cabc ⇒ abab³cabc²bab	[31]
25.	b²a²bc²b³cb ⇒ abab³(cabc)²	[26]
26.	abcba²bab³cabc ⇒ b(ba²bc)²cbab	[27]
27.	abc²abab³cabc ⇒ b⁴cabc²bab	[23]
28.	(ab³cab)²c ⇒ cbabcba²bc²bab	[29]
29.	b²a²bc²b⁵c ⇒ abab³cabc³b²a	[32]
30.	b²a(abab³c)² ⇒ abcba²bc²bab⁴a	[35]
31.	b⁴cabab³cabc ⇒ abc²abcba²bc²bab	[28]
32.	abcb²cabab³cabc ⇒ b(bcba)²abc²bab	[30]
33.	cb(abab³c)² ⇒ ab³cabc²bab⁴a	[37]
34.	b²a²bcab³cabab³c ⇒ abab³cabc²bab⁴a	[39]
35.	b²a²bc²ba²bab³cabc ⇒ abab³cabcba²bc²bab	[33]
36.	abcba(abab³c)² ⇒ b(ba²bc)²cbab⁴a	[41]
37.	abcb³cabab³cabc ⇒ b²a²bc²abcba²bc²bab	[34]
38.	abc²(abab³c)² ⇒ b⁴cabc²bab⁴a	[36]
39.	ab³c(abab³c)² ⇒ cbabcba²bc²bab⁴a	[40]
40.	b⁴c(abab³c)² ⇒ abc²abcba²bc²bab⁴a	[42]
41.	abcb²c(abab³c)² ⇒ b(bcba)²abc²bab⁴a	[43]
42.	b²a²bc²ba(abab³c)² ⇒ abab³cabcba²bc²bab⁴a	[45]
43.	b²a²bc²b³cabab³cabc ⇒ abab³(cabc)²ba²bc²bab	[38]
44.	abcb³c(abab³c)² ⇒ b²a²bc²abcba²bc²bab⁴a	[44]
45.	b²a²bc²b³c(abab³c)² ⇒ abab³(cabc)²ba²bc²bab⁴a	[46]

# ab:ababbba=bbab a/bc abbba=c morph:5/0 bbab=abc abbba=c ababc=cb abcbba=bbc abcbab=bbaabc abcabc=bbcb cbbba=abbbc abbbcb=cbabc abccbba=bbbbc bbbbaabc=abccbab abbbbbc=cbcbba abababbbc=cbbbba bbbbcb=abccabc abcbbcb=bbcbabc bbbbbbc=abcccbba bbaabccbab=ababbbcabc abcbbbbc=bbcbcbba abcababbbc=bbcbbbba abcbbbcb=bbaabccabc abcbbbbbc=bbaabcccbba bbbbaababbbc=abccbabbbba bbaababbbcabc=abcbaabccbab cbababbbcabc=abbbcabccbab bbaabcabbbcabc=ababbbcabccbab bbaabccbbbcb=ababbbcabccabc abcbaababbbcabc=bbaabcbaabccbab abccababbbcabc=bbbbcabccbab abbbcababbbcabc=cbabcbaabccbab bbaabccbbbbbc=ababbbcabcccbba bbaababbbcababbbc=abcbaabccbabbbba bbbbcababbbcabc=abccabcbaabccbab abcbbcababbbcabc=bbcbabcbaabccbab cbababbbcababbbc=abbbcabccbabbbba bbaabcabbbcababbbc=ababbbcabccbabbbba bbaabccbaababbbcabc=ababbbcabcbaabccbab abcbaababbbcababbbc=bbaabcbaabccbabbbba abcbbbcababbbcabc=bbaabccabcbaabccbab abccababbbcababbbc=bbbbcabccbabbbba abbbcababbbcababbbc=cbabcbaabccbabbbba bbbbcababbbcababbbc=abccabcbaabccbabbbba abcbbcababbbcababbbc=bbcbabcbaabccbabbbba bbaabccbaababbbcababbbc=ababbbcabcbaabccbabbbba bbaabccbbbcababbbcabc=ababbbcabccabcbaabccbab abcbbbcababbbcababbbc=bbaabccabcbaabccbabbbba bbaabccbbbcababbbcababbbc=ababbbcabccabcbaabccbabbbba