Certificate for #7504 ⟨a, b, c | ab=1, bbaa=cc⟩

Completion settings:

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

Axiom: ab=1.

Referenced by [5], [6], [24].

Axiom: bbaa=cc.

Flip LHS and RHS.

Referenced by [4], [5], [9], [10], [11].

Axiom: cbb=d.

Referenced by [4], [5], [7], [12].

Overlap of [2] cc=bbaa with [2] cc=bbaa:

Critical pair: cbbaa=bbaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [2] cc=bbaa with [3] cbb=d:

Critical pair: cd=bbaabb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [6], [7], [8], [9], [10], [11], [12], [13], [17].

Overlap of [1] ab=1 with [5] bb=cd:

Critical pair: acd=b.

Referenced by [16], [19].

Overlap of [3] cbb=d with [5] bb=cd:

Critical pair: cbcd=db.

Referenced by [9].

Overlap of [5] bb=cd with [5] bb=cd:

Critical pair: bcd=cdb.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [2] cc=bbaa with [8] cdb=bcd:

Critical pair: cbcd=bbaadb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [10].

Overlap of [2] cc=bbaa with [9] cdaadb=db:

Critical pair: cdb=bbaadaadb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [14].

Simplify [2] cc=bbaa.

Reduce RHS:

Referenced by [12], [15], [25].

Overlap of [3] cbb=d with [5] bb=cd:

Critical pair: ccd=d.

Reduce LHS:

Referenced by [14], [15], [16], [18], [23].

Overlap of [4] bbaac=daa with [5] bb=cd:

Critical pair: cdaac=daa.

Referenced by [22].

Overlap of [10] cdaadaadb=bcd with [12] cdaad=d:

Critical pair: daadb=bcd.

Flip LHS and RHS.

Referenced by [20].

Overlap of [11] cc=cdaa with [12] cdaad=d:

Critical pair: cd=cdaadaad.

Reduce RHS:

Defines rule #5.

Referenced by [17], [18], [20], [22], [23], [25].

Overlap of [6] acd=b with [12] cdaad=d:

Critical pair: ad=baad.

Flip LHS and RHS.

Referenced by [17], [19].

Overlap of [5] bb=cd with [16] baad=ad:

Critical pair: bad=cdaad.

Reduce RHS:

Referenced by [26].

Overlap of [12] cdaad=d with [15] cd=daad:

Critical pair: daadaad=d.

Referenced by [19], [21], [26].

Overlap of [6] acd=b with [18] daadaad=d:

Critical pair: acd=baadaad.

Reduce LHS:

Reduce RHS:

Defines rule #4.

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

Simplify [14] bcd=daadb.

Reduce LHS:

Reduce RHS:

Referenced by [21].

Overlap of [20] adaaddaad=daadadaad with [18] daadaad=d:

Critical pair: adaadd=daadadaadaad.

Reduce RHS:

Defines rule #1.

Simplify [13] cdaac=daa.

Reduce LHS:

Referenced by [23].

Overlap of [12] cdaad=d with [22] daadaac=daa:

Critical pair: cdaa=daac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [1] ab=1 with [19] b=adaad:

Critical pair: aadaad=1.

Defines rule #2.

Referenced by [28].

Simplify [11] cc=cdaa.

Reduce RHS:

Defines rule #7.

Simplify [17] bad=daadaad.

Reduce RHS:

Referenced by [27].

Overlap of [26] bad=d with [19] b=adaad:

Critical pair: adaadad=d.

Defines rule #3.

Overlap of [24] aadaad=1 with [23] daac=daadaa:

Critical pair: aadaadaadaa=aac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.