Certificate for #3151 ⟨a, b | aa=a, bbb=aba⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] aba=bbb

Axiom: bbb=aba.

Flip LHS and RHS.

Defines rule #2.

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

[3] abbb=bbb

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

a a aba

Critical pair: abbb=aba.

Reduce RHS:

[2](aba)
⇒ bbb

Defines rule #4.

[4] bbba=bbb

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

ab a aa

Critical pair: aba=bbba.

Reduce LHS:

[2](aba)
⇒ bbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] bbbbbb=bbbb

Overlap of [4] bbba=bbb with [2] aba=bbb:

bbb a aba

Critical pair: bbbbbb=bbbba.

Reduce RHS:

[4]b(bbba)
⇒ bbbb

Defines rule #5.