Certificate for #16238 ⟨a, b | aab=ba, abbb=ab⟩

Completion settings:

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

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] abbb=ab

Axiom: abbb=ab.

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaab=aaab

Overlap of [2] abbb=ab with [1] ba=aab:

abb b ba

Critical pair: abbaab=aba.

Reduce LHS:

[1]	ab(ba)ab
[1]	⇒ a(ba)abab
[1]	⇒ aaa(ba)bab
[1]	⇒ aaaaab(ba)b
[1]	⇒ aaaaa(ba)abb
[1]	⇒ aaaaaaa(ba)bb
[2]	⇒ aaaaaaaa(abbb)
	⇒ aaaaaaaaab

Reduce RHS:

[1]	a(ba)
	⇒ aaab

Defines rule #1.