Certificate for #5898 ⟨a, b | ababba=babab⟩

Completion settings:

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

Axiom: ababba=babab.

Defines rule #2.

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

Axiom: bbaba=c.

Defines rule #3.

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

Overlap of [1] ababba=babab with [2] bbaba=c:

Critical pair: abac=bababba.

Reduce RHS:

Defines rule #1.

Overlap of [2] bbaba=c with [1] ababba=babab:

Critical pair: bbbabab=cbba.

Reduce LHS:

Defines rule #4.

Referenced by [6].

Overlap of [2] bbaba=c with [1] ababba=babab:

Critical pair: bbabbabab=cbabba.

Reduce LHS:

Defines rule #6.

Referenced by [7].

Overlap of [4] bcb=cbba with [2] bbaba=c:

Critical pair: bcc=cbbababa.

Reduce RHS:

Defines rule #5.

Overlap of [5] bbacb=cbabba with [2] bbaba=c:

Critical pair: bbacc=cbabbababa.

Reduce RHS:

Defines rule #7.