Certificate for #16545 ⟨a, b | aba=bb, abb=aaa⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(a) = 0; deg(b) = 1

[1] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [2], [3], [5], [6].

[2] aaba=aaa

Axiom: abb=aaa.

Reduce LHS:

[1]	a(bb)
	⇒ aaba

Defines rule #3.

Referenced by [4], [5], [6], [7].

[3] baba=abab

Overlap of [1] bb=aba with [1] bb=aba:

b b bb

Critical pair: baba=abab.

Defines rule #7.

Referenced by [4], [5], [6], [7].

[4] aaaab=aaaa

Overlap of [2] aaba=aaa with [3] baba=abab:

aa ba baba

Critical pair: aaabab=aaaba.

Reduce LHS:

[2]	a(aaba)b
	⇒ aaaab

Reduce RHS:

[2]	a(aaba)
	⇒ aaaa

Defines rule #2.

Referenced by [5], [7].

[5] aaaaaa=aaaa

Overlap of [3] baba=abab with [2] aaba=aaa:

bab a aaba

Critical pair: babaaa=abababa.

Reduce LHS:

[3]	(baba)aa
[3]	⇒ a(baba)a
[2]	⇒ (aaba)ba
[2]	⇒ a(aaba)
	⇒ aaaa

Reduce RHS:

[3]	a(baba)ba
[2]	⇒ (aaba)bba
[1]	⇒ aaa(bb)a
[4]	⇒ (aaaab)aa
	⇒ aaaaaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[6] baaab=abaaaa

Overlap of [3] baba=abab with [3] baba=abab:

ba ba baba

Critical pair: baabab=ababba.

Reduce LHS:

[2]	b(aaba)b
	⇒ baaab

Reduce RHS:

[1]	aba(bb)a
[2]	⇒ ab(aaba)a
	⇒ abaaaa

Referenced by [7], [8].

[7] baaaa=aaaa

Overlap of [3] baba=abab with [6] baaab=abaaaa:

ba ba baaab

Critical pair: baabaaaa=ababaab.

Reduce LHS:

[2]	b(aaba)aaa
[5]	⇒ b(aaaaaa)
	⇒ baaaa

Reduce RHS:

[3]	a(baba)ab
[2]	⇒ (aaba)bab
[2]	⇒ a(aaba)b
[4]	⇒ (aaaab)
	⇒ aaaa

Defines rule #4.

Referenced by [8].

[8] baaab=aaaaa

Simplify [6] baaab=abaaaa.

Reduce RHS:

[7]	a(baaaa)
	⇒ aaaaa

Defines rule #6.