Certificate for #3301 ⟨a, b, c | bb=ac, caaa=1⟩

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

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Defines rule #1.

Referenced by [3], [6].

[2] caaa=1

Axiom: caaa=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] acbaaa=ba

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

ba c caaa

Critical pair: ba=acbaaa.

Flip LHS and RHS.

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

[5] cbaaa=caaba

Overlap of [2] caaa=1 with [4] acbaaa=ba:

caa a acbaaa

Critical pair: caaba=cbaaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] cbaaba=ca

Overlap of [5] cbaaa=caaba with [4] acbaaa=ba:

cbaa a acbaaa

Critical pair: cbaaba=caabacbaaa.

Reduce RHS:

[3]caa(bac)baaa
[2]⇒ (caaa)cbbaaa
[1]⇒ c(bb)aaa
[2]⇒ ca(caaa)
⇒ ca

Defines rule #6.

[7] acaaba=ba

Overlap of [4] acbaaa=ba with [5] cbaaa=caaba:

a cbaaa cbaaa

Critical pair: acaaba=ba.

Defines rule #5.