Certificate for #21110 ⟨a, b | bb=aa, abab=aaa⟩

Completion settings:

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

[1] aa=bb

Axiom: bb=aa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2], [3], [5], [6].

[2] abab=bba

Axiom: abab=aaa.

Reduce RHS:

[1]	(aa)a
	⇒ bba

Referenced by [4].

[3] bba=abb

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

a a aa

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #3.

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

[4] abab=abb

Simplify [2] abab=bba.

Reduce RHS:

[3]	(bba)
	⇒ abb

Defines rule #5.

Referenced by [5], [6].

[5] babbb=bbbb

Overlap of [1] aa=bb with [4] abab=abb:

a a abab

Critical pair: aabb=bbbab.

Reduce LHS:

[1]	(aa)bb
	⇒ bbbb

Reduce RHS:

[3]	b(bba)b
	⇒ babbb

Flip LHS and RHS.

Referenced by [7].

[6] abbb=bbbbb

Overlap of [4] abab=abb with [4] abab=abb:

ab ab abab

Critical pair: ababb=abbab.

Reduce LHS:

[4]	(abab)b
	⇒ abbb

Reduce RHS:

[3]	a(bba)b
[1]	⇒ (aa)bbb
	⇒ bbbbb

Defines rule #2.

Referenced by [7].

[7] bbbbbb=bbbb

Simplify [5] babbb=bbbb.

Reduce LHS:

[6]	b(abbb)
	⇒ bbbbbb

Defines rule #1.