Certificate for #5384 ⟨a, b, c | ab=a, bcac=b⟩

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

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3].

[2] bcac=b

Axiom: bcac=b.

Defines rule #5.

Referenced by [3], [4].

[3] acac=a

Overlap of [1] ab=a with [2] bcac=b:

a b bcac

Critical pair: ab=acac.

Reduce LHS:

[1](ab)
⇒ a

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] bac=bca

Overlap of [2] bcac=b with [3] acac=a:

bc ac acac

Critical pair: bca=bac.

Flip LHS and RHS.

Defines rule #3.

[5] aac=aca

Overlap of [3] acac=a with [3] acac=a:

ac ac acac

Critical pair: aca=aac.

Flip LHS and RHS.

Defines rule #2.