Certificate for #4582 ⟨a, b, c | abc=1, bcaa=b⟩

Back:⟨a, b, c | abc=1, bcaa=b⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Referenced by [3], [4].

[2] bcaa=b

Axiom: bcaa=b.

Defines rule #5.

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

[3] ab=aa

Overlap of [1] abc=1 with [2] bcaa=b:

a bc bcaa

Critical pair: ab=aa.

Defines rule #1.

Referenced by [4], [5].

[4] aac=1

Overlap of [1] abc=1 with [3] ab=aa:

abc ab

Critical pair: aac=1.

Defines rule #3.

Referenced by [6].

[5] bb=ba

Overlap of [2] bcaa=b with [3] ab=aa:

bca a ab

Critical pair: bcaaa=bb.

Reduce LHS:

[2](bcaa)a
⇒ ba

Flip LHS and RHS.

Defines rule #2.

[6] bac=bca

Overlap of [2] bcaa=b with [4] aac=1:

bca a aac

Critical pair: bca=bac.

Flip LHS and RHS.

Defines rule #4.