Certificate for #2968 ⟨a, b | aaabbabaaba=1⟩

Completion settings:

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

Axiom: aaabbabaaba=1.

Referenced by [4].

Axiom: abbab=c.

Referenced by [4], [7], [8], [13], [16], [19].

Axiom: caab=d.

Defines rule #3.

Referenced by [4], [7], [9], [14], [15], [28].

Overlap of [1] aaabbabaaba=1 with [2] abbab=c:

Critical pair: aacaaba=1.

Reduce LHS:

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

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

Critical pair: aad=ada.

Flip LHS and RHS.

Referenced by [6], [10].

Overlap of [4] aada=1 with [5] ada=aad:

Critical pair: aadaad=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [8], [14], [17], [18], [20], [22], [25], [26], [27], [28], [29], [30], [31], [32], [34], [38], [39], [41].

Overlap of [3] caab=d with [2] abbab=c:

Critical pair: cac=dbab.

Defines rule #5.

Referenced by [9], [40].

Overlap of [6] da=ad with [2] abbab=c:

Critical pair: dc=adbbab.

Flip LHS and RHS.

Referenced by [11].

Overlap of [7] cac=dbab with [3] caab=d:

Critical pair: cad=dbabaab.

Flip LHS and RHS.

Referenced by [12].

Overlap of [4] aada=1 with [5] ada=aad:

Critical pair: aaad=1.

Defines rule #2.

Referenced by [11], [12], [17], [18], [20], [22], [25], [26], [27], [29], [32], [33], [34], [41], [42], [43].

Overlap of [10] aaad=1 with [8] adbbab=dc:

Critical pair: aadc=bbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [13], [15], [21], [23].

Overlap of [10] aaad=1 with [9] dbabaab=cad:

Critical pair: aaacad=babaab.

Flip LHS and RHS.

Defines rule #11.

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

Overlap of [11] bbab=aadc with [2] abbab=c:

Critical pair: bbc=aadcbab.

Defines rule #13.

Overlap of [3] caab=d with [12] babaab=aaacad:

Critical pair: caaaaacad=dabaab.

Reduce RHS:

Referenced by [31].

Overlap of [11] bbab=aadc with [12] babaab=aaacad:

Critical pair: baaacad=aadcaab.

Reduce RHS:

Referenced by [17].

Overlap of [12] babaab=aaacad with [2] abbab=c:

Critical pair: babac=aaacadbab.

Defines rule #14.

Overlap of [15] baaacad=aadd with [6] da=ad:

Critical pair: baaacaad=aadda.

Reduce RHS:

Referenced by [18].

Overlap of [17] baaacaad=d with [6] da=ad:

Critical pair: baaacaaad=da.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [19], [20], [24], [25], [33], [39].

Overlap of [2] abbab=c with [18] baaac=ad:

Critical pair: abbaad=caaac.

Flip LHS and RHS.

Defines rule #6.

Referenced by [20], [26], [34], [35].

Overlap of [18] baaac=ad with [19] caaac=abbaad:

Critical pair: baaaabbaad=adaaac.

Reduce RHS:

Referenced by [21], [22].

Overlap of [11] bbab=aadc with [20] baaaabbaad=ac:

Critical pair: bbaac=aadcaaaabbaad.

Defines rule #16.

Overlap of [20] baaaabbaad=ac with [6] da=ad:

Critical pair: baaaabbaaad=aca.

Reduce LHS:

Defines rule #9.

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

Overlap of [22] baaaabb=aca with [11] bbab=aadc:

Critical pair: baaaabaadc=acabab.

Defines rule #18.

Overlap of [22] baaaabb=aca with [18] baaac=ad:

Critical pair: baaaabad=acaaaac.

Flip LHS and RHS.

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

Overlap of [18] baaac=ad with [24] acaaaac=baaaabad:

Critical pair: baabaaaabad=adaaaac.

Reduce RHS:

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

Overlap of [24] acaaaac=baaaabad with [19] caaac=abbaad:

Critical pair: acaaaaabbaad=baaaabadaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [24] acaaaac=baaaabad with [24] acaaaac=baaaabad:

Critical pair: acaaabaaaabad=baaaabadaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [3] caab=d with [25] baabaaaabad=aac:

Critical pair: caaaac=daabaaaabad.

Reduce RHS:

Defines rule #7.

Overlap of [12] babaab=aaacad with [25] baabaaaabad=aac:

Critical pair: babaaaac=aaacadaabaaaabad.

Reduce RHS:

Defines rule #20.

Overlap of [25] baabaaaabad=aac with [6] da=ad:

Critical pair: baabaaaabaad=aaca.

Referenced by [32].

Overlap of [14] caaaaacad=adbaab with [6] da=ad:

Critical pair: caaaaacaad=adbaaba.

Referenced by [41].

Overlap of [30] baabaaaabaad=aaca with [6] da=ad:

Critical pair: baabaaaabaaad=aacaa.

Reduce LHS:

Defines rule #12.

Referenced by [33].

Overlap of [32] baabaaaab=aacaa with [18] baaac=ad:

Critical pair: baabaaaaad=aacaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34], [35], [36], [37].

Overlap of [19] caaac=abbaad with [33] aacaaaaac=baabaa:

Critical pair: cabaabaa=abbaadaaaaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [38], [39].

Overlap of [33] aacaaaaac=baabaa with [19] caaac=abbaad:

Critical pair: aacaaaaaabbaad=baabaaaaac.

Flip LHS and RHS.

Defines rule #22.

Overlap of [33] aacaaaaac=baabaa with [24] acaaaac=baaaabad:

Critical pair: aacaaaabaaaabad=baabaaaaaac.

Flip LHS and RHS.

Defines rule #23.

Overlap of [33] aacaaaaac=baabaa with [33] aacaaaaac=baabaa:

Critical pair: aacaaabaabaa=baabaaaaaaac.

Flip LHS and RHS.

Defines rule #24.

Overlap of [6] da=ad with [34] abbaaaac=cabaabaa:

Critical pair: dcabaabaa=adbbaaaac.

Flip LHS and RHS.

Referenced by [42].

Overlap of [22] baaaabb=aca with [34] abbaaaac=cabaabaa:

Critical pair: baaacabaabaa=acaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [40].

Overlap of [7] cac=dbab with [39] acaaaaac=aadbaabaa:

Critical pair: caadbaabaa=dbabaaaaac.

Flip LHS and RHS.

Referenced by [43].

Overlap of [31] caaaaacaad=adbaaba with [6] da=ad:

Critical pair: caaaaacaaad=adbaabaa.

Reduce LHS:

Defines rule #8.

Overlap of [10] aaad=1 with [38] adbbaaaac=dcabaabaa:

Critical pair: aadcabaabaa=bbaaaac.

Flip LHS and RHS.

Defines rule #19.

Overlap of [10] aaad=1 with [40] dbabaaaaac=caadbaabaa:

Critical pair: aaacaadbaabaa=babaaaaac.

Flip LHS and RHS.

Defines rule #21.