Certificate for #2942 ⟨a, b | aaababbaaba=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. ababb=c
  2. caab=d

Axiom: aaababbaaba=1.

Referenced by [4].

Axiom: ababb=c.

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

Axiom: caab=d.

Defines rule #3.

Referenced by [4], [7], [9], [14], [15], [30], [34].

Overlap of [1] aaababbaaba=1 with [2] ababb=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 [7], [8], [16], [17], [18], [20], [22], [23], [24], [27], [29], [34], [35], [36], [38], [39].

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

Critical pair: cac=dabb.

Reduce RHS:

Defines rule #5.

Referenced by [9], [28].

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

Critical pair: dc=adbabb.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: cad=adbbaab.

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], [24], [25], [27], [29], [30], [32], [33], [35], [37], [38], [39], [41], [42], [43], [44], [45], [46].

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

Critical pair: aadc=babb.

Flip LHS and RHS.

Defines rule #9.

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

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

Critical pair: aacad=bbaab.

Flip LHS and RHS.

Defines rule #11.

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

Overlap of [11] babb=aadc with [11] babb=aadc:

Critical pair: babaadc=aadcabb.

Defines rule #18.

Overlap of [3] caab=d with [12] bbaab=aacad:

Critical pair: caaaacad=dbaab.

Referenced by [23].

Overlap of [11] babb=aadc with [12] bbaab=aacad:

Critical pair: baaacad=aadcaab.

Reduce RHS:

Referenced by [17].

Overlap of [12] bbaab=aacad with [2] ababb=c:

Critical pair: bbac=aacadabb.

Reduce RHS:

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], [26].

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

Critical pair: ababad=caaac.

Flip LHS and RHS.

Defines rule #6.

Referenced by [20], [29], [31], [38].

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

Critical pair: baaaababad=adaaac.

Reduce RHS:

Referenced by [21], [22].

Overlap of [11] babb=aadc with [20] baaaababad=ac:

Critical pair: babac=aadcaaaababad.

Defines rule #15.

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

Critical pair: baaaababaad=aca.

Referenced by [24].

Overlap of [14] caaaacad=dbaab with [6] da=ad:

Critical pair: caaaacaad=dbaaba.

Referenced by [27].

Overlap of [22] baaaababaad=aca with [6] da=ad:

Critical pair: baaaababaaad=acaa.

Reduce LHS:

Defines rule #10.

Referenced by [25], [26].

Overlap of [24] baaaabab=acaa with [11] babb=aadc:

Critical pair: baaaabaaadc=acaaabb.

Reduce LHS:

Defines rule #13.

Overlap of [24] baaaabab=acaa with [18] baaac=ad:

Critical pair: baaaabaad=acaaaaac.

Flip LHS and RHS.

Referenced by [38], [39], [40].

Overlap of [23] caaaacaad=dbaaba with [6] da=ad:

Critical pair: caaaacaaad=dbaabaa.

Reduce LHS:

Defines rule #7.

Referenced by [28], [29], [30], [31], [32], [40].

Overlap of [7] cac=adbb with [27] caaaac=dbaabaa:

Critical pair: cadbaabaa=adbbaaaac.

Flip LHS and RHS.

Referenced by [42].

Overlap of [19] caaac=ababad with [27] caaaac=dbaabaa:

Critical pair: caaadbaabaa=ababadaaaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [27] caaaac=dbaabaa with [3] caab=d:

Critical pair: caaaad=dbaabaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [27] caaaac=dbaabaa with [19] caaac=ababad:

Critical pair: caaaaababad=dbaabaaaaac.

Flip LHS and RHS.

Referenced by [45].

Overlap of [27] caaaac=dbaabaa with [27] caaaac=dbaabaa:

Critical pair: caaaadbaabaa=dbaabaaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [10] aaad=1 with [30] dbaabaaaab=ca:

Critical pair: aaaca=baabaaaab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [34], [35].

Overlap of [3] caab=d with [33] baabaaaab=aaaca:

Critical pair: caaaaaca=daabaaaab.

Reduce RHS:

Referenced by [41].

Overlap of [12] bbaab=aacad with [33] baabaaaab=aaaca:

Critical pair: bbaaaaaca=aacadaabaaaab.

Reduce RHS:

Referenced by [43].

Overlap of [6] da=ad with [29] ababaac=cbaabaa:

Critical pair: dcbaabaa=adbabaac.

Flip LHS and RHS.

Referenced by [37].

Overlap of [10] aaad=1 with [36] adbabaac=dcbaabaa:

Critical pair: aadcbaabaa=babaac.

Flip LHS and RHS.

Defines rule #16.

Overlap of [26] acaaaaac=baaaabaad with [19] caaac=ababad:

Critical pair: acaaaaaababad=baaaabaadaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [26] acaaaaac=baaaabaad with [26] acaaaaac=baaaabaad:

Critical pair: acaaaabaaaabaad=baaaabaadaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [27] caaaac=dbaabaa with [26] acaaaaac=baaaabaad:

Critical pair: caaabaaaabaad=dbaabaaaaaaac.

Flip LHS and RHS.

Referenced by [46].

Overlap of [34] caaaaaca=aadbaaaab with [10] aaad=1:

Critical pair: caaaaac=aadbaaaabaad.

Defines rule #8.

Overlap of [10] aaad=1 with [28] adbbaaaac=cadbaabaa:

Critical pair: aacadbaabaa=bbaaaac.

Flip LHS and RHS.

Defines rule #19.

Overlap of [35] bbaaaaaca=aacbaaaab with [10] aaad=1:

Critical pair: bbaaaaac=aacbaaaabaad.

Defines rule #21.

Overlap of [10] aaad=1 with [32] dbaabaaaaaac=cabaabaa:

Critical pair: aaacabaabaa=baabaaaaaac.

Flip LHS and RHS.

Defines rule #23.

Overlap of [10] aaad=1 with [31] dbaabaaaaac=caaaaababad:

Critical pair: aaacaaaaababad=baabaaaaac.

Flip LHS and RHS.

Defines rule #22.

Overlap of [10] aaad=1 with [40] dbaabaaaaaaac=caaabaaaabaad:

Critical pair: aaacaaabaaaabaad=baabaaaaaaac.

Flip LHS and RHS.

Defines rule #24.