Certificate for #2443 ⟨a, b | aaa=1, abbbb=b⟩

Back:⟨a, b | aaa=1, abbbb=b⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #3.

Referenced by [3], [5].

[2] abbbb=b

Axiom: abbbb=b.

Referenced by [3], [4].

[3] aab=bbbb

Overlap of [1] aaa=1 with [2] abbbb=b:

aa a abbbb

Critical pair: aab=bbbb.

Referenced by [4], [5].

[4] ab=bbbbbbb

Overlap of [3] aab=bbbb with [2] abbbb=b:

a ab abbbb

Critical pair: ab=bbbbbbb.

Defines rule #2.

Referenced by [5].

[5] bbbbbbbbbb=b

Overlap of [1] aaa=1 with [4] ab=bbbbbbb:

aa a ab

Critical pair: aabbbbbbb=b.

Reduce LHS:

[3](aab)bbbbbb
⇒ bbbbbbbbbb

Defines rule #1.