Certificate for #3071 ⟨a, b | aabababbbaa=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. bababbb=d

Axiom: aabababbbaa=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [8], [9], [10], [23], [31], [32], [33], [38], [39], [44], [48], [49], [52], [54].

Axiom: bababbb=d.

Referenced by [4], [12], [14].

Overlap of [1] aabababbbaa=1 with [3] bababbb=d:

Critical pair: aadaa=1.

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

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [18], [24], [42].

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

Critical pair: aad=daa.

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

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

Critical pair: aada=adaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [10].

Overlap of [2] aaaa=c with [6] aad=daa:

Critical pair: aadaa=cd.

Reduce LHS:

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

Overlap of [4] aadaa=1 with [6] aad=daa:

Critical pair: daaaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [10], [11], [13], [28], [35].

Overlap of [4] aadaa=1 with [6] aad=daa:

Critical pair: aadadaa=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [20], [21], [25], [26], [29], [30], [32], [33], [34], [40], [43], [45], [46], [50], [51], [53], [55], [56], [57], [58].

Simplify [8] dc=cd.

Reduce RHS:

Defines rule #2.

Referenced by [15], [19], [23], [31], [32], [33], [39], [44], [48], [49], [52], [54].

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

Critical pair: bababbd=dababbb.

Flip LHS and RHS.

Referenced by [13].

Overlap of [9] cd=1 with [12] dababbb=bababbd:

Critical pair: cbababbd=ababbb.

Flip LHS and RHS.

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

Overlap of [3] bababbb=d with [13] ababbb=cbababbd:

Critical pair: bcbababbd=d.

Referenced by [15].

Overlap of [14] bcbababbd=d with [11] dc=1:

Critical pair: bcbababb=dc.

Reduce RHS:

Referenced by [16], [17], [27].

Overlap of [15] bcbababb=1 with [15] bcbababb=1:

Critical pair: bcbabab=cbababb.

Flip LHS and RHS.

Referenced by [17].

Overlap of [16] cbababb=bcbabab with [15] bcbababb=1:

Critical pair: cbabab=bcbababcbababb.

Reduce RHS:

Defines rule #6.

Referenced by [18], [19], [22], [27], [29], [33], [49].

Overlap of [5] ac=ca with [17] cbabab=bcbaba:

Critical pair: abcbaba=cababab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [24].

Overlap of [11] dc=1 with [17] cbabab=bcbaba:

Critical pair: dbcbaba=babab.

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

Overlap of [10] ad=da with [19] dbcbaba=babab:

Critical pair: ababab=dabcbaba.

Flip LHS and RHS.

Referenced by [25].

Overlap of [19] dbcbaba=babab with [10] ad=da:

Critical pair: dbcbabda=bababd.

Referenced by [23].

Overlap of [19] dbcbaba=babab with [17] cbabab=bcbaba:

Critical pair: dbbcbaba=bababb.

Referenced by [26], [27].

Overlap of [21] dbcbabda=bababd with [2] aaaa=c:

Critical pair: dbcbabdc=bababdaaa.

Reduce LHS:

Defines rule #7.

Referenced by [40], [41].

Overlap of [5] ac=ca with [18] cababab=abcbaba:

Critical pair: aabcbaba=caababab.

Flip LHS and RHS.

Defines rule #11.

Referenced by [42].

Overlap of [10] ad=da with [20] dabcbaba=ababab:

Critical pair: aababab=daabcbaba.

Flip LHS and RHS.

Referenced by [43].

Overlap of [22] dbbcbaba=bababb with [10] ad=da:

Critical pair: dbbcbabda=bababbd.

Referenced by [44].

Overlap of [22] dbbcbaba=bababb with [17] cbabab=bcbaba:

Critical pair: dbbbcbaba=bababbb.

Reduce RHS:

Referenced by [28].

Overlap of [9] cd=1 with [27] dbbbcbaba=d:

Critical pair: cd=bbbcbaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30], [37].

Simplify [13] ababbb=cbababbd.

Reduce RHS:

Referenced by [33], [34].

Overlap of [28] bbbcbaba=1 with [10] ad=da:

Critical pair: bbbcbabda=d.

Referenced by [31], [34].

Overlap of [30] bbbcbabda=d with [2] aaaa=c:

Critical pair: bbbcbabdc=daaa.

Reduce LHS:

Defines rule #20.

Referenced by [32], [33], [34], [36].

Overlap of [31] bbbcbab=daaa with [31] bbbcbab=daaa:

Critical pair: bbbcbadaaa=daaabbcbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [17] cbabab=bcbaba with [29] ababbb=bbcbabda:

Critical pair: cbabbbcbabda=bcbabaabbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [30] bbbcbabda=d with [29] ababbb=bbcbabda:

Critical pair: bbbcbabdbbcbabda=dbabbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [9] cd=1 with [34] dbabbb=dbbbcbda:

Critical pair: cdbbbcbda=babbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [31] bbbcbab=daaa with [35] babbb=bbbcbda:

Critical pair: bbbcbbbcbda=daaabb.

Referenced by [48].

Overlap of [28] bbbcbaba=1 with [33] bcbabaabbb=cbda:

Critical pair: bbcbda=abbb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [38], [41], [47].

Overlap of [2] aaaa=c with [37] abbb=bbcbda:

Critical pair: aaabbcbda=cbbb.

Referenced by [39].

Overlap of [38] aaabbcbda=cbbb with [2] aaaa=c:

Critical pair: aaabbcbdc=cbbbaaa.

Reduce LHS:

Defines rule #13.

Referenced by [49].

Overlap of [10] ad=da with [23] dbcbab=bababdaaa:

Critical pair: abababdaaa=dabcbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [45].

Overlap of [23] dbcbab=bababdaaa with [37] abbb=bbcbda:

Critical pair: dbcbbbcbda=bababdaaabb.

Referenced by [52].

Overlap of [5] ac=ca with [24] caababab=aabcbaba:

Critical pair: aaabcbaba=caaababab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [10] ad=da with [25] daabcbaba=aababab:

Critical pair: aaababab=daaabcbaba.

Flip LHS and RHS.

Referenced by [49].

Overlap of [26] dbbcbabda=bababbd with [2] aaaa=c:

Critical pair: dbbcbabdc=bababbdaaa.

Reduce LHS:

Defines rule #16.

Referenced by [46], [47].

Overlap of [10] ad=da with [40] dabcbab=abababdaaa:

Critical pair: aabababdaaa=daabcbab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [50].

Overlap of [10] ad=da with [44] dbbcbab=bababbdaaa:

Critical pair: abababbdaaa=dabbcbab.

Flip LHS and RHS.

Defines rule #17.

Referenced by [51].

Overlap of [44] dbbcbab=bababbdaaa with [37] abbb=bbcbda:

Critical pair: dbbcbbbcbda=bababbdaaabb.

Referenced by [54].

Overlap of [36] bbbcbbbcbda=daaabb with [2] aaaa=c:

Critical pair: bbbcbbbcbdc=daaabbaaa.

Reduce LHS:

Defines rule #28.

Overlap of [43] daaabcbaba=aaababab with [17] cbabab=bcbaba:

Critical pair: daaabbcbaba=aaabababb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [10] ad=da with [45] daabcbab=aabababdaaa:

Critical pair: aaabababdaaa=daaabcbab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [10] ad=da with [46] dabbcbab=abababbdaaa:

Critical pair: aabababbdaaa=daabbcbab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [41] dbcbbbcbda=bababdaaabb with [2] aaaa=c:

Critical pair: dbcbbbcbdc=bababdaaabbaaa.

Reduce LHS:

Defines rule #21.

Referenced by [53].

Overlap of [10] ad=da with [52] dbcbbbcb=bababdaaabbaaa:

Critical pair: abababdaaabbaaa=dabcbbbcb.

Flip LHS and RHS.

Defines rule #22.

Referenced by [55].

Overlap of [47] dbbcbbbcbda=bababbdaaabb with [2] aaaa=c:

Critical pair: dbbcbbbcbdc=bababbdaaabbaaa.

Reduce LHS:

Defines rule #25.

Referenced by [56].

Overlap of [10] ad=da with [53] dabcbbbcb=abababdaaabbaaa:

Critical pair: aabababdaaabbaaa=daabcbbbcb.

Flip LHS and RHS.

Defines rule #23.

Referenced by [57].

Overlap of [10] ad=da with [54] dbbcbbbcb=bababbdaaabbaaa:

Critical pair: abababbdaaabbaaa=dabbcbbbcb.

Flip LHS and RHS.

Defines rule #26.

Referenced by [58].

Overlap of [10] ad=da with [55] daabcbbbcb=aabababdaaabbaaa:

Critical pair: aaabababdaaabbaaa=daaabcbbbcb.

Flip LHS and RHS.

Defines rule #24.

Overlap of [10] ad=da with [56] dabbcbbbcb=abababbdaaabbaaa:

Critical pair: aabababbdaaabbaaa=daabbcbbbcb.

Flip LHS and RHS.

Defines rule #27.