Certificate for #14293 ⟨a, b | abba=b, aaaaaa=1⟩

Completion settings:

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

Axiom: abba=b.

Referenced by [6], [7], [8], [9], [12], [14], [15], [17], [19], [20], [50].

Axiom: aaaaaa=1.

Defines rule #16.

Referenced by [7], [8], [21], [52].

Axiom: bbb=c.

Defines rule #9.

Referenced by [5], [6], [15], [20], [22], [23], [25], [30], [31], [38], [44], [46], [47], [51].

Axiom: abababa=d.

Referenced by [9], [10], [11], [13], [16], [18], [24], [34].

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

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [11], [19], [20], [28], [30], [31], [34], [38], [44], [46], [47], [48], [50], [51], [55], [57].

Overlap of [1] abba=b with [1] abba=b:

Critical pair: abbb=bbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [11], [19], [24], [26], [34], [35], [36], [38], [40], [41], [47].

Overlap of [1] abba=b with [2] aaaaaa=1:

Critical pair: abb=baaaaa.

Flip LHS and RHS.

Referenced by [13], [19].

Overlap of [2] aaaaaa=1 with [1] abba=b:

Critical pair: aaaaab=bba.

Referenced by [12].

Overlap of [1] abba=b with [4] abababa=d:

Critical pair: abbd=bbababa.

Flip LHS and RHS.

Referenced by [14], [35].

Overlap of [4] abababa=d with [4] abababa=d:

Critical pair: abd=dba.

Flip LHS and RHS.

Referenced by [17], [19], [22], [31], [39], [48].

Overlap of [6] ca=ac with [4] abababa=d:

Critical pair: cd=acbababa.

Reduce RHS:

Defines rule #1.

Referenced by [15], [19], [20], [21], [22], [25], [27], [31], [33], [38], [43], [44], [45], [46], [47], [48], [49], [50], [51], [53], [56].

Overlap of [8] aaaaab=bba with [1] abba=b:

Critical pair: aaaab=bbaba.

Referenced by [14], [19], [21], [36].

Overlap of [4] abababa=d with [7] baaaaa=abb:

Critical pair: ababaabb=daaaa.

Flip LHS and RHS.

Referenced by [19].

Overlap of [12] aaaab=bbaba with [1] abba=b:

Critical pair: aaab=bbababa.

Reduce RHS:

Referenced by [15], [16], [17], [18], [19], [29], [37].

Overlap of [1] abba=b with [14] aaab=abbd:

Critical pair: abbabbd=baab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [4] abababa=d with [14] aaab=abbd:

Critical pair: ababababbd=daab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [14] aaab=abbd with [1] abba=b:

Critical pair: aab=abbdba.

Reduce RHS:

Defines rule #15.

Referenced by [20], [21], [22], [23], [24], [29], [32], [34], [37], [38], [42], [47].

Overlap of [14] aaab=abbd with [4] abababa=d:

Critical pair: aad=abbdababa.

Flip LHS and RHS.

Referenced by [38].

Overlap of [14] aaab=abbd with [7] baaaaa=abb:

Critical pair: aaaabb=abbdaaaaa.

Reduce LHS:

Reduce RHS:

Referenced by [21], [35].

Overlap of [1] abba=b with [17] aab=bbd:

Critical pair: abbbbd=bab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24], [29], [30], [34], [36], [41], [42], [46].

Overlap of [2] aaaaaa=1 with [17] aab=bbd:

Critical pair: aaaabbd=b.

Reduce LHS:

Defines rule #4.

Referenced by [25], [26], [27], [46], [53], [60].

Overlap of [10] dba=abd with [17] aab=bbd:

Critical pair: dbbbd=abdab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32], [47].

Overlap of [17] aab=bbd with [3] bbb=c:

Critical pair: aac=bbdbb.

Defines rule #14.

Referenced by [31], [40].

Overlap of [17] aab=bbd with [4] abababa=d:

Critical pair: ad=bbdababa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [3] bbb=c with [21] bdddcc=b:

Critical pair: bbb=cdddcc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [28].

Overlap of [21] bdddcc=b with [6] ca=ac:

Critical pair: bdddcac=ba.

Reduce LHS:

Referenced by [39], [46].

Overlap of [21] bdddcc=b with [11] cd=dc:

Critical pair: bdddcdc=bd.

Reduce LHS:

Referenced by [33].

Overlap of [25] dddccc=c with [5] cb=bc:

Critical pair: dddccbc=cb.

Reduce LHS:

Reduce RHS:

Referenced by [43].

Overlap of [17] aab=bbd with [20] bab=abdc:

Critical pair: aaabdc=bbdab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38], [51].

Overlap of [20] bab=abdc with [3] bbb=c:

Critical pair: bac=abdcbb.

Reduce RHS:

Referenced by [38].

Overlap of [10] dba=abd with [23] aac=bbdbb:

Critical pair: dbbbdbb=abdac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36], [41].

Overlap of [17] aab=bbd with [22] abdab=ddc:

Critical pair: addc=bbddab.

Flip LHS and RHS.

Referenced by [34].

Overlap of [27] bddddcc=bd with [11] cd=dc:

Critical pair: bddddcdc=bdd.

Reduce LHS:

Referenced by [46].

Overlap of [4] abababa=d with [20] bab=abdc:

Critical pair: aabdcaba=d.

Reduce LHS:

Referenced by [39], [40], [48].

Overlap of [9] bbababa=abbd with [19] bbabab=bddcc:

Critical pair: bddcca=abbd.

Reduce LHS:

Referenced by [48].

Simplify [12] aaaab=bbaba.

Reduce RHS:

Referenced by [37].

Overlap of [36] aaaab=bddbbc with [14] aaab=abbd:

Critical pair: aabbd=bddbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38], [46], [47], [51].

Overlap of [18] abbdababa=aad with [29] bbdab=abbddc:

Critical pair: aabbddcaba=aad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [58].

Overlap of [10] dba=abd with [34] addacc=d:

Critical pair: dbd=abdddacc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [41], [42], [48], [50].

Overlap of [34] addacc=d with [6] ca=ac:

Critical pair: addacac=da.

Reduce LHS:

Flip LHS and RHS.

Referenced by [46], [47], [51], [59].

Overlap of [20] bab=abdc with [39] aba=dbd:

Critical pair: bdbd=abdca.

Reduce RHS:

Flip LHS and RHS.

Referenced by [45], [46], [51].

Overlap of [39] aba=dbd with [20] bab=abdc:

Critical pair: aabdc=dbdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [44], [46], [48], [50], [51], [54].

Overlap of [28] dddbccc=bc with [11] cd=dc:

Critical pair: dddbccdc=bcd.

Reduce LHS:

Reduce RHS:

Referenced by [46].

Overlap of [42] dbdb=bbddc with [42] dbdb=bbddc:

Critical pair: dbbbddc=bbddcdb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [46], [48], [50], [51].

Overlap of [41] ddbbc=bdbd with [11] cd=dc:

Critical pair: ddbbdc=bdbdd.

Referenced by [46], [47], [51], [55].

Simplify [26] bdddacc=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [47], [48], [50], [51].

Overlap of [22] abdab=ddc with [46] ba=abdbb:

Critical pair: abdaabdbb=ddca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [46] ba=abdbb with [34] addacc=d:

Critical pair: bd=abdbbddacc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [49].

Overlap of [48] dddbdcc=bd with [11] cd=dc:

Critical pair: dddbdcdc=bdd.

Reduce LHS:

Referenced by [53].

Overlap of [1] abba=b with [46] ba=abdbb:

Critical pair: ababdbb=b.

Reduce LHS:

Referenced by [51].

Overlap of [24] bbdbbddac=ad with [40] da=addbbdbbc:

Critical pair: bbdbbdaddbbdbbcc=ad.

Reduce LHS:

Referenced by [52].

Overlap of [2] aaaaaa=1 with [51] addddcc=ad:

Critical pair: aaaaaad=ddddcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [49] dddbddcc=bdd with [11] cd=dc:

Critical pair: dddbddcdc=bddd.

Reduce LHS:

Defines rule #6.

Referenced by [54], [58].

Overlap of [53] dddb=bddd with [42] dbdb=bbddc:

Critical pair: ddbbddc=bddddb.

Reduce RHS:

Referenced by [56].

Overlap of [45] ddbbdc=bdbdd with [5] cb=bc:

Critical pair: ddbbdbc=bdbddb.

Referenced by [57].

Overlap of [54] ddbbddc=bdbddd with [11] cd=dc:

Critical pair: ddbbdddc=bdbdddd.

Referenced by [60].

Overlap of [55] ddbbdbc=bdbddb with [5] cb=bc:

Critical pair: ddbbdbbc=bdbddbb.

Referenced by [59].

Simplify [38] aad=bbdbdddbdc.

Reduce RHS:

Defines rule #13.

Simplify [40] da=addbbdbbc.

Reduce RHS:

Referenced by [61].

Overlap of [56] ddbbdddc=bdbdddd with [21] bdddcc=b:

Critical pair: ddbb=bdbddddc.

Defines rule #8.

Referenced by [61].

Simplify [59] da=abdbddbb.

Reduce RHS:

Defines rule #10.