Certificate for #2087 ⟨a, b | abbbaaab=ba⟩

Completion settings:

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

Axiom: abbbaaab=ba.

Referenced by [4].

Axiom: abb=c.

Defines rule #21.

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

Axiom: cbaaa=d.

Referenced by [4], [5].

Overlap of [1] abbbaaab=ba with [2] abb=c:

Critical pair: cbaaab=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Referenced by [5], [6], [7], [8].

Overlap of [3] cbaaa=d with [4] ba=db:

Critical pair: cdbaa=d.

Reduce LHS:

Defines rule #1.

Referenced by [8], [9], [10], [12], [15], [18], [20], [22].

Overlap of [2] abb=c with [4] ba=db:

Critical pair: abdb=ca.

Flip LHS and RHS.

Defines rule #22.

Overlap of [4] ba=db with [2] abb=c:

Critical pair: bc=dbbb.

Flip LHS and RHS.

Referenced by [9], [11].

Overlap of [5] cdddb=d with [4] ba=db:

Critical pair: cddddb=da.

Flip LHS and RHS.

Defines rule #23.

Overlap of [5] cdddb=d with [7] dbbb=bc:

Critical pair: cddbc=dbb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [11], [14].

Overlap of [5] cdddb=d with [9] dbb=cddbc:

Critical pair: cddcddbc=db.

Defines rule #2.

Referenced by [12], [13], [14], [23].

Overlap of [7] dbbb=bc with [9] dbb=cddbc:

Critical pair: cddbcb=bc.

Defines rule #8.

Referenced by [14], [24].

Overlap of [10] cddcddbc=db with [5] cdddb=d:

Critical pair: cddcddbd=dbdddb.

Flip LHS and RHS.

Defines rule #6.

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

Overlap of [10] cddcddbc=db with [10] cddcddbc=db:

Critical pair: cddcddbdb=dbddcddbc.

Defines rule #11.

Overlap of [10] cddcddbc=db with [11] cddbcb=bc:

Critical pair: cddcddbbc=dbddbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [18], [19].

Overlap of [5] cdddb=d with [12] dbdddb=cddcddbd:

Critical pair: cddcddcddbd=ddddb.

Defines rule #3.

Referenced by [17], [19], [25].

Overlap of [12] dbdddb=cddcddbd with [12] dbdddb=cddcddbd:

Critical pair: dbddcddcddbd=cddcddbddddb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [15] cddcddcddbd=ddddb with [12] dbdddb=cddcddbd:

Critical pair: cddcddcdcddcddbd=ddddbddb.

Flip LHS and RHS.

Defines rule #10.

Overlap of [5] cdddb=d with [14] dbddbcb=cddcdcddbcc:

Critical pair: cddcddcdcddbcc=dddbcb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [20], [21].

Overlap of [15] cddcddcddbd=ddddb with [14] dbddbcb=cddcdcddbcc:

Critical pair: cddcddcdcddcdcddbcc=ddddbdbcb.

Flip LHS and RHS.

Defines rule #20.

Overlap of [5] cdddb=d with [18] dddbcb=cddcddcdcddbcc:

Critical pair: ccddcddcdcddbcc=dcb.

Defines rule #4.

Referenced by [22], [23], [24], [25], [26], [27].

Overlap of [12] dbdddb=cddcddbd with [18] dddbcb=cddcddcdcddbcc:

Critical pair: dbcddcddcdcddbcc=cddcddbdcb.

Flip LHS and RHS.

Defines rule #12.

Overlap of [20] ccddcddcdcddbcc=dcb with [5] cdddb=d:

Critical pair: ccddcddcdcddbcd=dcbdddb.

Flip LHS and RHS.

Defines rule #7.

Overlap of [20] ccddcddcdcddbcc=dcb with [10] cddcddbc=db:

Critical pair: ccddcddcdcddbcdb=dcbddcddbc.

Defines rule #14.

Overlap of [20] ccddcddcdcddbcc=dcb with [11] cddbcb=bc:

Critical pair: ccddcddcdcddbcbc=dcbddbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [20] ccddcddcdcddbcc=dcb with [15] cddcddcddbd=ddddb:

Critical pair: ccddcddcdcddbcddddb=dcbddcddcddbd.

Defines rule #17.

Overlap of [20] ccddcddcdcddbcc=dcb with [20] ccddcddcdcddbcc=dcb:

Critical pair: ccddcddcdcddbdcb=dcbddcddcdcddbcc.

Defines rule #15.

Overlap of [20] ccddcddcdcddbcc=dcb with [20] ccddcddcdcddbcc=dcb:

Critical pair: ccddcddcdcddbcdcb=dcbcddcddcdcddbcc.

Defines rule #16.