Certificate for #7025 ⟨a, b, c | ab=1, bbbca=c⟩

Completion settings:

• Auxiliary generators:
  1. d = ca
  2. e = bbc
  3. f = bbe
• Reduction order:
  • Right-to-left recursive path with deg(b) = 0; deg(f) = deg(e) = deg(c) = deg(d) = 1, f < e < c < d; deg(a) = 2

Axiom: ab=1.

Defines rule #24.

Referenced by [7], [8], [9], [12].

Axiom: bbbca=c.

Referenced by [6].

Axiom: ca=d.

Defines rule #23.

Referenced by [7], [10], [17], [18], [25].

Axiom: bbc=e.

Defines rule #4.

Referenced by [6], [9], [10], [13], [15], [27], [28], [31].

Axiom: bbe=f.

Defines rule #2.

Referenced by [8], [15], [16], [20], [22], [24], [29].

Overlap of [2] bbbca=c with [4] bbc=e:

Critical pair: bea=c.

Referenced by [11].

Overlap of [3] ca=d with [1] ab=1:

Critical pair: c=db.

Flip LHS and RHS.

Defines rule #7.

Referenced by [13], [14], [21], [23], [26], [30].

Overlap of [1] ab=1 with [5] bbe=f:

Critical pair: af=be.

Defines rule #25.

Referenced by [17].

Overlap of [1] ab=1 with [4] bbc=e:

Critical pair: ae=bc.

Defines rule #26.

Referenced by [18].

Overlap of [4] bbc=e with [3] ca=d:

Critical pair: bbd=ea.

Flip LHS and RHS.

Defines rule #22.

Referenced by [11], [24].

Simplify [6] bea=c.

Reduce LHS:

Defines rule #6.

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

Overlap of [1] ab=1 with [11] bbbd=c:

Critical pair: ac=bbd.

Defines rule #27.

Referenced by [25].

Overlap of [11] bbbd=c with [7] db=c:

Critical pair: bbbc=cb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [14], [15], [17], [18], [26].

Overlap of [7] db=c with [11] bbbd=c:

Critical pair: dc=cbbd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [4] bbc=e with [13] cb=be:

Critical pair: bbbe=eb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [19].

Overlap of [5] bbe=f with [15] eb=bf:

Critical pair: bbbf=fb.

Flip LHS and RHS.

Defines rule #1.

Overlap of [3] ca=d with [8] af=be:

Critical pair: cbe=df.

Reduce LHS:

Defines rule #9.

Referenced by [20], [21].

Overlap of [3] ca=d with [9] ae=bc:

Critical pair: cbc=de.

Reduce LHS:

Defines rule #11.

Referenced by [22], [23].

Overlap of [14] bebd=dc with [15] eb=bf:

Critical pair: bbfd=dc.

Defines rule #12.

Referenced by [26].

Overlap of [5] bbe=f with [17] bee=df:

Critical pair: bdf=fe.

Flip LHS and RHS.

Defines rule #8.

Overlap of [7] db=c with [17] bee=df:

Critical pair: ddf=cee.

Flip LHS and RHS.

Defines rule #14.

Referenced by [27].

Overlap of [5] bbe=f with [18] bec=de:

Critical pair: bde=fc.

Flip LHS and RHS.

Defines rule #10.

Overlap of [7] db=c with [18] bec=de:

Critical pair: dde=cec.

Flip LHS and RHS.

Defines rule #16.

Referenced by [28].

Overlap of [5] bbe=f with [10] ea=bbd:

Critical pair: bbbbd=fa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [12] ac=bbd with [3] ca=d:

Critical pair: ad=bbda.

Defines rule #28.

Overlap of [7] db=c with [19] bbfd=dc:

Critical pair: ddc=cbfd.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [29], [30].

Overlap of [4] bbc=e with [21] cee=ddf:

Critical pair: bbddf=eee.

Flip LHS and RHS.

Defines rule #13.

Overlap of [4] bbc=e with [23] cec=dde:

Critical pair: bbdde=eec.

Flip LHS and RHS.

Defines rule #15.

Overlap of [5] bbe=f with [26] befd=ddc:

Critical pair: bddc=ffd.

Flip LHS and RHS.

Defines rule #17.

Overlap of [7] db=c with [26] befd=ddc:

Critical pair: dddc=cefd.

Flip LHS and RHS.

Defines rule #20.

Referenced by [31].

Overlap of [4] bbc=e with [30] cefd=dddc:

Critical pair: bbdddc=eefd.

Flip LHS and RHS.

Defines rule #19.