Certificate for #13187 ⟨a, b | abb=aaa, bba=ab⟩

Completion settings:

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

[1] aaa=abb

Axiom: abb=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] ab=bba

Axiom: bba=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4], [5].

[3] aaa=bbbba

Simplify [1] aaa=abb.

Reduce RHS:

[2]	(ab)b
[2]	⇒ bb(ab)
	⇒ bbbba

Defines rule #4.

Referenced by [4], [5].

[4] bbbbbbbbaa=bbbbaa

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

a aa aaa

Critical pair: abbbba=bbbbaa.

Reduce LHS:

[2]	(ab)bbba
[2]	⇒ bb(ab)bba
[2]	⇒ bbbb(ab)ba
[2]	⇒ bbbbbb(ab)a
	⇒ bbbbbbbbaa

Referenced by [5], [6].

[5] bbbbbbbba=bbbbbba

Overlap of [3] aaa=bbbba with [2] ab=bba:

aa a ab

Critical pair: aabba=bbbbab.

Reduce LHS:

[2]	a(ab)ba
[2]	⇒ (ab)baba
[2]	⇒ bb(ab)aba
[2]	⇒ bbbba(ab)a
[2]	⇒ bbbb(ab)baa
[2]	⇒ bbbbbb(ab)aa
[4]	⇒ (bbbbbbbbaa)a
[3]	⇒ bbbb(aaa)
	⇒ bbbbbbbba

Reduce RHS:

[2]	bbbb(ab)
	⇒ bbbbbba

Defines rule #1.

Referenced by [6].

[6] bbbbbbaa=bbbbaa

Simplify [4] bbbbbbbbaa=bbbbaa.

Reduce LHS:

[5]	(bbbbbbbba)a
	⇒ bbbbbbaa

Defines rule #3.