Certificate for #4297 ⟨a, b | abababaab=ba⟩

Completion settings:

• Auxiliary generators:
  1. c = ab
  2. d = ccac
• Reduction order:
  • Left-to-right recursive path with deg(b) = deg(c) = 0, b < c; deg(d) = 1; deg(a) = 2

Axiom: abababaab=ba.

Referenced by [4].

Axiom: ab=c.

Defines rule #5.

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

Axiom: ccac=d.

Referenced by [4], [7].

Overlap of [1] abababaab=ba with [2] ab=c:

Critical pair: cababaab=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [5], [6], [10].

Overlap of [2] ab=c with [4] ba=cd:

Critical pair: acd=ca.

Flip LHS and RHS.

Defines rule #8.

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

Overlap of [4] ba=cd with [2] ab=c:

Critical pair: bc=cdb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

Simplify [3] ccac=d.

Reduce LHS:

Defines rule #6.

Referenced by [8], [9], [10], [11], [13], [14], [15].

Overlap of [7] acdcdc=d with [5] ca=acd:

Critical pair: acdcdacd=da.

Referenced by [15].

Overlap of [7] acdcdc=d with [6] cdb=bc:

Critical pair: acdcdbc=ddb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [4] ba=cd with [7] acdcdc=d:

Critical pair: bd=cdcdcdc.

Flip LHS and RHS.

Defines rule #4.

Overlap of [5] ca=acd with [7] acdcdc=d:

Critical pair: cd=acdcdcdc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [12], [15].

Overlap of [11] ddc=cd with [5] ca=acd:

Critical pair: ddacd=cda.

Referenced by [13], [14].

Overlap of [12] ddacd=cda with [7] acdcdc=d:

Critical pair: ddd=cdacdc.

Flip LHS and RHS.

Referenced by [14].

Overlap of [7] acdcdc=d with [13] cdacdc=ddd:

Critical pair: acdcdddd=ddacdc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [8] acdcdacd=da with [14] cdac=acdcdddd:

Critical pair: acdacdcddddd=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.