Certificate for #5352 ⟨a, b, c | ab=a, bacb=a⟩

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

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3].

[2] bacb=a

Axiom: bacb=a.

Defines rule #5.

Referenced by [3], [4], [5].

[3] aacb=aa

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

a b bacb

Critical pair: aa=aacb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] baca=aa

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

bac b bacb

Critical pair: baca=aacb.

Reduce RHS:

[3](aacb)
⇒ aa

Defines rule #4.

[5] aaca=aaa

Overlap of [3] aacb=aa with [2] bacb=a:

aac b bacb

Critical pair: aaca=aaacb.

Reduce RHS:

[3]a(aacb)
⇒ aaa

Defines rule #2.