Certificate for #3645 ⟨a, b | aa=1, abab=bbb⟩

Back:⟨a, b | aa=1, abab=bbb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #3.

Referenced by [3].

[2] abab=bbb

Axiom: abab=bbb.

Referenced by [3], [4].

[3] bab=abbb

Overlap of [1] aa=1 with [2] abab=bbb:

a a abab

Critical pair: abbb=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] bbbbbbb=bbbb

Overlap of [3] bab=abbb with [2] abab=bbb:

b ab abab

Critical pair: bbbb=abbbab.

Reduce RHS:

[3]abb(bab)
[3]⇒ ab(bab)bb
[2]⇒ (abab)bbbb
⇒ bbbbbbb

Flip LHS and RHS.

Defines rule #1.