Certificate for #9149 ⟨a, b | aa=a, abab=bbb⟩

Completion settings:

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

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [4].

[2] bbb=abab

Axiom: abab=bbb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] babab=ababb

Overlap of [2] bbb=abab with [2] bbb=abab:

b bb bbb

Critical pair: babab=ababb.

Defines rule #3.

Referenced by [4].

[4] ababbab=ababb

Overlap of [2] bbb=abab with [3] babab=ababb:

bb b babab

Critical pair: bbababb=abababab.

Reduce LHS:

[3]	b(babab)b
[3]	⇒ (babab)bb
[2]	⇒ aba(bbb)b
[1]	⇒ ab(aa)babb
[3]	⇒ a(babab)b
[1]	⇒ (aa)babbb
[2]	⇒ aba(bbb)
[1]	⇒ ab(aa)bab
[3]	⇒ a(babab)
[1]	⇒ (aa)babb
	⇒ ababb

Reduce RHS:

[3]	a(babab)ab
[1]	⇒ (aa)babbab
	⇒ ababbab

Flip LHS and RHS.

Defines rule #4.