Certificate for #5604 ⟨a, b, c | ab=c, cbac=a⟩

Back:⟨a, b, c | ab=c, cbac=a⟩

Completion settings:

[1] c=ab

Axiom: ab=c.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2].

[2] abbaab=a

Axiom: cbac=a.

Reduce LHS:

[1](c)bac
[1]⇒ abba(c)
⇒ abbaab

Defines rule #3.

Referenced by [3], [4].

[3] abaab=abbaa

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

abba ab abbaab

Critical pair: abbaa=abaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] aaab=abaa

Overlap of [2] abbaab=a with [3] abaab=abbaa:

abba ab abaab

Critical pair: abbaabbaa=aaab.

Reduce LHS:

[2](abbaab)baa
⇒ abaa

Flip LHS and RHS.

Defines rule #1.