Certificate for #2608 ⟨a, b | ababba=baab⟩

Completion settings:

• Auxiliary generators:
  1. c = bba
• Reduction order:
  • Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(b) = 1

Axiom: ababba=baab.

Referenced by [3].

Axiom: bba=c.

Defines rule #3.

Referenced by [3], [4], [5], [7], [10].

Overlap of [1] ababba=baab with [2] bba=c:

Critical pair: abac=baab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [4], [5], [6], [8], [9], [11], [14].

Overlap of [2] bba=c with [3] baab=abac:

Critical pair: babac=cab.

Defines rule #6.

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

Overlap of [3] baab=abac with [2] bba=c:

Critical pair: baac=abacba.

Flip LHS and RHS.

Defines rule #4.

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

Overlap of [3] baab=abac with [3] baab=abac:

Critical pair: baaabac=abacaab.

Defines rule #7.

Overlap of [2] bba=c with [4] babac=cab:

Critical pair: bcab=cbac.

Defines rule #2.

Referenced by [9], [10], [11], [12], [13], [15].

Overlap of [3] baab=abac with [4] babac=cab:

Critical pair: baacab=abacabac.

Flip LHS and RHS.

Defines rule #9.

Overlap of [3] baab=abac with [7] bcab=cbac:

Critical pair: baacbac=abaccab.

Defines rule #11.

Overlap of [7] bcab=cbac with [2] bba=c:

Critical pair: bcac=cbacba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [16], [17].

Overlap of [7] bcab=cbac with [3] baab=abac:

Critical pair: bcaabac=cbacaab.

Defines rule #8.

Overlap of [7] bcab=cbac with [4] babac=cab:

Critical pair: bcacab=cbacabac.

Flip LHS and RHS.

Defines rule #10.

Overlap of [7] bcab=cbac with [7] bcab=cbac:

Critical pair: bcacbac=cbaccab.

Defines rule #12.

Overlap of [3] baab=abac with [5] abacba=baac:

Critical pair: babaac=abacacba.

Defines rule #13.

Overlap of [7] bcab=cbac with [5] abacba=baac:

Critical pair: bcbaac=cbacacba.

Defines rule #14.

Overlap of [5] abacba=baac with [10] cbacba=bcac:

Critical pair: ababcac=baaccba.

Defines rule #15.

Overlap of [10] cbacba=bcac with [10] cbacba=bcac:

Critical pair: cbabcac=bcaccba.

Defines rule #16.