Certificate for #4864 ⟨a, b, c | ab=a, bbbcb=1⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with a < b < c

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [5].

Axiom: bbbcb=1.

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

Overlap of [1] ab=a with [2] bbbcb=1:

Critical pair: a=abbcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [5].

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

Critical pair: bbbc=bbcb.

Flip LHS and RHS.

Referenced by [6], [7].

Overlap of [3] acb=a with [2] bbbcb=1:

Critical pair: ac=abbcb.

Reduce RHS:

Defines rule #2.

Overlap of [4] bbcb=bbbc with [4] bbcb=bbbc:

Critical pair: bbcbbbc=bbbcbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [2] bbbcb=1 with [4] bbcb=bbbc:

Critical pair: bbbbc=1.

Defines rule #4.