Certificate for #7410 ⟨a, b, c | ab=1, acac=ba⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

Referenced by [4].

[2] acac=ba

Axiom: acac=ba.

Defines rule #2.

Referenced by [3], [5].

[3] baac=acba

Overlap of [2] acac=ba with [2] acac=ba:

ac ac acac

Critical pair: acba=baac.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] aacba=aac

Overlap of [1] ab=1 with [3] baac=acba:

a b baac

Critical pair: aacba=aac.

Defines rule #4.

Referenced by [5].

[5] aaccac=aacbba

Overlap of [4] aacba=aac with [2] acac=ba:

aacb a acac

Critical pair: aacbba=aaccac.

Flip LHS and RHS.

Defines rule #5.