Certificate for #2940 ⟨a, b | aaabababbba=1⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(c) = deg(d) = deg(b) = 0, c < d < b; deg(a) = 1
• Auxiliary generators:
  1. bbb=c
  2. aaaababa=d

Axiom: aaabababbba=1.

Referenced by [4].

Axiom: bbb=c.

Defines rule #5.

Referenced by [4], [5], [25], [39], [40], [41], [46], [50], [51], [52], [53], [57], [62], [63], [66], [69].

Axiom: aaaababa=d.

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

Overlap of [1] aaabababbba=1 with [2] bbb=c:

Critical pair: aaababaca=1.

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

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

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [15], [23], [40], [43], [45], [52].

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

Critical pair: aaababac=aababaca.

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

Overlap of [3] aaaababa=d with [4] aaababaca=1:

Critical pair: a=dca.

Flip LHS and RHS.

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

Overlap of [3] aaaababa=d with [4] aaababaca=1:

Critical pair: aaaabab=daababaca.

Referenced by [11], [18].

Overlap of [4] aaababaca=1 with [3] aaaababa=d:

Critical pair: aaababacd=aaababa.

Reduce LHS:

Referenced by [11], [19].

Overlap of [7] dca=a with [4] aaababaca=1:

Critical pair: dc=aaababaca.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [3] aaaababa=d with [10] aababacaa=dc:

Critical pair: aaaababdc=dababacaa.

Reduce LHS:

Referenced by [18].

Overlap of [4] aaababaca=1 with [10] aababacaa=dc:

Critical pair: adc=a.

Referenced by [15], [16].

Overlap of [10] aababacaa=dc with [3] aaaababa=d:

Critical pair: aababacd=dcaababa.

Reduce RHS:

Referenced by [20].

Overlap of [10] aababacaa=dc with [4] aaababaca=1:

Critical pair: aababac=dcababaca.

Reduce RHS:

Referenced by [15], [16], [17], [19], [20], [21].

Overlap of [10] aababacaa=dc with [10] aababacaa=dc:

Critical pair: aababacdc=dcbabacaa.

Reduce LHS:

Reduce RHS:

Referenced by [16], [17], [18], [19], [20], [21], [28].

Overlap of [4] aaababaca=1 with [12] adc=a:

Critical pair: aaababaca=dc.

Reduce LHS:

Referenced by [17], [22].

Overlap of [4] aaababaca=1 with [6] aaababac=aababaca:

Critical pair: aababacaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [22], [23], [26], [33], [34], [35], [36], [48], [59].

Simplify [8] aaaabab=daababaca.

Reduce RHS:

Referenced by [33].

Overlap of [9] aababacad=aaababa with [14] aababac=ababaca:

Critical pair: ababacaad=aaababa.

Reduce LHS:

Referenced by [35].

Overlap of [13] aababacd=aababa with [14] aababac=ababaca:

Critical pair: ababacad=aababa.

Reduce LHS:

Referenced by [36].

Simplify [14] aababac=ababaca.

Reduce RHS:

Referenced by [34].

Simplify [16] dbcabacaaaa=dc.

Reduce RHS:

Referenced by [24].

Overlap of [17] dc=1 with [5] cb=bc:

Critical pair: dbc=b.

Referenced by [24], [28].

Simplify [22] dbcabacaaaa=1.

Reduce LHS:

Referenced by [25], [27], [29], [30], [31], [32].

Overlap of [2] bbb=c with [24] babacaaaa=1:

Critical pair: bb=cabacaaaa.

Flip LHS and RHS.

Referenced by [26].

Overlap of [17] dc=1 with [25] cabacaaaa=bb:

Critical pair: dbb=abacaaaa.

Flip LHS and RHS.

Referenced by [27], [29], [31], [37].

Overlap of [24] babacaaaa=1 with [26] abacaaaa=dbb:

Critical pair: babacaaadbb=bacaaaa.

Referenced by [38].

Simplify [15] ababaca=dbcabacaa.

Reduce RHS:

Referenced by [29], [40].

Overlap of [28] ababaca=babacaa with [26] abacaaaa=dbb:

Critical pair: abdbb=babacaaaaa.

Reduce RHS:

Referenced by [30].

Overlap of [24] babacaaaa=1 with [29] abdbb=a:

Critical pair: babacaaaa=bdbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31], [39].

Overlap of [30] bdbb=1 with [24] babacaaaa=1:

Critical pair: bdb=abacaaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [31] dbb=bdb with [24] babacaaaa=1:

Critical pair: db=bdbabacaaaa.

Reduce RHS:

Defines rule #4.

Referenced by [33], [34], [35], [36], [37], [39], [44], [47], [48], [49], [51], [58], [59], [61], [64], [65], [67], [68], [70].

Simplify [18] aaaabab=ddbcabacaaa.

Reduce RHS:

Referenced by [51].

Simplify [21] aababac=dbcabacaa.

Reduce RHS:

Referenced by [40].

Overlap of [19] dbcabacaaad=aaababa with [32] db=bd:

Critical pair: bdcabacaaad=aaababa.

Reduce LHS:

Referenced by [38], [50].

Overlap of [20] dbcabacaad=aababa with [32] db=bd:

Critical pair: bdcabacaad=aababa.

Reduce LHS:

Referenced by [46].

Simplify [26] abacaaaa=dbb.

Reduce RHS:

Defines rule #20.

Referenced by [40], [51], [52], [54].

Overlap of [27] babacaaadbb=bacaaaa with [35] babacaaad=aaababa:

Critical pair: aaabababb=bacaaaa.

Defines rule #19.

Overlap of [30] bdbb=1 with [32] db=bd:

Critical pair: bbdb=1.

Reduce LHS:

Defines rule #2.

Referenced by [40], [41], [42], [51], [52], [57], [62], [63], [66], [69].

Overlap of [37] abacaaaa=bbd with [34] aababac=babacaa:

Critical pair: abacaaababacaa=bbdababac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41], [42].

Overlap of [2] bbb=c with [40] bbdababac=abaca:

Critical pair: babaca=cdababac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [43], [51].

Overlap of [40] bbdababac=abaca with [39] cd=1:

Critical pair: bbdababa=abacad.

Flip LHS and RHS.

Defines rule #7.

Referenced by [44], [55].

Overlap of [41] ababac=babaca with [5] cb=bc:

Critical pair: abababc=babacab.

Defines rule #8.

Referenced by [45].

Overlap of [42] abacad=bbdababa with [32] db=bd:

Critical pair: abacabd=bbdababab.

Defines rule #9.

Referenced by [47].

Overlap of [43] abababc=babacab with [5] cb=bc:

Critical pair: abababbc=babacabb.

Defines rule #10.

Overlap of [2] bbb=c with [36] babacaad=aababa:

Critical pair: bbaababa=cabacaad.

Flip LHS and RHS.

Referenced by [48].

Overlap of [44] abacabd=bbdababab with [32] db=bd:

Critical pair: abacabbd=bbdabababb.

Defines rule #11.

Overlap of [17] dc=1 with [46] cabacaad=bbaababa:

Critical pair: dbbaababa=abacaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [49], [56].

Overlap of [48] abacaad=bbdaababa with [32] db=bd:

Critical pair: abacaabd=bbdaababab.

Defines rule #14.

Referenced by [58].

Overlap of [2] bbb=c with [35] babacaaad=aaababa:

Critical pair: bbaaababa=cabacaaad.

Flip LHS and RHS.

Referenced by [59].

Overlap of [33] aaaabab=bdabacaaa with [41] ababac=babaca:

Critical pair: aaaabbabaca=bdabacaaaabac.

Reduce RHS:

Referenced by [52].

Overlap of [51] aaaabbabaca=bdac with [37] abacaaaa=bbd:

Critical pair: aaaabbbbd=bdacaaa.

Reduce LHS:

Defines rule #13.

Referenced by [53], [54], [55], [56], [60].

Overlap of [52] aaaab=bdacaaa with [2] bbb=c:

Critical pair: aaaac=bdacaaabb.

Flip LHS and RHS.

Referenced by [57].

Overlap of [52] aaaab=bdacaaa with [37] abacaaaa=bbd:

Critical pair: aaabbd=bdacaaaacaaaa.

Flip LHS and RHS.

Referenced by [62].

Overlap of [52] aaaab=bdacaaa with [42] abacad=bbdababa:

Critical pair: aaabbdababa=bdacaaaacad.

Flip LHS and RHS.

Referenced by [63].

Overlap of [52] aaaab=bdacaaa with [48] abacaad=bbdaababa:

Critical pair: aaabbdaababa=bdacaaaacaad.

Flip LHS and RHS.

Referenced by [66].

Overlap of [2] bbb=c with [53] bdacaaabb=aaaac:

Critical pair: bbaaaac=cdacaaabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [49] abacaabd=bbdaababab with [32] db=bd:

Critical pair: abacaabbd=bbdaabababb.

Defines rule #16.

Overlap of [17] dc=1 with [50] cabacaaad=bbaaababa:

Critical pair: dbbaaababa=abacaaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [60], [61].

Overlap of [52] aaaab=bdacaaa with [59] abacaaad=bbdaaababa:

Critical pair: aaabbdaaababa=bdacaaaacaaad.

Flip LHS and RHS.

Referenced by [69].

Overlap of [59] abacaaad=bbdaaababa with [32] db=bd:

Critical pair: abacaaabd=bbdaaababab.

Defines rule #18.

Overlap of [2] bbb=c with [54] bdacaaaacaaaa=aaabbd:

Critical pair: bbaaabbd=cdacaaaacaaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Overlap of [2] bbb=c with [55] bdacaaaacad=aaabbdababa:

Critical pair: bbaaabbdababa=cdacaaaacad.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [64].

Overlap of [63] acaaaacad=bbaaabbdababa with [32] db=bd:

Critical pair: acaaaacabd=bbaaabbdababab.

Defines rule #22.

Referenced by [65].

Overlap of [64] acaaaacabd=bbaaabbdababab with [32] db=bd:

Critical pair: acaaaacabbd=bbaaabbdabababb.

Defines rule #23.

Overlap of [2] bbb=c with [56] bdacaaaacaad=aaabbdaababa:

Critical pair: bbaaabbdaababa=cdacaaaacaad.

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Referenced by [67].

Overlap of [66] acaaaacaad=bbaaabbdaababa with [32] db=bd:

Critical pair: acaaaacaabd=bbaaabbdaababab.

Defines rule #25.

Referenced by [68].

Overlap of [67] acaaaacaabd=bbaaabbdaababab with [32] db=bd:

Critical pair: acaaaacaabbd=bbaaabbdaabababb.

Defines rule #26.

Overlap of [2] bbb=c with [60] bdacaaaacaaad=aaabbdaaababa:

Critical pair: bbaaabbdaaababa=cdacaaaacaaad.

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [70].

Overlap of [69] acaaaacaaad=bbaaabbdaaababa with [32] db=bd:

Critical pair: acaaaacaaabd=bbaaabbdaaababab.

Defines rule #28.