Certificate for #3064 ⟨a, b, c | abc=a, bca=c⟩

Completion settings:

[1] abc=a

Axiom: abc=a.

Defines rule #3.

Referenced by [3], [4].

[2] bca=c

Axiom: bca=c.

Defines rule #4.

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

[3] ac=aa

Overlap of [1] abc=a with [2] bca=c:

a bc bca

Critical pair: ac=aa.

Defines rule #1.

Referenced by [5].

[4] cbc=c

Overlap of [2] bca=c with [1] abc=a:

bc a abc

Critical pair: bca=cbc.

Reduce LHS:

[2](bca)
⇒ c

Flip LHS and RHS.

Defines rule #5.

[5] cc=ca

Overlap of [2] bca=c with [3] ac=aa:

bc a ac

Critical pair: bcaa=cc.

Reduce LHS:

[2](bca)a
⇒ ca

Flip LHS and RHS.

Defines rule #2.