Certificate for #2949 ⟨a, b | aaababbbaba=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. aaaa=c
  2. babbbab=d

Axiom: aaababbbaba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [9], [11], [19], [32], [38], [43], [45].

Axiom: babbbab=d.

Referenced by [4], [21], [26], [27], [28], [31].

Overlap of [1] aaababbbaba=1 with [3] babbbab=d:

Critical pair: aaada=1.

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

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [12], [15], [25], [29], [34], [39].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10], [11], [13], [14].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: aaad=aada.

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

Overlap of [6] cda=a with [2] aaaa=c:

Critical pair: cdc=aaaa.

Reduce RHS:

Referenced by [13].

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

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

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

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

Critical pair: cad=aaaada.

Reduce RHS:

Referenced by [12], [15], [20].

Overlap of [4] aaada=1 with [10] aadaa=cd:

Critical pair: aaadcd=adaa.

Reduce LHS:

Referenced by [13].

Overlap of [6] cda=a with [10] aadaa=cd:

Critical pair: cdcd=aadaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [10] aadaa=cd with [4] aaada=1:

Critical pair: aad=cdada.

Reduce RHS:

Referenced by [15], [16].

Overlap of [10] aadaa=cd with [10] aadaa=cd:

Critical pair: aadcd=cddaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [4] aaada=1 with [8] aaad=aada:

Critical pair: aadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [17], [18], [22], [26], [33], [36].

Simplify [13] adaaa=cd.

Reduce RHS:

Referenced by [19].

Overlap of [15] cddaa=ada with [16] cd=1:

Critical pair: daa=ada.

Flip LHS and RHS.

Referenced by [19].

Simplify [17] adaaa=1.

Reduce LHS:

Defines rule #2.

Referenced by [20], [24], [32], [41], [43], [45].

Overlap of [19] dc=1 with [11] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [23], [28], [30], [35], [40], [44].

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

Critical pair: babbd=dbbab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [22], [23].

Overlap of [16] cd=1 with [21] dbbab=babbd:

Critical pair: cbabbd=bbab.

Referenced by [24].

Overlap of [20] ad=da with [21] dbbab=babbd:

Critical pair: ababbd=dabbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [30].

Overlap of [22] cbabbd=bbab with [19] dc=1:

Critical pair: cbabb=bbabc.

Defines rule #6.

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

Overlap of [5] ac=ca with [24] cbabb=bbabc:

Critical pair: abbabc=cababb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [29].

Overlap of [24] cbabb=bbabc with [3] babbbab=d:

Critical pair: cd=bbabcbab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [3] babbbab=d with [26] bbabcbab=1:

Critical pair: babbba=dbabcbab.

Flip LHS and RHS.

Referenced by [36].

Overlap of [26] bbabcbab=1 with [3] babbbab=d:

Critical pair: bbabcbad=abbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [31].

Overlap of [5] ac=ca with [25] cababb=abbabc:

Critical pair: aabbabc=caababb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [34].

Overlap of [20] ad=da with [23] dabbab=ababbd:

Critical pair: aababbd=daabbab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [35].

Overlap of [3] babbbab=d with [28] abbbab=bbabcbda:

Critical pair: bbbabcbda=d.

Referenced by [32].

Overlap of [31] bbbabcbda=d with [2] aaaa=c:

Critical pair: bbbabcbdc=daaa.

Reduce LHS:

Defines rule #19.

Referenced by [33].

Overlap of [32] bbbabcb=daaa with [32] bbbabcb=daaa:

Critical pair: bbbabcdaaa=daaabbabcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [5] ac=ca with [29] caababb=aabbabc:

Critical pair: aaabbabc=caaababb.

Flip LHS and RHS.

Defines rule #14.

Referenced by [42].

Overlap of [20] ad=da with [30] daabbab=aababbd:

Critical pair: aaababbd=daaabbab.

Flip LHS and RHS.

Defines rule #15.

Referenced by [41].

Overlap of [16] cd=1 with [27] dbabcbab=babbba:

Critical pair: cbabbba=babcbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37], [39].

Overlap of [26] bbabcbab=1 with [36] babcbab=bbabcba:

Critical pair: bbabcbabbabcba=abcbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [38], [39].

Overlap of [2] aaaa=c with [37] abcbab=babcba:

Critical pair: aaababcba=cbcbab.

Referenced by [40].

Overlap of [37] abcbab=babcba with [36] babcbab=bbabcba:

Critical pair: abcbbabcba=babcbacbab.

Reduce RHS:

Referenced by [44].

Overlap of [38] aaababcba=cbcbab with [20] ad=da:

Critical pair: aaababcbda=cbcbabd.

Referenced by [43].

Overlap of [33] daaabbabcb=bbbabaaa with [35] daaabbab=aaababbd:

Critical pair: aaababbdcb=bbbabaaa.

Reduce LHS:

Defines rule #18.

Referenced by [42].

Overlap of [34] caaababb=aaabbabc with [41] aaababbb=bbbabaaa:

Critical pair: cbbbabaaa=aaabbabcb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [40] aaababcbda=cbcbabd with [2] aaaa=c:

Critical pair: aaababcbdc=cbcbabdaaa.

Reduce LHS:

Defines rule #13.

Overlap of [39] abcbbabcba=babcbcabab with [20] ad=da:

Critical pair: abcbbabcbda=babcbcababd.

Referenced by [45].

Overlap of [44] abcbbabcbda=babcbcababd with [2] aaaa=c:

Critical pair: abcbbabcbdc=babcbcababdaaa.

Reduce LHS:

Defines rule #20.