Certificate for #3115 ⟨a, b | aabbabaaaab=1⟩

Completion settings:

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

Axiom: aabbabaaaab=1.

Referenced by [4].

Axiom: bbaba=c.

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

Axiom: baaca=d.

Referenced by [5], [6], [9], [16], [22].

Overlap of [1] aabbabaaaab=1 with [2] bbaba=c:

Critical pair: aacaaab=1.

Referenced by [5], [6], [8], [14].

Overlap of [3] baaca=d with [4] aacaaab=1:

Critical pair: b=daab.

Flip LHS and RHS.

Referenced by [7], [9].

Overlap of [3] baaca=d with [4] aacaaab=1:

Critical pair: baac=dacaaab.

Flip LHS and RHS.

Referenced by [15].

Overlap of [5] daab=b with [2] bbaba=c:

Critical pair: daac=bbaba.

Reduce RHS:

Referenced by [8].

Overlap of [7] daac=c with [4] aacaaab=1:

Critical pair: d=caaab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [9], [10], [14], [15], [28], [32], [35], [40].

Overlap of [3] baaca=d with [8] caaab=d:

Critical pair: baad=daab.

Reduce RHS:

Referenced by [11].

Overlap of [8] caaab=d with [2] bbaba=c:

Critical pair: caaac=dbaba.

Defines rule #6.

Referenced by [28], [41], [43].

Overlap of [2] bbaba=c with [9] baad=b:

Critical pair: bbab=cad.

Referenced by [12], [13], [21], [24], [25].

Overlap of [2] bbaba=c with [11] bbab=cad:

Critical pair: cada=c.

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

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

Critical pair: bbacad=cadbab.

Flip LHS and RHS.

Referenced by [26].

Overlap of [4] aacaaab=1 with [8] caaab=d:

Critical pair: aad=1.

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

Overlap of [6] dacaaab=baac with [8] caaab=d:

Critical pair: dad=baac.

Flip LHS and RHS.

Referenced by [16], [20].

Overlap of [3] baaca=d with [12] cada=c:

Critical pair: baac=dda.

Reduce LHS:

Referenced by [17], [18], [20], [21].

Overlap of [14] aad=1 with [16] dad=dda:

Critical pair: aadda=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [18], [21], [24], [25], [26], [27], [28], [29], [31], [35], [36], [37], [38], [39], [43], [44], [46], [48].

Overlap of [17] ad=da with [16] dad=dda:

Critical pair: adda=daad.

Reduce LHS:

Reduce RHS:

Referenced by [19], [21].

Overlap of [14] aad=1 with [18] ddaa=d:

Critical pair: aad=daa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [23], [28], [31], [33], [35], [36], [37], [38], [39], [40], [43], [44], [49], [50], [51].

Simplify [15] baac=dad.

Reduce RHS:

Defines rule #3.

Referenced by [21], [38].

Overlap of [11] bbab=cad with [20] baac=dda:

Critical pair: bbadda=cadaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [22], [47].

Overlap of [3] baaca=d with [21] cac=bbd:

Critical pair: baabbd=dc.

Referenced by [23].

Overlap of [22] baabbd=dc with [19] daa=1:

Critical pair: baabb=dcaa.

Defines rule #11.

Referenced by [24], [39].

Overlap of [11] bbab=cad with [23] baabb=dcaa:

Critical pair: bbadcaa=cadaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Simplify [11] bbab=cad.

Reduce RHS:

Defines rule #9.

Referenced by [30], [33].

Simplify [13] cadbab=bbacad.

Reduce RHS:

Referenced by [27].

Overlap of [26] cadbab=bbacda with [17] ad=da:

Critical pair: cdabab=bbacda.

Defines rule #16.

Overlap of [10] caaac=dbaba with [8] caaab=d:

Critical pair: caaad=dbabaaaab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [17] ad=da with [28] dbabaaaab=ca:

Critical pair: aca=dababaaaab.

Flip LHS and RHS.

Referenced by [31].

Overlap of [28] dbabaaaab=ca with [25] bbab=cda:

Critical pair: dbabaaaacda=cabab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [17] ad=da with [29] dababaaaab=aca:

Critical pair: aaca=daababaaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

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

Overlap of [8] caaab=d with [31] babaaaab=aaca:

Critical pair: caaaaaca=dabaaaab.

Referenced by [35], [36], [42].

Overlap of [25] bbab=cda with [31] babaaaab=aaca:

Critical pair: bbaaaca=cdaabaaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [28] dbabaaaab=ca with [31] babaaaab=aaca:

Critical pair: dbabaaaaaaca=caabaaaab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [32] caaaaaca=dabaaaab with [8] caaab=d:

Critical pair: caaaaad=dabaaaabaab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [32] caaaaaca=dabaaaab with [32] caaaaaca=dabaaaab:

Critical pair: caaaaadabaaaab=dabaaaabaaaaca.

Reduce LHS:

Defines rule #20.

Overlap of [17] ad=da with [35] dabaaaabaab=caaa:

Critical pair: acaaa=daabaaaabaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [40].

Overlap of [35] dabaaaabaab=caaa with [20] baac=dda:

Critical pair: dabaaaabaadda=caaaaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [35] dabaaaabaab=caaa with [23] baabb=dcaa:

Critical pair: dabaaaabaadcaa=caaaaabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [8] caaab=d with [37] baaaabaab=acaaa:

Critical pair: caaaacaaa=daaaabaab.

Reduce RHS:

Referenced by [41], [42], [43], [44], [45].

Overlap of [10] caaac=dbaba with [40] caaaacaaa=aabaab:

Critical pair: caaaaabaab=dbabaaaaacaaa.

Defines rule #22.

Overlap of [32] caaaaaca=dabaaaab with [40] caaaacaaa=aabaab:

Critical pair: caaaaaaabaab=dabaaaabaaacaaa.

Defines rule #24.

Overlap of [40] caaaacaaa=aabaab with [10] caaac=dbaba:

Critical pair: caaaadbaba=aabaabc.

Reduce LHS:

Referenced by [48].

Overlap of [40] caaaacaaa=aabaab with [17] ad=da:

Critical pair: caaaacaada=aabaabd.

Reduce LHS:

Referenced by [46], [47].

Overlap of [40] caaaacaaa=aabaab with [40] caaaacaaa=aabaab:

Critical pair: caaaaaabaab=aabaabacaaa.

Defines rule #23.

Overlap of [44] caaaaca=aabaabd with [17] ad=da:

Critical pair: caaaacda=aabaabdd.

Referenced by [49].

Overlap of [44] caaaaca=aabaabd with [21] cac=bbd:

Critical pair: caaaabbd=aabaabdc.

Referenced by [51].

Overlap of [43] caababa=aabaabc with [17] ad=da:

Critical pair: caababda=aabaabcd.

Referenced by [50].

Overlap of [46] caaaacda=aabaabdd with [19] daa=1:

Critical pair: caaaac=aabaabdda.

Defines rule #7.

Overlap of [48] caababda=aabaabcd with [19] daa=1:

Critical pair: caabab=aabaabcda.

Defines rule #17.

Overlap of [47] caaaabbd=aabaabdc with [19] daa=1:

Critical pair: caaaabb=aabaabdcaa.

Defines rule #19.