Certificate for #16289 ⟨a, b | aab=bb, abaa=aa⟩

Back:⟨a, b | aab=bb, abaa=aa⟩

Completion settings:

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

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

[2] abaa=aa

Axiom: abaa=aa.

Defines rule #5.

Referenced by [3], [4].

[3] aaa=bbaa

Overlap of [1] aab=bb with [2] abaa=aa:

a ab abaa

Critical pair: aaa=bbaa.

Defines rule #4.

[4] abbb=bb

Overlap of [2] abaa=aa with [1] aab=bb:

ab aa aab

Critical pair: abbb=aab.

Reduce RHS:

[1](aab)
⇒ bb

Referenced by [5], [6].

[5] abb=bbbb

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

a ab abbb

Critical pair: abb=bbbb.

Defines rule #2.

Referenced by [6].

[6] bbbbb=bb

Overlap of [4] abbb=bb with [5] abb=bbbb:

abbb abb

Critical pair: bbbbb=bb.

Defines rule #1.