Certificate for #16380 ⟨a, b | aba=ab, aaab=bb⟩

Back:⟨a, b | aba=ab, aaab=bb⟩

Completion settings:

[1] aba=ab

Axiom: aba=ab.

Defines rule #1.

Referenced by [3], [4].

[2] aaab=bb

Axiom: aaab=bb.

Defines rule #3.

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

[3] abbb=abb

Overlap of [1] aba=ab with [2] aaab=bb:

ab a aaab

Critical pair: abbb=abaab.

Reduce RHS:

[1](aba)ab
[1]⇒ (aba)b
⇒ abb

Defines rule #4.

[4] bba=bb

Overlap of [2] aaab=bb with [1] aba=ab:

aa ab aba

Critical pair: aaab=bba.

Reduce LHS:

[2](aaab)
⇒ bb

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] bbbb=bbb

Overlap of [4] bba=bb with [2] aaab=bb:

bb a aaab

Critical pair: bbbb=bbaab.

Reduce RHS:

[4](bba)ab
[4]⇒ (bba)b
⇒ bbb

Defines rule #5.