Certificate for #2985 ⟨a, b | aaabbbaabba=1⟩

Completion settings:

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

Axiom: aaabbbaabba=1.

Referenced by [4].

Axiom: bbb=c.

Defines rule #5.

Referenced by [4], [5], [16], [18], [20], [27], [30], [31], [36], [37], [38], [41], [47].

Axiom: aabbaaaa=d.

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

Overlap of [1] aaabbbaabba=1 with [2] bbb=c:

Critical pair: aaacaabba=1.

Referenced by [6], [7], [8], [9], [10], [11], [12], [14].

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

Critical pair: bc=cb.

Defines rule #3.

Referenced by [13], [15], [20], [32], [34], [45], [47].

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

Critical pair: aaacaabb=aacaabba.

Flip LHS and RHS.

Referenced by [8], [14], [27].

Overlap of [3] aabbaaaa=d with [4] aaacaabba=1:

Critical pair: aabbaa=dacaabba.

Flip LHS and RHS.

Referenced by [26], [28].

Overlap of [3] aabbaaaa=d with [4] aaacaabba=1:

Critical pair: aabbaaa=daacaabba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [4] aaacaabba=1 with [3] aabbaaaa=d:

Critical pair: aaacd=aaa.

Referenced by [10].

Overlap of [4] aaacaabba=1 with [9] aaacd=aaa:

Critical pair: aaacaabbaaa=aacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] aaacaabba=1 with [10] aacd=aa:

Critical pair: aaacaabbaa=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [4] aaacaabba=1 with [11] acd=a:

Critical pair: aaacaabba=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [13], [17], [18], [21], [24], [25], [26], [40], [42], [43], [46].

Overlap of [5] bc=cb with [12] cd=1:

Critical pair: b=cbd.

Flip LHS and RHS.

Referenced by [15], [22].

Overlap of [4] aaacaabba=1 with [6] aacaabba=aaacaabb:

Critical pair: aaaacaabb=1.

Referenced by [16], [19].

Overlap of [5] bc=cb with [13] cbd=b:

Critical pair: bb=cbbd.

Flip LHS and RHS.

Referenced by [18].

Overlap of [14] aaaacaabb=1 with [2] bbb=c:

Critical pair: aaaacaac=b.

Referenced by [17], [18].

Overlap of [16] aaaacaac=b with [12] cd=1:

Critical pair: aaaacaa=bd.

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

Overlap of [16] aaaacaac=b with [15] cbbd=bb:

Critical pair: aaaacaabb=bbbd.

Reduce LHS:

Reduce RHS:

Referenced by [19], [20].

Overlap of [14] aaaacaabb=1 with [18] bdbb=1:

Critical pair: aaaacaab=dbb.

Reduce LHS:

Referenced by [20].

Overlap of [18] bdbb=1 with [5] bc=cb:

Critical pair: bdbcb=c.

Reduce LHS:

Referenced by [21].

Overlap of [20] dcc=c with [12] cd=1:

Critical pair: dc=cd.

Reduce RHS:

Defines rule #2.

Referenced by [22], [27], [29], [31], [36], [45], [47].

Overlap of [21] dc=1 with [13] cbd=b:

Critical pair: db=bd.

Flip LHS and RHS.

Defines rule #4.

Referenced by [23], [33], [35], [40], [42], [44].

Simplify [17] aaaacaa=bd.

Reduce RHS:

Defines rule #18.

Referenced by [24], [27], [44], [45].

Overlap of [23] aaaacaa=db with [23] aaaacaa=db:

Critical pair: aaaacdb=dbaacaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [12] cd=1 with [24] dbaacaa=aaaab:

Critical pair: caaaab=baacaa.

Flip LHS and RHS.

Defines rule #13.

Referenced by [30], [36].

Overlap of [12] cd=1 with [7] dacaabba=aabbaa:

Critical pair: caabbaa=acaabba.

Referenced by [27], [38].

Overlap of [26] caabbaa=acaabba with [23] aaaacaa=db:

Critical pair: caabbadb=acaabbaaaacaa.

Reduce RHS:

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

Overlap of [7] dacaabba=aabbaa with [27] caabbadb=acaa:

Critical pair: daacaa=aabbaadb.

Defines rule #12.

Overlap of [21] dc=1 with [27] caabbadb=acaa:

Critical pair: dacaa=aabbadb.

Defines rule #7.

Referenced by [33].

Overlap of [25] baacaa=caaaab with [27] caabbadb=acaa:

Critical pair: baaacaa=caaaabbbadb.

Reduce RHS:

Defines rule #17.

Overlap of [27] caabbadb=acaa with [2] bbb=c:

Critical pair: caabbadc=acaabb.

Reduce LHS:

Defines rule #6.

Referenced by [32], [36], [37], [38].

Overlap of [5] bc=cb with [31] caabba=acaabb:

Critical pair: bacaabb=cbaabba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [34].

Overlap of [22] bd=db with [29] dacaa=aabbadb:

Critical pair: baabbadb=dbacaa.

Flip LHS and RHS.

Defines rule #9.

Referenced by [35], [36].

Overlap of [5] bc=cb with [32] cbaabba=bacaabb:

Critical pair: bbacaabb=cbbaabba.

Flip LHS and RHS.

Defines rule #10.

Overlap of [22] bd=db with [33] dbacaa=baabbadb:

Critical pair: bbaabbadb=dbbacaa.

Flip LHS and RHS.

Defines rule #11.

Overlap of [33] dbacaa=baabbadb with [31] caabba=acaabb:

Critical pair: dbaacaabb=baabbadbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

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

Overlap of [2] bbb=c with [36] baabbaa=aaaac:

Critical pair: bbaaaac=caabbaa.

Reduce RHS:

Referenced by [40].

Overlap of [26] caabbaa=acaabba with [36] baabbaa=aaaac:

Critical pair: caabaaaac=acaabbabbaa.

Reduce RHS:

Referenced by [43], [44].

Overlap of [36] baabbaa=aaaac with [36] baabbaa=aaaac:

Critical pair: baabaaaac=aaaacbbaa.

Referenced by [46].

Overlap of [37] bbaaaac=aacaabb with [12] cd=1:

Critical pair: bbaaaa=aacaabbd.

Reduce RHS:

Defines rule #15.

Referenced by [47].

Overlap of [8] daaacaabb=aabbaaa with [2] bbb=c:

Critical pair: daaacaac=aabbaaab.

Referenced by [42].

Overlap of [41] daaacaac=aabbaaab with [12] cd=1:

Critical pair: daaacaa=aabbaaabd.

Reduce RHS:

Defines rule #16.

Overlap of [38] caabaaaac=aacaacbaa with [12] cd=1:

Critical pair: caabaaaa=aacaacbaad.

Defines rule #19.

Overlap of [38] caabaaaac=aacaacbaa with [23] aaaacaa=db:

Critical pair: caabdb=aacaacbaaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [23] aaaacaa=db with [44] aacaacbaaaa=caadbb:

Critical pair: aaaaccaadbb=dbcaacbaaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.

Referenced by [47].

Overlap of [39] baabaaaac=aaaacbbaa with [12] cd=1:

Critical pair: baabaaaa=aaaacbbaad.

Defines rule #21.

Overlap of [2] bbb=c with [45] baacbaaaa=aaaaccaadbb:

Critical pair: bbaaaaccaadbb=caacbaaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.