Certificate for #13137 ⟨a, b | aab=aaa, bba=ab⟩

Completion settings:

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

[1] aaa=aab

Axiom: aab=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] ab=bba

Axiom: bba=ab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3], [4].

[3] aaa=bbbbaa

Simplify [1] aaa=aab.

Reduce RHS:

[2]	a(ab)
[2]	⇒ (ab)ba
[2]	⇒ bb(ab)a
	⇒ bbbbaa

Defines rule #3.

Referenced by [4].

[4] bbbbbbbbbbbbaa=bbbbbbbbaa

Overlap of [3] aaa=bbbbaa with [3] aaa=bbbbaa:

a aa aaa

Critical pair: abbbbaa=bbbbaaa.

Reduce LHS:

[2]	(ab)bbbaa
[2]	⇒ bb(ab)bbaa
[2]	⇒ bbbb(ab)baa
[2]	⇒ bbbbbb(ab)aa
[3]	⇒ bbbbbbbb(aaa)
	⇒ bbbbbbbbbbbbaa

Reduce RHS:

[3]	bbbb(aaa)
	⇒ bbbbbbbbaa

Defines rule #2.