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

Back:⟨a, b | aa=a, abab=bbb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abab=bbb

Axiom: abab=bbb.

Defines rule #2.

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

[3] abbb=bbb

Overlap of [1] aa=a with [2] abab=bbb:

a a abab

Critical pair: abbb=abab.

Reduce RHS:

[2](abab)
⇒ bbb

Defines rule #3.

Referenced by [4], [5].

[4] bbbab=bbbb

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

ab ab abab

Critical pair: abbbb=bbbab.

Reduce LHS:

[3](abbb)b
⇒ bbbb

Flip LHS and RHS.

Defines rule #4.

[5] bbbbb=bbbb

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

ab ab abbb

Critical pair: abbbb=bbbbb.

Reduce LHS:

[3](abbb)b
⇒ bbbb

Flip LHS and RHS.

Defines rule #5.