Certificate for #501 ⟨a, b, c | bb=ac, caa=1⟩

Back:⟨a, b, c | bb=ac, caa=1⟩

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Defines rule #1.

Referenced by [3], [6].

[2] caa=1

Axiom: caa=1.

Defines rule #3.

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

[3] bac=acb

Overlap of [1] bb=ac with [1] bb=ac:

b b bb

Critical pair: bac=acb.

Defines rule #2.

Referenced by [4], [6].

[4] acbaa=ba

Overlap of [3] bac=acb with [2] caa=1:

ba c caa

Critical pair: ba=acbaa.

Flip LHS and RHS.

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

[5] cbaa=caba

Overlap of [2] caa=1 with [4] acbaa=ba:

ca a acbaa

Critical pair: caba=cbaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] cbaba=ca

Overlap of [5] cbaa=caba with [4] acbaa=ba:

cba a acbaa

Critical pair: cbaba=cabacbaa.

Reduce RHS:

[3]ca(bac)baa
[2]⇒ (caa)cbbaa
[1]⇒ c(bb)aa
[2]⇒ ca(caa)
⇒ ca

Defines rule #6.

[7] acaba=ba

Overlap of [4] acbaa=ba with [5] cbaa=caba:

a cbaa cbaa

Critical pair: acaba=ba.

Defines rule #5.