Certificate for #5913 ⟨a, b | abbaab=aabaa⟩

Completion settings:

• Auxiliary generators:
  1. c = aba
  2. d = bba
• Reduction order:
  • Left-to-right shortlex with a < b < d < c

Axiom: abbaab=aabaa.

Referenced by [4].

Axiom: aba=c.

Defines rule #1.

Referenced by [4], [6], [7], [8], [10], [11], [12], [16].

Axiom: bba=d.

Defines rule #2.

Referenced by [5], [7], [9], [11], [13], [17].

Simplify [1] abbaab=aabaa.

Reduce RHS:

Referenced by [5].

Overlap of [4] abbaab=aca with [3] bba=d:

Critical pair: adab=aca.

Defines rule #5.

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

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

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #4.

Overlap of [3] bba=d with [2] aba=c:

Critical pair: bbc=dba.

Flip LHS and RHS.

Defines rule #3.

Overlap of [2] aba=c with [5] adab=aca:

Critical pair: abaca=cdab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [3] bba=d with [5] adab=aca:

Critical pair: bbaca=ddab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [5] adab=aca with [2] aba=c:

Critical pair: adc=acaa.

Flip LHS and RHS.

Defines rule #7.

Referenced by [16], [17].

Overlap of [5] adab=aca with [3] bba=d:

Critical pair: adad=acaba.

Reduce RHS:

Defines rule #6.

Referenced by [12], [13], [14], [15], [19], [21].

Overlap of [2] aba=c with [11] adad=acc:

Critical pair: abacc=cdad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [20], [21].

Overlap of [3] bba=d with [11] adad=acc:

Critical pair: bbacc=ddad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [18], [19].

Overlap of [11] adad=acc with [5] adab=aca:

Critical pair: adaca=accab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [11] adad=acc with [11] adad=acc:

Critical pair: adacc=accad.

Flip LHS and RHS.

Defines rule #15.

Overlap of [2] aba=c with [10] acaa=adc:

Critical pair: abadc=ccaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [3] bba=d with [10] acaa=adc:

Critical pair: bbadc=dcaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [13] ddad=dcc with [5] adab=aca:

Critical pair: ddaca=dccab.

Flip LHS and RHS.

Defines rule #16.

Overlap of [13] ddad=dcc with [11] adad=acc:

Critical pair: ddacc=dccad.

Flip LHS and RHS.

Defines rule #17.

Overlap of [12] cdad=ccc with [5] adab=aca:

Critical pair: cdaca=cccab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [12] cdad=ccc with [11] adad=acc:

Critical pair: cdacc=cccad.

Flip LHS and RHS.

Defines rule #19.