Certificate for #4359 ⟨a, b | abbbbbbba=ab⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with a < d < c < b
• Auxiliary generators:
  1. bbb=c
  2. acccc=d

Axiom: abbbbbbba=ab.

Referenced by [4].

Axiom: bbb=c.

Defines rule #9.

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

Axiom: acccc=d.

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

Overlap of [1] abbbbbbba=ab with [2] bbb=c:

Critical pair: acbbbba=ab.

Reduce LHS:

Referenced by [6], [7], [8], [9], [16], [17].

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

Critical pair: bc=cb.

Defines rule #1.

Referenced by [6], [7], [8], [9], [10], [11], [12], [17], [20], [24], [33], [35], [37], [38], [39].

Overlap of [4] accba=ab with [3] acccc=d:

Critical pair: accbd=abcccc.

Reduce RHS:

Referenced by [8], [10], [13], [18], [24].

Overlap of [4] accba=ab with [4] accba=ab:

Critical pair: accbab=abccba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [9], [10], [11], [12], [19], [20].

Overlap of [4] accba=ab with [6] accbd=db:

Critical pair: accbdb=abccbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [10], [25].

Overlap of [4] accba=ab with [7] accbba=abb:

Critical pair: accbabb=abccbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13], [14], [21], [22].

Overlap of [7] accbba=abb with [6] accbd=db:

Critical pair: accbbdb=abbccbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [26].

Overlap of [7] accbba=abb with [7] accbba=abb:

Critical pair: accbbabb=abbccbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [7] accbba=abb with [9] accca=ac:

Critical pair: accbbac=abbccca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [9] accca=ac with [6] accbd=db:

Critical pair: acccdb=acccbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [9] accca=ac with [9] accca=ac:

Critical pair: acccac=acccca.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [16], [17], [18], [19], [20], [21], [22], [23], [24], [25], [26], [27], [28], [29].

Overlap of [3] acccc=d with [14] acc=da:

Critical pair: dacc=d.

Reduce LHS:

Defines rule #3.

Referenced by [23], [33], [34], [35].

Overlap of [4] accba=ab with [14] acc=da:

Critical pair: daba=ab.

Defines rule #12.

Overlap of [4] accba=ab with [14] acc=da:

Critical pair: accbda=abcc.

Reduce LHS:

Reduce RHS:

Referenced by [30].

Overlap of [6] accbd=db with [14] acc=da:

Critical pair: dabd=db.

Defines rule #13.

Referenced by [24], [30], [36], [37], [38], [39].

Overlap of [7] accbba=abb with [14] acc=da:

Critical pair: dabba=abb.

Defines rule #20.

Overlap of [7] accbba=abb with [14] acc=da:

Critical pair: accbbda=abbcc.

Reduce LHS:

Reduce RHS:

Referenced by [31].

Overlap of [9] accca=ac with [14] acc=da:

Critical pair: daca=ac.

Defines rule #10.

Referenced by [33].

Overlap of [9] accca=ac with [14] acc=da:

Critical pair: acccda=accc.

Reduce LHS:

Reduce RHS:

Referenced by [32].

Overlap of [15] dda=d with [14] acc=da:

Critical pair: ddda=dcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [24].

Overlap of [6] accbd=db with [23] dcc=dd:

Critical pair: accbdd=dbcc.

Reduce LHS:

Reduce RHS:

Defines rule #8.

Referenced by [33], [35], [36], [38].

Overlap of [8] accbbd=dbb with [14] acc=da:

Critical pair: dabbd=dbb.

Defines rule #21.

Referenced by [31].

Overlap of [10] acccd=dc with [14] acc=da:

Critical pair: dacd=dc.

Defines rule #11.

Referenced by [32], [34], [35].

Overlap of [11] acccba=acb with [14] acc=da:

Critical pair: dacba=acb.

Defines rule #18.

Overlap of [12] acccbba=acbb with [14] acc=da:

Critical pair: dacbba=acbb.

Defines rule #24.

Overlap of [13] acccbd=dcb with [14] acc=da:

Critical pair: dacbd=dcb.

Defines rule #19.

Referenced by [39].

Overlap of [17] dabda=dab with [18] dabd=db:

Critical pair: dba=dab.

Defines rule #7.

Referenced by [33], [35], [37], [39].

Overlap of [20] dabbda=dabb with [25] dabbd=dbb:

Critical pair: dbba=dabb.

Defines rule #16.

Overlap of [22] dacda=dac with [26] dacd=dc:

Critical pair: dca=dac.

Defines rule #4.

Overlap of [24] dbd=ddb with [21] daca=ac:

Critical pair: dbac=ddbaca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [37].

Overlap of [15] dda=d with [26] dacd=dc:

Critical pair: ddc=dcd.

Flip LHS and RHS.

Defines rule #5.

Overlap of [24] dbd=ddb with [26] dacd=dc:

Critical pair: dbdc=ddbacd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [38].

Overlap of [18] dabd=db with [24] dbd=ddb:

Critical pair: dabddb=dbbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [18] dabd=db with [33] dcba=dacb:

Critical pair: dabdacb=dbcba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [18] dabd=db with [35] dcbd=ddcb:

Critical pair: dabddcb=dbcbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [18] dabd=db with [29] dacbd=dcb:

Critical pair: dabdcb=dbacbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #25.