Certificate for #4232 ⟨a, b, c | aab=1, baca=c⟩

Completion settings:

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

Axiom: aab=1.

Defines rule #20.

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

Axiom: baca=c.

Referenced by [5].

Axiom: ca=d.

Defines rule #7.

Referenced by [5], [7], [9], [13], [14], [18], [20], [21].

Axiom: ba=e.

Defines rule #16.

Referenced by [5], [6], [8], [10].

Overlap of [2] baca=c with [4] ba=e:

Critical pair: eca=c.

Reduce LHS:

Defines rule #3.

Referenced by [11], [12], [14], [15], [16], [17], [18], [19].

Overlap of [1] aab=1 with [4] ba=e:

Critical pair: aae=a.

Defines rule #13.

Referenced by [9], [10], [11].

Overlap of [3] ca=d with [1] aab=1:

Critical pair: c=dab.

Flip LHS and RHS.

Defines rule #18.

Referenced by [18].

Overlap of [4] ba=e with [1] aab=1:

Critical pair: b=eab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] ca=d with [6] aae=a:

Critical pair: ca=dae.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [14], [15].

Overlap of [4] ba=e with [6] aae=a:

Critical pair: ba=eae.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

Overlap of [6] aae=a with [5] ed=c:

Critical pair: aac=ad.

Defines rule #14.

Referenced by [21].

Overlap of [10] eae=e with [5] ed=c:

Critical pair: eac=ed.

Reduce RHS:

Defines rule #6.

Referenced by [13].

Overlap of [12] eac=c with [3] ca=d:

Critical pair: ead=ca.

Reduce RHS:

Defines rule #12.

Overlap of [5] ed=c with [9] dae=d:

Critical pair: ed=cae.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [16], [17].

Overlap of [9] dae=d with [5] ed=c:

Critical pair: dac=dd.

Defines rule #10.

Referenced by [20].

Overlap of [5] ed=c with [14] de=c:

Critical pair: ec=ce.

Flip LHS and RHS.

Defines rule #1.

Overlap of [14] de=c with [5] ed=c:

Critical pair: dc=cd.

Flip LHS and RHS.

Defines rule #4.

Overlap of [5] ed=c with [7] dab=c:

Critical pair: ec=cab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [19].

Overlap of [5] ed=c with [18] db=ec:

Critical pair: eec=cb.

Flip LHS and RHS.

Defines rule #8.

Overlap of [15] dac=dd with [3] ca=d:

Critical pair: dad=dda.

Defines rule #17.

Overlap of [11] aac=ad with [3] ca=d:

Critical pair: aad=ada.

Defines rule #19.