Certificate for #4340 ⟨a, b | abbabaaab=aa⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(d) = deg(c) = 0, d < c; deg(b) = deg(a) = 1, b < a
• Auxiliary generators:
  1. bbaba=c
  2. ccac=d

Axiom: abbabaaab=aa.

Referenced by [4].

Axiom: bbaba=c.

Defines rule #23.

Referenced by [4], [6], [8], [10], [11], [12].

Axiom: ccac=d.

Defines rule #2.

Referenced by [5], [7], [9], [16], [18], [20], [31].

Overlap of [1] abbabaaab=aa with [2] bbaba=c:

Critical pair: acaab=aa.

Defines rule #15.

Referenced by [6], [7], [8], [13], [17], [19], [21], [28].

Overlap of [3] ccac=d with [3] ccac=d:

Critical pair: ccad=dcac.

Flip LHS and RHS.

Defines rule #1.

Overlap of [2] bbaba=c with [4] acaab=aa:

Critical pair: bbabaa=ccaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [9], [10], [12], [14].

Overlap of [3] ccac=d with [4] acaab=aa:

Critical pair: ccaa=daab.

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

Overlap of [4] acaab=aa with [2] bbaba=c:

Critical pair: acaac=aababa.

Flip LHS and RHS.

Defines rule #29.

Referenced by [28], [29], [30].

Overlap of [3] ccac=d with [6] ccaab=ca:

Critical pair: ccaca=dcaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [11], [15].

Overlap of [6] ccaab=ca with [2] bbaba=c:

Critical pair: ccaac=cababa.

Flip LHS and RHS.

Defines rule #25.

Overlap of [9] dcaab=da with [2] bbaba=c:

Critical pair: dcaac=dababa.

Flip LHS and RHS.

Defines rule #24.

Overlap of [7] daab=ccaa with [2] bbaba=c:

Critical pair: daac=ccaababa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [13], [14], [15], [29].

Overlap of [4] acaab=aa with [12] caaba=daac:

Critical pair: adaac=aaa.

Defines rule #10.

Referenced by [20], [21], [22].

Overlap of [6] ccaab=ca with [12] caaba=daac:

Critical pair: cdaac=caa.

Defines rule #4.

Referenced by [18], [19], [23].

Overlap of [9] dcaab=da with [12] caaba=daac:

Critical pair: ddaac=daa.

Defines rule #3.

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

Overlap of [15] ddaac=daa with [3] ccac=d:

Critical pair: ddaad=daacac.

Flip LHS and RHS.

Defines rule #13.

Referenced by [22], [23], [24].

Overlap of [15] ddaac=daa with [4] acaab=aa:

Critical pair: ddaaa=daaaab.

Flip LHS and RHS.

Defines rule #21.

Overlap of [14] cdaac=caa with [3] ccac=d:

Critical pair: cdaad=caacac.

Flip LHS and RHS.

Defines rule #14.

Overlap of [14] cdaac=caa with [4] acaab=aa:

Critical pair: cdaaa=caaaab.

Flip LHS and RHS.

Defines rule #22.

Overlap of [13] adaac=aaa with [3] ccac=d:

Critical pair: adaad=aaacac.

Flip LHS and RHS.

Defines rule #20.

Referenced by [25], [26], [27].

Overlap of [13] adaac=aaa with [4] acaab=aa:

Critical pair: adaaa=aaaaab.

Flip LHS and RHS.

Defines rule #28.

Overlap of [13] adaac=aaa with [16] daacac=ddaad:

Critical pair: addaad=aaaac.

Flip LHS and RHS.

Defines rule #18.

Referenced by [25].

Overlap of [14] cdaac=caa with [16] daacac=ddaad:

Critical pair: cddaad=caaac.

Flip LHS and RHS.

Defines rule #9.

Referenced by [26].

Overlap of [15] ddaac=daa with [16] daacac=ddaad:

Critical pair: dddaad=daaac.

Flip LHS and RHS.

Defines rule #8.

Referenced by [27].

Overlap of [22] aaaac=addaad with [20] aaacac=adaad:

Critical pair: aadaad=addaadac.

Flip LHS and RHS.

Defines rule #19.

Overlap of [23] caaac=cddaad with [20] aaacac=adaad:

Critical pair: cadaad=cddaadac.

Flip LHS and RHS.

Defines rule #12.

Overlap of [24] daaac=dddaad with [20] aaacac=adaad:

Critical pair: dadaad=dddaadac.

Flip LHS and RHS.

Defines rule #11.

Overlap of [4] acaab=aa with [8] aababa=acaac:

Critical pair: acacaac=aaaba.

Flip LHS and RHS.

Defines rule #26.

Referenced by [30].

Overlap of [12] caaba=daac with [8] aababa=acaac:

Critical pair: cacaac=daacba.

Flip LHS and RHS.

Defines rule #17.

Overlap of [28] aaaba=acacaac with [8] aababa=acaac:

Critical pair: aacaac=acacaacba.

Flip LHS and RHS.

Defines rule #30.

Referenced by [31].

Overlap of [3] ccac=d with [30] acacaacba=aacaac:

Critical pair: ccaacaac=dacaacba.

Flip LHS and RHS.

Defines rule #27.