Certificate for #5139 ⟨a, b, c | aa=a, bacb=a⟩

Back:⟨a, b, c | aa=a, bacb=a⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] bacb=a

Axiom: bacb=a.

Referenced by [3], [5].

[3] acb=baca

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

bac b bacb

Critical pair: baca=aacb.

Reduce RHS:

[1](aa)cb
⇒ acb

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] abaca=baca

Overlap of [1] aa=a with [3] acb=baca:

a a acb

Critical pair: abaca=acb.

Reduce RHS:

[3](acb)
⇒ baca

Defines rule #2.

[5] bbaca=a

Overlap of [2] bacb=a with [3] acb=baca:

b acb acb

Critical pair: bbaca=a.

Defines rule #4.