Certificate for #27641 ⟨a, b | aa=1, ababab=bbb⟩

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

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [3].

[2] ababab=bbb

Axiom: ababab=bbb.

Referenced by [3], [4].

[3] babab=abbb

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

a a ababab

Critical pair: abbb=babab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[4] bbbab=abbbb

Overlap of [2] ababab=bbb with [2] ababab=bbb:

ab abab ababab

Critical pair: abbbb=bbbab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] bbabbb=ababbbb

Overlap of [4] bbbab=abbbb with [3] babab=abbb:

bb bab babab

Critical pair: bbabbb=abbbbab.

Reduce RHS:

[4]ab(bbbab)
⇒ ababbbb

Defines rule #4.