Certificate for #4107 ⟨a, b | bab=aaa, bbbb=1⟩

Completion settings:

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

Axiom: bab=aaa.

Referenced by [10].

Axiom: bbbb=1.

Referenced by [5].

Axiom: bbb=c.

Referenced by [5], [6], [7], [8].

Axiom: caacaacaac=d.

Referenced by [18], [19], [20], [21], [27].

Overlap of [2] bbbb=1 with [3] bbb=c:

Critical pair: cb=1.

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

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

Critical pair: bc=cb.

Reduce RHS:

Referenced by [13].

Overlap of [5] cb=1 with [3] bbb=c:

Critical pair: cc=bb.

Flip LHS and RHS.

Referenced by [8], [9].

Overlap of [3] bbb=c with [7] bb=cc:

Critical pair: bbcc=cb.

Reduce LHS:

Reduce RHS:

Defines rule #17.

Referenced by [11], [12], [14], [19], [39].

Overlap of [5] cb=1 with [7] bb=cc:

Critical pair: ccc=b.

Flip LHS and RHS.

Defines rule #18.

Referenced by [10], [13].

Simplify [1] bab=aaa.

Reduce LHS:

Referenced by [11], [12].

Overlap of [10] cccaccc=aaa with [8] cccc=1:

Critical pair: ccca=aaac.

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

Overlap of [8] cccc=1 with [10] cccaccc=aaa:

Critical pair: caaa=accc.

Flip LHS and RHS.

Referenced by [16].

Overlap of [6] bc=1 with [11] ccca=aaac:

Critical pair: baaac=cca.

Reduce LHS:

Referenced by [20], [22].

Overlap of [8] cccc=1 with [11] ccca=aaac:

Critical pair: caaac=a.

Referenced by [15], [16], [17], [18], [20], [23], [29].

Overlap of [14] caaac=a with [14] caaac=a:

Critical pair: caaaa=aaaac.

Flip LHS and RHS.

Referenced by [21], [24].

Overlap of [14] caaac=a with [12] accc=caaa:

Critical pair: caacaaa=acc.

Flip LHS and RHS.

Referenced by [17], [21], [30].

Overlap of [14] caaac=a with [16] acc=caacaaa:

Critical pair: caacaacaaa=ac.

Referenced by [18], [21], [31].

Overlap of [4] caacaacaac=d with [14] caaac=a:

Critical pair: caacaacaaa=daaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [8] cccc=1 with [4] caacaacaac=d:

Critical pair: cccd=aacaacaac.

Flip LHS and RHS.

Referenced by [32].

Overlap of [13] aaacaac=cca with [4] caacaacaac=d:

Critical pair: aaad=ccaaacaac.

Reduce RHS:

Referenced by [25], [26].

Overlap of [16] acc=caacaaa with [4] caacaacaac=d:

Critical pair: acd=caacaaaaacaacaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [27], [31].

Overlap of [18] daaac=ac with [13] aaacaac=cca:

Critical pair: dcca=acaac.

Flip LHS and RHS.

Referenced by [32].

Overlap of [18] daaac=ac with [14] caaac=a:

Critical pair: daaaa=acaaac.

Reduce RHS:

Referenced by [24], [25].

Overlap of [23] daaaa=aa with [15] aaaac=caaaa:

Critical pair: dcaaaa=aac.

Flip LHS and RHS.

Defines rule #7.

Referenced by [28], [29], [30], [32], [41].

Overlap of [23] daaaa=aa with [20] aaad=a:

Critical pair: daaa=aaad.

Reduce RHS:

Defines rule #3.

Referenced by [26], [33].

Overlap of [25] daaa=a with [20] aaad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #1.

Referenced by [28], [29], [32], [33], [35], [37], [41], [44], [46].

Overlap of [4] caacaacaac=d with [21] caacaaca=acd:

Critical pair: acdac=d.

Referenced by [33], [34], [35], [40], [42].

Simplify [11] ccca=aaac.

Reduce RHS:

Defines rule #14.

Overlap of [14] caaac=a with [24] aac=dcaaaa:

Critical pair: cadcaaaa=a.

Reduce LHS:

Referenced by [32].

Simplify [16] acc=caacaaa.

Reduce RHS:

Defines rule #11.

Referenced by [37], [41].

Overlap of [17] caacaacaaa=ac with [21] caacaaca=acd:

Critical pair: acdaa=ac.

Defines rule #5.

Referenced by [36], [38], [41], [43].

Overlap of [19] aacaacaac=cccd with [22] acaac=dcca:

Critical pair: adccaaac=cccd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [39].

Overlap of [25] daaa=a with [27] acdac=d:

Critical pair: daad=acdac.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [35], [36], [37], [42], [43], [44], [45].

Overlap of [27] acdac=d with [27] acdac=d:

Critical pair: acdd=ddac.

Flip LHS and RHS.

Defines rule #8.

Referenced by [37], [45].

Overlap of [33] ddaa=d with [27] acdac=d:

Critical pair: ddad=dcdac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37], [40].

Overlap of [33] ddaa=d with [31] acdaa=ac:

Critical pair: ddaac=dcdaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [37], [38], [41], [45], [46].

Overlap of [36] dcdaa=dc with [30] acc=cdcaaaaaaa:

Critical pair: dcdacdcaaaaaaa=dccc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [44].

Overlap of [36] dcdaa=dc with [31] acdaa=ac:

Critical pair: dcdaac=dccdaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [8] cccc=1 with [32] cccd=daca:

Critical pair: cdaca=d.

Referenced by [40].

Overlap of [39] cdaca=d with [27] acdac=d:

Critical pair: cdacd=dcdac.

Reduce RHS:

Referenced by [41], [42], [43].

Overlap of [30] acc=cdcaaaaaaa with [40] cdacd=ddda:

Critical pair: acddda=cdcaaaaaaadacd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [40] cdacd=ddda with [27] acdac=d:

Critical pair: cdd=dddaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [45].

Overlap of [40] cdacd=ddda with [31] acdaa=ac:

Critical pair: cdac=dddaaa.

Reduce RHS:

Defines rule #9.

Referenced by [44].

Overlap of [37] dccc=acda with [43] cdac=dda:

Critical pair: dccdda=acdadac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [42] ddc=cdd with [41] cdcdcaaaaaa=acddda:

Critical pair: ddacddda=cdddcdcaaaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [46].

Overlap of [45] cdcdcaa=acddddda with [26] ad=da:

Critical pair: cdcdcada=acdddddad.

Reduce LHS:

Reduce RHS:

Defines rule #15.