Certificate for #1502 ⟨a, b | abaabbbaab=1⟩

Completion settings:

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

Axiom: abaabbbaab=1.

Referenced by [4].

Axiom: aa=c.

Defines rule #2.

Referenced by [3], [4], [5], [7], [10], [27], [29], [40], [43], [45], [48], [50], [53].

Axiom: bbbaabab=d.

Reduce LHS:

Defines rule #15.

Referenced by [6], [8], [9], [14], [19], [20], [21], [28], [33], [35], [37], [45].

Overlap of [1] abaabbbaab=1 with [2] aa=c:

Critical pair: abcbbbaab=1.

Reduce LHS:

Referenced by [7], [8], [9], [11], [13], [18], [22].

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

Critical pair: ac=ca.

Defines rule #1.

Referenced by [12], [15], [26], [35], [37], [39], [47], [52].

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

Critical pair: bbbcbad=dbbcbab.

Flip LHS and RHS.

Referenced by [31].

Overlap of [2] aa=c with [4] abcbbbcb=1:

Critical pair: a=cbcbbbcb.

Flip LHS and RHS.

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

Overlap of [4] abcbbbcb=1 with [3] bbbcbab=d:

Critical pair: abcd=ab.

Referenced by [10].

Overlap of [4] abcbbbcb=1 with [3] bbbcbab=d:

Critical pair: abcbbbcd=bbcbab.

Referenced by [16].

Overlap of [2] aa=c with [8] abcd=ab:

Critical pair: aab=cbcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] abcbbbcb=1 with [10] cbcd=cb:

Critical pair: abcbbbcb=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [14], [16], [30], [44], [46], [51].

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

Critical pair: a=cad.

Flip LHS and RHS.

Referenced by [24].

Overlap of [4] abcbbbcb=1 with [7] cbcbbbcb=a:

Critical pair: abcbbba=cbbbcb.

Referenced by [17].

Overlap of [7] cbcbbbcb=a with [3] bbbcbab=d:

Critical pair: cbcbbbcd=abbcbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [7] cbcbbbcb=a with [7] cbcbbbcb=a:

Critical pair: cbcbbba=acbbbcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [9] abcbbbcd=bbcbab with [11] cd=1:

Critical pair: abcbbb=bbcbab.

Referenced by [17], [18], [19], [20], [22].

Overlap of [13] abcbbba=cbbbcb with [16] abcbbb=bbcbab:

Critical pair: bbcbaba=cbbbcb.

Flip LHS and RHS.

Defines rule #12.

Referenced by [35], [37].

Overlap of [4] abcbbbcb=1 with [16] abcbbb=bbcbab:

Critical pair: bbcbabcb=1.

Referenced by [21], [22], [23].

Overlap of [16] abcbbb=bbcbab with [3] bbbcbab=d:

Critical pair: abcbd=bbcbabbcbab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [35], [36], [37].

Overlap of [16] abcbbb=bbcbab with [3] bbbcbab=d:

Critical pair: abcbbd=bbcbabbbcbab.

Reduce RHS:

Referenced by [25].

Overlap of [3] bbbcbab=d with [18] bbcbabcb=1:

Critical pair: b=dcb.

Flip LHS and RHS.

Referenced by [23].

Overlap of [4] abcbbbcb=1 with [18] bbcbabcb=1:

Critical pair: abcbbbc=bcbabcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35], [40].

Overlap of [21] dcb=b with [18] bbcbabcb=1:

Critical pair: dc=bbcbabcb.

Reduce RHS:

Defines rule #3.

Referenced by [24], [26], [32], [35], [38], [40], [45], [48], [53].

Overlap of [23] dc=1 with [12] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #5.

Referenced by [25], [30], [31], [44], [49], [51], [52].

Simplify [20] abcbbd=bbcbad.

Reduce RHS:

Referenced by [26].

Overlap of [25] abcbbd=bbcbda with [23] dc=1:

Critical pair: abcbb=bbcbdac.

Reduce RHS:

Defines rule #8.

Referenced by [27], [35], [37], [52].

Overlap of [2] aa=c with [26] abcbb=bbcba:

Critical pair: abbcba=cbcbb.

Referenced by [28], [29].

Overlap of [3] bbbcbab=d with [27] abbcba=cbcbb:

Critical pair: bbbcbcbcbb=dbcba.

Defines rule #23.

Referenced by [36].

Overlap of [27] abbcba=cbcbb with [2] aa=c:

Critical pair: abbcbc=cbcbba.

Referenced by [30].

Overlap of [29] abbcbc=cbcbba with [11] cd=1:

Critical pair: abbcb=cbcbbad.

Reduce RHS:

Defines rule #7.

Referenced by [34], [40], [41], [45].

Simplify [6] dbbcbab=bbbcbad.

Reduce RHS:

Defines rule #14.

Referenced by [34].

Overlap of [23] dc=1 with [15] cabbbcb=cbcbbba:

Critical pair: dcbcbbba=abbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [33], [37], [42].

Overlap of [3] bbbcbab=d with [32] abbbcb=bcbbba:

Critical pair: bbbcbbcbbba=dbbcb.

Referenced by [43].

Overlap of [31] dbbcbab=bbbcbda with [30] abbcb=cbcbbda:

Critical pair: dbbcbcbcbbda=bbbcbdabcb.

Referenced by [53].

Overlap of [17] cbbbcb=bbcbaba with [19] bbcbcbcbbb=abcbd:

Critical pair: cbabcbd=bbcbabacbcbbb.

Reduce RHS:

Referenced by [38].

Overlap of [28] bbbcbcbcbb=dbcba with [19] bbcbcbcbbb=abcbd:

Critical pair: babcbd=dbcbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [41], [42].

Overlap of [32] abbbcb=bcbbba with [19] bbcbcbcbbb=abcbd:

Critical pair: ababcbd=bcbbbacbcbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [35] cbabcbd=bcbab with [23] dc=1:

Critical pair: cbabcb=bcbabc.

Defines rule #6.

Referenced by [39], [40].

Overlap of [5] ac=ca with [38] cbabcb=bcbabc:

Critical pair: abcbabc=cababcb.

Flip LHS and RHS.

Defines rule #9.

Overlap of [38] cbabcb=bcbabc with [22] bcbabcb=bbcbabc:

Critical pair: cbabbcbabc=bcbabcabcb.

Reduce LHS:

Referenced by [46].

Overlap of [36] dbcbab=babcbd with [30] abbcb=cbcbbda:

Critical pair: dbcbcbcbbda=babcbdbcb.

Referenced by [48].

Overlap of [36] dbcbab=babcbd with [32] abbbcb=bcbbba:

Critical pair: dbcbbcbbba=babcbdbbcb.

Referenced by [50].

Overlap of [33] bbbcbbcbbba=dbbcb with [2] aa=c:

Critical pair: bbbcbbcbbbc=dbbcba.

Referenced by [44].

Overlap of [43] bbbcbbcbbbc=dbbcba with [11] cd=1:

Critical pair: bbbcbbcbbb=dbbcbad.

Reduce RHS:

Defines rule #25.

Referenced by [45].

Overlap of [44] bbbcbbcbbb=dbbcbda with [3] bbbcbab=d:

Critical pair: bbbcbbcbbd=dbbcbdabbcbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [40] cbcbcbbbc=bcbabcabcb with [11] cd=1:

Critical pair: cbcbcbbb=bcbabcabcbd.

Defines rule #16.

Referenced by [47].

Overlap of [5] ac=ca with [46] cbcbcbbb=bcbabcabcbd:

Critical pair: abcbabcabcbd=cabcbcbbb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [41] dbcbcbcbbda=babcbdbcb with [2] aa=c:

Critical pair: dbcbcbcbbdc=babcbdbcba.

Reduce LHS:

Defines rule #18.

Referenced by [49].

Overlap of [24] ad=da with [48] dbcbcbcbb=babcbdbcba:

Critical pair: ababcbdbcba=dabcbcbcbb.

Flip LHS and RHS.

Defines rule #19.

Overlap of [42] dbcbbcbbba=babcbdbbcb with [2] aa=c:

Critical pair: dbcbbcbbbc=babcbdbbcba.

Referenced by [51].

Overlap of [50] dbcbbcbbbc=babcbdbbcba with [11] cd=1:

Critical pair: dbcbbcbbb=babcbdbbcbad.

Reduce RHS:

Defines rule #22.

Referenced by [52].

Overlap of [24] ad=da with [51] dbcbbcbbb=babcbdbbcbda:

Critical pair: ababcbdbbcbda=dabcbbcbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [34] dbbcbcbcbbda=bbbcbdabcb with [2] aa=c:

Critical pair: dbbcbcbcbbdc=bbbcbdabcba.

Reduce LHS:

Defines rule #20.