Certificate for #3051 ⟨a, b | aabaabbbbba=1⟩

Completion settings:

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

Axiom: aabaabbbbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [14], [26], [28], [39].

Axiom: baabbbbb=d.

Referenced by [4], [12], [16], [17], [18], [19], [20].

Overlap of [1] aabaabbbbba=1 with [3] baabbbbb=d:

Critical pair: aada=1.

Referenced by [6], [7], [8], [9], [10].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [27], [29], [37], [38], [39], [40].

Overlap of [2] aaa=c with [4] aada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aad=ada.

Referenced by [8], [9], [10], [11].

Overlap of [6] cda=a with [4] aada=1:

Critical pair: cd=aada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9], [10].

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

Critical pair: adaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [10], [11], [13], [24], [25], [33], [35].

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

Critical pair: aadada=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [14], [16], [30], [31], [32], [34], [36].

Overlap of [2] aaa=c with [10] ad=da:

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [14], [15], [26], [37], [39].

Overlap of [3] baabbbbb=d with [3] baabbbbb=d:

Critical pair: baabbbbd=daabbbbb.

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [9] cd=1 with [12] daabbbbb=baabbbbd:

Critical pair: cbaabbbbd=aabbbbb.

Flip LHS and RHS.

Referenced by [31].

Overlap of [10] ad=da with [12] daabbbbb=baabbbbd:

Critical pair: abaabbbbd=daaabbbbb.

Reduce RHS:

Referenced by [15].

Overlap of [14] abaabbbbd=bbbbb with [11] dc=1:

Critical pair: abaabbbb=bbbbbc.

Defines rule #20.

Referenced by [16], [21], [22], [23], [28].

Overlap of [15] abaabbbb=bbbbbc with [3] baabbbbb=d:

Critical pair: ad=bbbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Referenced by [17], [18], [19], [20], [21], [22], [23], [24], [36], [37].

Overlap of [3] baabbbbb=d with [16] bbbbbcb=da:

Critical pair: baabda=dbcb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [25].

Overlap of [3] baabbbbb=d with [16] bbbbbcb=da:

Critical pair: baabbda=dbbcb.

Flip LHS and RHS.

Defines rule #12.

Overlap of [3] baabbbbb=d with [16] bbbbbcb=da:

Critical pair: baabbbda=dbbbcb.

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] baabbbbb=d with [16] bbbbbcb=da:

Critical pair: baabbbbda=dbbbbcb.

Flip LHS and RHS.

Defines rule #18.

Overlap of [15] abaabbbb=bbbbbc with [16] bbbbbcb=da:

Critical pair: abaabda=bbbbbcbbcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [30].

Overlap of [15] abaabbbb=bbbbbc with [16] bbbbbcb=da:

Critical pair: abaabbda=bbbbbcbbbcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [32].

Overlap of [15] abaabbbb=bbbbbc with [16] bbbbbcb=da:

Critical pair: abaabbbda=bbbbbcbbbbcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [34].

Overlap of [16] bbbbbcb=da with [16] bbbbbcb=da:

Critical pair: bbbbbcda=dabbbbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [9] cd=1 with [17] dbcb=baabda:

Critical pair: cbaabda=bcb.

Referenced by [26].

Overlap of [25] cbaabda=bcb with [2] aaa=c:

Critical pair: cbaabdc=bcbaa.

Reduce LHS:

Defines rule #6.

Referenced by [27], [28], [31].

Overlap of [5] ac=ca with [26] cbaab=bcbaa:

Critical pair: abcbaa=cabaab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [29].

Overlap of [26] cbaab=bcbaa with [15] abaabbbb=bbbbbc:

Critical pair: cbabbbbbc=bcbaaaabbbb.

Reduce RHS:

Referenced by [35], [36].

Overlap of [5] ac=ca with [27] cabaab=abcbaa:

Critical pair: aabcbaa=caabaab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [10] ad=da with [21] dabcb=abaabda:

Critical pair: aabaabda=daabcb.

Flip LHS and RHS.

Defines rule #11.

Simplify [13] aabbbbb=cbaabbbbd.

Reduce RHS:

Defines rule #21.

Referenced by [39].

Overlap of [10] ad=da with [22] dabbcb=abaabbda:

Critical pair: aabaabbda=daabbcb.

Flip LHS and RHS.

Defines rule #14.

Overlap of [9] cd=1 with [24] dabbbbcb=bbbbba:

Critical pair: cbbbbba=abbbbcb.

Flip LHS and RHS.

Defines rule #19.

Overlap of [10] ad=da with [23] dabbbcb=abaabbbda:

Critical pair: aabaabbbda=daabbbcb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [28] cbabbbbbc=bcbcabbbb with [9] cd=1:

Critical pair: cbabbbbb=bcbcabbbbd.

Defines rule #23.

Referenced by [38].

Overlap of [28] cbabbbbbc=bcbcabbbb with [16] bbbbbcb=da:

Critical pair: cbada=bcbcabbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [16] bbbbbcb=da with [36] bcbcabbbbb=cbdaa:

Critical pair: bbbbbccbdaa=dacbcabbbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [39].

Overlap of [5] ac=ca with [35] cbabbbbb=bcbcabbbbd:

Critical pair: abcbcabbbbd=cababbbbb.

Flip LHS and RHS.

Defines rule #26.

Referenced by [40].

Overlap of [2] aaa=c with [37] abcabbbbb=bbbbbccbdaa:

Critical pair: aabbbbbccbdaa=cbcabbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [5] ac=ca with [38] cababbbbb=abcbcabbbbd:

Critical pair: aabcbcabbbbd=caababbbbb.

Flip LHS and RHS.

Defines rule #27.