Certificate for #16253 ⟨a, b | aab=ba, babb=aa⟩

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 [2], [3].

[2] aabbb=aa

Axiom: babb=aa.

Reduce LHS:

[1]	(ba)bb
	⇒ aabbb

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaa=aaa

Overlap of [2] aabbb=aa with [1] ba=aab:

aabb b ba

Critical pair: aabbaab=aaa.

Reduce LHS:

[1]	aab(ba)ab
[1]	⇒ aa(ba)abab
[1]	⇒ aaaa(ba)bab
[1]	⇒ aaaaaab(ba)b
[1]	⇒ aaaaaa(ba)abb
[1]	⇒ aaaaaaaa(ba)bb
[2]	⇒ aaaaaaaa(aabbb)
	⇒ aaaaaaaaaa

Defines rule #1.