Certificate for #1410 ⟨a, b | aabaabbaba=1⟩

Completion settings:

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

Axiom: aabaabbaba=1.

Referenced by [4].

Axiom: baabb=c.

Defines rule #9.

Referenced by [4], [8], [9], [12], [13], [15], [18], [29].

Axiom: acab=d.

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

Overlap of [1] aabaabbaba=1 with [2] baabb=c:

Critical pair: aacaba=1.

Reduce LHS:

Referenced by [5], [6], [7], [11].

Overlap of [4] ada=1 with [4] ada=1:

Critical pair: ad=da.

Defines rule #1.

Referenced by [6], [7], [23], [25], [26], [30], [37], [40], [41].

Overlap of [4] ada=1 with [5] ad=da:

Critical pair: daa=1.

Defines rule #2.

Referenced by [9], [15], [17], [19], [20], [21], [22], [23], [24], [25], [27], [28], [30], [31], [32], [37], [39], [41].

Overlap of [4] ada=1 with [3] acab=d:

Critical pair: add=cab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [2] baabb=c with [2] baabb=c:

Critical pair: baabc=caabb.

Defines rule #13.

Overlap of [7] cab=dda with [2] baabb=c:

Critical pair: cac=ddaaabb.

Reduce RHS:

Defines rule #5.

Referenced by [10].

Overlap of [9] cac=dabb with [3] acab=d:

Critical pair: cd=dabbab.

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] ada=1 with [10] dabbab=cd:

Critical pair: acd=bbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [12], [13], [14], [15], [16], [35], [38].

Overlap of [2] baabb=c with [11] bbab=acd:

Critical pair: baaacd=cab.

Reduce RHS:

Referenced by [17].

Overlap of [2] baabb=c with [11] bbab=acd:

Critical pair: baabacd=cbab.

Referenced by [22].

Overlap of [7] cab=dda with [11] bbab=acd:

Critical pair: caacd=ddabab.

Referenced by [21].

Overlap of [11] bbab=acd with [2] baabb=c:

Critical pair: bbac=acdaabb.

Reduce RHS:

Defines rule #14.

Overlap of [11] bbab=acd with [11] bbab=acd:

Critical pair: bbaacd=acdbab.

Referenced by [24].

Overlap of [12] baaacd=dda with [6] daa=1:

Critical pair: baaac=ddaaa.

Reduce RHS:

Defines rule #4.

Referenced by [18], [19], [30], [32].

Overlap of [2] baabb=c with [17] baaac=da:

Critical pair: baabda=caaac.

Flip LHS and RHS.

Defines rule #7.

Referenced by [19], [20], [33].

Overlap of [17] baaac=da with [18] caaac=baabda:

Critical pair: baaabaabda=daaaac.

Reduce RHS:

Referenced by [27], [28].

Overlap of [18] caaac=baabda with [18] caaac=baabda:

Critical pair: caaabaabda=baabdaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [14] caacd=ddabab with [6] daa=1:

Critical pair: caac=ddababaa.

Defines rule #6.

Referenced by [23].

Overlap of [13] baabacd=cbab with [6] daa=1:

Critical pair: baabac=cbabaa.

Defines rule #15.

Overlap of [21] caac=ddababaa with [7] cab=dda:

Critical pair: caadda=ddababaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [16] bbaacd=acdbab with [6] daa=1:

Critical pair: bbaac=acdbabaa.

Defines rule #16.

Overlap of [5] ad=da with [23] ddababaaab=cda:

Critical pair: acda=dadababaaab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [26], [28].

Overlap of [5] ad=da with [25] dbabaaab=acda:

Critical pair: aacda=dababaaab.

Flip LHS and RHS.

Referenced by [37].

Overlap of [19] baaabaabda=aac with [6] daa=1:

Critical pair: baaabaab=aaca.

Defines rule #11.

Referenced by [29], [30].

Overlap of [25] dbabaaab=acda with [19] baaabaabda=aac:

Critical pair: dbabaaaaac=acdaaaabaabda.

Reduce RHS:

Referenced by [40].

Overlap of [27] baaabaab=aaca with [2] baabb=c:

Critical pair: baaabaac=aacaaabb.

Defines rule #18.

Overlap of [27] baaabaab=aaca with [17] baaac=da:

Critical pair: baaabaada=aacaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31], [32], [33], [34].

Overlap of [6] daa=1 with [30] aacaaaac=baaaba:

Critical pair: dbaaaba=caaaac.

Flip LHS and RHS.

Defines rule #8.

Overlap of [17] baaac=da with [30] aacaaaac=baaaba:

Critical pair: babaaaba=daaaaac.

Reduce RHS:

Referenced by [35], [36].

Overlap of [30] aacaaaac=baaaba with [18] caaac=baabda:

Critical pair: aacaaaabaabda=baaabaaaac.

Flip LHS and RHS.

Defines rule #21.

Overlap of [30] aacaaaac=baaaba with [30] aacaaaac=baaaba:

Critical pair: aacaabaaaba=baaabaaaaac.

Flip LHS and RHS.

Defines rule #23.

Overlap of [11] bbab=acd with [32] babaaaba=aaac:

Critical pair: bbaaaac=acdabaaaba.

Defines rule #19.

Overlap of [32] babaaaba=aaac with [32] babaaaba=aaac:

Critical pair: babaaaaaac=aaacbaaaba.

Defines rule #24.

Overlap of [5] ad=da with [26] dababaaab=aacda:

Critical pair: aaacda=daababaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [38].

Overlap of [37] babaaab=aaacda with [11] bbab=acd:

Critical pair: babaaaacd=aaacdabab.

Referenced by [39].

Overlap of [38] babaaaacd=aaacdabab with [6] daa=1:

Critical pair: babaaaac=aaacdababaa.

Defines rule #20.

Overlap of [5] ad=da with [28] dbabaaaaac=acaabaabda:

Critical pair: aacaabaabda=dababaaaaac.

Flip LHS and RHS.

Referenced by [41].

Overlap of [5] ad=da with [40] dababaaaaac=aacaabaabda:

Critical pair: aaacaabaabda=daababaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.