Certificate for #3106 ⟨a, b | aabbaabaaba=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. bbaabaab=d

Axiom: aabbaabaaba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [15], [16], [17], [18], [19], [21], [25], [27], [30], [33], [35], [37], [39].

Axiom: bbaabaab=d.

Defines rule #11.

Referenced by [4], [12], [16].

Overlap of [1] aabbaabaaba=1 with [3] bbaabaab=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 [14], [19], [20].

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

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], [16], [26], [31], [34], [36], [38].

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], [12], [26], [31], [34], [36], [37].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [17], [22], [29], [37], [39].

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

Critical pair: bbaabaad=dbaabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [13], [17], [23].

Overlap of [9] cd=1 with [12] dbaabaab=bbaabdaa:

Critical pair: cbbaabdaa=baabaab.

Referenced by [14], [15].

Overlap of [5] ac=ca with [13] cbbaabdaa=baabaab:

Critical pair: abaabaab=cabbaabdaa.

Flip LHS and RHS.

Referenced by [28].

Overlap of [13] cbbaabdaa=baabaab with [2] aaa=c:

Critical pair: cbbaabdc=baabaaba.

Reduce LHS:

Defines rule #8.

Referenced by [16], [18], [20], [24].

Overlap of [15] cbbaab=baabaaba with [3] bbaabaab=d:

Critical pair: cd=baabaabaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [12] dbaabaab=bbaabdaa with [16] baabaabcb=1:

Critical pair: dbaa=bbaabdaaaabcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [27].

Overlap of [15] cbbaab=baabaaba with [16] baabaabcb=1:

Critical pair: cbbaa=baabaabaaabaabcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [19], [20], [21], [27].

Overlap of [2] aaa=c with [18] aabcb=cbbaa:

Critical pair: acbbaa=cbcb.

Reduce LHS:

Referenced by [22], [28].

Overlap of [15] cbbaab=baabaaba with [18] aabcb=cbbaa:

Critical pair: cbbcbbaa=baabaabacb.

Reduce RHS:

Referenced by [33].

Overlap of [18] aabcb=cbbaa with [16] baabaabcb=1:

Critical pair: aabc=cbbaaaabaabcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [11] dc=1 with [19] cabbaa=cbcb:

Critical pair: dcbcb=abbaa.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [12] dbaabaab=bbaabdaa with [22] abbaa=bcb:

Critical pair: dbaababcb=bbaabdaabaa.

Defines rule #15.

Overlap of [15] cbbaab=baabaaba with [22] abbaa=bcb:

Critical pair: cbbabcb=baabaababaa.

Defines rule #13.

Overlap of [22] abbaa=bcb with [2] aaa=c:

Critical pair: abbc=bcba.

Referenced by [26].

Overlap of [25] abbc=bcba with [9] cd=1:

Critical pair: abb=bcbad.

Reduce RHS:

Defines rule #6.

Referenced by [32], [37].

Overlap of [17] bbaababcb=dbaa with [16] baabaabcb=1:

Critical pair: bbaababc=dbaaaabaabcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [14] cabbaabdaa=abaabaab with [19] cabbaa=cbcb:

Critical pair: cbcbbdaa=abaabaab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [32].

Overlap of [11] dc=1 with [21] cbbcabcbbaa=aabc:

Critical pair: daabc=bbcabcbbaa.

Flip LHS and RHS.

Referenced by [30].

Overlap of [29] bbcabcbbaa=daabc with [2] aaa=c:

Critical pair: bbcabcbbc=daabca.

Referenced by [31].

Overlap of [30] bbcabcbbc=daabca with [9] cd=1:

Critical pair: bbcabcbb=daabcad.

Reduce RHS:

Defines rule #18.

Overlap of [28] abaabaab=cbcbbdaa with [26] abb=bcbda:

Critical pair: abaababcbda=cbcbbdaab.

Referenced by [39].

Overlap of [20] cbbcbbaa=baabaabcab with [2] aaa=c:

Critical pair: cbbcbbc=baabaabcaba.

Referenced by [34].

Overlap of [33] cbbcbbc=baabaabcaba with [9] cd=1:

Critical pair: cbbcbb=baabaabcabad.

Reduce RHS:

Defines rule #12.

Overlap of [27] dbcabcbbaa=bbaababc with [2] aaa=c:

Critical pair: dbcabcbbc=bbaababca.

Referenced by [36].

Overlap of [35] dbcabcbbc=bbaababca with [9] cd=1:

Critical pair: dbcabcbb=bbaababcad.

Reduce RHS:

Defines rule #14.

Referenced by [37].

Overlap of [10] ad=da with [36] dbcabcbb=bbaababa:

Critical pair: abbaababa=dabcabcbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38].

Overlap of [9] cd=1 with [37] dabcabcbb=bcbbaba:

Critical pair: cbcbbaba=abcabcbb.

Flip LHS and RHS.

Defines rule #16.

Overlap of [32] abaababcbda=cbcbbdaab with [2] aaa=c:

Critical pair: abaababcbdc=cbcbbdaabaa.

Reduce LHS:

Defines rule #17.