Certificate for #11510 ⟨a, b | ababa=a, bbaaa=1⟩

Completion settings:

[1] ababa=a

Axiom: ababa=a.

Referenced by [3].

[2] bbaaa=1

Axiom: bbaaa=1.

Defines rule #2.

Referenced by [3].

[3] baba=1

Overlap of [2] bbaaa=1 with [1] ababa=a:

bbaa a ababa

Critical pair: bbaaa=baba.

Reduce LHS:

[2](bbaaa)
⇒ 1

Flip LHS and RHS.

Defines rule #1.