Certificate for #16450 ⟨a, b | aba=bb, aabb=ba⟩

Completion settings:

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

[1] aba=bb

Axiom: aba=bb.

Defines rule #6.

Referenced by [3], [4], [7], [8].

[2] aabb=ba

Axiom: aabb=ba.

Defines rule #5.

Referenced by [4], [5], [6], [8].

[3] bbba=abbb

Overlap of [1] aba=bb with [1] aba=bb:

ab a aba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [8].

[4] abba=bbabb

Overlap of [1] aba=bb with [2] aabb=ba:

ab a aabb

Critical pair: abba=bbabb.

Defines rule #7.

Referenced by [5], [6], [7].

[5] baa=bbabbbb

Overlap of [2] aabb=ba with [4] abba=bbabb:

a abb abba

Critical pair: abbabb=baa.

Reduce LHS:

[4]	(abba)bb
	⇒ bbabbbb

Flip LHS and RHS.

Defines rule #8.

Referenced by [7], [8].

[6] babbbbbbb=bab

Overlap of [4] abba=bbabb with [2] aabb=ba:

abb a aabb

Critical pair: abbba=bbabbabb.

Reduce LHS:

[3]	a(bbba)
[2]	⇒ (aabb)b
	⇒ bab

Reduce RHS:

[4]	bb(abba)bb
[3]	⇒ b(bbba)bbbb
	⇒ babbbbbbb

Flip LHS and RHS.

Defines rule #2.

[7] bbabbbbbb=bba

Overlap of [1] aba=bb with [5] baa=bbabbbb:

a ba baa

Critical pair: abbabbbb=bba.

Reduce LHS:

[4]	(abba)bbbb
	⇒ bbabbbbbb

Defines rule #3.

[8] bbbbbbbbb=bbb

Overlap of [5] baa=bbabbbb with [2] aabb=ba:

ba a aabb

Critical pair: baba=bbabbbbabb.

Reduce LHS:

[1]	b(aba)
	⇒ bbb

Reduce RHS:

[3]	bbab(bbba)bb
[1]	⇒ bb(aba)bbbbb
	⇒ bbbbbbbbb

Flip LHS and RHS.

Defines rule #1.