Certificate for #13237 ⟨a, b | baa=abb, bba=ab⟩

Completion settings:

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

[1] baa=abb

Axiom: baa=abb.

Referenced by [3].

[2] ab=bba

Axiom: bba=ab.

Flip LHS and RHS.

Defines rule #2.

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

[3] baa=bbbba

Simplify [1] baa=abb.

Reduce RHS:

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

Defines rule #3.

Referenced by [4], [5].

[4] bbbbbbbba=bbbbbba

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

ba a ab

Critical pair: babba=bbbbab.

Reduce LHS:

[2]	b(ab)ba
[2]	⇒ bbb(ab)a
[3]	⇒ bbbb(baa)
	⇒ bbbbbbbba

Reduce RHS:

[2]	bbbb(ab)
	⇒ bbbbbba

Referenced by [5].

[5] bbbbbbba=bbbbbba

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

a b baa

Critical pair: abbbba=bbaaa.

Reduce LHS:

[2]	(ab)bbba
[2]	⇒ bb(ab)bba
[2]	⇒ bbbb(ab)ba
[2]	⇒ bbbbbb(ab)a
[4]	⇒ (bbbbbbbba)a
[3]	⇒ bbbbb(baa)
[4]	⇒ b(bbbbbbbba)
	⇒ bbbbbbba

Reduce RHS:

[3]	b(baa)a
[3]	⇒ bbbb(baa)
[4]	⇒ (bbbbbbbba)
	⇒ bbbbbba

Defines rule #1.