Certificate for #26689 ⟨a, b | aa=1, babbbbab=b⟩

Completion settings:

• Auxiliary generators:
  1. c = bab
• Reduction order:
  • Left-to-right shortlex with a < b < c

Axiom: aa=1.

Defines rule #1.

Axiom: babbbbab=b.

Referenced by [4].

Axiom: bab=c.

Defines rule #2.

Referenced by [4], [5], [7], [10], [11], [12], [13].

Overlap of [2] babbbbab=b with [3] bab=c:

Critical pair: cbbbab=b.

Reduce LHS:

Defines rule #8.

Referenced by [6], [7], [8], [10], [11].

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

Critical pair: bac=cab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7], [8], [11], [12].

Overlap of [4] cbbc=b with [4] cbbc=b:

Critical pair: cbbb=bbbc.

Defines rule #7.

Referenced by [7], [9].

Overlap of [4] cbbc=b with [5] cab=bac:

Critical pair: cbbbac=bab.

Reduce LHS:

Reduce RHS:

Referenced by [8].

Overlap of [7] bbbcac=c with [4] cbbc=b:

Critical pair: bbbcab=cbbc.

Reduce LHS:

Reduce RHS:

Referenced by [9].

Overlap of [6] cbbb=bbbc with [8] bbbbac=b:

Critical pair: cb=bbbcbac.

Flip LHS and RHS.

Referenced by [10], [11].

Overlap of [3] bab=c with [9] bbbcbac=cb:

Critical pair: bacb=cbbcbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [12].

Overlap of [5] cab=bac with [9] bbbcbac=cb:

Critical pair: cacb=bacbbcbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [10] bbac=bacb with [5] cab=bac:

Critical pair: bbabac=bacbab.

Reduce LHS:

Reduce RHS:

Defines rule #5.

Referenced by [13].

Overlap of [3] bab=c with [12] bcac=bacc:

Critical pair: babacc=ccac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.