Certificate for #16260 ⟨a, b | aab=ba, bbaa=bb⟩

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 #1.

Referenced by [2].

[2] aaaaaaaabb=bb

Axiom: bbaa=bb.

Reduce LHS:

[1]	b(ba)a
[1]	⇒ (ba)aba
[1]	⇒ aa(ba)ba
[1]	⇒ aaaab(ba)
[1]	⇒ aaaa(ba)ab
[1]	⇒ aaaaaa(ba)b
	⇒ aaaaaaaabb

Defines rule #2.