Certificate for #1585 ⟨a, b, c | aaa=bc, acb=1⟩

Completion settings:

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

Axiom: aaa=bc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [5], [6].

Axiom: acb=1.

Referenced by [4].

Axiom: cb=d.

Defines rule #5.

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

Overlap of [2] acb=1 with [3] cb=d:

Critical pair: ad=1.

Defines rule #1.

Referenced by [7], [8], [9], [10], [11], [13].

Overlap of [1] bc=aaa with [3] cb=d:

Critical pair: bd=aaab.

Flip LHS and RHS.

Referenced by [14].

Overlap of [3] cb=d with [1] bc=aaa:

Critical pair: caaa=dc.

Flip LHS and RHS.

Defines rule #7.

Referenced by [7], [13].

Overlap of [4] ad=1 with [6] dc=caaa:

Critical pair: acaaa=c.

Referenced by [8].

Overlap of [7] acaaa=c with [4] ad=1:

Critical pair: acaa=cd.

Referenced by [9].

Overlap of [8] acaa=cd with [4] ad=1:

Critical pair: aca=cdd.

Referenced by [10].

Overlap of [9] aca=cdd with [4] ad=1:

Critical pair: ac=cddd.

Defines rule #6.

Referenced by [11], [12].

Overlap of [10] ac=cddd with [3] cb=d:

Critical pair: ad=cdddb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12], [13].

Overlap of [10] ac=cddd with [11] cdddb=1:

Critical pair: a=cddddddb.

Flip LHS and RHS.

Referenced by [13].

Overlap of [6] dc=caaa with [12] cddddddb=a:

Critical pair: da=caaaddddddb.

Reduce RHS:

Defines rule #2.

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

Overlap of [13] da=1 with [5] aaab=bd:

Critical pair: dbd=aab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [15].

Overlap of [13] da=1 with [14] aab=dbd:

Critical pair: ddbd=ab.

Referenced by [16].

Overlap of [15] ddbd=ab with [13] da=1:

Critical pair: ddb=aba.

Defines rule #4.