Certificate for #4553 ⟨a, b, c | abc=1, baab=a⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Defines rule #2.

Referenced by [3].

[2] baab=a

Axiom: baab=a.

Defines rule #3.

Referenced by [3], [4].

[3] ac=ba

Overlap of [2] baab=a with [1] abc=1:

ba ab abc

Critical pair: ba=ac.

Flip LHS and RHS.

Defines rule #1.

[4] aaab=baaa

Overlap of [2] baab=a with [2] baab=a:

baa b baab

Critical pair: baaa=aaab.

Flip LHS and RHS.

Defines rule #4.