Certificate for #4283 ⟨a, b | ababaaaab=aa⟩

Completion settings:

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

Axiom: ababaaaab=aa.

Referenced by [5].

Axiom: ab=c.

Defines rule #23.

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

Axiom: aaaaa=d.

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

Axiom: cca=e.

Defines rule #3.

Referenced by [5], [6], [7], [10], [12], [15], [22], [24], [28], [30].

Overlap of [1] ababaaaab=aa with [2] ab=c:

Critical pair: cabaaaab=aa.

Reduce LHS:

Defines rule #5.

Referenced by [7], [13], [25], [27], [29].

Overlap of [4] cca=e with [2] ab=c:

Critical pair: ccc=eb.

Flip LHS and RHS.

Defines rule #21.

Overlap of [5] eaac=aa with [4] cca=e:

Critical pair: eaae=aaca.

Flip LHS and RHS.

Defines rule #9.

Referenced by [11], [12], [13], [14], [16], [17].

Overlap of [3] aaaaa=d with [2] ab=c:

Critical pair: aaaac=db.

Flip LHS and RHS.

Referenced by [21].

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

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #4.

Referenced by [22], [26], [28], [30].

Overlap of [4] cca=e with [3] aaaaa=d:

Critical pair: ccd=eaaaa.

Flip LHS and RHS.

Referenced by [19].

Overlap of [3] aaaaa=d with [7] aaca=eaae:

Critical pair: aaaeaae=dca.

Referenced by [22].

Overlap of [4] cca=e with [7] aaca=eaae:

Critical pair: cceaae=eaca.

Defines rule #6.

Referenced by [27], [28].

Overlap of [5] eaac=aa with [7] aaca=eaae:

Critical pair: eeaae=aaa.

Flip LHS and RHS.

Defines rule #8.

Referenced by [15], [16], [17], [18], [19], [20], [21], [22], [25], [26], [27], [28], [29], [30].

Overlap of [7] aaca=eaae with [7] aaca=eaae:

Critical pair: aaceaae=eaaeaca.

Defines rule #16.

Overlap of [4] cca=e with [13] aaa=eeaae:

Critical pair: cceeaae=eaa.

Defines rule #7.

Overlap of [7] aaca=eaae with [13] aaa=eeaae:

Critical pair: aaceeaae=eaaeaa.

Defines rule #17.

Overlap of [13] aaa=eeaae with [7] aaca=eaae:

Critical pair: aeaae=eeaaeca.

Defines rule #11.

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

Overlap of [13] aaa=eeaae with [13] aaa=eeaae:

Critical pair: aeeaae=eeaaea.

Defines rule #12.

Referenced by [22], [28], [30].

Simplify [10] eaaaa=ccd.

Reduce LHS:

Defines rule #10.

Referenced by [22], [23], [25], [27], [28], [29], [30].

Overlap of [3] aaaaa=d with [13] aaa=eeaae:

Critical pair: eeaaeaa=d.

Defines rule #15.

Referenced by [25], [26].

Simplify [8] db=aaaac.

Reduce RHS:

Defines rule #22.

Referenced by [23].

Overlap of [11] aaaeaae=dca with [13] aaa=eeaae:

Critical pair: eeaaeeaae=dca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [22] dca=eed with [2] ab=c:

Critical pair: dcc=eedb.

Reduce RHS:

Referenced by [24].

Overlap of [23] dcc=eccdc with [4] cca=e:

Critical pair: de=eccdca.

Reduce RHS:

Defines rule #2.

Overlap of [20] eeaaeaa=d with [5] eaac=aa:

Critical pair: eeaaaa=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [28], [30].

Overlap of [20] eeaaeaa=d with [13] aaa=eeaae:

Critical pair: eeaaeeeaae=da.

Reduce RHS:

Defines rule #18.

Overlap of [12] cceaae=eaca with [5] eaac=aa:

Critical pair: cceaaaa=eacaaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [12] cceaae=eaca with [17] aeaae=eeaaeca:

Critical pair: cceaeeaaeca=eacaaae.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [17] aeaae=eeaaeca with [5] eaac=aa:

Critical pair: aeaaaa=eeaaecaaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [17] aeaae=eeaaeca with [17] aeaae=eeaaeca:

Critical pair: aeaeeaaeca=eeaaecaaae.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.