Certificate for #1099 ⟨a, b | aabbba=baa⟩

Completion settings:

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

Axiom: aabbba=baa.

Referenced by [5].

Axiom: bbb=c.

Defines rule #22.

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

Axiom: ccaa=d.

Referenced by [7], [9], [15].

Axiom: acaca=e.

Defines rule #11.

Referenced by [8], [9], [10], [11], [12], [13], [14], [20], [21], [29], [30], [31], [32].

Overlap of [1] aabbba=baa with [2] bbb=c:

Critical pair: aaca=baa.

Flip LHS and RHS.

Defines rule #15.

Referenced by [7], [11], [12], [18], [20].

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

Critical pair: bc=cb.

Defines rule #21.

Referenced by [7].

Overlap of [6] bc=cb with [3] ccaa=d:

Critical pair: bd=cbcaa.

Reduce RHS:

Defines rule #14.

Referenced by [8].

Overlap of [2] bbb=c with [7] bd=dca:

Critical pair: bbdca=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Overlap of [3] ccaa=d with [4] acaca=e:

Critical pair: ccae=dcaca.

Referenced by [16].

Overlap of [4] acaca=e with [4] acaca=e:

Critical pair: ace=eca.

Defines rule #3.

Referenced by [24].

Overlap of [2] bbb=c with [5] baa=aaca:

Critical pair: bbaaca=caa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [13], [14], [15], [19], [21], [22], [24].

Overlap of [5] baa=aaca with [4] acaca=e:

Critical pair: bae=aacacaca.

Reduce RHS:

Defines rule #17.

Overlap of [4] acaca=e with [11] caa=aeca:

Critical pair: acaaeca=ea.

Reduce LHS:

Referenced by [17].

Overlap of [11] caa=aeca with [4] acaca=e:

Critical pair: cae=aecacaca.

Reduce RHS:

Defines rule #7.

Referenced by [15], [16], [17], [18], [19], [20], [21], [23], [24], [30], [32].

Overlap of [3] ccaa=d with [11] caa=aeca:

Critical pair: caeca=d.

Reduce LHS:

Defines rule #12.

Referenced by [17], [20], [21], [22], [23], [26], [30], [32].

Overlap of [9] ccae=dcaca with [14] cae=aece:

Critical pair: caece=dcaca.

Reduce LHS:

Defines rule #13.

Referenced by [20], [21], [30], [32].

Overlap of [13] aaecaeca=ea with [14] cae=aece:

Critical pair: aaeaececa=ea.

Reduce LHS:

Defines rule #1.

Referenced by [18], [19].

Overlap of [5] baa=aaca with [17] aaed=ea:

Critical pair: bea=aacaed.

Reduce RHS:

Referenced by [27].

Overlap of [11] caa=aeca with [17] aaed=ea:

Critical pair: cea=aecaed.

Reduce RHS:

Flip LHS and RHS.

Referenced by [24], [28].

Overlap of [5] baa=aaca with [15] aececa=d:

Critical pair: bad=aacaececa.

Reduce RHS:

Defines rule #19.

Overlap of [11] caa=aeca with [15] aececa=d:

Critical pair: cad=aecaececa.

Reduce RHS:

Defines rule #9.

Overlap of [15] aececa=d with [11] caa=aeca:

Critical pair: aeceaeca=da.

Referenced by [25].

Overlap of [15] aececa=d with [14] cae=aece:

Critical pair: aeceaece=de.

Referenced by [24], [26].

Overlap of [11] caa=aeca with [19] aeaeced=cea:

Critical pair: cacea=aecaeaeced.

Reduce LHS:

Reduce RHS:

Referenced by [25].

Simplify [22] aeceaeca=da.

Reduce LHS:

Defines rule #2.

Overlap of [23] aeceaece=de with [15] aececa=d:

Critical pair: aeced=deca.

Referenced by [27], [28].

Simplify [18] bea=aaaeced.

Reduce RHS:

Defines rule #16.

Referenced by [31], [32].

Overlap of [19] aeaeced=cea with [26] aeced=deca:

Critical pair: aedeca=cea.

Flip LHS and RHS.

Defines rule #6.

Referenced by [29], [30].

Overlap of [28] cea=aedeca with [4] acaca=e:

Critical pair: cee=aedecacaca.

Reduce RHS:

Defines rule #8.

Overlap of [28] cea=aedeca with [15] aececa=d:

Critical pair: ced=aedecaececa.

Reduce RHS:

Defines rule #10.

Overlap of [27] bea=aadeca with [4] acaca=e:

Critical pair: bee=aadecacaca.

Reduce RHS:

Defines rule #18.

Overlap of [27] bea=aadeca with [15] aececa=d:

Critical pair: bed=aadecaececa.

Reduce RHS:

Defines rule #20.