Certificate for #3306 ⟨a, b, c | bb=ac, ccaa=1⟩

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

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Defines rule #1.

Referenced by [3], [6].

[2] ccaa=1

Axiom: ccaa=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] acbcaa=ba

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

ba c ccaa

Critical pair: ba=acbcaa.

Flip LHS and RHS.

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

[5] cbcaa=ccaba

Overlap of [2] ccaa=1 with [4] acbcaa=ba:

cca a acbcaa

Critical pair: ccaba=cbcaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] cbcaba=ca

Overlap of [5] cbcaa=ccaba with [4] acbcaa=ba:

cbca a acbcaa

Critical pair: cbcaba=ccabacbcaa.

Reduce RHS:

[3]cca(bac)bcaa
[2]⇒ (ccaa)cbbcaa
[1]⇒ c(bb)caa
[2]⇒ ca(ccaa)
⇒ ca

Defines rule #6.

[7] accaba=ba

Overlap of [4] acbcaa=ba with [5] cbcaa=ccaba:

a cbcaa cbcaa

Critical pair: accaba=ba.

Defines rule #5.