Certificate for #2845 ⟨a, b | aaaabaaabba=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. aaaaa=c
  2. baaabb=d

Axiom: aaaabaaabba=1.

Referenced by [4].

Axiom: aaaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [10], [15], [17], [19], [21], [28], [31], [34], [45], [46].

Axiom: baaabb=d.

Referenced by [4], [11], [23].

Overlap of [1] aaaabaaabba=1 with [3] baaabb=d:

Critical pair: aaaada=1.

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

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [29], [42], [44], [45], [46].

Overlap of [2] aaaaa=c with [4] aaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [2] aaaaa=c with [4] aaaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [10].

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

Critical pair: aaaad=aaada.

Referenced by [9], [12], [19].

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

Critical pair: cd=aaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13].

Overlap of [7] cada=aa with [4] aaaada=1:

Critical pair: cad=aaaaada.

Reduce RHS:

Referenced by [18].

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

Critical pair: baaabd=daaabb.

Flip LHS and RHS.

Referenced by [20], [21].

Overlap of [4] aaaada=1 with [8] aaaad=aaada:

Critical pair: aaadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [13], [15], [19], [20], [27], [33], [35], [38], [39], [40].

Simplify [9] aaadaa=cd.

Reduce RHS:

Referenced by [14], [16].

Overlap of [13] aaadaa=1 with [13] aaadaa=1:

Critical pair: aaad=adaa.

Referenced by [15], [16], [19].

Overlap of [2] aaaaa=c with [14] aaad=adaa:

Critical pair: aaadaa=cd.

Reduce LHS:

Reduce RHS:

Referenced by [16], [17].

Overlap of [13] aaadaa=1 with [14] aaad=adaa:

Critical pair: aaadaadaa=aad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [21].

Overlap of [16] aad=daa with [15] adaaaa=1:

Critical pair: a=daaaaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [17] dca=a with [10] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [19], [35], [37], [40], [41], [43].

Overlap of [2] aaaaa=c with [18] ad=da:

Critical pair: aaaada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [21], [22], [24], [30], [43], [44], [45], [46].

Overlap of [12] cd=1 with [11] daaabb=baaabd:

Critical pair: cbaaabd=aaabb.

Flip LHS and RHS.

Referenced by [23], [32], [37].

Overlap of [16] aad=daa with [11] daaabb=baaabd:

Critical pair: aabaaabd=daaaaabb.

Reduce RHS:

Referenced by [22].

Overlap of [21] aabaaabd=bb with [19] dc=1:

Critical pair: aabaaab=bbc.

Defines rule #11.

Referenced by [26].

Overlap of [3] baaabb=d with [20] aaabb=cbaaabd:

Critical pair: bcbaaabd=d.

Referenced by [24].

Overlap of [23] bcbaaabd=d with [19] dc=1:

Critical pair: bcbaaab=dc.

Reduce RHS:

Referenced by [25], [26], [28], [32].

Overlap of [24] bcbaaab=1 with [24] bcbaaab=1:

Critical pair: bcbaaa=cbaaab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [29], [30], [32], [37].

Overlap of [24] bcbaaab=1 with [22] aabaaab=bbc:

Critical pair: bcbabbc=aaab.

Referenced by [27].

Overlap of [26] bcbabbc=aaab with [12] cd=1:

Critical pair: bcbabb=aaabd.

Referenced by [28], [36].

Overlap of [24] bcbaaab=1 with [27] bcbabb=aaabd:

Critical pair: bcbaaaaaabd=cbabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [42], [43].

Overlap of [5] ac=ca with [25] cbaaab=bcbaaa:

Critical pair: abcbaaa=cabaaab.

Flip LHS and RHS.

Defines rule #8.

Overlap of [19] dc=1 with [25] cbaaab=bcbaaa:

Critical pair: dbcbaaa=baaab.

Referenced by [31], [32].

Overlap of [30] dbcbaaa=baaab with [2] aaaaa=c:

Critical pair: dbcbc=baaabaa.

Referenced by [40].

Overlap of [30] dbcbaaa=baaab with [25] cbaaab=bcbaaa:

Critical pair: dbbcbaaa=baaabb.

Reduce RHS:

Referenced by [33].

Overlap of [12] cd=1 with [32] dbbcbaaa=d:

Critical pair: cd=bbcbaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [33] bbcbaaa=1 with [2] aaaaa=c:

Critical pair: bbcbc=aa.

Referenced by [35], [36].

Overlap of [34] bbcbc=aa with [12] cd=1:

Critical pair: bbcb=aad.

Reduce RHS:

Defines rule #13.

Referenced by [38], [43], [44].

Overlap of [34] bbcbc=aa with [27] bcbabb=aaabd:

Critical pair: bbcaaabd=aababb.

Flip LHS and RHS.

Defines rule #18.

Simplify [20] aaabb=cbaaabd.

Reduce RHS:

Defines rule #12.

Referenced by [45], [46].

Overlap of [35] bbcb=daa with [35] bbcb=daa:

Critical pair: bbcdaa=daabcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [12] cd=1 with [38] daabcb=bbaa:

Critical pair: cbbaa=aabcb.

Flip LHS and RHS.

Defines rule #10.

Overlap of [31] dbcbc=baaabaa with [12] cd=1:

Critical pair: dbcb=baaabaad.

Reduce RHS:

Defines rule #7.

Referenced by [41].

Overlap of [18] ad=da with [40] dbcb=baaabdaa:

Critical pair: abaaabdaa=dabcb.

Flip LHS and RHS.

Defines rule #9.

Overlap of [5] ac=ca with [28] cbabb=bcbcabd:

Critical pair: abcbcabd=cababb.

Flip LHS and RHS.

Defines rule #16.

Overlap of [28] cbabb=bcbcabd with [35] bbcb=daa:

Critical pair: cbadaa=bcbcabdcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [35] bbcb=daa with [43] bcbcabb=cbdaaa:

Critical pair: bbccbdaaa=daacbcabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [45], [46].

Overlap of [2] aaaaa=c with [44] aabcabb=bbccbdaaa:

Critical pair: aaabbccbdaaa=cbcabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [2] aaaaa=c with [44] aabcabb=bbccbdaaa:

Critical pair: aaaabbccbdaaa=cabcabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.