Certificate for #4647 ⟨a, b | aabababa=baa⟩

Completion settings:

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

Axiom: aabababa=baa.

Referenced by [4].

Axiom: ababa=c.

Defines rule #13.

Referenced by [4], [8], [9], [10], [11], [12].

Axiom: acb=d.

Defines rule #7.

Referenced by [4], [5], [6], [7], [13], [14].

Overlap of [1] aabababa=baa with [2] ababa=c:

Critical pair: acba=baa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [5], [6], [9], [11].

Overlap of [3] acb=d with [4] baa=da:

Critical pair: acda=daa.

Referenced by [15].

Overlap of [4] baa=da with [3] acb=d:

Critical pair: bad=dacb.

Reduce RHS:

Defines rule #10.

Referenced by [7], [9], [10], [12].

Overlap of [3] acb=d with [6] bad=dd:

Critical pair: acdd=dad.

Referenced by [16].

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

Critical pair: abc=cba.

Defines rule #11.

Overlap of [2] ababa=c with [4] baa=da:

Critical pair: abada=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Overlap of [2] ababa=c with [6] bad=dd:

Critical pair: abadd=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [4] baa=da with [2] ababa=c:

Critical pair: bac=dababa.

Reduce RHS:

Defines rule #12.

Referenced by [12], [13], [14].

Overlap of [2] ababa=c with [11] bac=dc:

Critical pair: abadc=cc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [3] acb=d with [11] bac=dc:

Critical pair: acdc=dac.

Reduce LHS:

Defines rule #3.

Overlap of [11] bac=dc with [3] acb=d:

Critical pair: bd=dcb.

Defines rule #8.

Overlap of [5] acda=daa with [10] cd=addd:

Critical pair: aaddda=daa.

Defines rule #1.

Overlap of [7] acdd=dad with [10] cd=addd:

Critical pair: aadddd=dad.

Defines rule #2.