Certificate for #3071 ⟨a, b, c | abc=b, bca=c⟩

Completion settings:

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

Axiom: abc=b.

Referenced by [4].

Axiom: bca=c.

Referenced by [5].

Axiom: bc=d.

Referenced by [4], [6].

Overlap of [1] abc=b with [3] bc=d:

Critical pair: ad=b.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6].

Overlap of [2] bca=c with [4] b=ad:

Critical pair: adca=c.

Referenced by [7].

Overlap of [3] bc=d with [4] b=ad:

Critical pair: adc=d.

Referenced by [7], [8].

Simplify [5] adca=c.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

Overlap of [6] adc=d with [7] c=da:

Critical pair: adda=d.

Defines rule #1.

Referenced by [9].

Overlap of [8] adda=d with [8] adda=d:

Critical pair: addd=ddda.

Flip LHS and RHS.

Defines rule #2.