Certificate for #1714 ⟨a, b, c | aab=bc, cba=1⟩

Completion settings:

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

Axiom: aab=bc.

Flip LHS and RHS.

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

Axiom: cba=1.

Referenced by [4], [5], [6], [7], [10], [11], [14], [18].

Axiom: ac=d.

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

Overlap of [2] cba=1 with [3] ac=d:

Critical pair: cbd=c.

Referenced by [15].

Overlap of [3] ac=d with [2] cba=1:

Critical pair: a=dba.

Flip LHS and RHS.

Referenced by [8], [19].

Overlap of [1] bc=aab with [2] cba=1:

Critical pair: b=aabba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [7], [8], [9], [22], [31].

Overlap of [2] cba=1 with [6] aabba=b:

Critical pair: cbb=abba.

Referenced by [10], [12], [16].

Overlap of [5] dba=a with [6] aabba=b:

Critical pair: dbb=aabba.

Reduce RHS:

Referenced by [13], [23].

Overlap of [6] aabba=b with [6] aabba=b:

Critical pair: aabbb=babba.

Flip LHS and RHS.

Defines rule #5.

Referenced by [22], [27].

Overlap of [7] cbb=abba with [1] bc=aab:

Critical pair: cbaab=abbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [2] cba=1 with [10] abbd=ab:

Critical pair: cbab=bbd.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [7] cbb=abba with [11] bbd=b:

Critical pair: cb=abbad.

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

Overlap of [8] dbb=b with [11] bbd=b:

Critical pair: db=bd.

Flip LHS and RHS.

Referenced by [21], [24].

Overlap of [2] cba=1 with [12] cb=abbad:

Critical pair: abbada=1.

Referenced by [18], [19].

Overlap of [4] cbd=c with [12] cb=abbad:

Critical pair: abbadd=c.

Flip LHS and RHS.

Defines rule #11.

Referenced by [17], [18], [20].

Overlap of [7] cbb=abba with [12] cb=abbad:

Critical pair: abbadb=abba.

Referenced by [17].

Overlap of [12] cb=abbad with [11] bbd=b:

Critical pair: cb=abbadbd.

Reduce LHS:

Reduce RHS:

Referenced by [18].

Overlap of [2] cba=1 with [14] abbada=1:

Critical pair: cb=bbada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [5] dba=a with [14] abbada=1:

Critical pair: db=abbada.

Reduce RHS:

Defines rule #1.

Referenced by [20], [21], [24], [25], [26].

Overlap of [19] db=1 with [1] bc=aab:

Critical pair: daab=c.

Reduce RHS:

Referenced by [21].

Overlap of [20] daab=abbadd with [13] bd=db:

Critical pair: daadb=abbaddd.

Reduce LHS:

Defines rule #3.

Overlap of [6] aabba=b with [9] babba=aabbb:

Critical pair: aabaabbb=bbba.

Referenced by [28].

Overlap of [8] dbb=b with [18] bbada=abbad:

Critical pair: dabbad=bada.

Flip LHS and RHS.

Defines rule #4.

Referenced by [25].

Simplify [13] bd=db.

Reduce RHS:

Defines rule #2.

Referenced by [28], [29], [30], [32], [33], [34].

Overlap of [19] db=1 with [23] bada=dabbad:

Critical pair: ddabbad=ada.

Referenced by [26].

Overlap of [25] ddabbad=ada with [19] db=1:

Critical pair: ddabba=adab.

Defines rule #6.

Referenced by [27].

Overlap of [26] ddabba=adab with [9] babba=aabbb:

Critical pair: ddabaabbb=adabbba.

Referenced by [32].

Overlap of [22] aabaabbb=bbba with [24] bd=1:

Critical pair: aabaabb=bbbad.

Referenced by [29].

Overlap of [28] aabaabb=bbbad with [24] bd=1:

Critical pair: aabaab=bbbadd.

Referenced by [30].

Overlap of [29] aabaab=bbbadd with [24] bd=1:

Critical pair: aabaa=bbbaddd.

Defines rule #10.

Referenced by [31].

Overlap of [6] aabba=b with [30] aabaa=bbbaddd:

Critical pair: aabbbbbaddd=babaa.

Flip LHS and RHS.

Defines rule #8.

Overlap of [27] ddabaabbb=adabbba with [24] bd=1:

Critical pair: ddabaabb=adabbbad.

Referenced by [33].

Overlap of [32] ddabaabb=adabbbad with [24] bd=1:

Critical pair: ddabaab=adabbbadd.

Referenced by [34].

Overlap of [33] ddabaab=adabbbadd with [24] bd=1:

Critical pair: ddabaa=adabbbaddd.

Defines rule #9.