Certificate for #6229 ⟨a, b, c | aa=1, baccab=1⟩

Completion settings:

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

Axiom: aa=1.

Defines rule #1.

Referenced by [7], [8], [10], [12], [15], [16], [18].

Axiom: baccab=1.

Referenced by [4].

Axiom: cab=d.

Defines rule #3.

Referenced by [4], [5], [9], [14], [15], [17], [19].

Overlap of [2] baccab=1 with [3] cab=d:

Critical pair: bacd=1.

Defines rule #8.

Referenced by [5], [6], [9], [13].

Overlap of [3] cab=d with [4] bacd=1:

Critical pair: ca=dacd.

Flip LHS and RHS.

Defines rule #10.

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

Overlap of [4] bacd=1 with [5] dacd=ca:

Critical pair: bacca=acd.

Referenced by [8], [9].

Overlap of [5] dacd=ca with [5] dacd=ca:

Critical pair: dacca=caacd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [11].

Overlap of [6] bacca=acd with [1] aa=1:

Critical pair: bacc=acda.

Defines rule #9.

Referenced by [11].

Overlap of [6] bacca=acd with [3] cab=d:

Critical pair: bacd=acdb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [10].

Overlap of [1] aa=1 with [9] acdb=1:

Critical pair: a=cdb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [15].

Overlap of [8] bacc=acda with [7] ccd=dacca:

Critical pair: badacca=acdad.

Flip LHS and RHS.

Referenced by [12], [13].

Overlap of [1] aa=1 with [11] acdad=badacca:

Critical pair: abadacca=cdad.

Flip LHS and RHS.

Defines rule #11.

Overlap of [4] bacd=1 with [11] acdad=badacca:

Critical pair: bbadacca=ad.

Referenced by [14].

Overlap of [13] bbadacca=ad with [3] cab=d:

Critical pair: bbadacd=adb.

Reduce LHS:

Referenced by [15], [16], [17].

Overlap of [3] cab=d with [14] bbaca=adb:

Critical pair: caadb=dbaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [14] bbaca=adb with [1] aa=1:

Critical pair: bbac=adba.

Defines rule #4.

Overlap of [14] bbaca=adb with [3] cab=d:

Critical pair: bbad=adbb.

Defines rule #2.

Overlap of [15] dbaca=a with [1] aa=1:

Critical pair: dbac=aa.

Reduce RHS:

Defines rule #6.

Overlap of [15] dbaca=a with [3] cab=d:

Critical pair: dbad=ab.

Defines rule #5.