Certificate for #16318 ⟨a, b | aab=bb, babb=ab⟩

Back:⟨a, b | aab=bb, babb=ab⟩

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #1.

Referenced by [3], [5].

[2] babb=ab

Axiom: babb=ab.

Referenced by [3], [4].

[3] bab=abb

Overlap of [1] aab=bb with [2] babb=ab:

aa b babb

Critical pair: aaab=bbabb.

Reduce LHS:

[1]a(aab)
⇒ abb

Reduce RHS:

[2]b(babb)
⇒ bab

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] abbb=ab

Overlap of [2] babb=ab with [3] bab=abb:

babb bab

Critical pair: abbb=ab.

Defines rule #3.

Referenced by [5].

[5] bbbb=bb

Overlap of [1] aab=bb with [4] abbb=ab:

a ab abbb

Critical pair: aab=bbbb.

Reduce LHS:

[1](aab)
⇒ bb

Flip LHS and RHS.

Defines rule #4.