Certificate for #1492 ⟨a, b | abaabaabab=1⟩

Completion settings:

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

Axiom: abaabaabab=1.

Referenced by [3].

Axiom: aba=c.

Defines rule #5.

Referenced by [3], [4], [6], [8], [9], [11].

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

Critical pair: cabaabab=1.

Reduce LHS:

Defines rule #2.

Referenced by [5], [6], [7], [10], [12], [13], [14], [15], [16].

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

Critical pair: abc=cba.

Referenced by [5], [8], [13], [16].

Overlap of [4] abc=cba with [3] cccb=1:

Critical pair: ab=cbaccb.

Flip LHS and RHS.

Referenced by [6].

Overlap of [5] cbaccb=ab with [5] cbaccb=ab:

Critical pair: cbacab=abaccb.

Reduce RHS:

Referenced by [7], [8].

Overlap of [3] cccb=1 with [6] cbacab=1:

Critical pair: cc=acab.

Flip LHS and RHS.

Referenced by [9].

Overlap of [4] abc=cba with [6] cbacab=1:

Critical pair: ab=cbabacab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [7] acab=cc with [2] aba=c:

Critical pair: acc=cca.

Referenced by [10].

Overlap of [9] acc=cca with [3] cccb=1:

Critical pair: ac=ccaccb.

Reduce RHS:

Defines rule #3.

Referenced by [13], [16].

Overlap of [8] cbccab=ab with [2] aba=c:

Critical pair: cbccc=aba.

Reduce RHS:

Referenced by [12].

Overlap of [11] cbccc=c with [3] cccb=1:

Critical pair: cbc=ccb.

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

Overlap of [4] abc=cba with [12] cbc=ccb:

Critical pair: abccb=cbabc.

Reduce LHS:

Reduce RHS:

Referenced by [16].

Overlap of [12] cbc=ccb with [12] cbc=ccb:

Critical pair: cbccb=ccbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [3] cccb=1 with [14] ccbbc=b:

Critical pair: cb=bc.

Flip LHS and RHS.

Defines rule #1.

Overlap of [4] abc=cba with [14] ccbbc=b:

Critical pair: abb=cbacbbc.

Reduce RHS:

Defines rule #4.