Certificate for #3153 ⟨a, b | aabbbbaaaba=1⟩

Completion settings:

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

Axiom: aabbbbaaaba=1.

Referenced by [4].

Axiom: bbb=c.

Defines rule #5.

Referenced by [4], [5], [6], [7], [18], [19], [23].

Axiom: aaab=d.

Referenced by [4], [6].

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

Critical pair: aacbaaaba=1.

Reduce LHS:

Referenced by [7], [8].

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

Critical pair: bc=cb.

Defines rule #2.

Referenced by [11], [20], [24].

Overlap of [3] aaab=d with [2] bbb=c:

Critical pair: aaac=dbb.

Referenced by [7], [12].

Overlap of [6] aaac=dbb with [4] aacbda=1:

Critical pair: a=dbbbda.

Reduce RHS:

Flip LHS and RHS.

Referenced by [8].

Overlap of [7] dcda=a with [4] aacbda=1:

Critical pair: dcd=aacbda.

Reduce RHS:

Referenced by [9], [10].

Overlap of [8] dcd=1 with [8] dcd=1:

Critical pair: dc=cd.

Defines rule #1.

Referenced by [10], [13], [14], [18], [19], [20], [22], [23], [24].

Overlap of [8] dcd=1 with [9] dc=cd:

Critical pair: cdd=1.

Defines rule #3.

Referenced by [11], [12], [14], [17], [18], [19], [21], [22], [23], [25].

Overlap of [5] bc=cb with [10] cdd=1:

Critical pair: b=cbdd.

Flip LHS and RHS.

Referenced by [13].

Overlap of [6] aaac=dbb with [10] cdd=1:

Critical pair: aaa=dbbdd.

Referenced by [15].

Overlap of [9] dc=cd with [11] cbdd=b:

Critical pair: db=cdbdd.

Flip LHS and RHS.

Referenced by [14].

Overlap of [9] dc=cd with [13] cdbdd=db:

Critical pair: ddb=cddbdd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [15], [18].

Simplify [12] aaa=dbbdd.

Reduce RHS:

Defines rule #9.

Referenced by [16].

Overlap of [15] aaa=dddbb with [15] aaa=dddbb:

Critical pair: adddbb=dddbba.

Flip LHS and RHS.

Referenced by [17], [18].

Overlap of [10] cdd=1 with [16] dddbba=adddbb:

Critical pair: cadddbb=dbba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [22].

Overlap of [14] bdd=ddb with [16] dddbba=adddbb:

Critical pair: bdadddbb=ddbddbba.

Reduce RHS:

Referenced by [19].

Overlap of [18] bdadddbb=dda with [2] bbb=c:

Critical pair: bdadddc=ddab.

Reduce LHS:

Referenced by [20].

Overlap of [19] bdad=ddab with [9] dc=cd:

Critical pair: bdacd=ddabc.

Reduce RHS:

Referenced by [21].

Overlap of [20] bdacd=ddacb with [10] cdd=1:

Critical pair: bda=ddacbd.

Defines rule #6.

Overlap of [10] cdd=1 with [17] dbba=cadddbb:

Critical pair: cdcadddbb=bba.

Reduce LHS:

Referenced by [23].

Overlap of [22] ccdadddbb=bba with [2] bbb=c:

Critical pair: ccdadddc=bbab.

Reduce LHS:

Referenced by [24].

Overlap of [23] ccdad=bbab with [9] dc=cd:

Critical pair: ccdacd=bbabc.

Reduce RHS:

Referenced by [25].

Overlap of [24] ccdacd=bbacb with [10] cdd=1:

Critical pair: ccda=bbacbd.

Defines rule #7.