Certificate for #7531 ⟨a, b | aaa=1, abbbbb=b⟩

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

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #3.

Referenced by [3], [5].

[2] abbbbb=b

Axiom: abbbbb=b.

Referenced by [3], [4].

[3] aab=bbbbb

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

aa a abbbbb

Critical pair: aab=bbbbb.

Referenced by [4], [5].

[4] ab=bbbbbbbbb

Overlap of [3] aab=bbbbb with [2] abbbbb=b:

a ab abbbbb

Critical pair: ab=bbbbbbbbb.

Defines rule #2.

Referenced by [5].

[5] bbbbbbbbbbbbb=b

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

aa a ab

Critical pair: aabbbbbbbbb=b.

Reduce LHS:

[3](aab)bbbbbbbb
⇒ bbbbbbbbbbbbb

Defines rule #1.