Certificate for #4063 ⟨a, b, c | abc=1, bacbb=1⟩

Completion settings:

[1] abc=1

Axiom: abc=1.

Defines rule #1.

[2] bacbb=1

Axiom: bacbb=1.

Referenced by [3], [4].

[3] bacb=acbb

Overlap of [2] bacbb=1 with [2] bacbb=1:

bacb b bacbb

Critical pair: bacb=acbb.

Referenced by [4], [5].

[4] acbbb=1

Overlap of [2] bacbb=1 with [3] bacb=acbb:

bacbb bacb

Critical pair: acbbb=1.

Defines rule #3.

Referenced by [5], [6].

[5] bacacbb=ac

Overlap of [3] bacb=acbb with [3] bacb=acbb:

bac b bacb

Critical pair: bacacbb=acbbacb.

Reduce RHS:

[3]acb(bacb)
[3]⇒ ac(bacb)b
[4]⇒ ac(acbbb)
⇒ ac

Referenced by [6].

[6] bac=acb

Overlap of [5] bacacbb=ac with [4] acbbb=1:

bac acbb acbbb

Critical pair: bac=acb.

Defines rule #2.