Certificate for #3180 ⟨a, b | abaaaababba=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. aababb=c
  2. caab=d

Axiom: abaaaababba=1.

Referenced by [4].

Axiom: aababb=c.

Referenced by [4], [7], [8], [14].

Axiom: caab=d.

Defines rule #3.

Referenced by [5], [8], [10], [23], [35].

Overlap of [1] abaaaababba=1 with [2] aababb=c:

Critical pair: abaaca=1.

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

Overlap of [4] abaaca=1 with [3] caab=d:

Critical pair: abaad=ab.

Referenced by [6].

Overlap of [4] abaaca=1 with [5] abaad=ab:

Critical pair: abaacab=baad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7].

Overlap of [2] aababb=c with [6] baad=b:

Critical pair: aababb=caad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9], [13].

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

Critical pair: cc=dabb.

Referenced by [10], [22].

Overlap of [4] abaaca=1 with [7] caad=c:

Critical pair: abaac=ad.

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

Overlap of [8] cc=dabb with [3] caab=d:

Critical pair: cd=dabbaab.

Flip LHS and RHS.

Referenced by [20].

Overlap of [4] abaaca=1 with [9] abaac=ad:

Critical pair: ada=1.

Referenced by [12], [14], [16], [17].

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

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #1.

Referenced by [13], [14], [20], [22], [24], [25], [27], [28], [29], [32], [34], [39], [40], [41], [43].

Overlap of [7] caad=c with [12] da=ad:

Critical pair: caaad=ca.

Referenced by [16].

Overlap of [12] da=ad with [2] aababb=c:

Critical pair: dc=adababb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [15], [18], [24], [26], [30].

Overlap of [14] babb=dc with [14] babb=dc:

Critical pair: babdc=dcabb.

Defines rule #15.

Overlap of [9] abaac=ad with [13] caaad=ca:

Critical pair: abaaca=adaaad.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [19], [21], [24], [25], [29], [32], [34], [35], [37], [38], [39], [40], [41], [43], [44], [45], [46], [47], [48].

Overlap of [11] ada=1 with [9] abaac=ad:

Critical pair: adad=baac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [18], [25], [31].

Overlap of [14] babb=dc with [17] baac=d:

Critical pair: babd=dcaac.

Flip LHS and RHS.

Referenced by [19].

Overlap of [16] aad=1 with [18] dcaac=babd:

Critical pair: aababd=caac.

Flip LHS and RHS.

Defines rule #6.

Referenced by [25], [34], [36], [40].

Simplify [10] dabbaab=cd.

Reduce LHS:

Referenced by [21].

Overlap of [16] aad=1 with [20] adbbaab=cd:

Critical pair: acd=bbaab.

Flip LHS and RHS.

Defines rule #11.

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

Simplify [8] cc=dabb.

Reduce RHS:

Defines rule #5.

Referenced by [33].

Overlap of [3] caab=d with [21] bbaab=acd:

Critical pair: caaacd=dbaab.

Referenced by [28].

Overlap of [21] bbaab=acd with [14] babb=dc:

Critical pair: bbaadc=acdabb.

Reduce LHS:

Reduce RHS:

Defines rule #13.

Overlap of [17] baac=d with [19] caac=aababd:

Critical pair: baaaababd=daac.

Reduce RHS:

Referenced by [26], [27].

Overlap of [14] babb=dc with [25] baaaababd=c:

Critical pair: babc=dcaaaababd.

Defines rule #14.

Overlap of [25] baaaababd=c with [12] da=ad:

Critical pair: baaaababad=ca.

Referenced by [29].

Overlap of [23] caaacd=dbaab with [12] da=ad:

Critical pair: caaacad=dbaaba.

Referenced by [32].

Overlap of [27] baaaababad=ca with [12] da=ad:

Critical pair: baaaababaad=caa.

Reduce LHS:

Defines rule #10.

Referenced by [30], [31].

Overlap of [29] baaaabab=caa with [14] babb=dc:

Critical pair: baaaabadc=caaabb.

Defines rule #18.

Overlap of [29] baaaabab=caa with [17] baac=d:

Critical pair: baaaabad=caaaac.

Flip LHS and RHS.

Defines rule #8.

Referenced by [40], [41], [42].

Overlap of [28] caaacad=dbaaba with [12] da=ad:

Critical pair: caaacaad=dbaabaa.

Reduce LHS:

Defines rule #7.

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

Overlap of [22] cc=adbb with [32] caaac=dbaabaa:

Critical pair: cdbaabaa=adbbaaac.

Flip LHS and RHS.

Referenced by [44].

Overlap of [19] caac=aababd with [32] caaac=dbaabaa:

Critical pair: caadbaabaa=aababdaaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [43].

Overlap of [32] caaac=dbaabaa with [3] caab=d:

Critical pair: caaad=dbaabaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38].

Overlap of [32] caaac=dbaabaa with [19] caac=aababd:

Critical pair: caaaaababd=dbaabaaaac.

Flip LHS and RHS.

Referenced by [47].

Overlap of [32] caaac=dbaabaa with [32] caaac=dbaabaa:

Critical pair: caaadbaabaa=dbaabaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [46].

Overlap of [16] aad=1 with [35] dbaabaaaab=ca:

Critical pair: aaca=baabaaaab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [39].

Overlap of [21] bbaab=acd with [38] baabaaaab=aaca:

Critical pair: bbaaaaca=acdaabaaaab.

Reduce RHS:

Referenced by [45].

Overlap of [31] caaaac=baaaabad with [19] caac=aababd:

Critical pair: caaaaaababd=baaaabadaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [31] caaaac=baaaabad with [31] caaaac=baaaabad:

Critical pair: caaaabaaaabad=baaaabadaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [32] caaac=dbaabaa with [31] caaaac=baaaabad:

Critical pair: caaabaaaabad=dbaabaaaaaac.

Flip LHS and RHS.

Referenced by [48].

Overlap of [12] da=ad with [34] aababac=cbaabaa:

Critical pair: dcbaabaa=adababac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [16] aad=1 with [33] adbbaaac=cdbaabaa:

Critical pair: acdbaabaa=bbaaac.

Flip LHS and RHS.

Defines rule #19.

Overlap of [39] bbaaaaca=acbaaaab with [16] aad=1:

Critical pair: bbaaaac=acbaaaabad.

Defines rule #21.

Overlap of [16] aad=1 with [37] dbaabaaaaac=cabaabaa:

Critical pair: aacabaabaa=baabaaaaac.

Flip LHS and RHS.

Defines rule #23.

Overlap of [16] aad=1 with [36] dbaabaaaac=caaaaababd:

Critical pair: aacaaaaababd=baabaaaac.

Flip LHS and RHS.

Defines rule #22.

Overlap of [16] aad=1 with [42] dbaabaaaaaac=caaabaaaabad:

Critical pair: aacaaabaaaabad=baabaaaaaac.

Flip LHS and RHS.

Defines rule #24.