Certificate for #3535 ⟨a, b, c | bb=ac, bca=c⟩

Completion settings:

• Auxiliary generators:
  1. d = abc
• Reduction order:
  • Left-to-right recursive path with deg(a) = deg(b) = deg(d) = 0, a < b < d; deg(c) = 1

Axiom: bb=ac.

Flip LHS and RHS.

Referenced by [4], [5].

Axiom: bca=c.

Referenced by [4], [8], [9].

Axiom: abc=d.

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

Overlap of [3] abc=d with [2] bca=c:

Critical pair: ac=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [6].

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

Critical pair: dbb=bbc.

Flip LHS and RHS.

Referenced by [6], [8].

Overlap of [4] da=bb with [3] abc=d:

Critical pair: dd=bbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

Overlap of [6] bdbb=dd with [6] bdbb=dd:

Critical pair: bdbdd=dddbb.

Flip LHS and RHS.

Defines rule #5.

Overlap of [5] bbc=dbb with [2] bca=c:

Critical pair: bc=dbba.

Referenced by [9], [10].

Overlap of [2] bca=c with [8] bc=dbba:

Critical pair: dbbaa=c.

Flip LHS and RHS.

Defines rule #6.

Overlap of [3] abc=d with [8] bc=dbba:

Critical pair: adbba=d.

Defines rule #3.

Referenced by [11].

Overlap of [10] adbba=d with [10] adbba=d:

Critical pair: adbbd=ddbba.

Flip LHS and RHS.

Defines rule #4.