Certificate for #2941 ⟨a, b | aaababbaaab=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. babbaaab=d

Axiom: aaababbaaab=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [3], [4], [5], [9], [20], [22], [30].

Axiom: babbaaab=d.

Reduce LHS:

Referenced by [4], [8], [10], [13].

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

Critical pair: cbabbaaab=1.

Reduce LHS:

Defines rule #1.

Referenced by [6], [8], [10], [11], [15], [19], [22], [31].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [6], [7], [25], [26], [28].

Overlap of [5] ac=ca with [4] cd=1:

Critical pair: a=cad.

Flip LHS and RHS.

Referenced by [7], [24].

Overlap of [5] ac=ca with [6] cad=a:

Critical pair: aa=caad.

Flip LHS and RHS.

Referenced by [9], [16], [22].

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

Critical pair: babbcd=dabbcb.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [7] caad=aa with [8] dabbcb=babb:

Critical pair: caababb=aaabbcb.

Reduce RHS:

Referenced by [14].

Overlap of [8] dabbcb=babb with [3] babbcb=d:

Critical pair: dabbcd=babbabbcb.

Reduce LHS:

Reduce RHS:

Referenced by [11], [12].

Overlap of [4] cd=1 with [10] dabb=babd:

Critical pair: cbabd=abb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [12], [13], [14], [19].

Overlap of [8] dabbcb=babb with [10] dabb=babd:

Critical pair: babdcb=babb.

Reduce RHS:

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

Overlap of [3] babbcb=d with [11] abb=cbabd:

Critical pair: bcbabdcb=d.

Reduce LHS:

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

Overlap of [9] caababb=cbbcb with [11] abb=cbabd:

Critical pair: caabcbabd=cbbcb.

Referenced by [16].

Overlap of [13] bcbcbabd=d with [12] babdcb=bcbabd:

Critical pair: bcbcbcbabd=dcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [14] caabcbabd=cbbcb with [12] babdcb=bcbabd:

Critical pair: caabcbcbabd=cbbcbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [18].

Overlap of [15] dcb=b with [16] cbbcbcb=aa:

Critical pair: daa=bbcbcb.

Flip LHS and RHS.

Defines rule #14.

Referenced by [19], [25], [26].

Overlap of [16] cbbcbcb=aa with [16] cbbcbcb=aa:

Critical pair: cbbcbaa=aabcbcb.

Flip LHS and RHS.

Defines rule #12.

Overlap of [11] abb=cbabd with [17] bbcbcb=daa:

Critical pair: adaa=cbabdcbcb.

Reduce RHS:

Referenced by [20], [21].

Overlap of [19] adaa=1 with [2] aaa=c:

Critical pair: adc=a.

Referenced by [22].

Overlap of [19] adaa=1 with [19] adaa=1:

Critical pair: ada=daa.

Referenced by [22].

Overlap of [20] adc=a with [7] caad=aa:

Critical pair: adaa=aaad.

Reduce LHS:

Reduce RHS:

Defines rule #2.

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

Overlap of [13] bcbcbabd=d with [22] dc=1:

Critical pair: bcbcbab=dc.

Reduce RHS:

Referenced by [25], [26], [27].

Overlap of [22] dc=1 with [6] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [31], [32].

Overlap of [17] bbcbcb=daa with [23] bcbcbab=1:

Critical pair: bbc=daacbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [17] bbcbcb=daa with [23] bcbcbab=1:

Critical pair: bbcbc=daacbcbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [23] bcbcbab=1 with [23] bcbcbab=1:

Critical pair: bcbcba=cbcbab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [28], [29].

Overlap of [5] ac=ca with [27] cbcbab=bcbcba:

Critical pair: abcbcba=cabcbab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [22] dc=1 with [27] cbcbab=bcbcba:

Critical pair: dbcbcba=bcbab.

Referenced by [30].

Overlap of [29] dbcbcba=bcbab with [2] aaa=c:

Critical pair: dbcbcbc=bcbabaa.

Referenced by [31].

Overlap of [30] dbcbcbc=bcbabaa with [4] cd=1:

Critical pair: dbcbcb=bcbabaad.

Reduce RHS:

Defines rule #9.

Referenced by [32].

Overlap of [24] ad=da with [31] dbcbcb=bcbabdaa:

Critical pair: abcbabdaa=dabcbcb.

Flip LHS and RHS.

Defines rule #11.